Compendium

Formal Verification & Fuzzing — Model Checking, SAT/SMT, Proof Assistants, AFL

18 min read

Formal Verification & Fuzzing

Two complementary disciplines aimed at the same goal — high assurance about program behavior. Formal verification proves a program (or a model of it) satisfies a specification: the absence of certain classes of bugs becomes a theorem. Fuzzing is the empirical opposite — generate enormous numbers of inputs cheaply and watch for crashes or assertion failures. In practice both are used together: formal methods on the small, critical core (microkernels, compilers, cryptographic primitives, consensus protocols); fuzzing on the much larger periphery that is impossible to fully specify.

The dividing line has moved repeatedly. SMT solvers made symbolic execution tractable on real C; coverage-guided fuzzing made bug-finding cheap enough to deploy continuously; refinement types and lightweight verifiers (Dafny, Liquid Haskell, F*) closed much of the cost gap with traditional proof assistants. The result is that, by the mid-2020s, both Microsoft Azure and AWS routinely ship TLA+ specs alongside distributed systems code, OSS-Fuzz continuously runs thousands of fuzzers on open-source dependencies, and verified C compilers and microkernels are deployed in real aerospace and defense systems.

This note is a reference catalog of the techniques, tools, papers, people, and high-profile findings of both fields.

1. Theoretical foundations

Program semantics — the formal meaning of code — comes in three classical styles:

  • Denotational semantics — programs as mathematical functions over domains. Scott-Strachey 1970s; categorical foundations.
  • Operational semantics — programs as labeled transition systems. Plotkin’s structural operational semantics SOS (1981) is the workhorse for most modern language definitions.
  • Axiomatic semantics — programs characterized by which logical assertions hold before and after them.

The axiomatic foundation for verification was laid by C.A.R. Hoare’s 1969 paper “An Axiomatic Basis for Computer Programming”. Hoare logic uses triples {P} S {Q}: if precondition P holds, executing statement S terminates in a state satisfying Q. Composition, conditional, and (especially) loop invariants give a syntax-directed proof system. Dijkstra’s weakest-precondition calculus (1975) is the predicate-transformer dual.

For pointers and heap mutation, classical Hoare logic falls apart — frame conditions explode. Separation logic (Reynolds 2002, “Separation Logic: A Logic for Shared Mutable Data Structures”, building on John C. Reynolds, Peter O’Hearn, Hongseok Yang, and earlier Burstall work) introduced the separating conjunction P * Q — meaning P and Q hold over disjoint heap regions — and the frame rule, enabling local reasoning. Concurrent Separation Logic (CSL) (Brookes-O’Hearn 2007) extends this to shared-memory concurrency by attaching invariants to locks and resources. The 2019 ACM Turing Award went to O’Hearn (jointly noted for Facebook Infer, which is a separation-logic-derived static analyzer).

Iris (Jung, Krebbers, Birkedal, Bizjak, Mansky, Dreyer, Vafeiadis, “Iris from the Ground Up” JFP 2018) is the modern, higher-order, impredicative, step-indexed concurrent separation logic implemented as a library in Coq. It is the foundation of RustBelt (Jung-Jourdan-Krebbers-Dreyer 2018), which formally verified that Rust’s type system soundly guarantees memory safety despite the use of unsafe.

2. Model checking

Model checking exhaustively explores the state space of a (usually finite-state) abstraction of the system. The 2007 Turing Award went to Clarke, Emerson, and Sifakis for inventing it.

2.1 Explicit-state model checking

  • SPIN — Gerard Holzmann, Bell Labs, 1991+. The input language is Promela (Process Meta-Language); properties expressed as LTL. SPIN won the 2001 ACM Software System Award. Used historically for Mars rover protocols, telephony switches, and many concurrent-algorithm correctness arguments.
  • TLA+ — Leslie Lamport, 1999. “Specifying Systems” (2002) is the canonical book. Properties expressed in Temporal Logic of Actions; checking via the TLC model checker; proof obligations via TLAPS. The PlusCal algorithmic frontend (Lamport 2009) compiles to TLA+. Amazon famously adopted TLA+ for DynamoDB and S3 specifications — Chris Newcombe et al., “How Amazon Web Services Uses Formal Methods” CACM 2015, reporting concrete bugs caught in Dynamo, EBS, and S3 designs. Microsoft uses TLA+ inside Azure Cosmos DB for consistency level proofs. MongoDB, Elastic, and CockroachDB have all used TLA+ for replication protocols.
  • mCRL2 — successor of CRL/μCRL; process algebra; Eindhoven University.

2.2 Symbolic model checking

  • NuSMV / nuXmv — Cimatti, Bozzano, et al., FBK Trento. BDD- and SAT-based; supports CTL/LTL.
  • CMC, SAL — SRI International.
  • VIS — Berkeley; predecessor of many academic tools.

2.3 Bounded model checking (BMC)

Clarke-Biere-Cimatti-Zhu, “Symbolic Model Checking without BDDs” TACAS 1999 — unwind the transition relation k steps, send the resulting formula to a SAT/SMT solver. Tools:

  • CBMC — Bounded model checker for C/C++ (Kroening, Oxford).
  • ESBMC — Efficient SMT-based BMC (Cordeiro, Manchester).
  • CPAchecker — Configurable Program Analysis, Beyer et al., Munich.
  • JBMC — Java variant of CBMC.
  • KLEE — Cadar-Dunbar-Engler 2008, OSDI. Symbolic execution on LLVM IR; finds bugs by exploring path constraints fed to STP/Z3. Used to find serious bugs in GNU coreutils, BusyBox.

2.4 Statistical and timed model checking

  • UPPAAL — Behrmann, David, Larsen et al., Aalborg + Uppsala. Timed automata for real-time and hybrid systems; statistical model checking variant SMC-UPPAAL.
  • PRISM — probabilistic model checker (Birmingham, Oxford).
  • Storm — probabilistic model checker (Aachen).

3. SAT solvers

Boolean satisfiability is the original NP-complete problem (Cook 1971; Levin independently 1973). Modern SAT solvers implement CDCL — Conflict-Driven Clause Learning — derived from the DPLL algorithm (Davis-Putnam-Logemann-Loveland 1962). Key innovations: two-watched literals, VSIDS variable scoring, restarts, clause minimization, preprocessing.

Important solvers (most are SAT Competition winners across years):

  • MiniSat — Eén-Sörensson 2003. Tiny, hackable reference implementation; foundation of countless derivatives.
  • Glucose — Audemard-Simon 2009; LBD-based clause-quality metric.
  • Lingeling / Plingeling / Treengeling — Armin Biere, JKU Linz.
  • MapleSAT, Maple-LCM-Dist — Toronto.
  • CaDiCaL — Biere, modern clean-room successor to Lingeling.
  • kissat — Biere; SAT Competition main-track winner in 2020, 2021, 2022 (variants), and the basis for many subsequent winners.
  • CryptoMiniSat — Soos; XOR-aware, used in cryptanalysis.

For unsatisfiability proofs the DRAT-trim format and checker (Heule et al.) is now the SAT Competition standard.

4. SMT solvers

SMT — Satisfiability Modulo Theories — adds first-order theories (linear arithmetic over Z or Q, bit-vectors, arrays, uninterpreted functions, strings, floating-point, datatypes) to SAT. The SMT-LIB standard (Barrett-Stump-Tinelli 2010+) defines a common input format.

Major solvers:

  • Z3 — Microsoft Research, Leonardo de Moura and Nikolaj Bjørner, “Z3: An Efficient SMT Solver” TACAS 2008. Open-sourced 2015 (MIT). The de facto industrial workhorse — Boogie, Dafny, F*, Liquid Haskell, Viper, Klee, SAGE all use it. Recent extensions: model-based quantifier instantiation, NL arithmetic.
  • CVC5 — Stanford and Iowa, successor of CVC4. Strong on quantifiers, theories, and proof production.
  • Yices2 — SRI International, Bruno Dutertre. Very fast on quantifier-free linear arithmetic; used in industrial settings (Galois, Cisco).
  • MathSAT — Bruttomesso, Cimatti, Franzén, Griggio, Sebastiani, FBK Trento.
  • Bitwuzla — Niemetz-Preiner, modern bit-vector specialist (successor to Boolector).
  • Alt-Ergo — OCamlPro/INRIA; used by Why3 and Frama-C.
  • veriT — used in Isabelle’s smt tactic.

5. Proof assistants (interactive theorem provers)

Proof assistants are languages where the user constructs a machine-checked proof term, usually in a dependently-typed logic.

5.1 Coq / Rocq

Coquand-Huet 1989 (INRIA). Based on the Calculus of Inductive Constructions — a dependent type theory where propositions are types and proofs are programs (the Curry-Howard correspondence). Rebranded as Rocq in 2024 to avoid the obvious naming problem. Canonical textbook: Bertot-Castéran, “Interactive Theorem Proving and Program Development” 2004.

Landmark Coq verifications:

  • CompCert — Xavier Leroy, INRIA 2009+. A formally verified optimizing C compiler — every pass is proven to preserve program semantics. About 100k lines of Coq. Used commercially (AbsInt). Yang-Chen-Eide-Regehr’s Csmith fuzzer ran against major C compilers and found dozens of miscompilation bugs in GCC and Clang while finding essentially none in CompCert.
  • Four Color Theorem — Georges Gonthier 2005.
  • Feit-Thompson Odd-Order Theorem — Gonthier et al. 2012. Roughly 250-page paper formalized.
  • VST (Verified Software Toolchain) — Princeton, Andrew Appel. Coq-based separation-logic program logic for CompCert C.
  • IronFleet — Microsoft Research; verified Paxos/Multi-Paxos and a key-value store.

5.2 Lean

Leonardo de Moura, Microsoft Research, started Lean in 2013. Lean 4 (2021) is self-hosting (the elaborator is written in Lean itself) and macro-friendly. The community-driven mathlib library (mathlib4 in Lean 4 since 2023) now contains over 100,000 definitions and theorems and is the largest unified mathematics library ever assembled.

Two landmark mathematics formalizations show the trajectory:

  • Liquid Tensor Experiment (2020-2022) — Peter Scholze (Fields Medalist) challenged formalizers to mechanize a key step in his condensed mathematics. Kevin Buzzard and a Lean community team completed it in roughly 18 months.
  • Polynomial Freiman-Ruzsa conjecture (2023) — Terence Tao announced the result with collaborators and the Lean community formalized the full proof in about 2 weeks.

Lean is also the backbone of AlphaProof (DeepMind 2024), which reached IMO silver-medal level.

5.3 Isabelle/HOL

Larry Paulson (Cambridge) and Tobias Nipkow (Munich), since the late 1980s. Based on classical higher-order logic (Church’s simple type theory) rather than dependent types — less expressive but easier to automate. Strong automation via Sledgehammer (calls external ATPs and SMT solvers and reconstructs proofs).

The most famous Isabelle/HOL verification is seL4 — Gerwin Klein, Kolanski, Andronick, Heiser et al. at NICTA → Data61/CSIRO, “seL4: Formal Verification of an OS Kernel” SOSP 2009. About 9,000 lines of C kernel against a Haskell executable spec, proved correct and free of buffer overflows, null-pointer derefs, etc. Total proof: roughly 200,000+ lines of Isabelle. Deployed in military aviation, automotive, and industrial control via the seL4 Foundation.

5.4 Agda

Ulf Norell, Chalmers 2007. Dependently typed, focused on programming with proofs rather than industrial proof automation. Used heavily in HoTT/cubical type theory research.

5.5 F*

Microsoft Research and INRIA; Nikhil Swamy lead. F* is an ML-family language with refinement types and dependent types, discharging proof obligations through Z3. The flagship application is Project Everest, a verified HTTPS stack:

  • HACL* — verified cryptographic library (Curve25519, ChaCha20, Poly1305, AES, SHA-2/3). Extracted to C; deployed in Mozilla NSS, Linux kernel, and Wireguard implementations.
  • miTLS — verified TLS 1.3 reference implementation.
  • EverParse — verified binary parsers.
  • EverCrypt — multiplexed verified crypto provider.

5.6 Other proof assistants

  • Idris / Idris 2 — Edwin Brady. Pragmatic dependently-typed language; emphasizes effects, totality, and dependent quantitative types.
  • ACL2 — Bob Boyer, J Strother Moore, Matt Kaufmann. First-order pure Lisp. Industrial hardware verification: AMD K5/K7 floating-point microcode; Centaur Technology; Intel; Rockwell Collins flight controls. ACL2 received the 2005 ACM Software System Award.
  • Twelf — Frank Pfenning, Carsten Schürmann, CMU. Logical Framework LF; used heavily for metatheory of programming languages (POPLmark).
  • PVS — SRI International; classical higher-order logic with predicate subtypes.
  • HOL Light — John Harrison; minimal, ML-based; used heavily at Intel for floating-point verification.
  • Mizar — original mathematical proof system, Poland 1973.

6. Refinement types and lightweight verification

Sitting between unsound static analysis and full proof assistants:

  • Liquid Haskell — Vazou-Jhala-Seidel, “Refinement Types For Haskell” ICFP 2014. SMT-discharged refinement types on top of GHC.
  • Dafny — K. Rustan M. Leino, Microsoft Research 2010. Imperative language with pre/post-conditions, ghost code, and loop invariants discharged by Z3 via the Boogie intermediate verification language. AWS used Dafny heavily for AWS Encryption SDK and parts of authentication code.
  • Why3 — INRIA + LRI. WhyML intermediate language and multi-prover backend (Z3, Alt-Ergo, CVC5, Coq).
  • Frama-C — CEA-LIST. C analyzer using the ACSL specification language; Why3 backend for proofs. Deployed in nuclear, automotive, and aerospace certification.
  • Viper — ETH Zürich (Müller). Permission-based verification IVL; used by Prusti (Rust verifier) and several research projects.
  • VST (Verified Software Toolchain) — Princeton (Appel). Coq-based program logic for CompCert C.

7. Hardware verification

The Intel FDIV bug in the Pentium (1994) cost Intel about USD 475 million in replacements and was the catalyst for the modern hardware-formal-verification industry. Today the field is enormous.

  • ACL2 — AMD K7/K8/Bulldozer floating-point microcode; Centaur Technology (their entire VIA x86 designs); Rockwell Collins.
  • Cadence JasperGold — acquired Jasper Design Automation 2014. The dominant commercial formal property checker on RTL Verilog/VHDL.
  • Synopsys VC Formal — competitor.
  • OneSpin — acquired by Siemens EDA 2021. Strong in safety-critical and high-assurance ASIC flows.

Specification languages: SVA SystemVerilog Assertions, PSL Property Specification Language, e specification language. Equivalence checking between RTL and netlist is now standard at synthesis sign-off.

Hardware fuzzers are an active research area — see Section 9.

8. Verified software systems — additional case studies

  • CompCert — Section 5.1.
  • seL4 — Section 5.3.
  • CertiKOS — Yale (Zhong Shao). Verified concurrent OS kernel with multicore support, Coq-based.
  • IronFleet — Microsoft Research, “IronFleet: Proving Practical Distributed Systems Correct” SOSP 2015. Verified Paxos + key-value store in Dafny.
  • IronClad Apps — Microsoft Research 2014. Verified application stacks (notebook, password hasher, etc.).
  • VeriBetrFS / BetrFS — Stony Brook + others; verified write-optimized file system.
  • vAlc — verified Algorand BA* consensus, Project Everest collaborators.
  • CakeML — verified compiler for an ML dialect (Owens, Myreen, Tan et al.); the compiler bootstraps itself within HOL4.
  • Linux Kernel Memory Model (LKMM) — Alglave, Maranget, McKenney 2018; a formal model of Linux memory ordering used to drive kernel-internal consistency arguments.
  • TLA+ industrial deployments — Section 2.1; Amazon DynamoDB/S3; Microsoft Cosmos DB; Cosmos Hub / Cosmos SDK consensus; MongoDB replication; CockroachDB Raft variant; OpenJDK locking primitives (Doug Lea).

9. Fuzzing — coverage-guided

The modern era began with AFL — American Fuzzy Lop — Michał Zalewski (Google) 2013. AFL instruments target binaries (or recompiles them with afl-gcc/afl-clang), executes with random or mutated inputs, and uses edge-coverage feedback to retain interesting inputs in a corpus. Genetic-algorithm-style mutation (bitflips, arithmetic, dictionary-driven, splicing, havoc) makes it surprisingly effective. AFL found thousands of bugs in OpenSSL, libtiff, BIND, sqlite, ffmpeg, ImageMagick, etc.

The active fork is AFL++ (Fioraldi et al., community, 2019+) — adds CmpLog, RedQueen, custom mutators, QEMU+Unicorn modes for binary-only targets, persistent mode, and many performance improvements. AFL++ is now the default reference.

libFuzzer — LLVM in-process coverage-guided fuzzer (Serebryany, Google). Tests a LLVMFuzzerTestOneInput(data, size) entry point. Replaced or complemented by AFL++ in many flows but still the default for OSS-Fuzz integration in C/C++.

Other coverage-guided fuzzers:

  • Honggfuzz — Robert Swiecki, Google. Multi-process, hardware-assisted (Intel PT, BTS) coverage.
  • Jazzer — JVM coverage-guided fuzzer based on libFuzzer (Code Intelligence).
  • Atheris — Python coverage-guided fuzzer (Google).
  • cargo-fuzz / libfuzzer-sys / AFL.rs — Rust integrations.
  • go-fuzz and Go 1.18+ native fuzzing (go test -fuzz).
  • syzkaller — Vyukov, Google. Kernel fuzzer; written specifically for Linux/Windows/FreeBSD/macOS kernels via syscall descriptions; thousands of kernel CVEs to date.

10. Symbolic and concolic execution

  • KLEE — Cadar-Dunbar-Engler 2008, OSDI. Symbolic execution on LLVM IR with constraint solving (STP/Z3); see Section 2.3.
  • SAGE — Patrice Godefroid, Microsoft Research 2008+. Scalable Automated Guided Execution — whitebox fuzzing. Famously used to find serious bugs in Windows file parsers (ANI, JPG, etc.).
  • Angr — UCSB Shellphish (CGC participants). Python-based binary analysis platform: symbolic execution, VEX IR lifting, integration with Unicorn, claripy constraint solver.
  • Driller — Stephens et al., NDSS 2016. Combines AFL with Angr — AFL drives shallow exploration cheaply; Angr concolically solves hard branches; the resulting input feeds back to AFL.
  • S2E — EPFL; selective symbolic execution.
  • Manticore — Trail of Bits; Python symbolic executor for x86/ARM and EVM.

11. Grammar-based and structure-aware fuzzing

  • Grammarinator — generator-based grammar fuzzer (Ericsson).
  • Peach Fuzzer — protocol-aware (acquired by Peach Tech → GitLab → discontinued; the term lives on).
  • Radamsa — Aki Helin / OUSPG; mutational general-purpose.
  • Domato — Ivan Fratric, Google Project Zero. DOM/HTML fuzzer that found many browser bugs.
  • boofuzz — Python protocol fuzzer (successor of Sulley).
  • Dharma — Mozilla; generator using BNF-like grammars.

12. Differential fuzzing

Run the same input through two or more implementations of a spec and flag divergence.

  • Csmith — Yang-Chen-Eide-Regehr, “Finding and Understanding Bugs in C Compilers” PLDI 2011. Generates random valid C programs; runs them through GCC, Clang, etc.; reports miscompilations. Found hundreds of GCC/Clang bugs and zero in CompCert.
  • YARPGen — Yet Another Random Program Generator (Intel); successor of Csmith for modern C++.
  • YugaByte / CockroachDB SQL fuzzers — differential against Postgres.
  • TLS-Attacker / frankencerts (Brubaker-Jana-Ray-Khurshid-Shmatikov 2014) for TLS implementations.
  • Mempool / Mempool-fuzz for crypto verifier corner cases.

13. Fuzzing services and infrastructure

  • OSS-Fuzz — Google 2016+. Continuous fuzzing infrastructure on ClusterFuzz, free for qualifying open-source projects. As of 2025 OSS-Fuzz monitors more than 1,000 projects and has found roughly 46,000 bugs, including thousands of security-relevant ones. Notable: it found dozens of bugs in OpenSSL after Heartbleed.
  • ClusterFuzz — Google’s internal infrastructure, open-sourced 2019.
  • Microsoft OneFuzz — open-sourced 2020, archived 2024 (Microsoft moved to internal-only).
  • Mayhem — ForAllSecure (Brumley, CMU). Won the DARPA Cyber Grand Challenge 2016. Now commercial.
  • Fuzzbench — Google benchmarking platform for fuzzer comparison.
  • Atheris/Jazzer/Cargo-Fuzz CI integration — increasingly default in language ecosystems.

Bug bounty intermediaries — HackerOne, Bugcrowd, Synack, YesWeHack. Corporate VRPs — Google VRP, Apple Security Bounty (up to USD 2M for full chains), Microsoft, Meta. The economic model now sustains a substantial professional fuzzing/exploit-development community.

14. Hardware and low-level fuzzing

  • DifuzzRTL — Hur, Song, et al., USENIX Security 2021. Coverage-guided RTL fuzzing on Verilog designs; found bugs in RocketChip and BOOM.
  • Cocofuzz — Cocotb-based RTL fuzzing.
  • RFUZZ — Laeufer et al., ICCAD 2018; RTL fuzzing with mux toggling coverage.
  • Snapchange — AWS open-source snapshot fuzzer using KVM (2023).
  • Nyx — Schumilo et al., USENIX Security 2021; hypervisor-based snapshot fuzzing.
  • What the Fuzz (wtf) — Axel Souchet (2020+); cross-platform snapshot fuzzer.

15. Static analysis ecosystem (adjacent to verification)

Static analysis trades soundness for scale. Commercial heavyweights:

  • Coverity — Stanford spin-out → Synopsys. Industry standard for enterprise C/C++.
  • Klocwork — Perforce.
  • CodeSonar — GrammaTech (acquired by Roche / now spun out as CodeSecure).
  • PVS-Studio — Russian/Tula company; strong on C/C++/C# pattern detection.
  • Astrée — AbsInt + ENS-Paris. Abstract-interpretation-based; deployed on Airbus A380 flight-control software, where it proved absence of runtime errors on roughly 800k lines of C.
  • Polyspace — MathWorks; abstract interpretation.
  • Facebook Infer — open-sourced 2015. Separation-logic-based interprocedural analyzer; foundation of compositional analyses now used across Facebook/Meta and open-source.
  • Semmle / CodeQL — Semmle founded by Oege de Moor; acquired by GitHub 2019. Treats code as a database; relational query language. Free for open source.
  • Snyk Code (formerly DeepCode, acquired 2020).
  • Checkmarx, Veracode, Fortify — enterprise SAST suites.

Rust-specific:

  • Clippy — official lints.
  • cargo-deny — supply-chain auditing.
  • MIRAI — Facebook abstract interpreter for Rust MIR.
  • Kani — AWS-funded, model-checker for Rust based on CBMC.
  • Prusti — ETH Zürich; Viper-based deductive verifier.
  • Creusot — INRIA; Why3-backed.

16. AI/LLM-assisted formal verification

A genuine research frontier since 2020 — language models trained to suggest tactics in Coq/Lean.

  • GPT-f / Polu et al. — OpenAI 2020, “Generative Language Modeling for Automated Theorem Proving”. Transformer-based tactic prediction in Metamath.
  • Lean GPT-f / PACT — “Proof Artifact Co-Training for Theorem Proving with Language Models” Han-Rute-Wu-Ayers-Polu 2022.
  • Llemma — Princeton/EleutherAI 2023; open-source math LLM tuned on Proof-Pile-2.
  • AlphaProof + AlphaGeometry / AlphaGeometry 2 — DeepMind 2024. AlphaProof works in Lean; AlphaGeometry uses a custom symbolic engine. Together reached an IMO 2024 silver-medal score (28/42).
  • Coq Tactician, TacticToe, CoqGym, HOList — earlier ML-for-ITP infrastructure.

Classical ATPs (still relevant): Vampire (Voronkov), E (Schulz), iProver (Korovin), CVC5 in quantifier mode, Z3 in quantifier mode.

17. Industrial high-assurance deployments

Concrete deployed examples:

  • TLA+ — Amazon (DynamoDB, S3, EBS); Microsoft Cosmos DB; OpenJDK locking primitives; Cosmos SDK; MongoDB; CockroachDB. Newcombe et al. CACM 2015 is the canonical reference.
  • seL4 — military aircraft (Boeing MUM-T efforts); automotive (autonomous driving stacks); industrial control.
  • CompCert — used by ANSSI and by safety-critical avionics; AbsInt commercial product.
  • Project Everest / HACL* — Mozilla Firefox NSS, Linux kernel crypto (lib/crypto/curve25519-hacl64.c), WireGuard kernel implementations, Microsoft Symcrypt parts.
  • AWS Cryptographic libraries — large fractions verified with Dafny, Coq (via HACL*), and SAW.
  • Cardano Plutus + Ouroboros — extensive Agda and Isabelle formalizations.
  • Algorand — formal proofs of BA* consensus.
  • Boeing 787 / Airbus A380 — Astrée abstract interpretation.

18. Famous bugs found by formal methods or fuzzing

  • Intel FDIV (1994) — found by Thomas Nicely doing twin-prime computations; spawned the hardware formal verification industry.
  • Heartbleed (CVE-2014-0160, OpenSSL) — found by Codenomicon’s fuzzer (and independently by Neel Mehta of Google). Catalyst for OSS-Fuzz and the Core Infrastructure Initiative.
  • Shellshock (CVE-2014-6271, Bash) — found by Stephane Chazelas via manual review, but stress-fuzzing afterwards found many adjacent bugs.
  • DROWN, ROBOT, Bleichenbacher variants — RSA-PKCS1 padding-oracle attacks found through differential analysis of TLS implementations.
  • KASLR bypass / Foreshadow / Plundervolt / Æpic Leak — SGX side channels.
  • SROP (Sigreturn-Oriented Programming) — Bosman-Bos 2014.
  • ROP (Return-Oriented Programming) — Shacham 2007.
  • TCP/IP stack bugs in Ripple20, URGENT/11, NUMBER:JACK — found by JSOF, Armis, Forescout using fuzzing and review of long-tail embedded stacks.

19. Bug reduction and triage

Once a fuzzer finds a crash, reducing it to a small reproducer is essential.

  • Delta debugging — Andreas Zeller, “Simplifying and Isolating Failure-Inducing Input” TSE 2002. The ddmin algorithm.
  • C-Reduce — Regehr-Yang-Eide, PLDI 2012. Reduces failing C programs; widely used in compiler bug reports.
  • creduce / cvise — modern C-Reduce successors.
  • tree-sitter-reduce — language-agnostic via Tree-sitter grammars.

20. Where to learn

Books and courses:

  • Bertot-Castéran, Interactive Theorem Proving and Program Development (Coq).
  • Pierce et al., Software Foundations (free, web). Coq-based, multi-volume.
  • Avigad et al., Theorem Proving in Lean / Mathematics in Lean.
  • Nipkow-Klein, Concrete Semantics with Isabelle/HOL.
  • Clarke-Grumberg-Peled, Model Checking. The classic textbook (2nd ed. 2018).
  • Baier-Katoen, Principles of Model Checking.
  • Bradley-Manna, The Calculus of Computation.
  • Holzmann, The SPIN Model Checker.
  • The Fuzzing Book — Zeller et al., open online textbook.

Conferences: POPL, PLDI, CAV, TACAS, OOPSLA, ITP, CPP, ICFP, FMCAD (hardware), NDSS / S&P / USENIX Security / CCS for fuzzing and security.

Adjacent

  • cryptography-fundamentals — what HACL*, miTLS, and many ZKP libraries (Section on ZK in privacy note) actually verify.
  • concurrency-primitives — separation logic, CSL, and Iris are the verification machinery for the primitives there.
  • compiler-design — CompCert and CakeML are verified compilers; differential fuzzing (Csmith) targets unverified ones.
  • consensus-protocols — TLA+ in DynamoDB/Cosmos DB, IronFleet’s verified Paxos, formal Algorand and Tendermint proofs.
  • lock-free-data-structures-and-rdma — Iris and RustBelt are used to verify lock-free algorithms with relaxed memory.
  • logic-foundations — Hoare logic, separation logic, Curry-Howard, dependent type theory.

Graph View