Our great sponsors
-
-
tlaplus
TLC is a model checker for specifications written in TLA+. The TLA+Toolbox is an IDE for TLA+.
-
WorkOS
The modern identity platform for B2B SaaS. The APIs are flexible and easy-to-use, supporting authentication, user identity, and complex enterprise features like SSO and SCIM provisioning.
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/) 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). 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), 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.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/) 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.
One advantage of formal methods is in determining "what was expected" (including all the goofy edge cases) without having to burrow into the details of code.
Take a look at Alloy (http://alloytools.org/) and TLA+ (https://lamport.azurewebsites.net/tla/tla.html) for example. (Or even the ancient Z ("Zed") notation (https://www.cs.cmu.edu/~15819/zedbook.pdf)).
behave as if it does. The other extreme would be a GUI program.
[1] http://www.animats.com/papers/verifier/verifiermanual.pdf
[2] https://github.com/John-Nagle/pasv