I'm not sure if the author is here, or if my comment attempt was successful. So, can I suggest you take a look at a third leg of the formal methods stool? If y

I'm not sure if the author is here, or if my comment attempt was successful. So, can I suggest you take a look at a third leg of the formal methods stool? If you are familiar with C, check out Frama-C (https://frama-c.com/ https://frama-c.com/) and the WP and RTE plugins. The approach is based on Tony Hoare and EWD's axiomatic semantics (https://en.wikipedia.org/wiki/Hoare_logic https://en.wikipedia.org/wiki/Hoare_logic). It does not have a good memory management story, as far as I know, but is very good for demonstrating value correctness (RTE automatically generates assertions for numeric runtime errors, for example) and many memory errors. If you are familiar with Ada, check out SPARK (https://www.adacore.com/about-spark https://www.adacore.com/about-spark), which is similar to Frama-C but has a much better interface in the AdaCore GNAT toolkit and IDE. Both work similarly: Assertions in normal Ada or C code as well as the code itself are translated into SMT statements and fed to a SMT solver to find counterexamples---errors. I have some blog posts from several years ago about Frama-C:https://maniagnosis.crsr.net/tags/applied%20formal%20logic.html https://maniagnosis.crsr.net/tags/applied%20formal%20logic.h... (And I really should get back into it; it's a lot of fun.) If you are not familiar with Ada or C, Dafny (https://dafny.org/ https://dafny.org/) is another option based on .NET and devoleped at Microsoft. It seems nigh-on perfect for this approach. (The language uses a garbage collector.) At the time I was looking, there was little documentation on Dafny, but that seems to have improved.