Engineering notes · Formal verification
How formal verification works, what it can establish about a program, and how its conclusions depend on the specification and assumptions.
Recent work from Anthropic and GitHub has brought more attention to formal verification in AI-assisted programming. In these projects, an agent produces code or proofs that can be checked against a mathematical specification. What does that check establish about the software?
In Anthropic’s work with Theorem, existing fuzz harnesses became the basis for formal statements about compiled programs. Claude constructed proofs that Rocq checked. GitHub Next and Microsoft Research are exploring a workflow in which a human reviews a specification and an agent’s implementation is checked against it using Verus.
Verification of 239 entry points across 123 libraries
The study establishes crash-freedom for inputs below 64 MB, under stated RISC-V, Linux and memory assumptions.
Anthropic’s research report ↗ Proof-driven development with PDD Kit
This research prototype uses Verus to check Rust implementations against specifications, alongside tests and human review.
PDD Kit and its login example ↗ What does it mean to specify a program mathematically, and how can we prove that the code satisfies that specification?
We have spent a lot of time at Keller AI thinking about how software can be checked against the requirements and policies it is supposed to follow. Formal verification gives us a way to establish some of those properties precisely. Understanding how it works and where its guarantees end helps us choose what to prove, interpret the results, and recognize what still needs to be checked.
A sorting function gives us a small example where we can state what we want and examine the reasoning in detail.
What would we prove #
about a sort?
Suppose we have some code that is supposed to sort a list of integers. What would convince us that it does so correctly?
There are a few properties we can check to give us confidence. The output should be ordered. It should have the same length as its input. It should contain the same elements as its input, including the same number of duplicates. For [4, 2, 4, 1], we expect [1, 2, 4, 4].
The example below checks these three properties for a given input. The alternative implementations each introduce a different error, so we can see which properties detect it.
Each incorrect implementation can pass some checks while failing others. A list of zeros can be ordered and the right length while containing the wrong elements; an empty list has no pair of elements out of order. The checks complement one another, covering different aspects of what we mean by sorting. When an implementation passes all of them across a range of inputs, we gain reasonable confidence that it sorts correctly.
Notice that the checks an incorrect implementation passes also depend on the input. Reversing the sorted result fails the ordering check for [4, 2, 4, 1], but passes every check for [7]. This is the limitation of testing particular cases: a failing example can disprove a universal claim, but passing examples do not establish that it always holds.
But we have only run examples. How would we establish these properties for every input?
This is where proofs come in. For this sorting algorithm, we can use induction: establish that an empty list satisfies the properties, then show that each insertion preserves ordering and adds exactly the intended element. The argument applies no matter how many elements we process, allowing us to establish the properties for every finite list of integers without testing each one.
Induction is the proof technique used here. AI can construct such proofs, while a deterministic proof checker verifies that an accepted conclusion follows from the stated definitions and assumptions. To understand what makes this possible, we need to look more closely at how proofs are put together.
How can a proof cover #
every valid case?
How can an argument establish something about inputs we have never tried? To understand that, we need to look at how a proof is built: which facts it starts from, and how those facts combine to establish something new. In the Elements, Euclid organized earlier mathematical knowledge into a system where proofs build on definitions, starting assumptions and previously proved results. A geometric construction makes those steps easier to see.
To illustrate this, let’s look at a geometric construction from the first proposition in Euclid’s Elements. Start with two distinct points, A and B. Draw a circle around each point with radius AB, and choose one intersection, C. We want to prove that the triangle ABC formed by these points is always equilateral.
We could move the points and measure the sides repeatedly. Like testing a function on different inputs, this checks individual cases. Measurements have limited precision, and the cases we try do not establish the claim for every possible placement.
What lets us prove it? Euclid’s postulates permit drawing the lines and circles. The definition of a circle makes every point on its circumference equally distant from its center. The equality principle lets us conclude that quantities equal to the same quantity are equal to each other. The proof combines these facts.
C lies on A’s circle, so AC equals AB. It also lies on B’s circle, so BC equals AB. Therefore AC, BC and AB are equal. No measurement was needed: moving A and B preserves the relationships that establish the result.
What can we do with a proved result? We can use it in another proof without repeating its argument, provided its assumptions apply. Later propositions reuse this construction. This is how a small set of foundations supports a growing body of mathematical knowledge.
A modern proof assistant checks that each step follows from definitions, assumptions or established results. An agent may search for an argument and make mistakes; the checker determines whether the steps are justified. In software, reusable results include function contracts and facts about control flow. The sorting proof already used this approach: the insertion helper’s contract supported the argument about the loop.
Our partner Archway Labs works on translating code into formal mathematics that can be reasoned about in the style of Euclid. They explain how compositional code is important for combining statements to accumulate verified knowledge, and why it is valuable to make contextual assumptions explicit.
Lean checks formal proofs through its kernel; Verus uses automated solvers to verify supported Rust code. Both require precise claims and justified connections to the program.
How does this scale #
to a real system?
Suppose we are adding a module that lets users download private documents. One property we want to establish is that every successful download is authorized for the person making the request. How can we prove that about the new code?
We can organize the work into two phases. First, we build a mathematical model of the relevant parts of the application. We define what users, documents and permissions mean, represent the behavior of existing functions, and establish their contracts. Reading source code can suggest a contract; proving that the implementation satisfies it is a further step. For external services, we record the assumptions we rely on.
This model, expressed in a formal language such as Lean, supplies both a vocabulary for specifications and reusable statements about the system. It distinguishes definitions, proved contracts and assumptions. We can extend it as new work requires more of the application to be modeled.
In the second phase, we express the new requirement using that vocabulary and verify the new code against it. The result may be a proof, a demonstrated violation, or an unresolved question with the current model and tools. A successful proof adds another reusable result, together with the assumptions it depends on.
The puzzle below illustrates the second phase. Its contracts for authenticate, lookupOwner and canRead come from our model of existing components. Here, we treat those contracts as assumptions. The guard is part of the new handler, and its behavior follows from the code. Combining these pieces lets us establish the download property.
In this example, permission to read an organization’s documents covers the requested document. The shared variables connect the pieces: the permission check must concern the same caller and the organization that owns that document.
The two branches establish complementary facts: an allowed check grants access to this document, and the handler reaches the download only after that check passes for the caller. Together, they establish that every successful download is authorized, under the stated contracts and assumptions.
This is how the model grows. Once the corresponding implementation proof is checked, the handler’s contract becomes available for later reasoning. Its dependencies remain attached: permission for another organization would not justify this download, and a change to an assumed component contract may require us to revisit the proof.
What do we need to get right #
before relying on the proof?
The two phases leave us with two questions. Does the mathematical model faithfully describe the system, including its external dependencies? And does the formal claim faithfully express the requirement we intended? A checked proof establishes a result within that model; relying on it also requires us to get those connections right.
Do the assumptions describe reality?
Writing an API contract into a proof does not make it true. Suppose our model treats a positive permission check as evidence that the user is authorized now, but the integration supplies a cached decision from before access was revoked. That decision may accurately describe the old permission state. It does not establish permission at the time of the new request.
The implication may still be mathematically valid. Its premise no longer describes our system. We need to know which assumptions we made, why they are justified, and which changes require us to revisit them. Integration tests, provider guarantees and configuration checks help establish those connections.
Does the specification preserve our intent?
Our business requirement might say, “Once access is revoked, new download requests must be denied.” The technical specification might instead say, “A session carrying read permission may download.” Both sound like access control. They differ when the session survives revocation.
Suppose a session is issued at 09:00 with read permission, access is revoked at 10:00, and a new download request arrives at 10:05. The session is still valid and still contains the original permission, so the implementation returns the document. It satisfies the session-based specification while violating the business requirement.
Here, the specification can describe the implementation accurately and still express the wrong policy. A proof that the code follows that specification will not resolve the disagreement.
We have to decide when revocation takes effect, how the application learns about it, and what happens to work already in progress. Those decisions determine the property the specification needs to express.
The sorting example had the same issue: “the output is ordered” allows an empty result for every input. The specification also has to require preservation of the original elements.
As agents take on more implementation, people may spend more time reviewing specifications. That review needs to establish whether the technical statement accurately expresses the requirement, including cases such as revocation.
What has the model left out?
A token comparison may return the right boolean result while revealing information through execution time. Imagine comparing characters in order and returning at the first mismatch. More matching characters can mean more work before returning the same false.
For a stored token `ABCD`, a comparison that stops at the first mismatch examines one character for `XBCD` and four for `ABCX`. Both comparisons correctly return `false`. A specification that mentions only the returned Boolean cannot distinguish their different amounts of work.
If those differences are observable, repeated measurements may leak information about a secret. [BearSSL explains the gap between an abstract computation and observable execution](https://www.bearssl.org/constanttime.html). Formal methods can address timing properties, given an appropriate model. A proof about return values alone does not acquire that coverage. Examining all four characters would remove the difference in character counts in this example, but equal counts alone do not establish constant-time execution: the compiler and hardware also affect observable behavior.
There are simpler omissions too. Our verified download handler could sit beside an unchecked export endpoint exposing the same documents. The handler’s theorem remains true; the application-wide policy does not follow.
Finally, a tool may be unable to finish the proof. It may need a missing lemma, lack support for an operation, or time out. “Not proved” does not automatically mean “false” or inherently unverifiable. We must distinguish an established result, a demonstrated violation and an unresolved question.
A missing definition, a more precise specification or a justified assumption may make a claim tractable. Adding an assumption makes the result conditional on it; it does not prove that assumption. Any refinement of the specification still needs to preserve the original requirement.
We ran one experiment on this ourselves. We built a synthetic bank codebase with 27 written obligations and 270 code changes, some of which quietly break a rule, and gave them to seven automated reviewer setups. None of them is our product. On the 88 rule-breaking changes we sealed before scoring, the best reviewer approved 1. That sounds solved until you multiply: at that rate, a program with 100 such changes has about a two-in-three chance that one gets through. The misses that worried us most were changes where an earlier proof or test record no longer covered the code that changed, and the reviewer trusted it anyway. Even the best reviewer declined to clear about a quarter of the changes that were properly approved. It’s a small, synthetic test, each reviewer ran once, and nobody outside has reproduced it yet. The cases, results and corrections are public, alongside the full write-up.
How do we connect the specification #
to the business requirement?
The revocation example leaves us with a question that checking the implementation alone cannot resolve. How do we establish that a technical specification expresses what the organization actually requires?
A business requirement informs a design, which is expressed through specifications for individual services and then implemented in code. Regulations and internal policies may constrain each decision. We need to be able to trace which technical properties address each requirement, and identify where an interpretation or assumption was introduced.
Today, people carry much of that understanding in their heads. They remember why an exception exists, which service owns a decision and why a small API change affects another team. If agents manage repositories and merge their own pull requests, we need a way to maintain and inspect that understanding as the system changes.
In my experience with our own engineering work, this begins to bite when coding velocity reaches the point where no human understands the code line by line anymore, and review becomes painful. Consider changing a requirement from “a session with read permission may download” to “new requests after revocation must be denied.” We need to revise the technical property to specify when revocation takes effect. We then need to check whether the design can obtain a sufficiently current permission decision and what it does when that decision is unavailable. Finally, we need evidence that the implementation satisfies the revised property. A proof of the old session-based rule may remain valid, but it does not establish the new requirement. That is why, at least in the way I see software development playing out in the coming year, formal verification and evidence that gets re-checked whenever the requirement or the code changes become a necessity.
Keeping those connections explicit lets a reviewer follow a requirement through the specification, the design and the evidence. Some connections can be checked mechanically; others depend on a documented interpretation or a decision by the people responsible for the policy.
This is part of our work at Keller AI: examining the relationship between business requirements, architecture and technical specifications. We want to identify where a design omits a requirement, where a specification changes its meaning, or where an assumption needs to be reconsidered.
Translating business intent is not yet as mechanically checkable as verifying a formal theorem. Making a requirement precise often reveals a decision someone still has to make. Recording those decisions and their reasoning makes them available for subsequent review.
Proofs are one part of that evidence. Formal verification checks precise mathematical claims under stated assumptions. Unit tests exercise concrete behavior. Integration tests check real component boundaries. UI checks reveal whether the intended workflow exists. Human feedback tells us when a correctly implemented feature still fails the people using it. That feedback must change the requirements and travel back through the design.
Formal verification can establish that an implementation satisfies a specification under stated assumptions. Using that result requires us to understand the specification, justify the assumptions, and review both when the requirements or system change.
If you review or approve changes in a regulated codebase, we’d like to hear what you check and what you’ve seen slip through.