And that's where model checking / formal verification is a tremendous help (or would be if it was easier to use). There are many properties of multithreaded/di

And that's where model checking / formal verification is a tremendous help (or would be if it was easier to use). There are many properties of multithreaded/distributed systems that are emergent and that current static compilers don't address. In distributed systems it's becoming more common to use TLA+[1] to model the system and ensure that we don't have bugs at the design level (rather than just the system level). In particular for message-passing, I'm quite curious about the state of the research on Communicating Finite State Machines[1] and Petri Nets[2] and if there are actual products that could be integrated in regular languages and are not just of academic interest only. I expect that Ada/Sparks[1] has some support for this pattern though Ada multithreading story is not there yet (?). I'm quite excited about the future Z3 prover integration in Nim[5] and the potential to write concurrent programs free of design bugs[6] to address both ends of the concurrency bugs: - bugs in the low-level concurrent data structure via formal verification (which is something I used int he past to prove that my design was bug-free and that the deadlock I experienced was a condition variable bugs in Glibc[7] and I had to directly use futexes instead. - bugs in the high-level design, implemented as event-loop / finite state-machine reacting to events as received by channels Are there people working on model checkers or formal verification in Rust? Like the author, i think addressing memory bugs.the borrow checker is only a part of the "fearless concurrency" story and preventing design bugs would be extremely valuable. [1]: https://lamport.azurewebsites.net/tla/tla.html https://lamport.azurewebsites.net/tla/tla.html [2]: https://en.wikipedia.org/wiki/Communicating_finite-state_machine https://en.wikipedia.org/wiki/Communicating_finite-state_mac... [3]: https://en.wikipedia.org/wiki/Petri_net https://en.wikipedia.org/wiki/Petri_net [4]: https://www.adacore.com/sparkpro https://www.adacore.com/sparkpro [5]: https://nim-lang.org/docs/drnim.html https://nim-lang.org/docs/drnim.html [6]: https://github.com/nim-lang/RFCs/issues/222 https://github.com/nim-lang/RFCs/issues/222 [7]: https://github.com/mratsim/weave/issues/56 https://github.com/mratsim/weave/issues/56 And shameless plug, my talk at the NimConf on debugging multithreading programs (data structure and design): https://www.youtube.com/watch?v=NOAI2wH9Cf0&list=PLxLdEZg8DRwTIEzUpfaIcBqhsj09mLWHx&index=11 https://www.youtube.com/watch?v=NOAI2wH9Cf0&list=PLxLdEZg8DR... Slides: https://docs.google.com/presentation/d/e/2PACX-1vRq2wvd4q_mohbu2a_bYnhJwO487XY1s3cTYs52_p5_PmF0Uc3AcNnBg45Y9AtJ0WMnanip9UewRZd3/pub?start=false&loop=false&delayms=3000 https://docs.google.com/presentation/d/e/2PACX-1vRq2wvd4q_mo...