[inaseer]

We've used Coyote (https://microsoft.github.io/coyote/) which offers an actor-based programming model, as well as as async/await programming model on top of .NET's Tasks to express the concurrency in our services. Coyote includes a powerful systematic testing and exploration engine which explores the various states your programs can be in and helps you find violations to safety and liveness properties. This gives us the same benefits you get when using a model checker like TLA+ but on our actual production code as opposed to a model of the code. If your services are written in .NET, I seriously recommend taking a deeper look here.

[mratsim]

Wow, that looks like a killer feature for .Net

I will definitely steal some ideas from Coyote to drive Nim formally verification story of concurrent code forward.

On the Rust side, i feel like Loom has a lot of potential https://github.com/tokio-rs/loom and I'm keeping tabs on them.

[inaseer]

Looms looks quite interesting and is similar to Coyote in a lot of ways. The exploration engine used by Coyote is based on years of investigation by Microsoft Research so it scales nicely on real world programs. I believe the Coyote team is looking into exposing the systematic exploration capabilities in a language and platform agnostic way so developers can create language-specific bindings in their language of choice and benefit from all the research done over decades. No timelines that I'm aware of but it is on the road map I believe.

[mratsim]

Yes I'm in the middle of many Microsoft papers[1] to add model checking to Nim, in particular CHESS.[2]

[1]: https://github.com/mratsim/weave/issues/18

[2]: Finding and Reproducing Heisenbugs in Concurrent Programs, http://www.cs.ucr.edu/~neamtiu/pubs/osdi08musuvathi.pdf