> is that it's hard to tell if a particular C++ or Rust implementation conforms to the spec.

You can use either TLC's graph output or simulation mode to generate lots of TLA+ traces. Then you write an orchestrator that reads the trace as JSON and run the same actions in each step on the program, then confirm they have the same final states. You can go the other way, too, where you take program traces and map them onto the TLA+ state space.

It's a bit tricky to set up, but it's possible. I've had several clients who've built something similar.

https://www.microsoft.com/en-us/research/blog/p-programming-... makes the case better than I can on why it's important to have the specification and implementation come from the same source as opposed to maintaining two and then verify via traces that they're compatible.

But definitely worth doing (like Jepsen does) to find problems in the implementation.

Yeah, if you can do it economically, having a single source is preferable.

This is, incidentally, one of the kinds of use cases that informed part of our product functionality.

1. A way to write down fairly complicated system/behavior-level specs for distributed systems.

2. A way to instrument implementations to get the necessary signal out of the system to verify it nominally.

3. A way to automatically explore adverse conditions to validate that the system keeps behaving as needed and specifically isolate contributing factors for when it doesn't.

The very first prototype was leveraged (in-part, as there was much more too the system under test) in a consensus mechanism that was central to the correct, stable, and most importantly... safe... operation of some critical software infrastructure. It was necessary to try to explore where the model assumptions broke down in practice in a real system.

> The issue is that rust is a very large language and it's hard to get it right.

In my experience, Rust type system (especially the Send and Sync traits, which prevent data races) makes it easier − not harder − to get big things work.

My intention is to reuse the rust type system where we can and yet keep the language small enough to be able to implement and verify non-trivial real world programs.

https://github.com/adsharma/py2many/blob/main/doc/langspec.m... https://github.com/adsharma/py2many/blob/main/CHANGELOG.md#r...

you can abstract IO and async'ness from the implementation, and model it as a pure function. Then build and inspect the state space. A detailed description was done here:

https://incubaid.wordpress.com/2012/10/25/caulking-your-dist...