[mikedodds]

This is a great question, and unfortunately the existing proof tools are very fragmented when it comes to target languages. E.g. there are a lot of C / LLVM and Java tools, a few C++ tools, a few Rust tools. I don't know of any proof tool that is production-ready that targets Go, Swift, and Kotlin.

One thing I will say is that proof is usually an expensive technique, and not just for the reasons in my post. Even setting up a proof can be demanding. So it's worth asking where in the project it's worth applying this kind of assurance? For example, Galois often applied proofs to cryptography, which are security critical and self-contained in small pieces of code. Proof and formal methods aren't one tool, but rather a toolbox that can solve different assurance problems. There's a big difference from a scalable static analysis like Infer and a fine-grained proof tool like Coq or Galois' SAW tool.

One easy place that formal methods can be useful is in modeling features of a project design for consistency. E.g. this is useful for protocols, state machines and similar. This means you can 'debug your designs' before building them into software. If that sounds like it might useful, I would suggest taking a look at Hillel Wayne's website: https://www.hillelwayne.com

[touisteur]

I think there's already an industrial-grade middleground that is used by at least 2 major automated and interactive proof environments: Why3. Spark and Frama-C use it and it seems part of their success is from it and the ability to use all the SMT engines that Why3 talks to, and also there are bridges to Coq and Isabelle. I've seen people use 'em!

Sadly most of us don't get to rewrite or greenfield stuff, and although Spark is designed to be very progressive and modular, the proof of code that wasn't "written with proof in mind" is still quite the effort.