TheoremDrivenDevelopment

AI can write a great deal of code in very little time, but our ability to review it as human beings hasn't become correspondingly faster. AI-assisted review can help, but it can also overlook requirements whose importance depends on context that was never written down. Each change still needs to preserve requirements established throughout the program's history, including ones that aren't obvious from the code being changed. Carefully reviewing every generated change risks nullifying the productivity gains, while accepting changes without review risks silently breaking those requirements. We need a way to encode them and have the compiler enforce them as the software evolves.

Theorems let us encode these requirements. We still have to read the theorems to decide whether they express what we want, but the compiler handles the tedious, repetitive work of checking that the implementation satisfies them after every change.

Tests and theorems

Suppose we have a function that increments a counter. A test might check that 7 becomes 8, but the requirement is more general: incrementing the counter should never decrease it. Here's how we can express this in Lim:

(#fn increment (: counter #u8) #u8
  (#return (#u8::add-saturate counter 1u8)))

(#theorem increment-never-decreases
  (#proof-for-all ((counter #u8))
    (#u8::ge (#call increment (: counter counter)) counter)))

The addition saturates, meaning that 255 stays 255. The theorem says that for every possible counter value, the result is at least the input. Change add-saturate to add-wrap and the compiler gives us a counterexample: 255 now becomes zero.

Lim checks this using symbolic execution and a solver, within its supported model. Unsupported behavior or exhausted resources cause an error. An AI can change the implementation, but the new implementation still has to satisfy the theorem.

Property based testing

Property based testing lets us state the same property. Tools like Proptest generate inputs and shrink failures to simpler examples. Such a test might find our wrapping bug by generating 255. However, a successful run usually tells us only that the property held for the inputs it tried.

The theorem establishes more: the solver rules out a counterexample over all 256 byte values within its model. We could also test all 256 values exhaustively. That covers this domain too, but exhaustive testing becomes impractical as the number of possible inputs grows. A symbolic argument may still be manageable, though it also has limits.

Contracts between functions

The counter theorem concerns one function. In the recent theorem work in Lim, I've also been looking at relationships between functions. Suppose we must validate a request before processing it. Calling a validator somewhere isn't enough: we might validate one request and process another, or change the request after validating it.

Lim can enforce an extraneous contract between these functions: processing requires successful validation of the same object, with relevant changes invalidating that validation. Their individual signatures don't express this relationship, so we declare it separately.

The contract applies globally across supported call paths from a chosen entry function, including helper calls. Moving processing into another function doesn't remove the obligation. We must cover the entry points we care about; checking one doesn't cover every caller. This saves us from repeatedly doing the GlobalVsLocalReasoning ourselves.

Other requirements might include permission checks before actions, initialization before use, or no IO beneath a calculation. Each needs a precise statement and suitable checker support.

Mathematical proofs

Alongside checks of executable code, Lim has a small proof kernel inspired by Lean 4. It can check induction over unbounded natural numbers and proofs involving indexed datatypes, such as vectors whose types carry their lengths.

To apply these results to executable code, we also need to check the connection to its representation. Mathematical natural numbers don't overflow; machine integers can. A mathematical law alone doesn't establish that an implementation behaves the same way.

Fermat's Last Theorem

A mathematical proof illustrates how much reasoning can sit behind a short statement. In September 2026, Anthropic published a Lean formalization of Fermat's Last Theorem: no positive whole numbers a, b, and c satisfy aⁿ + bⁿ = cⁿ when n is greater than two.

Here's an equivalent wrapper around their published theorem, based on their final check:

import Theorems.Thm_fermat_last_theorem

example : ∀ (n : ℕ), n ≥ 3 → ∀ (a b c : ℕ),
    a > 0 → b > 0 → c > 0 → a^n + b^n ≠ c^n := fermat_last_theorem

Here ℕ means natural numbers and ∀ means "for all". The expression after := supplies the existing proof. We can read this small statement while Lean's kernel checks the proof terms behind it. Executable compilation is a separate step.

This is where the confidence comes from: a readable declaration connected to checked evidence. Writing the statement alone proves nothing. Its proof and dependencies must be checked under the intended definitions and axioms. Anthropic's final check audits axiom dependencies so unfinished proofs admitted through sorry cannot pass.

Lim hasn't imported this development or checked the full Fermat proof. It can express the proposition, which is different from proving it.

A higher level test framework

We can start much smaller: a counter never decreases, decoding an encoded value returns the original, or a failed operation preserves the original state. These theorems give us a higher level test framework. Tests remain useful for integration, performance, and behavior outside the proof model.

We still have to choose useful statements. A contract with an impossible precondition, or validation that always returns true, can establish little of value. We also depend on the correctness of the checker and its connection to the code that runs.

AI makes implementations cheaper, but it doesn't give us unlimited time to understand them. I think readable theorems are a practical way to preserve what matters as that code changes.