Hello, I'm Shrijith Venkatramana, and I'm building LiveReview — a blast-radius aware AI code review built for your business-critical systems. Star us to help devs discover the project, give it a try, and share your feedback to help improve the product.
A test suite can pass while a program still violates an invariant nobody thought to test.
A counter exceeds its limit. A retry handler executes a payment twice. A pagination function silently skips records. A resource allocator assigns more capacity than the system has available.
These bugs often survive because tests examine particular executions while requirements describe what must hold across many possible executions.
What if you could express a requirement as a mathematical proposition, implement the behavior, and ask a computer to verify that your implementation satisfies that proposition?
That is the idea behind Lean, a programming language and interactive theorem prover. Lean lets developers define functions, express their properties mathematically, and construct machine-checked proofs about those properties.
You do not need to formalize an entire application to use it. Start with one function, one invariant, and one proof.
Tests check examples; specifications define obligations
Consider a function that increments a counter without allowing it to exceed a configured limit.
An ordinary test suite might cover these cases:
- The counter increases when it is below the limit.
- The counter stays at the limit when it reaches the limit.
- The counter does not exceed the limit when given an unexpectedly large input.
These are useful tests. But suppose the function accepts integers in a large domain. How many inputs should you test? Ten? A thousand? A million?
For a function over unbounded mathematical integers, exhaustive enumeration is impossible.
Property-based testing improves coverage by generating many inputs and checking general properties. Formal verification takes a different approach: it attempts to establish a property for every input in the mathematical domain described by the specification.
The distinction is between testing selected executions and proving a proposition about all executions represented by a model.
This approach has a long history. In 1969, computer scientist C. A. R. Hoare published An Axiomatic Basis for Computer Programming, helping establish a systematic foundation for reasoning about program correctness.
One of the central ideas associated with this work is the Hoare triple:
{P} C {Q}
Here, P is a precondition, C is a command, and Q is a postcondition.
Read it as: if P holds before executing C, then a terminating execution of C establishes Q.
For our counter, we might write:
{current < limit} increment(current) {result = current + 1}
This describes the increment behavior when the counter is below the limit. It does not specify the other cases, such as what happens when the counter has already reached its limit.
A complete specification must cover those cases as well.
Lean provides a language in which we can represent these requirements precisely and have a proof checker verify the resulting arguments.
Translate the requirement into a mathematical contract
Let's begin with three requirements:
- The result must never exceed the limit.
- When the current counter is below the limit, increment it by one.
- When the current counter is at or above the limit, return the limit.
We can express the implementation in Lean:
def boundedInc (limit current : Nat) : Nat :=
if current < limit then current + 1 else limit
A few details matter here.
Nat is Lean's type of natural numbers: 0, 1, 2, and so on. The function receives two natural numbers and returns another natural number.
The expression if current < limit then ... else ... selects one of two branches, depending on the comparison.
Now let's specify the required behavior independently of the implementation.
def BoundedIncSpec (limit current result : Nat) : Prop :=
result <= limit ∧
(current < limit -> result = current + 1) ∧
(limit <= current -> result = limit)
This definition introduces three obligations.
The expression result <= limit says that the result must stay within the limit.
The symbol ∧ means logical AND: both propositions must hold.
The expression P -> Q means that if proposition P holds, proposition Q must follow.
Finally, Prop is Lean's type of propositions. The definition BoundedIncSpec describes a proposition about the relationship between the inputs and the result.
Notice that result is an independent parameter. We have described what constitutes a correct result without assuming how the result is calculated.
This separation matters. The same specification could be satisfied by different implementations: a conditional expression, a library function, or a more complicated implementation optimized for a particular environment.
A specification describes the obligation. An implementation supplies the mechanism.
One subtlety deserves attention: our specification is deliberately tailored to natural numbers and the stated requirements. It does not say that the function must preserve information about how far an input exceeded the limit. That is intentional. Formal specification forces us to distinguish essential requirements from incidental implementation details.
Prove that the implementation satisfies the contract
We now have a function and a specification. Can Lean establish that the function satisfies the specification for every possible pair of natural numbers?
Here is a complete example for a Lean project using Mathlib, Lean's mathematical library.
import Mathlib
def boundedInc (limit current : Nat) : Nat :=
if current < limit then current + 1 else limit
def BoundedIncSpec (limit current result : Nat) : Prop :=
result <= limit ∧
(current < limit -> result = current + 1) ∧
(limit <= current -> result = limit)
theorem boundedInc_le_limit (limit current : Nat) :
boundedInc limit current <= limit := by
unfold boundedInc
split_ifs <;> omega
theorem boundedInc_eq_succ (limit current : Nat)
(h : current < limit) :
boundedInc limit current = current + 1 := by
simp [boundedInc, h]
theorem boundedInc_eq_limit (limit current : Nat)
(h : limit <= current) :
boundedInc limit current = limit := by
have h' : ¬ current < limit := by omega
simp [boundedInc, h']
theorem boundedInc_correct (limit current : Nat) :
BoundedIncSpec limit current (boundedInc limit current) := by
unfold BoundedIncSpec
constructor
· exact boundedInc_le_limit limit current
constructor
· intro h
exact boundedInc_eq_succ limit current h
· intro h
exact boundedInc_eq_limit limit current h
The main result is the final theorem:
theorem boundedInc_correct (limit current : Nat) :
BoundedIncSpec limit current (boundedInc limit current)
It says that for every natural-number limit and every natural-number counter value, the result of boundedInc satisfies the specification.
There is no finite test set here. The theorem covers the entire declared input domain.
How does the proof work?
First, boundedInc_le_limit establishes that the result never exceeds the limit. The unfold tactic exposes the function definition. split_ifs separates the two branches of the conditional, and omega solves the resulting natural-number arithmetic obligations.
Next, boundedInc_eq_succ proves the increment behavior under its precondition. The simp tactic simplifies the conditional using the supplied hypothesis.
Then, boundedInc_eq_limit proves the other branch. Given that the limit is less than or equal to the current value, omega establishes that the condition current < limit cannot hold.
Finally, boundedInc_correct combines these three results. The constructor tactic decomposes the conjunction into its component obligations. Each obligation is discharged by one of the preceding theorems.
The keyword by introduces a proof constructed using tactics. Lean checks that the resulting proof establishes the stated proposition.
The tactics are convenient ways of constructing proofs; they are not substitutes for proof checking. Lean's trusted kernel checks the resulting proof terms.
The distinction is fundamental: the machine is not merely accepting a developer's assertion that the function is correct. It checks a formal argument that the implementation satisfies the proposition.
Understand exactly what the proof establishes
It is tempting to interpret a verified function as a guarantee that the corresponding production feature cannot fail. That conclusion would be too broad.
Our theorem proves a property of a mathematical function over natural numbers. It does not prove that a production implementation using a 32-bit integer behaves identically.
A 32-bit unsigned integer has a finite representable range. Depending on the language and implementation, arithmetic near the boundary may wrap, trap, or follow other specified behavior. Lean's Nat does not impose that machine-level limit.
To verify the production version, we would need a model that represents the relevant integer bounds and behavior, then establish the corresponding properties of that model and the implementation.
The same distinction applies to external systems. A proof about an authorization function does not automatically prove that a database transaction commits atomically, that a remote identity provider returns trustworthy data, or that a network retry cannot duplicate an external side effect.
Those are separate obligations.
A useful verification project therefore makes its assumptions and boundaries explicit.
What does the function assume about its inputs? Which properties are established by the proof? Which properties depend on the runtime, compiler, database, or external services?
These questions are not peripheral details. They determine what assurance the proof actually provides.
Lean's architecture helps with this distinction. The language combines programming and theorem proving within a type-theoretic framework, and its kernel checks proof terms produced with the help of tactics.
That design allows developers to use automation without treating the automation itself as the ultimate authority on correctness.
There is another limitation worth understanding: a formally verified implementation can satisfy an incorrect specification perfectly.
Suppose the business requirement says a customer must never withdraw more than their available balance. A developer mistakenly specifies that a withdrawal must never exceed the original balance at account creation. Lean might help prove the latter property, but it would not establish that the business requirement had been captured correctly.
Formal verification reduces ambiguity in the specification and provides evidence about its implementation. Human judgment remains necessary to determine whether the specification describes the system we actually want.
Move from function contracts to state invariants
Many important software properties concern not just the output of a function, but how a system's state changes over time.
Consider inventory management.
An application tracks how many units of a product are available and how many have been reserved. When a customer places an order, the system must transfer units from available inventory to reserved inventory.
Two requirements are immediate:
- A reservation must not consume more units than are available.
- A successful reservation must conserve the total number of tracked units.
We can represent the state as a structure:
structure Inventory where
available : Nat
reserved : Nat
The first field counts available units; the second counts reserved units.
Next, define the reservation operation. If sufficient inventory exists, it returns the updated state. Otherwise, it fails.
def reserve (i : Inventory) (qty : Nat) : Option Inventory :=
if qty <= i.available then
some {
available := i.available - qty
reserved := i.reserved + qty
}
else
none
Option Inventory represents either a successful result (some updatedInventory) or failure (none).
The operation subtracts the requested quantity from the available inventory and adds it to the reserved inventory. It performs no update when the requested quantity is too large.
Now we can express a useful invariant: whenever the operation succeeds, the sum of available and reserved inventory remains unchanged.
theorem reserve_preserves_total
(i : Inventory) (qty : Nat) (next : Inventory)
(h : reserve i qty = some next) :
next.available + next.reserved =
i.available + i.reserved := by
unfold reserve at h
split_ifs at h with hEnough
· injection h with hNext
cases hNext
simp
omega
· simp at h
The theorem does not merely test a reservation of three units or ten units. It covers every natural-number inventory state and every requested quantity. It says that if the operation returns a successful result, the total tracked inventory is conserved.
The key assumption is that the result of reserve equals some next. In the successful branch, Lean can use that equality to identify the returned state with the state constructed by the implementation. The arithmetic proof then follows from the condition that the requested quantity did not exceed the available inventory.
This example demonstrates why it is useful to think in terms of invariants.
A state invariant is a property that should remain true across permitted state transitions. Examples include:
- The sum of reserved and available resources remains constant.
- A financial balance never becomes negative.
- A completed order cannot return to the pending state.
- A user cannot gain permissions through an unauthorized transition.
- A distributed protocol never reaches a forbidden combination of states, under its formal assumptions.
In production, inventory correctness involves additional concerns such as database transactions, concurrent reservations, inventory adjustments, and retries. The theorem above proves only a property of the modeled operation. It does not establish that a real database-backed application implements that operation atomically.
Even so, the proof provides a precise foundation around which to build the rest of the verification effort.
This is a useful pattern for developers: isolate the state transition, write down what must remain true, and prove that each permitted transition preserves the invariant. For a system with many transitions, the proof structure can follow the design of the system itself.
Integrate specification into the development workflow
A proof is most useful when it is part of the regular engineering process rather than an isolated research exercise.
One workable process looks like this:
:::mermaid
flowchart TD
A["Write the requirement"] --> B["Define the model and contract"]
B --> C["Implement the function"]
C --> D["Prove the contract"]
D --> E{"Does Lean accept the proof?"}
E -->|No| F["Review the code, proof, and specification"]
F --> D
E -->|Yes| G["Review assumptions and system boundaries"]
G --> H["Run tests and verification in CI"]
:::
Start with a pure function: a function whose output depends only on its inputs and that has no external side effects. Pure functions are easier to specify because their behavior can be described without modeling a database, network connection, clock, or mutable environment.
For an existing application, identify a calculation or state transition and separate it from the surrounding I/O where practical. Define its inputs, outputs, and invariants in Lean. Prove the desired properties and keep those definitions and proofs alongside the implementation.
Then add the relevant build and verification commands to continuous integration. If a code change makes a theorem unprovable, the verification build should fail.
This is valuable because it turns an invariant into an explicit engineering constraint. Instead of relying on every future developer to remember why a particular condition matters, the team maintains a checked proposition that must continue to hold.
Formalization can also improve code review. A reviewer can examine the specification independently of the implementation and ask whether it captures the intended behavior. A second review can focus on the proof and its assumptions.
The separation makes two different questions visible:
Are we implementing the right requirement?
Does the implementation satisfy that requirement?
Those questions are related, but they are not interchangeable.
Testing remains part of this workflow. Unit tests exercise concrete examples, integration tests examine interactions with dependencies, and operational monitoring reveals behavior in the deployed environment. Lean contributes another form of evidence: a proof about the modeled properties of the code.
A practical adoption strategy is to begin with one small component, integrate its proof into the build, and expand only when the approach proves useful to the team.
Start with one invariant
The most effective first Lean project is probably not a complete application or an attempt to verify every line of an existing codebase.
Choose a function with a meaningful invariant: a bounded counter, a pagination helper, a resource allocator, a validation routine, or a state transition. State the requirement precisely, encode the implementation, and prove that the implementation satisfies it.
The broader idea has been around since the foundations of program logic. Lean makes this style of reasoning available in a modern programming environment, bringing together executable definitions, mathematical propositions, proof automation, and machine-checked proofs.
The shift is from documenting what code is supposed to do to encoding a requirement that a machine can check against a formal model of the implementation.
The scope of the guarantee depends on the quality of the specification and the boundary of the model. That makes choosing the right invariant an important engineering task in its own right.
Which invariant in your codebase would be most valuable to turn into a machine-checked theorem?
Your team's attention is limited, and the deluge of AI-generated code is making it harder to keep production reliable and secure without slowing you down.
I'm building LiveReview, a blast-radius aware AI code review built for your business-critical systems.
Instead of presenting every diff with equal emphasis, LiveReview scores each change by blast radius — how far its impact reaches through your call graph — so you can focus attention where it actually matters.
Spend code review effort where business risk is highest — not spread evenly across every diff.
⭐ Star it on GitHub:
HexmosTech
/
LiveReview
Risk-Aware AI Code Review for Business-Critical Systems
LiveReview: Risk-Aware AI Code Review for Business-Critical Systems
LiveReview is built for engineering teams that ship often, but also care about keeping production stable for customers. It approves some 40-50% of low-risk changes automatically, and it gives your team the tools to handle the rest:
- Understand risky changes faster.
- Fix problems in those changes, with human attention directed to the work that needs it.
- Enforce your engineering standards.
- Learn from production outcomes, such as incidents, rollbacks, and queue wait times.
- Improve the review process over time and make it more efficient.
- Connect to the major engineering tools that your team already uses.
Auto-Approve: Ship the Safe 50% Without a Human
Auto-Approve Upto 50% of Your Pull Requests, Safely. Risk scoring decides which MRs/PRs are safe enough to ship without a human, so your team only spends review time on risky and critical changes.
demo.mp4
LiveReview auto-approving a low-risk change while…
Click below to try LiveReview with your codebase:
Top comments (0)