# Formal methods Formal methods reason mathematically over a specification or a program instead of sampling inputs. Where that reasoning is complete, a pass rules a failure out rather than failing to find one. That is the strongest guarantee available and the reason the family is worth its cost. It is a *family*, not a single method: the sub-pages give the recipe per technique, and this page helps pick the right one. The common substance is a *specification*. [Contracts as specifications](https://quality.stereobooster.com/contracts-as-specifications.md) sets out what a specification is, why a contract is one, and the spectrum of ways to discharge the same predicate, from a runtime check through an SMT proof to a hand-written proof term. It is the conceptual map behind the family, not a technique itself. ## What the family catches Each sub-page covers its specific bug classes. At the family level: - Bugs that only an *exhaustive* search of the state space finds. Distributed-protocol interleavings, consensus races, cache-coherence violations — the DynamoDB-style 35-step trace. No example test reaches these; the model checker does. - Bugs that *defy testing by construction*. Verified compilers ([CompCert](https://compcert.org/): zero wrong-code bugs under six CPU-years of [Csmith](https://github.com/csmith-project/csmith) testing (Leroy 2009; Yang et al. 2011)[^leroy2009] [^yang2011]). Once proven, the bug class is gone, not "not yet observed." - Spec ambiguity. Writing the spec formally is what surfaces the ambiguities nobody had noticed; AWS reports this as the largest day-to-day value of formal methods, not the bugs the checker finds. - Decision-logic gaps. Decision tables enumerate every combination of conditions and force the author to confront rows they would otherwise overlook. What the family does **not** catch: the gap between the spec and the implementation. A verified spec the code diverges from is verified-against-the-wrong-thing. The standard countermeasure is to pair formal methods with [property-based testing](https://quality.stereobooster.com/property-based-testing.md), [differential testing](https://quality.stereobooster.com/differential-testing.md), or [deterministic simulation testing](https://quality.stereobooster.com/deterministic-simulation-testing.md) against the implementation surface. ## Picking the right tier | If you are… | Reach for | | ---------------------------------------------------------- | -------------------------------------------------------------------- | | Writing a distributed protocol or consensus algorithm | [Model checking](https://quality.stereobooster.com/model-checking.md) ([TLA+](https://lamport.azurewebsites.net/tla/tla.html)) | | Building business logic with several conditions | [Decision tables](https://quality.stereobooster.com/decision-tables.md) | | Managing a non-trivial state machine | [State machines](https://quality.stereobooster.com/state-machines.md) | | Optimizing an algorithm against an obvious reference | [Executable specifications](https://quality.stereobooster.com/executable-specifications.md) | | Verifying an OS kernel, crypto primitive, compiler | [Theorem proving](https://quality.stereobooster.com/theorem-proving.md) ([Coq](https://rocq-prover.org/), [F\*](https://www.fstar-lang.org/), [Lean](https://lean-lang.org/)) | | Hunting reachability bugs in a parser or syscall surface | [Symbolic execution](https://quality.stereobooster.com/symbolic-execution.md) ([KLEE](https://klee-se.org/), [angr](https://angr.io/)) | | Researching vulnerabilities in a binary | [Symbolic execution](https://quality.stereobooster.com/symbolic-execution.md) (angr, [Manticore](https://github.com/trailofbits/manticore)) | | Proving a real-time / driver loop or smart contract always halts | [Termination analysis](https://quality.stereobooster.com/termination-analysis.md) ([AProVE](https://aprove.informatik.rwth-aachen.de/), [Ultimate](https://ultimate-pa.org/)) | | Proving absence of runtime errors in safety-critical embedded C | [Abstract interpretation](https://quality.stereobooster.com/abstract-interpretation.md) (Astrée, [Frama-C](https://www.frama-c.com/)) | | Bounding a hard-real-time task's worst-case execution time | [WCET analysis](https://quality.stereobooster.com/wcet-analysis.md) (aiT, [OTAWA](https://gitlab.com/otawa)) | The sub-techniques compose. The most comprehensive industrial case studies — DynamoDB (Newcombe et al. 2015)[^newcombe2015], ShardStore (Bornholt et al. 2021)[^bornholt2021], Firecracker (Brooker and Desai 2024)[^brooker2024] — combine multiple sub-techniques plus property-based testing on the implementation. ## When to use, when not **Use:** - When the cost of a bug exceeds the cost of the verification — kernels, crypto, financial logic, distributed protocols, safety-critical embedded. - For spec writing on any system that will outlive its implementation. The formal spec is durable; the implementation may not be. - At the lightweight tier, *liberally*. The decision-table tax is five minutes; the bug-catch rate is high. **Don't:** - At the heavyweight tier for business logic that already type-checks cleanly and has good property tests. The marginal value is low. - As a substitute for testing the implementation. Verified specs don't make wrong code right; pair with empirical methods on the implementation surface. - Without a long-term commitment at the heavyweight tier. Half-finished proofs rot. ## Evidence The family-level evidence is concentrated in industrial deployments: - **AWS** uses model checking (TLA+) on DynamoDB and S3 (Newcombe et al. 2015)[^newcombe2015], lightweight formal methods as daily practice, and theorem proving ([Dafny](https://dafny.org/)) on Cedar (Brooker and Desai 2024)[^brooker2024]. - **[seL4](https://sel4.systems/)** is the canonical theorem-proving deployment: 144 bugs caught during verification of an 8,700-LOC kernel (Klein et al. 2009)[^klein2009]. - **ShardStore** combined lightweight formal methods and property-based testing to catch 16 production-bound bugs on a key-value node for S3 (Bornholt et al. 2021)[^bornholt2021]. Sub-page evidence sections cite the per-technique primary sources. ## Referenced by - [Quality dimensions](https://quality.stereobooster.com/quality-dimensions.md) · Quality dimensions - [Deterministic simulation testing](https://quality.stereobooster.com/deterministic-simulation-testing.md) · Methods - [Methods](https://quality.stereobooster.com/methods.md) · Methods - [Probabilistic model checking](https://quality.stereobooster.com/probabilistic-model-checking.md) · Methods - [Testing machine-learning systems](https://quality.stereobooster.com/testing-ml-systems.md) · Methods - [AI tooling for formal methods](https://quality.stereobooster.com/ai-formal.md) · AI - [Choosing methods](https://quality.stereobooster.com/choosing.md) · Overview ## References [^leroy2009]: Leroy, Xavier. 2009. "[Formal Verification of a Realistic Compiler](https://xavierleroy.org/publi/compcert-CACM.pdf)." *Communications of the ACM* 52 (7): 107–15. . [^yang2011]: Yang, Xuejun, Yang Chen, Eric Eide, and John Regehr. 2011. "[Finding and Understanding Bugs in C Compilers](https://users.cs.utah.edu/~regehr/papers/pldi11-preprint.pdf)." *Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '11)*, 283–94. . [^newcombe2015]: Newcombe, Chris, Tim Rath, Fan Zhang, Bogdan Munteanu, Marc Brooker, and Michael Deardeuff. 2015. "[How Amazon Web Services Uses Formal Methods](https://cacm.acm.org/research/how-amazon-web-services-uses-formal-methods/)." *Communications of the ACM* 58 (4): 66–73. . [^bornholt2021]: Bornholt, James, Rajeev Joshi, Vytautas Astrauskas, et al. 2021. "[Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3](https://www.cs.utexas.edu/~bornholt/papers/shardstore-sosp21.pdf)." *Proceedings of the 28th ACM Symposium on Operating Systems Principles (SOSP '21)*, 836–50. . [^brooker2024]: Brooker, Marc, and Ankush Desai. 2024. "[Systems Correctness Practices at Amazon Web Services](https://cacm.acm.org/practice/systems-correctness-practices-at-amazon-web-services/)." *Communications of the ACM*, ahead of print. . [^klein2009]: Klein, Gerwin, Kevin Elphinstone, Gernot Heiser, et al. 2009. "[seL4: Formal Verification of an OS Kernel](https://www.sigops.org/s/conferences/sosp/2009/papers/klein-sosp09.pdf)." *Proceedings of the 22nd ACM Symposium on Operating Systems Principles (SOSP '09)*, 207–20. . ## Acronyms - LOC — lines of code - SMT — satisfiability modulo theories - WCET — worst-case execution time