Chris

Mounted police patrolling streets
Picture by Martijn Stoof via Pexels

Formal verification and the cost of separation

August 16, 2026 • 13 minute read Loop invariants are hard. Keeping a specification in one language and the program in another, in sync, for years, is what actually keeps verification out of ordinary code.

A test lives in the file you already have open. You write it in the language you ship, you run it, and when it fails you get an input you can look at. The first week with a verifier doesn’t work like that. You pick a function you already understand, you write down what it should guarantee, and you wait. What comes back is often unknown, a timeout, or an error pointing at a formula you never typed. The function was ten lines. Getting the tool to accept those ten lines is the rest of the week.

The proof is asking about every run that meets the spec, and that claim needs more than an example. Bertrand Meyer’s version of this, in Design by Contract, is the one that still makes sense to people who ship code: the caller promises the preconditions, the callee promises the postconditions if those promises are kept. You already do a sloppy version of that in your head. The tool wants it written down, in a form it can check, and it won’t take “obviously” for an answer.

Preconditions, postconditions, framing, permissions, ownership: none of those are hard on their own, and none of them are what most people were hired to think about. You learn them while you learn the verifier, while you learn which of its errors mean the program is wrong and which mean the solver got bored. That’s a lot to hold at once. It would be a lot even if the spec lived in the same language as the code. In the systems we’ve actually built, it usually doesn’t.

Proof obligations and disappointment

The loop is where this stops being a vocabulary problem. Five lines of code. The invariant that makes those five lines provable can take days, because it has to hold on entry, survive every iteration, and imply the postcondition when the loop exits. Dijkstra knew that, and so did the people who designed the tools. You find out by watching a verifier reject a program you’re sure is correct.

When the proof fails, three things could be wrong: the code, the specification, or the tool’s ability to see why the specification holds. A unit test fails with a counterexample you can run. A verifier often fails with a shrug. Rustan Leino has spent years making that interaction less miserable, in what he calls auto-active verification: you stay in the editor, the tool tries to prove what it can, and you add assertions, lemmas, and ghost code until the solver goes through. That’s better than a thousand-line Coq script, and it’s still a second job. The ghost code is a program that exists only to convince a solver, written in a dialect whose diagnostics are about Z3’s search that afternoon.

In 2009, Gerwin Klein and colleagues published the functional correctness proof of the seL4 microkernel. The kernel was about 8,700 lines of C and 600 lines of assembly. The proof, in Isabelle/HOL, was about 200,000 lines of script. They weren’t padding. A machine-checked claim that a kernel always matches its spec is a large claim, and large claims produce large artifacts. By the time the same group wrote up nearly a decade of keeping that proof alive as the kernel grew, the Isabelle corpus was around 480,000 lines. Xavier Leroy’s CompCert is the same shape on the compiler side: a Coq development that lets you believe a property of the C still holds of the assembly. A team with a 200-line service and a sprint deadline doesn’t start there. The proof is a second codebase, in a second language, maintained by people who can read both.

Two programs, one product

The other thing you notice, once you’ve picked a tool, is that you’ve also picked a language you have to keep. A Dafny spec doesn’t become a JML spec, and a Coq development doesn’t become a SPARK annotation. You don’t get to change your mind in year three without rewriting the argument.

The field tried to share the painful part. Boogie and WhyML exist so a frontend can lower “real” code into a smaller logic and hand the rest to an SMT solver. Jean-Christophe Filliâtre and Andrei Paskevich’s Why3 will send the same problem toward Alt-Ergo, CVC, Z3, or Coq, depending on what’s installed. Microsoft’s Boogie sits under Dafny. Verifier authors get to avoid rewriting SMT encodings every time. Someone trying to verify a program they already have now has three languages in play: the one they ship, the one they wrote the spec in, and the one the error actually happened in. Debugging a failed proof means debugging an encoding.

AWS paid that bill in public. Cedar is the authorization language behind Amazon Verified Permissions. The team wanted to prove things about the authorizer that you actually care about in access control: a request is denied unless a permit says otherwise, and a forbid still wins if both apply. They proved those properties against a model written in Dafny. The thing they shipped was Rust. To believe the Rust, they ran differential random testing: generate policies, data, and requests, feed them to both programs, and see if they agree. Mike Hicks’s writeup from May 2023 is worth reading for the texture. They used cargo fuzz. They wrote extra generators because pure random policies almost never mention the same groups as the random requests, so you spend all your time in error-handling code and never touch the authorizer. By the time he published, a nightly run was on the order of a hundred million tests. That process found real bugs, including a bad IP-address parse in a Rust package they depended on, and mismatches in how missing application data got handled. Hicks also noted that the Dafny authorizer was about a sixth the size of the production one, which is why they could stand to read it.

Hicks walks through a version of isAuthorized that looks right on a first read: if any forbid policy applies, deny, otherwise allow. That gets “forbids override permits” for free. It also allows a request when no policy applied at all, which is the opposite of the default-deny rule they thought they had. Dafny refused the lemma. The fix is checking that a permit actually applied, the kind of thing a code review can miss because the function still “looks like” access control. They found more of those while proving the validator sound: policies that type-checked and then blew up at evaluation in ways the design hadn’t named yet.

The language you can prove things about and the language you can ship were different languages, so a lot of the assurance budget went to showing they still meant the same thing. Most teams don’t have that budget. They pick one side of the split and hope. The people who can keep a Dafny model and a Rust implementation aligned through a year of feature work are a research group. Testing never needed that group. JUnit, pytest, and cargo test live in the language the code is already in.

Who the room is for

Some of what’s left is social, and pretending otherwise doesn’t help.

Formal methods grew up in universities and national labs. The currency is papers. The prestige objects are complete proofs of kernels and compilers. Those proofs matter. They also set the temperature of the field. A newcomer who asks for a tutorial that starts from a web handler is quietly given the impression they showed up to the wrong conference. Diagnostics assume you already know the logic. Examples are sorted lists and binary search, which is honest about the state of automation and dishonest about the programs people actually ship. If the price of entry is sequent calculus, the room stays small, and the smallness gets misread as seriousness. I don’t think most of the researchers involved intend that. I do think the tools encode it. A system that requires a new language, a new IDE, and a new way of reading error messages will be used by people who already wanted to be there.

The industry work that exists, Cedar included, is still specialist teams around components whose failure is expensive enough to justify the second language. They don’t make the ordinary case cheaper.

Testing won the ordinary case because it lived where the code already was. The closest thing verification has to that story is property-based testing, and the interesting part is how little language it needed.

Koen Claessen and John Hughes published QuickCheck at ICFP in 2000. The trick wasn’t a new logic. Properties were Haskell functions. Generators were Haskell functions. You imported a module and you wrote prop_ names in the same files as the code. When a property failed, you got a counterexample, often a small one, because the library would shrink the input. You could do this on a lunch break, without asking anyone for a license or a seminar. Hypothesis later did the same thing for Python, and the idea spread into languages that will never run Isabelle, because you didn’t have to leave. “Write a property, get a counterexample” became a normal skill, even though a property isn’t a proof. The adoption still tells you where the notation has to sit: in the file that’s already open, in the language the compiler already understands.

When the spec isn’t the program

Most verification systems ask you to leave the language you’re shipping. Dafny is the clean version of that bet: you write the program in Dafny, specify it in Dafny, and compile to C# or Java after the proof goes through. The translation between that language and the one you ship is now part of the trusted computing base. If the verifier’s idea of what a loop means and the compiler’s idea of what a loop means ever drift, you can prove a property of a program you didn’t ship. CompCert exists partly because that drift is real for C. Cedar’s Dafny-plus-Rust split is the same crack, accepted as an engineering process. Joshua Cohen’s foundationally verified Why3 exists because the community already knows those mappings are large, trusted, and mostly unchecked.

Specs rot the way comments rot, only with more confidence attached. A specification that can’t be type-checked, refactored, and reviewed with the same tools as the program will be maintained like a comment: carefully at first, then not at all. Two syntaxes means two formatters, two jump-to-definitions, two code reviews. In practice the spec loses, because the compiler is the one that ships.

A separate specification language also has to have a meaning, and that meaning is almost never the meaning of the host language. It’s a logic chosen to sit well with SMT: restricted quantification, a particular heap model, a particular story about frames and permissions. You have to learn that logic and the mapping from your language into it. The mapping is where the unsoundness bugs live.

I don’t think this split was a mistake in 2005. Boogie and Why3 made it possible to build verifiers without rebuilding SMT encodings every time. An intermediate language is a good backend, the way LLVM is a good backend. LLVM isn’t a language you ask application developers to think in. WhyML and Boogie have become that, even when the README says they’re intermediate. Error messages leak into the mental model. Eventually you’re debugging the encoding.

I don’t want anyone thinking in WhyML in order to ship a Rust program.

Verification as a library

I’d put the contracts in a module you can import: preconditions as ordinary expressions, ghost state as data the compiler erases, lemmas as functions whose bodies are proofs, checked and then discarded. The verifier is a checker for that library. The solver stays internal.

QuickCheck already showed that a spec in a library gets used. The next step is to keep that shape and strengthen the checker: same notation, a static proof where the library can see enough, tests where it can’t.

In 2023, Verus showed you can write the specs and the proofs in Rust. There’s a mode system that distinguishes executable code, spec, and proof, and ghost permissions go through Rust’s own borrow checker, which is the whole reason you’d bother: the type system you already fight with is also the type system the proof can use. Ghost code is erased. The SMT solver is still there. The programmer-facing language is Rust. That’s as close as I’ve seen to something a systems team might actually open on a Tuesday. It still isn’t a crate you add to Cargo.toml and forget about. Modes and ghost annotations are language extensions. The fragment the solver can handle is baked into the tool, not into an API you could version.

I’d go further. Make even those ordinary: types and attributes the compiler already has, plus a checker that understands a documented fragment. SMT solvers like restricted logics. A full modern language is a bad input to Z3. The library can draw that line. It exports the predicates, ghost types, and proof combinators the checker knows how to handle, and it refuses the rest at the import boundary. That’s a boundary in the ordinary engineering sense: named interactions, everything else excluded by default. The restriction lives in an API, which can grow.

Ghost code has to erase, so proofs don’t ship. Spec-only functions can’t be called from executable code by accident. Error messages have to point at the source you wrote, not at a Boogie file. And the expression in a requires clause has to mean what it means in an if. If the checker and the compiler ever disagree about that expression, that’s a compiler bug.

You inherit the host language’s mess. If the language has undefined behavior, a library can’t wish it away. SPARK’s answer was a subset of Ada, encoded as types and banned constructs, without a new parser. Automation will be worse, at first, than in a language designed around the solver. Some properties will stay out of reach until the library grows a lemma collection the way Lean grew mathlib: slowly, in public, by people solving their own problems and leaving the lemma behind. A lemma about maps, written against a verification library, can be depended on by the next program in the same language. A lemma about maps, written in WhyML, helps the next WhyML program. There aren’t many of those.

I’ve been turning this over while working on BigTalk, which is supposed to have verification without asking people to leave the language to get it. Once you’re already deciding what a type is, what an effect is, and what a region is, adding a second meaning for “the same” program starts to look like the kind of forgotten decision you’ll spend years apologizing for. The library is the decision I’d rather defend: verification as code, in the program, with a checker that shares the compiler’s meaning of that code.

References

architecture language-design

Further Reading