The Proof Passed. The Wrong Thing Ran.

In 2017 Mathy Vanhoef and Frank Piessens published an attack on the handshake that protects WPA2 Wi-Fi. They knew what they were up against: the 4-way handshake and CCMP "have been formally proven as secure". They broke the handshake anyway, and then reported something stranger: "our attacks do not violate the security properties proven in formal analysis of the 4-way and group key handshake". The theorems stayed true. "Instead, the problem is that the proofs do not model key installation" (Vanhoef and Piessens, 2017). A step that implementations ran was absent from the object the proofs were about. The authors place the weakness "in the Wi-Fi standard itself, and not in individual products or implementations" (krackattacks.com), so a faithful implementation inherited it.

Thesis. "Verified" names a link, not a system. Between a theorem about a policy and the request that runs sit an adapter, a description of what the tools do, a build and a checker. Each is a separate obligation, and several cannot be stated in the logic the policy was proved in. For an AI agent wrapped around other people's tools, the next unit of checking effort should go to those boundaries before it goes to more proof of the policy. A release should be refused, mechanically, until every link has evidence bound to the digest actually deployed.

The claim that would embarrass me is "before". If defect data from verified agent deployments shows the failures mainly inside the proved policy, I have the order wrong, and the first prediction below says how that would be seen.

The thesis has two sets of opponents. The seL4 paper opens with "Complete formal verification is the only known way to guarantee that a system is free of programming errors" (Klein et al., 2009). I accept that as a statement about guarantees and argue that a firm wrapping an agent around vendor tools cannot buy one, so it has to rank the links. The testing school says to drop the theorems altogether, and I answer it below.

A disclosure. I build AI systems for law firms, and I have a commercial interest in "formally verified" sounding reliable. The Lean this book offers about agent systems is about models. A Trace Is Not a Replay says of its own gap that it "would need differential testing of the deployed harness against replay, which I have not done". In this book I report no refinement of an agent system against running code, so what follows comes from someone who has specified things in Lean and has not closed this gap.

A green theorem and a wrong request

The Ashdown instruction is the book's recurring example, and it is invented. A client instructs a firm, the firm's intake agent holds a grant, a research agent holds a narrower one, and one document is privileged. This compiles, in lean/BuildingInSteel/ProofPassed.lean:

theorem intake_never_sends_privileged (t : Tick) :
    intakeGrant.permits .intakeAgent (.sendExternally .privilegedAdvice) t = false := by
  simp [Grant.permits, intakeGrant]

It holds for every tick and for that one grant, and it would be false if the grant listed the action. A second theorem, narrowing_never_sends, covers every grant that narrows the research grant: none of them permits an external send, for any principal, document or tick. These are correct, and they are the sentences a vendor would put on a slide.

Now deploy it. A request arrives as two strings. An adapter decides what the policy is asked about, the policy answers, and the tool does what it does. Also from ProofPassed.lean, compiling:

def lenientDoc (s : String) : Doc := (parseDoc s).getD .publicFiling

def brokenAdapter (w : Wire) : Option (List Action) :=
  let d := lenientDoc w.doc
  match w.tool with
  | "read"          => some [.read d]
  | "summarise"     => some [.summarise d]
  | "share_summary" => some [.summarise d]
  | "send"          => some [.sendExternally d]
  | _               => none

It has two defects. The tool share_summary summarises a document and sends the result out, and the adapter asks the policy about the summarising, which is what the tool is named for. And lenientDoc matches document names exactly and falls through to the public filing, while the document store ignores case. Given Privileged-Advice, the adapter asks about sending the public filing and the store fetches the privileged advice. That second defect is a parser differential [two parsers disagreeing about one input].

green_theorem_wrong_thing_ran is a conjunction: the policy theorem for every tick, and the privileged advice appearing in the deployed step's effects on that one request at tick 4. The second conjunct is computed, not general. green_theorem_wrong_tool is the same shape for the first defect. No proof in the file is wrong, the kernel accepts all of it, and the policy did not change. I invented both defects and do not report that they occurred anywhere. Real relatives of the second appear under "Where the defects were".

The obligation, stated exactly

Proving that a concrete representation implements an abstract one is old: Hoare's 1972 paper on proving data representations correct is one root, and for Abadi and Lamport "Refinement mappings are used to prove that a lower-level specification correctly implements a higher-level one" (1988 report, published 1991). The seL4 proofs reduce refinement to forward simulation between state machines. What follows is much smaller: one request, one step, no shared state, no concurrency, no failure. It is the shape of the argument, compiling, from the same file:

def Refines (ad : Adapter) (eff : Effects) : Prop :=
  ∀ w as, ad w = some as → ∀ e ∈ eff w, e ∈ as

theorem refines_iff_safe (ad : Adapter) (eff : Effects) :
    Refines ad eff ↔
      ∀ (g : Grant) (p : Principal) (t : Tick) (w : Wire) (e : Action),
        e ∈ exec ad eff g p t w → g.permits p e t = true :=
  ⟨fun h g p t w e he => refines_safe ad eff h g p t w e he, safe_refines ad eff⟩

Read it as: every effect of a tool must be among the actions the policy was asked about. This is general over adapter, effects, grant, principal, tick and request. The forward direction (refines_safe) says that an adapter meeting the obligation does nothing the policy did not permit. The converse (safe_refines) is the part that could have failed: it builds a grant listing exactly what the adapter asked about, and shows that any effect outside that list runs unpermitted. So if safety is to hold under every grant, nothing weaker than Refines will do. A particular grant may tolerate a failing adapter.

Refinement does not imply usefulness. refuse_all_refines shows that an adapter refusing everything meets the obligation, which is the subject of Never Breaks a Rule, Never Finishes. Nor can this model express a check that goes stale before the act, which is Yesterday's Permission.

The repair is old as well. Saltzer and Schroeder's complete mediation says "Every access to every object must be checked for authority" (1975). Ask the policy about the effects, not about the request. effectGuard_refines proves that an adapter defined that way refines any effect table, by construction, so the proof is three lines and carries no information about Ashdown. On the two bad requests, effectGuard_refuses_both computes an empty result, and effectGuard_still_works computes that the research agent can still summarise at tick 4.

That moves the burden, and does not remove it, because the effect table is also a model. In telemetry_breaks_effect_guard the real read tool also uploads what it read, through a vendor library nobody listed. The effect guard refines the table and does not refine the tool. Lean cannot tell the difference, because Lean sees only the table. The table also decides what happens to a tool it omits. deployedEffects returns the empty list, so the effect guard asks the policy about nothing and the gate opens, where brokenAdapter refused: effectGuard_opens_unlisted computes this for a tool named shell. A deployment must refuse any tool with no table entry. Agent stacks live with exactly this: the Model Context Protocol says "clients MUST consider tool annotations to be untrusted unless they come from trusted servers" (MCP specification, latest, read 02/11/2026). No theorem closes that. An observation of the tool has to. seL4's own page reaches the same floor: "there will always be some bottom level of assumptions about the physical world left" (seL4, What the Proofs Assume).

What closing it cost

seL4 is the precedent for going link by link, and its numbers deserve to be read rather than gestured at. Floating Theories covers its assumption list. These are the prices, as its authors report them. The effort figures here are, in their words, "rough, conservative estimates".

The project's self-report is the strongest data point for this chapter. It claims "no functional correctness defects in verified code since the functional correctness proof completed in 2009", and also says that even in verified configurations it has "detected small defects in every class of unverified code in the kernel in that time" (seL4 Proofs). That is the party with most to gain, reporting on itself. Even so it describes the pattern of this chapter one level down, and it adds the adapter problem one level up: the security result holds "when used correctly", and the theorem statements "provide requirements on how the system must be set up".

I need to correct something here. In How High Can You Build in Mud? I wrote, "A proof from specification to implementation costs what seL4 cost." That treats one price as the price. The authors themselves call theirs low, at $362 per line against an industry rule of thumb of $1,000 per line for a lower certification level, with a footnote admitting that the 2009 paper's "$10k/LOC" was "an embarrassing typo". The kernel was also designed together with its proof, and the code inside the proved boundary was the project's own. An agent's adapter has vendors directly beneath it. So seL4 is not a price list for agents. It shows what a link costs when you control both sides of it, and agent builders usually do not.

Where the defects were

The closest thing to a direct measurement is Fonseca and colleagues' study of three verified distributed systems, IronFleet, Verdi and Chapar (Fonseca et al., 2017). They found 16 bugs: 11 in the shim layer [the hand-written glue between verified code and the operating system], 3 in verification tools, 2 in specifications. The bugs "occur at the interface between verified and other components", in parts that "typically consist of only a few hundred lines". Two of the tool bugs had the stated impact "Verify incorrect programs". They found no protocol bugs in the verified systems, against 12 reported in the corresponding components of the unverified systems they sampled. So proof worked where it applied, and that is half my argument. The limits are real: three systems, one team, code review and testing, and not finding a bug is not proving its absence. The authors add that "it is possible that our results could under-represent bugs in other parts of the TCB". A toolkit they built around those interfaces detected 13 of the 16.

Cedar, Amazon's authorisation policy language, is nearer to the Ashdown shape: a decision engine in front of an application. Its team wrote executable Lean models, proved properties of them, and tested the Rust production code against the models (Disselkoen et al., 2024). Table 1 gives 1,673 lines of Lean model and 5,714 of proof, against 15,693 of production Rust. Proofs found 4 bugs in the validator. Differential and property testing found 21 more. Those counts are not a contest: testing did not find the non-termination bug that the proof work found. But look at what the testing did find: a bug in a third-party Rust package "for parsing IP addresses", and an unreleased string-size method whose model and production code disagreed about "bytes vs. codepoints vs. graphemes". Both are disagreements about how to read an input, in real authorisation code. The paper's appendix also lists one bug in the model itself: it "incorrectly rejected "::" when parsing IPv6 addresses". So the differential run checks the model as well as the code. The parsers themselves "are not modeled in Lean". And its generators produce only syntactically correct policies, so they missed parser bugs triggered by malformed ones.

The strongest numbers against my order of work are seL4's. Internal use and a port found 16 defects, and "the formal verification has uncovered another 144 defects". Those 144 came from proving code against a specification, which is closing a link on code the project owned, and more proof of a policy model would not have reached them. But "None of the bugs found in the C verification stage were deep in the sense that the corresponding algorithm was flawed". The deep ones came earlier, from a proof between two models: refining the abstract specification to the executable one led to "some 300 changes in the abstract spec and 200 in the executable spec", and about half "relate to bugs in the associated algorithms or design" (Klein et al., 2009). Cedar's non-termination bug is the same point on one model. A specialist will say that proof of a model finds design bugs nothing else finds, so ranking boundaries first leaves those undiscovered. I accept the finding and narrow the order. A kernel's algorithms and Cedar's validator have the logic to hide such bugs, whereas the policy in front of an agent's tools, as in Ashdown, can be a list of grants, and there the next unit of effort still goes to the boundary. A policy with real algorithmic content should get its proof first, and the first prediction below is how I would learn that agent policies are of that kind.

Cedar's generator limit has a formal analogue in my file. refinesOn runs the obligation over a finite list of requests, and refinesOn_sound shows a pass gives the obligation on the list's own members. catalogue_passes_obligation_fails then computes one adapter, with the first defect repaired and the second kept, that passes all twelve canonical requests and still fails Refines. No catalogue entry spells Privileged-Advice. A differential test is evidence about its generator's range, and its attestation should say what that range was.

S3's ShardStore team shows the cheap end. Their reference models are "1% of the implementation code", their property definitions and harnesses together are "12% of the ShardStore code base", and they "accept weaker correctness guarantees than full formal verification". They say the checks "prevented 16 issues from reaching production" (Bornholt et al., 2021). "Prevented" there means caught before release. Nobody can run the counterfactual.

Ordered from least to most commitment, and not comparable across systems:

None of these is an agent system, and "agents have the same distribution" is my extrapolation, class speculative. My reason for making it is that an agent's boundary is larger than any of these: its tools belong to other people, change without notice and describe themselves in prose.

The assurance manifest

If "verified" names a link, a release decision is a check over all the links. This is the artefact, from the same file, compiling:

inductive Evidence (claim : Option Prop) where
  | proved (thm : String) (checkedAt : Digest) (h : Formal claim)
  | attested (signer : String) (checkedAt : Digest)
  | none

def Obligation.status (rel : Release) (o : Obligation) : Status :=
  match o.evidence with
  | .proved _ d _   => if rel o.subject = some d then .proved else .open
  | .attested _ d   => if rel o.subject = some d then .attested else .open
  | .none           => .open

Three things are decided. Status is proved, attested or open. An obligation is discharged if its status is enough for what it requires, so an attestation does not discharge a proof-only link. A release is releasable if every artefact has an obligation and every obligation is discharged. Digest is a natural number standing in for a hash, and nothing here computes SHA-256. Here is Ashdown, with six links:

green_theorem_red_manifest computes the first two rows of the broken-adapter column and its verdict: the policy link proved, the adapter link open, the release refused. green_manifest_releasable computes the effect-guard verdict, using the real proof term of effectGuard_refines. adapter_change_reopens computes that changing the adapter code's digest refuses the release again.

Some of this holds in general. proved_status_has_proof says that status proved means a proof of the claim exists, which would be false of a manifest storing a label. outside_logic_never_proved says a claim outside the logic, written none, can never reach proved, so the four rows marked "either" can in this file only ever be attested, and broken_cannot_be_marked_proved shows the false refinement cannot be marked proved either. stale_proof_is_open and stale_attestation_is_open say evidence for any other digest counts for nothing, which is the fail-closed rule and also the answer to an attestation replayed from another digest. releasable_sound gives coverage of every artefact and proved status on every proof-only link. empty_manifest_refused says an empty manifest does not pass.

Three things the check cannot see are shown in the file. forged_attestation_passes computes a release passing with an attestation signed "nobody", because signatures are not modelled. vacuous_claim_passes computes a release passing with the adapter link's claim replaced by True, because the check confirms a proof of the claim and not that it is the right claim. And green_theorem_red_manifest and green_manifest_releasable run against one ashdownRelease, so digest 102 stands for the broken adapter model in one column and the effect guard in the other, and the same attestation at digest 103 says the adapter code matches either. A digest here is a number the evidence quotes. Nothing ties it to the term proved, and evidence about a link between two artefacts binds only one of them. The fourth row of the table is only as good as whoever recorded the effects. The last row is a named acceptance of an assumption, and it is no evidence that the kernel is correct.

A deployment would need what the model leaves out. Digests must be computed from the artefact, and evidence about a link between two artefacts, such as adapter code and adapter model, must bind both digests. Signer roles must be distinct: the test harness, the tool owner, the build service and the release owner hold different keys. Evidence should use existing formats, where in-toto's statement requires each subject to "have digest set" (in-toto Statement v1). Signatures and revoked keys are checked before this check runs, and a failure there means the evidence is none. A compromised signer is not detectable here at all. Logs and witnesses are covered in A Trace Is Not a Replay, whose proposed manifest concerns agent runs, whereas this one concerns a release.

Prior art, and it is close. SLSA's Verification Summary Attestation is "an attestation that some entity (verifier) verified one or more software artifacts (the subject of an in-toto attestation Statement) by evaluating the artifact and a bundle of attestations against some policy" (SLSA v1.2). My check is one of those, and it should be built as one. Assurance cases go further than I do: Assurance 2.0 asks for "explicit identification of defeaters and counterevidence" (Bloomfield and Rushby, 2020), whereas my manifest is a flat list with no argument and no defeaters. Proof-carrying code and translation validation are ways to discharge a link, and the manifest only records that someone did. I add two small things: proved holds a proof term of the stated claim, and the list names the adapter's two links and the match between tool and effect table as links of their own, although the effect table has no digest in this model.

What exists and what is proposed

Exists and compiles: ProofPassed.lean, 539 lines, whose #print axioms lines report at most propext, Quot.sound and Classical.choice. Lines are the only cost I report for it, and the figure is not comparable with anything in the tables above.

General, proved: the policy theorems (intake_never_sends_privileged for one grant, narrowing_never_sends for all narrowing grants), refines_safe, safe_refines, refines_iff_safe, refuse_all_refines, effectGuard_refines, refinesOn_sound, and the general manifest theorems named above.

Computed on the Ashdown definitions, by kernel reduction: the second conjuncts of green_theorem_wrong_thing_ran and green_theorem_wrong_tool, broken_not_refines, catalogue_passes_obligation_fails, telemetry_breaks_effect_guard, effectGuard_opens_unlisted, and the manifest computations.

Not formal, sketched: that the table in this chapter maps onto any real deployment.

Proposed, not built: the manifest as a release gate on a running system, its signatures, and a differential harness for an agent adapter. No part of this has been run against deployed code, and it does not look inside the language model. It complements interpretability work and does not replace it: both are needed, for different failures.

A manifest could also be public while tool code stays private. Publish the claims, digests and signers. A reader can then check the signatures and the shape, and has to take the private code on the signer's word.

Objections

"Write the whole system in the prover and extract it. Then there is no adapter." This is the best answer where it is available. Fonseca's group "found no shim layer bugs in IronFleet, which is the system studied with fewest unverified components", which supports it, and IronFleet still had specification and tool bugs in the same table, which limits it. Extraction moves the boundary down to whatever the extracted code calls, and for an agent that is a vendor's API. Verdict: accepted for code you own, not a route for tools you do not. I would change my mind if third-party agent tools shipped with machine-checked effect specifications that a client could verify.

"Just test. Types, contract tests and property tests give most of the value, and the Lean is decoration." On adapter code I largely agree, which is why the manifest accepts attestations there, and ShardStore is the evidence. It fails on one point. Testing needs a statement of what to test, and refines_iff_safe is that statement: compare effects with what the policy was asked. Without it a team tests whether the tool works, and both Ashdown defects can pass that test. A short written specification might do as well, and I concede that the theorem's value over a clear paragraph is modest. Verdict: partly accepted. I would drop the Lean here if teams given the paragraph alone found these defects as often as teams given the theorem. That experiment has not been run, by me or anyone I can cite.

"Your refinement is one stateless step, and your repair is true by construction. seL4's simulation had a kernel's state to carry." Correct, and the hardest objection. effectGuard_refines is true by construction, and the converse is a short proof. A real adapter has sessions, retries, partial failure and check-then-act races, and none of those can even be stated here. What the file gives is the obligation's shape, the counterexamples, and a check that refuses a green theorem with an open link. Verdict: accepted as a limit on what is proved; the thesis does not rest on the toy's depth. It rests on the empirical sources. I would change my mind about the chapter's usefulness if adapter defects in practice were mainly stateful, because then this obligation would be aimed at the wrong class.

"Some tools have no effect table. A shell can do anything." Then the tool-code link cannot be attested honestly at any useful scope, and the manifest stays open. That holds only if the signer declines, because the check does not notice a missing table and forged_attestation_passes shows it accepts any signer. I think staying open is the correct answer, and containment at a lower layer is what is left, which is the subject of The Hands. Verdict: accepted. The release is refused only if the signer refuses, and the adapter must refuse tools with no table entry. I would change my mind if open-ended tools could be recorded reliably enough that "the effects of this run" became attestable after the fact, since that would shift the check from release time to run time.

Goodhart, and what is lost

Score a team on green manifests and it will shrink what counts as an artefact, write the claim the proof already establishes, pick a signer who signs, and narrow the generator until the differential run passes. vacuous_claim_passes is the second of those in Lean. So the list of links and the wording of each claim must be set by someone with no stake in the release, and "percentage of links discharged" should never be reported. One open link refuses the release, whatever the percentage.

Formalising loses something too. "This adapter feels wrong" is a real signal from an experienced engineer, and a green manifest gives a manager a way to overrule it. Which links belong on the list, what each must require and whether a test's range is good enough all remain judgement, and the check decides none of them. A human veto has to stay outside it.

Predictions

1. By 31/12/2028, the first published study of defects across at least three formally verified AI-agent or LLM tool-wrapping systems will find most defects in specifications, adapters or tool descriptions, not in proved policy code. Refuted by such a study finding the majority inside proved policy code. If no such study exists by then, the prediction is untested and I will say so.
2. On 31/12/2027, the current Model Context Protocol specification will still not require verifiable declarations of a tool's effects. Refuted by a published revision making them normative for clients or servers. Baseline: on 02/11/2026 it treats annotations as untrusted unless the server is trusted.
3. By 31/12/2028, none of Amazon, Google, Microsoft, OpenAI or Anthropic will publish, for a production agent guardrail described as formally verified, a list of what lies between the proof and the deployed code in the manner of seL4's assumptions page. Refuted by one such publication. Untested if none of them describes a guardrail that way.

If those hold, the phrase worth distrusting in an agent product is "formally verified" with no list beside it. Ask which link, against which digest, and who signed the others.

About the author: Eduardo Aguilar Pelaez is CTO and co-founder at Legal Engine Ltd. He writes on formal methods, AI agents, and the discipline of building systems that survive being walked away from.