what would the recommended approach be for someone that's building a piece of software today in a common language ( go, swift, kotlin, ...) and wants to start building proofs around his codebase ?
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
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.
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.
I figure it can't hurt to also mention the Coq/software foundations style separation logic book. In it you build a sequential separation logic, and prove some properties such as soundness (rather than a concurrent separation logic like e.g. Iris above).
The related work section of the summary paper also has a rather extensive list of projects using separation logic, though i'll note I didn't see Infer [1], listed.
