Skip to content

Software Quality

Theorem proving

Theorem proving establishes that a program meets a specification by machine-checked proof. The proof is itself a piece of code (in Coq, Lean, Isabelle, F*, or Dafny), and a small kernel of the proof assistant — a few hundred lines — is what is trusted; everything else is checked against the kernel's rules. The result is the strongest guarantee on the verification spectrum: a verified program cannot exhibit the proven property as a bug under the assumed semantics. The cost is also the highest.

What it catches

  • Wrong-code bugs in verified components. The CompCert verified compiler's middle-end shipped with zero wrong-code bugs after six CPU-years of Csmith testing (Leroy 2009; Yang et al. 2011)1 2.
  • Memory-safety, functional-correctness, and security properties. Once proved, the bug class is gone — not tested for and not found.
  • Spec/implementation disagreement that no testing pipeline can find. A refinement proof forces every gap between the code and its spec to surface as an unmet obligation.
  • Cross-implementation correctness for crypto. Fiat-Crypto's proof eliminates an entire class of arithmetic-correctness bugs (timing-side-channel safety is separate — it comes from the generated code being constant-time, not from the proof).

Theorem proving does not catch bugs outside the spec. A verified-correct implementation of a wrong spec is verified against the wrong thing. This is the spec-gap risk and it is the operative limit on the technique.

Tools

Interactive proof assistants

  • Coq / Rocq — a general-purpose proof assistant; the basis for a large body of verified systems software, including CompCert (Leroy 2009)1, CertiKOS, and Fiat-Crypto (Erbsen et al. 2019)3.
  • Lean 4 — a proof assistant whose dependent-type foundation suits both mathematics and program verification; mathlib4 is the largest formalized mathematics library in the world.
  • Isabelle/HOL — the seL4 specification language; the C kernel was refined against a HOL spec (Klein et al. 2009)4.
  • Agda — dependently typed; less production use than Coq, more use in teaching.

SMT-assisted, semi-automated

  • Dafny — verification-oriented language; SMT-backed; used for the AWS encryption SDK.
  • F* — dependent types + SMT; Project Everest's verified TLS stack (used in Microsoft Edge's QUIC implementation).
  • Verus — Rust-flavored verification language; SMT-backed; a research project aimed at making proof-carrying Rust ergonomic.
  • Why3 — multi-prover frontend; dispatches goals to Coq, Alt-Ergo, Z3, CVC5.
  • Lean's automated tactics (omega, polyrith, decide, aesop) — reduce the amount of manual proof in Lean developments.

Correct-by-construction refinement

The B-method and Event-B are a development style rather than a separate method: the program is built by stepwise refinement from an abstract specification, and each step emits proof obligations whose discharge shows the refinement preserves behavior, so the code is correct by construction rather than proven after the fact. Atelier B and Rodin are the toolchains, and the approach's record is in railway signaling — the Paris Métro line 14 controller. The verification underneath is the same machine-checked proof; refinement organizes the development around it.

Trusted base

  • SMT solvers are not trusted on their own; Coq, Lean, F*, Dafny, and Why3 either re-check SMT-generated proof certificates or run the proof against the trusted kernel. The SMT solver is an oracle, not a verifier.
  • Z3, CVC5, Yices2, Alt-Ergo are the dominant SMT back-ends.

When to use, when not

Use:

  • Components with high blast radius and small surface: OS kernels, hypervisors, bootloaders, crypto primitives, TLS stacks, formally verified compilers. The ratio of cost to defects-eliminated favors verification at this end.
  • Spec writing for any system that must outlive its implementation. The proof is a durable artifact; the implementation may not be.
  • After a major incident attributable to a class of bug a proof could have eliminated. The cost of the incident often justifies the cost of the verification afterwards.

Don't:

  • For business logic, CRUD, glue code. The cost ratio is wrong. Use contracts for the same shape at orders of magnitude less effort.
  • As a substitute for testing the spec itself. Test the spec at least as hard as the code; Csmith against CompCert is the canonical pairing.
  • Without a long-term commitment. An abandoned proof leaves the code with unmet obligations and no guarantee.

Evidence

  • seL4. Formal verification of an 8,700-LOC microkernel against an Isabelle/HOL spec; 144 defects found during proof; ~11 person-years for the proof itself (≈20 including tooling and research) (Klein et al. 2009)4.
  • CompCert. Compiler correctness proved end to end in Coq (Leroy 2009)1.
  • Fiat-Crypto. Machine-checked elliptic-curve field arithmetic, generated by the proof and deployed in Chrome and Android (Erbsen et al. 2019)3.
  • Project Everest. Verified TLS 1.3 stack and crypto primitives in F*; verification surfaced TLS 1.3 spec ambiguities that were fed back into the IETF process. HACL* / EverCrypt is deployed in Mozilla NSS (Firefox), the Linux kernel, Windows kernel / Hyper-V, and Python's hashlib.
  • AWS Cedar. Machine-checked verification (Dafny) of the authorization-policy engine (Brooker and Desai 2024)5.

The empirical record is concentrated in deployments where the cost/benefit is unusually favorable: kernels, crypto, compilers. At those targets the empirical support is direct and repeated across independent projects. For typical CRUD applications, no published evidence supports the ratio.

Oracle: predicate

All four answer the same question — does property P hold? — and differ only in how that answer is obtained, from cheapest-and-weakest to strongest:

  • Runtime contracts — check P during execution, on the inputs you actually run, and crash if it's violated.
  • Property-based testing — check P on many generated inputs; empirical, with no guarantee past what was sampled.
  • Refinement & dependent types — encode P in the type, so the compiler rejects any program that could violate it (sound within what the type can express).
  • Theorem proving — prove P holds for all inputs, ahead of time.

Classification

  • Quality dimensions: Functionality, Security (proves adversarial security properties — kernel isolation and information-flow non-interference (seL4)).
  • Area: OS kernels and hypervisors, verified compilers, crypto primitives and TLS stacks, safety-critical embedded software.
  • Guarantee: Mathematical — within the assumed semantics, no failure exists at all.

Referenced by

References

  1. Leroy, Xavier. 2009. "Formal Verification of a Realistic Compiler." Communications of the ACM 52 (7): 107–15. https://doi.org/10.1145/1538788.1538814. ↩↩↩

  2. Yang, Xuejun, Yang Chen, Eric Eide, and John Regehr. 2011. "Finding and Understanding Bugs in C Compilers." Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '11), 283–94. https://doi.org/10.1145/1993498.1993532. ↩

  3. Erbsen, Andres, Jade Philipoom, Jason Gross, Robert Sloan, and Adam Chlipala. 2019. "Simple High-Level Code for Cryptographic Arithmetic: With Proofs, Without Compromises." IEEE Symposium on Security and Privacy (s&p '19), 1202–19. https://doi.org/10.1109/SP.2019.00005. ↩↩

  4. Klein, Gerwin, Kevin Elphinstone, Gernot Heiser, et al. 2009. "seL4: Formal Verification of an OS Kernel." Proceedings of the 22nd ACM Symposium on Operating Systems Principles (SOSP '09), 207–20. https://doi.org/10.1145/1629575.1629596. ↩↩

  5. Brooker, Marc, and Ankush Desai. 2024. "Systems Correctness Practices at Amazon Web Services." Communications of the ACM, ahead of print. https://doi.org/10.1145/3729175. ↩