The Way of Building Software That Proves Correctness Itself

"Beware of bugs in the above code; I have only proved it correct, not tried it." — Donald Knuth

There is a quiet revolution happening in how we decide that something is true.

For most of computing's history, "true" has meant "I ran it and it didn't break." We write code, we write tests, we watch the green checkmarks, and we ship. Testing asks a finite number of questions and accepts a finite number of answers. It is honest work, but it is fundamentally a sampling of reality. We poke the system in the places we thought to poke it, and we infer the rest. The bugs that hurt most are, almost by definition, in the places we didn't think to poke.

Proof is a different kind of claim. When a theorem is proven, it is not probably true, not true in the cases we tried, it is true for every input the universe could hand it, forever. For most of history that level of certainty was the exclusive luxury of mathematicians, paid for in years of careful human labor. What's changed is that machines can now carry that labor. In Lean 4, a working mathematician states a theorem, interactively proves the theorem, and a machine checks every step. This is no longer exotic; it is becoming a well-recognized and accepted method by mathematicians all over the world.

This blog is a little endeavor from my experience, about using that fire for everyday software. Not for proving the Fermat’s Last Theorem, but for proving that your use-case like authorization logic, scheduling, proving safety based on heuristics, comparing correctness of ground-truth with optimized output and much more. The thesis is simple: the certainty mathematicians reserve for theorems is available to ordinary systems, if you learn to model them the right way.

You will also see how to automatically “best-effort” prove the theorems you need for inputs on the fly with an automation tactic we will talk about.

TL;DR — In case you want a rough idea of the workflow beforehand. Pick your types deliberately (three values beat two). Find the algebra hiding in your domain (combinators are monoids). Feed small lemmas to simp/grind and let automation close the big theorems. The loop, visually:

What Lean Actually Is (and Isn't)

Lean 4 is yet another programming language. You can write loops and data structures and compile real binaries in it. But it has a second nature: it is a proof assistant. Alongside your implementation you can write propositions about that implementation, "this optimized policy never grants more access than the original", and Lean will not let you claim the proposition until every case genuinely holds. It forces the vague parts of your thinking to become precise, and very often the act of making them precise is where you discover the bug, not in the proof, but in your understanding.

It's worth being honest about the boundary of this power, because the boundary is where the real insight lives.

Lean cannot tell you that your idea is good. If your security heuristic is wrong-headed, Lean will happily help you prove, with total rigor, that your wrong-headed code faithfully implements your wrong-headed idea. A perfect proof of a flawed specification is still a flawed system. Garbage in, garbage proven.

That reframing is the first mindset shift: Formal proof is less about certifying code and more about interrogating your own assumptions until they confess.

Modeling Your System - A Problem Statement to Tackle

"The beginning of wisdom is the definition of terms.", attributed to Socrates

If you remember one thing from this entire blog, make it this: the single most consequential decision in a Lean model is the choice of your core type. Everything downstream, how clean your laws are, whether your automation thrives or chokes, how many cases you have to babysit by hand, is decided, silently, the moment you pick the type that represents your domain.

This is not a Lean-specific truth. It is one of the oldest lessons in all of engineering, just stated unusually sharply. Get the abstraction right and the system seems to want to be correct; the right cases line up, the laws are obvious, the proofs fall out. Get it wrong and you spend the rest of the project fighting your own foundation, patching special cases that should never have existed.

So let's model access control, and watch a single deliberate choice change everything.

The Trap of the Obvious Type

The obvious instinct is: a rule looks at a request and returns a Bool. Allowed, or not. True, or false. What could be simpler?

This is a trap, and it's worth slowing down to see exactly why, because the kind of mistake it represents is universal.

A Bool can express "allow" and "forbid." What it cannot express is "this rule has no opinion." And that third state, silence, no-match, none-of-my-business, is not a minor edge case in access control. It is the whole ballgame. The difference between a rule that actively denies you and a rule that simply doesn't apply to you is the exact seam where real-world security breaches live. Collapse those two into a single false and you have thrown away the most important distinction in your domain before you've written a single proof.

The lesson generalizes far beyond authorization: when your type can't represent a state your domain actually has, you haven't simplified the problem, you've hidden it. And hidden problems don't disappear. They wait.

So we make the decision three-valued with one extra constructor notApplicable, and we do it on purpose:

With the core type in hand, the rest of the domain model follows naturally. A Request is what gets checked. A Rule is what checks it — a predicate over requests, plus the Decision it hands down when it matches. evaluate runs a policy against a request by collecting the outcomes of every matching rule, then resolving them with the combinator:

Combinators: Where the Math Quietly Lives

A real authorization system never has one rule. It has hundreds of them, based on different kinda of inputs and system heuristics. It is not just about authorization policy but any system has its own rules to follow and they should be mathematically sound. How you resolve that disagreement is the actual logic of your system. It is not a detail; it is the thing itself.

There are a few classic strategies here, and each is its own combinator:

• deny-overrides, if any rule says deny, the answer is deny. The cautious default of most security systems, and a good default for anything where the cost of a wrong "yes" exceeds the cost of a wrong "no."
• permit-overrides, if any rule says permit, the answer is permit. For permissive systems where access is the norm.
• first-applicable, walk the rules in order; the first one with an opinion wins. This is how firewalls and routing tables think.
• You can come up with your own. For example, say $(permit)_1 \land (deny)_2 = deny$, like Boolean Algebra. You can also have notApplicable as no power i.e. an expression with and without notApplicable has the same output.

Here's the beautiful part, and it's the kind of structural observation that separates a model that flourishes from one that merely functions. Each of these combinators is a fold over a list of decisions, with notApplicable as the starting value, the identity element. And the moment you can say "a fold with an identity element," you have said a magic word: monoid. You've just told the mathematics that your operation is associative and has a neutral element, and in return the mathematics hands you a stack of laws for free, laws you didn't invent, that were true the instant you chose the structure, waiting to be noticed.

This is one of the deep pleasures of good modeling, and worth pausing on. You don't impose the laws onto your system. You choose a structure, and the laws were already there, waiting for you. Find the right algebra and you stop inventing facts and start rediscovering them.

And now the laws are no longer abstract incantations. They are concrete, nameable properties of your code, each one a small truth you can prove and then weaponize:

• Identity: dropping the notApplicable rules never changes the result. (Silence doesn't vote.)
• Absorption: once a deny appears, everything after it is irrelevant. (Caution is sticky.)
• Idempotence: a deny on top of a deny is still just deny. (No double-counting.),

etc.

Each of these reads like common sense once stated, and that's the point. The right model makes the truths feel inevitable. These small, obvious-in-hindsight facts are the bricks. In the next section, we turn them into automation.

The Workflow for your System

Here is the rhythm of the entire discipline, the loop you will run a thousand times:

Define → prove small laws → register them with automation → let automation prove the big goals.

Let’s bring the picture again:

Once you have defined your Function, Lean provides you multiple and powerful ways to feed it the input.

1. Create your DSL(Domain Specific language): Create your own syntax in Lean while models what other Languages uses. You can even convert Python, SQL, Rust, etc to Lean. Pretty sure your use-case will be simpler.
2. Pass it on in JSON: Write your input in JSON or similar formats, and pass it onto Lean
3. Stdin/Stdout: You can pass the input via subprocess Stdin and get output via Stdout

Here's what option 1 looks like in practice. Three keywords — allow, forbid, and abstain — turn policy rules into prose that reads like the policy document itself:

With those three keywords, a fleet of AI agents' access policy looks like this:

The abstain line is the one that earns its place. The auditor rule is not a gap in the policy — it is an explicit, typed no-opinion. A Bool-based model could never write that line.

Now based on your syntax(and some metaprogramming) you have now modelled your input in Lean, which you can feed to your verifier to check for correctness, safety, etc. whatever your model is meant for. You can prove those theorems via tactics as explained in sections below/

Now they output you get is mathematically checked, verified and you can proceed with it.

But how do you prove the theorems in Lean automatically on the fly?

Searching Your Proof also Proves the Theorem

Now, here is the practical problem that makes this interesting rather than academic.

In a real automated workflow, say an AI agent assembling a set of permissions, a service validating thousands of inputs an hour against a rulebook, you cannot sit down and hand-craft an elegant proof for each case on spot. The inputs don't exist yet. They arrive at runtime, unpredictable and unrepeatable. You can't summon a mathematician every time a request comes in.

What you need instead is a best-effort automatic proof. You hand the goal to Lean's automation and let the machine search for the argument. If it finds one, you trust the result and act on it. If it can't, that silence is itself information, it's the system raising its hand and saying this one deserves a human.

This is what I mean by "searching your proof." Not writing proofs, searching for them, automatically, the way a chess engine searches for a move. Lean ships with a genuinely impressive arsenal for this: simp, grind, omega, nlinarith, and a growing family of tactics that will attempt your goal, grind through the cases, and report back. You plug them in and they try.

But, and this is the heart of the craft, these tactics are only as strong as the facts you've taught them. A bare grind on a hard goal will flail. The same grind, armed with two dozen small lemmas you proved earlier, will close the goal in a blink. Automation is not magic; it is leverage applied to knowledge you supplied. Most of the real work, and most of this blog, is about building that body of knowledge so the automation has something to stand on.

Proving on the Fly

The key question is: what laws should you prove? Look for properties universal to your domain — commutativity, associativity, identities. If you work with sets, think about how your functions interact with union and intersection. The goal is breadth, not depth.

Notice what this loop is not. It is not "sit down and write a heroic, clever proof of the main theorem." Almost nobody works that way, and the people who try usually fail. There's a philosophy buried in here, and it's worth saying out loud: big correctness is an emergent property of many small correctnesses. You do not build a cathedral by carving one perfect monolith. You lay honest brick after honest brick, and the structure rises out of their accumulation. The more you lay out the weapons you have, the better your automation proof will become.

Small Lemmas Are Food for the Machine

A lemma worth registering has three qualities: it's small, it's general, and it rewrites in a single, predictable direction, turning a more complex thing into a simpler one.

Look closely at that @[simp, grind] attribute, because it is doing something quietly profound. You are not merely proving a fact and filing it away. You are teaching the machine a reflex. Every lemma you tag with @[simp, grind] becomes part of the automation machinery by Lean4 which uses these theorems when you call simp; grind in your proof.

Bottling the Theory: auth_prove

Once the lemmas are in place, you can go one step further: wrap the whole body of knowledge into a single custom tactic. Instead of spelling out simp [...] <;> grind [...] with six arguments on every theorem, you write one word.

decide handles concrete inputs by computation. grind +locals handles symbolic goals using every tagged lemma. The same word closes both kinds of goal. Part of the value here is documentation: when a new teammate reads a proof that ends in auth_prove, they know exactly which body of theory closed it.

The Headline Theorem Closes Itself

So we arrive at the payoff, the theorem that says an optimized policy (dead rules stripped out, silent rules pruned, ordering normalized) decides every possible request exactly as the original naive policy did. After all that buildup, the proof is almost insultingly short, and that anticlimax is the entire point:

grind mounts a search using everything you've taught it, the tagged simp lemmas, the ones you handed it explicitly, case analysis, congruence reasoning, and grinds the goal down until nothing remains. If grind proves it, you are done. Not just grind, but a combination of all such lemma’s will help you automatically prove.

The Tactics, Briefly

A working vocabulary, you don't need many to go far:

• simp, rewrites the goal using your tagged lemmas. One of the most useful ones.
• grind, the heavy closer. Combines simp-style rewriting with case-splitting and congruence reasoning, and finishes goals. This is your MAIN engine for auto formalizing your theorems on fly.
• omega, a decision procedure for linear arithmetic over integers.
• nlinarith, a heavy lifter for linear arithmetic and equations.

A Result Worth More Than Equivalence

Equivalence is satisfying. But there's a property in the neighborhood that matters even more, the kind of guarantee that lets you sleep the night after a big refactor:

Optimization must never widen access. If the original policy denied a request, no optimized version is allowed to permit it.

Sit with how hard this property is to gain confidence in by testing. The dangerous case, the one request where a well-meaning optimization quietly opens a door that should have stayed shut, is, by its nature, the case nobody wrote a test for. It's invisible precisely because it's unexpected. Testing is structurally blind to the bugs you didn't anticipate; proof is not. Here, the guarantee is free, one line, leaning on the equivalence you already built. This is the asymmetry that makes formal methods worth the trouble: the bugs that are hardest to find by testing are often the easiest to rule out by proof.

Proving Concrete Requests

Abstract theorems over all policies are satisfying, but the practical payoff is proving specific agent requests against the real policy. All three possible outcomes, each closed in one word:

The third and fourth theorems are the ones a Bool-based model literally cannot state. "No opinion" and "deliberate silence" are different things, and now they're different theorems.

It's Best-Effort, and That Honesty Is a Feature

Let me be straight: automation will not close everything. Some goals need a clever induction the machine won’t stumble onto. When that happens, grind doesn’t lie — it fails plainly and stops. That’s not a verdict of incorrectness; it’s the system asking for a missing lemma. Add it, and try again. If you suspect your goal is actually false, plausible can hunt for a counterexample. The more lemmas you register, the stronger the search becomes.

Where Lean Fits Among Other Languages

Lean is still young. Its community is growing fast but doesn’t yet have the ecosystem depth of Python or Rust — so rewriting your entire stack in it isn’t practical today.

What is practical is something more surgical: locating the one slice of your system where "probably correct" is not good enough — the slice where a wrong answer means a breach, a double-charge, a corrupted ledger — and replacing the probably with a proof. That act of discernment, knowing which slice deserves this treatment, is itself a kind of engineering maturity. The things that do are usually obvious once you ask, and they are usually the things that keep you up at night.

Conclusion

"Program testing can be used to show the presence of bugs, but never to show their absence.", Edsger Dijkstra

Dijkstra wrote that in 1970, as something between a warning and a lament. For half a century it stood as a limit we simply lived with. What’s quietly remarkable about this moment is that the limit is lifting. The absence of bugs, the thing testing can never show, is now, for the right slice of the right systems, something an afternoon of careful modeling can deliver.

Access control was never the point, it was the vehicle. Swap in a pricing engine, a scheduler, a double-entry ledger, and the shape is identical: choose a type that tells the truth, find the algebra already hiding in your domain, lay small honest lemmas until grind closes the thing you care about most.

It won’t cover everything. But the slice it does cover, the part that keeps you up at night, it covers completely. That’s not a modest superpower. That’s the only kind worth having. Lean 4 is where that superpower lives today, and the earlier you pick it up, the stronger your systems become.