Formal Methods is the study of how we can use mathematics to write bug-free software. FM is on the bleeding-edge of software verification techniques and has already had many high-profile industry success stories.
At a broad level, FM divides into two subfields: proving that the code we write is correct, and proving that the designs we intend to implement are correct. I specialize in the latter, and most of this blog is about design verification. I have written a little about the verification of code but do not consider myself proficient in it.
Designs we can formally verify are also called specifications.
- Highlights
- Highlights for specific FM languages, like TLA+ and Alloy, are on the relevant tags.
- Why Don’t People Use Formal Methods?: An investigation into the history, limitations, and current issues with mass-adoption of formal methods. See also Software correctness is a lot like flossing, a followup I wrote 2 years later about UX/UI challenges in FM tooling.
- The Great Theorem Prover Showdown: A challenge I ran in 2018 on formally verifying three algorithms. Notable for a lot of developers of FM languages, like Edwin Brady and Ranjit Jala, writing up solutions.
- Let’s Prove Leftpad (offsite): After the Theorem Prover Showdown, I contacted all of the contributers and asked them to write up explanations of their tools and leftpad proofs. Let’s Prove Leftpad aggregates all of the proofs so beginners can compare them. An excellent introduction to verifying code.
- Subtopics
-
- Decision Tables: Arguably the simplest formal method to learn, and very useful in a lot of situations.
- TLA+: A specification language for modeling concurrent and distributed systems.
- Alloy: Useful for domain modeling and “graphlike” problems.
- PRISM: For modeling probabilistic systems, like “this fails and retries 20% of the time.”