There are few tools that are both geared to mainstream programming languages and reasonable to work with. But probably the best place to start is Infer [1]. It'

There are few tools that are both geared to mainstream programming languages and reasonable to work with. But probably the best place to start is Infer [1]. It's marketed as a static analyzer, in other words a way to prove some properties, but the separation logic at its heart is a powerful and general program proof technique. In time, I hope and expect that the RustBelt project[2] will become a practical tool to prove Rust programs correct. It's already found some bugs in the standard library, and the main focus is currently to firm up the semantics of the language. Its separation logic engine (Iris) builds on work from Infer. Lastly, there are less mainstream languages that are better adapted to formal proving. To pick one, I'd probably go with Idris, as it is probably best at being a general purpose programming language in addition to a mathematical tool. But there are others. Lean is exciting because it is being used as the basis of an ambitious project to formalize mathematics, and its latest version (Lean 4) is trying to be a better programming language. Coq is mature and has been used for a lot of formal proving work (it underlies Iris, mentioned above), but is not a great executable programming language. ATS 2 generates extremely efficient code (it often wins benchmarks) but is inscrutable - probably only a handful of people in the world can write nontrivial programs in it. [1]: https://fbinfer.com/ https://fbinfer.com/ [2]: https://plv.mpi-sws.org/rustbelt/ https://plv.mpi-sws.org/rustbelt/