About the TLA+ specifications of MongoDB

Hi folks!

I’m a researcher instrested in the TLA+ specifications of MongoDB.
The github repo provides multiple specifications for different components of MongoDB, e.g.,

It is interesting to find that some specifications are commented that they are specified according to the code implementation. For example, the comment of PriorityTicketHolder.tla says that this spec describes the implementation of priority_ticketholder.cpp, and will be evolved with the target code in sync. However, other specifications do not have such comments.

Typically, a formal specification can be written:

  • before the code is implemented. System developers may design the high-level protocol first, and use the formal specification to describe the protocol design, verify its correctness, and then use it to guide the code implementation.

  • after the implementation is done. In this case, the specifications is written to model the target aspects of the code implementation and verify its correctness. It reflects the real system implementation, and should be evolved in sync with the code.

There exist two questions that I am really curious about:

  1. For the specifications without clear comments, when were they specified? Were they specified according to the implementation after the code was implemented, or before the code was implemented? (e.g., RaftMongo.tla, RaftMongoWithRaftReconfig.tla, MongoReplReconfig.tla, MultiTenantMigrations.tla, ShardMerge.tla & RaftMongoReplTimestamp.tla)

  2. For the specifications that reflect the real system implementation, do they stay in sync with the code during the evolution of MongoDB?

Looking forward to receiving feedback from the MongoDB community! Thanks!