Why does bounded model checking of C blow up on loops, and how do function contracts fix it? Title: Function Contracts for Bounded Model Checking of C Programs URL: ❓ Why is BMC so heavy? It unrolls loops N times and inlines every call. A function with an N-iteration loop called from K sites costs roughly N×K. 💡 What changes with contracts? The body is verified once against its contract, and each call is replaced by a stub derived from that contract. No unrolling is needed, so cost no longer scales with call count. ❓ What is new here? The authors add contract support to ESBMC. The assigns clause is checked observationally: snapshot the locations that must not change on entry, compare them at exit. Formula size depends on the number of globals, not the number of writes, unlike CBMC. The algebraic core is machine-checked in Lean 4. ❓ How well does it work? ・N=20,K=10: direct verification times out past 120 s, modular finishes in 12.5 s ・N=10,K=10: 42.0 s down to 1.8 s (23.3x) ・With 500 writes, ESBMC emits 5 VCCs vs. 521 for CBMC ・At the FIPS-203 ML-KEM size, monolithic runs exceed 10 minutes in both tools, but modular completes Note that at K=1 it is slower. #FormalVerification# #ModelChecking#

while i'm quite bullish on formal methods, i think it's worth tempering expectations and doing your own research on it (disclaimer: i am not an expert in it). it cannot guarantee your code is bug free, only that it matches the spec under certain assumptions, and the specs come from what people want, not math. as long as we build software for humans, nothing can prove that your spec is right, only you can judge. i created the /statechart skill in pstack primarily because it helps make the state machines implicit in your code more obvious and legible to you, so you can shrink the review surface and review the work at a higher level: does it actually match your intent and goal? i used this skill a ton while building my game below you can see the statechart for story mode where i was able to find many bugs with it. in that sense, i think model checking (eg TLA+ with TLC) is quite useful for understanding and checking properties of your system e2e, and you don't have to write tons of new verification code for it. the spec isn't your actual code so there's always a risk of drift, but so far i've had good experiences finding actual bugs with it. i tend to pair it with empirical verification (running the code) also to confirm it's real other types of formal verification like proving theorems (eg Lean, Dafny), bounded model checking (eg CBMC, Kani) etc have their own tradeoffs. proofs cover every possible input, but only for the properties specified, and it takes a lot more code/work. bounded model checking can run on your actual code, which avoids drift, but it only checks up to a certain number of steps, so it's better at finding bugs than proving there aren't any so i think in the near-medium term you'll still need to layer your codebase: constraints and guardrails (types, lint rules, api design, refactoring), empirical verification (tests, evals, real usage), and formal verification for the parts that really need it. none of these catch everything on their own, but layered together, they catch a lot more and shrink what's left for you to review but also maybe in the limit, the bitter lesson will prevail and flawless code will just be printed out perfectly every time with no bugs. even in that scenario, /statechart still seems very helpful in confirming that the agent understood your intent correctly. give it a try if you haven't already!

Don't learn formal methods. Writing proofs by hand is what kept formal methods niche for over 75 years. seL4 took about 20 person-years to prove 8,700 lines of C. Agents take that part now. What's left for you is the spec, and knowing which language fits the job. That's why the history matters. Formal methods means stating what a program or system must do in precise math, then using a tool to check that the code or design meets it. Here's how we got here, what each language is good for, and where I'd start. FOUNDATIONS (1947 to 1979) 1947: Goldstine and von Neumann annotate program flow diagrams with "assertion boxes" stating what holds at each point. 1949: Alan Turing's "Checking a Large Routine" proves a short program correct using assertions. The idea mostly sits unused for over a decade. 1962: Carl Adam Petri's dissertation introduces Petri nets for modeling concurrent systems. 1963: John McCarthy, "A Basis for a Mathematical Theory of Computation". 1966-67: Peter Naur and Robert Floyd independently show how to prove programs with assertions attached to points in the code. 1967: N. G. de Bruijn starts Automath, the first language for computer-checked mathematical proofs. 1969: Tony Hoare publishes Hoare logic, {P} C {Q}. Nearly every contract language since builds on it. 1972: Robin Milner's Stanford LCF. Its Edinburgh successor (1979) introduces ML as its scripting language, the ancestor of Standard ML, OCaml and F#. 1973: Mizar starts in Poland. Formalized math that reads close to a textbook. 1975: Dijkstra's guarded commands and weakest preconditions. 1977: Amir Pnueli brings temporal logic to programs. Patrick and Radhia Cousot publish abstract interpretation, the theory behind sound static analyzers. 1978: Hoare's CSP for concurrent processes. Milner's CCS (1980) and the pi-calculus (1992) follow. 1970s: VDM at IBM's Vienna lab. Jean-Raymond Abrial proposes Z, later developed at Oxford. Boyer and Moore build their theorem prover. TOOLS PEOPLE USED (1980 to 1999) 1981-82: Model checking, invented independently by Clarke and Emerson and by Queille and Sifakis. Turing Award in 2007. 1980s: Synchronous languages Esterel and Lustre in France. Lustre becomes SCADE, which Airbus uses to design flight control software. 1984: Nuprl at Cornell. 1985: Coquand and Huet's Calculus of Constructions, the logic under Coq. 1986: Isabelle (Larry Paulson). Late 1980s: SPARK, a provable subset of Ada. 1988: HOL (Mike Gordon). 1989: Coq's first public release. Renamed Rocq in 2025. 1990: Symbolic model checking with BDDs handles 10^20 states. McMillan's SMV follows. 1991: SPIN model checker goes public (Gerard Holzmann, Bell Labs). 1992: PVS at SRI. Oxford and IBM win the Queen's Award for using Z on IBM's CICS transaction system. 1993: Metamath, a proof language simple enough to check with a few hundred lines of code. 1994: Lamport's TLA. TLA+ follows in 1999. 1994-95: Intel's Pentium division bug costs it $475 million. AMD uses ACL2, Kaufmann and Moore's successor to the Boyer-Moore prover, to prove its K5 floating-point division correct. Intel hires John Harrison in 1998 and uses his HOL Light to verify floating-point algorithms. 1996: Abrial's B-Book. 1997: Alloy (Daniel Jackson, MIT). 1998: Paris Metro line 14 opens driverless, with safety software built in the B method. The KeY project for Java verification starts. 1999: Agda (Catarina Coquand). JML, a contract language for Java. VERIFIERS MEET REAL CODE (2000 to 2019) 2000: Microsoft's SLAM project starts. It ships as the Static Driver Verifier in the Windows driver kit. 2001-02: Separation logic (Reynolds, O'Hearn, Yang) makes pointer-heavy code provable. 2002: ESC/Java. Spec# (2004) and the Boogie verifier (2005) follow at Microsoft Research. 2003: Astrée proves the Airbus A340's primary flight control software free of run-time errors. 2004: CBMC, bounded model checking for C. 2005: Georges Gonthier finishes a Coq proof of the four color theorem. 2006: CompCert, a C compiler proved correct in Coq (Xavier Leroy). Event-B gets its Rodin toolset around the same time. 2007: Agda 2. Idris first appears (Edwin Brady). 2008: Z3 SMT solver (Microsoft Research). Frama-C. VeriFast. 2009: Dafny (Rustan Leino). seL4, the first general-purpose OS kernel with a machine-checked proof that its C code matches its spec. 2010: Why3. 2011: F*. 2012: A Coq proof of the Feit-Thompson odd order theorem is completed. 2013: Lean (Leonardo de Moura, Microsoft Research). P language at Microsoft. 2014: CakeML, a verified ML compiler. Liquid Haskell. Flyspeck finishes a formal proof of the Kepler conjecture. 2014-15: AWS reports TLA+ found bugs in S3 and DynamoDB that testing missed. IronFleet proves distributed systems correct in Dafny. 2015: Iris, a separation logic framework in Coq. Facebook open-sources Infer. 2016: Project Everest starts, aiming for a verified HTTPS stack. Viper. 2017: HACL*, verified crypto written in F*, ships in Firefox 57. Lean's mathlib starts. 2018: AWS Zelkova checks IAM and S3 policies with SMT solvers. 2019: Fiat Cryptography's Coq-generated code lands in BoringSSL, used by Chrome. Prusti for Rust. LLMS MEET PROOF CHECKERS (2020 to 2025) 2020: OpenAI's GPT-f finds shorter Metamath proofs that get accepted into the main library, a first for deep learning. 2021: Lean 4. 2022: Kani (AWS) and Creusot for Rust. Aeneas translates Rust into Lean. The Liquid Tensor Experiment finishes the Lean proof Peter Scholze asked for. 2023: Verus for Rust. AWS releases Cedar, a policy language built with proofs in Dafny and later Lean. LeanDojo gives models a programmatic interface to Lean. Terence Tao's team formalizes the PFR conjecture proof in Lean in three weeks. July 2024: DeepMind's AlphaProof reaches IMO silver-medal standard with proofs in Lean. Sept 2024: Quint 1.0, TLA+ ideas with ordinary programming syntax. Mar 2025: Imandra launches CodeLogician, an agent that turns code into its IML logic and checks it. Apr 2025: AWS publishes how it rewrote its authorization engine, called a billion times per second, in Dafny with proofs. July 2025: Harmonic's Aristotle reaches IMO gold-medal level with formal Lean proofs. Sept 2025: The vericoding benchmark tests LLMs writing verified code from 12,504 specs. Off-the-shelf models pass 82% in Dafny, 44% in Verus, 27% in Lean. LANGUAGES BUILT FOR AGENTS (2026) Feb 22, 2026: Vera. "A programming language designed for LLMs to write, not humans." Feb 25, 2026: Vow. "A Programming Language for Agentic Coding." Mar 9, 2026: Kōdo. "Designed for AI agents to write." Z3-checked contracts, JSON errors with patches. Sept 17, 2026: Bend 2. Dependent types and Lean-style proofs, C-like speed, CPU and GPU parallelism, Python-like syntax. WHAT EACH LANGUAGE IS GOOD FOR Specs and models Z: precise requirements docs. Little tooling today. VDM, B, Event-B: refining a spec step by step into code. Railways and safety-critical control. CSP (with the FDR checker): concurrent protocols. Petri nets: workflows and concurrent processes. TLA+ and Quint: distributed system designs, consensus, race conditions before you write code. Checks the design, not the code. Alloy: fast counterexamples in data models and access rules. Bounded, so finding no counterexample isn't a proof. P: modeling and testing event-driven distributed services at AWS and Microsoft. Model checkers SPIN: concurrency protocols, as abstract models. NuSMV and other SMV descendants: hardware and finite-state control logic. CBMC: bounded checking of C code. Kani: bounded checking of Rust, including unsafe code. Static analysis Astrée: proving embedded C has no run-time errors. Avionics. Static Driver Verifier: Windows drivers using kernel APIs correctly. Infer: memory and null bugs across large codebases. Proof assistants ACL2: hardware and microcode. HOL4, HOL Light: hardware and floating-point proofs. Isabelle/HOL: seL4-scale systems proofs, strong automation. Rocq: verified compilers (CompCert), crypto (Fiat), big math proofs. Slow and hard to learn. PVS: aerospace, much of NASA's formal methods work. Agda: type theory research and teaching. Lean 4: math (mathlib) and AI theorem proving. Hardest of the big three for LLMs off the shelf (27%). Mizar, Metamath: large formal math libraries with simple checkers. Verifying real code SPARK: avionics, defense, rail. Dafny: verified business logic, compiles to C#, Java, Go, Python, JS. AWS uses it for its authorization engine. Easiest for LLMs off the shelf (82%). F*: verified crypto (HACL*, in Firefox and the Linux kernel). Frama-C, Why3: C in safety-critical settings. KeY, JML: Java. VeriFast, Viper: separation-logic proofs about heap-heavy code. Liquid Haskell: proofs added to existing Haskell. Idris: general-purpose programming with dependent types. Verus, Prusti, Creusot, Aeneas: proofs about Rust code. WHY IT NEVER SCALED Formal methods worked. They didn't scale, because a person had to write every proof. Back to seL4. Its 8,700 lines of C needed roughly 200,000 lines of Isabelle proof, more than 20 lines of proof per line of code. IronFleet's verified distributed systems took 3.7 person-years, including inventing the method. So formal methods stayed where a bug costs more than the proof: flight control, railways, crypto, kernels, cloud authorization. Agents change that math. The proof is the tedious part, and an agent will grind on it all night. You also don't have to trust the agent, because the verifier accepts the proof or rejects it. What stays human is the spec. A green proof of the wrong spec is still wrong, so that's where your review time goes. WHERE I'D START I would start with the Verus formal language. The agent is the new part, so I'd pair it with a verifier that isn't. For agents writing verified code. It checks ordinary Rust against specs and proofs written in Rust, then erases them before compiling, so what you prove is what ships. It has peer-reviewed results since 2023, real systems built on it (Kubernetes controllers, OS kernel, etc), and use at Microsoft and Amazon. For other jobs: - Checking a distributed design: TLA+ - Math: Lean - Bend 2, Vera, Vow and Kōdo: worth watching, still very early though. Follow me for more on verification and agentic engineering.