Hello, I'm Shrijith Venkatramana. I'm building git-lrc, an AI code reviewer that runs on every commit. Star Us to help devs discover the project. Do give it a try and share your feedback for improving the product.
Most programmers already write specifications.
They just don't call them that.
Whenever you write:
assert user.id is not None
or:
if (!task.completedAt) throw Error(...)
you are encoding invariants informally.
The problem is:
the compiler does not know them.
So your system eventually drifts into illegal states.
That is where Lean 4 becomes interesting.
Lean is not merely a theorem prover. It is a programming language where:
- types can encode invariants,
- proofs are first-class objects,
- illegal states can become unrepresentable.
In this article, we will build a tiny todo system in Lean 4 and prove some properties about it.
Not because todo apps matter.
But because mundane software hides surprisingly rich semantics.
Installing Lean 4
The easiest path is:
curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh -sSf | sh
Then:
lake new todo-proof
cd todo-proof
Open it in VSCode with the Lean extension.
Your First Lean Program
Let's start with a simple structure.
structure Task where
id : Nat
title : String
completed : Bool
deriving Repr
This is similar to:
@dataclass
class Task:
id: int
title: "str"
completed: bool
Now create a value:
def task1 : Task :=
{ id := 1
title := "Learn Lean"
completed := false }
And evaluate it:
#eval task1.title
Functions are Pure
Let's write a function to complete a task.
def completeTask (t : Task) : Task :=
{ t with completed := true }
Test it:
#eval (completeTask task1).completed
Unlike mutable application code, Lean encourages modeling transitions explicitly.
That becomes important once proofs enter the picture.
Lists of Tasks
Now define a todo list.
abbrev TodoList := List Task
Add tasks:
def addTask (todos : TodoList) (task : Task) : TodoList :=
task :: todos
Example:
def todos :=
addTask [] task1
The First Invariant
Real systems care about invariants.
Suppose:
No two tasks should share the same ID.
In JavaScript this is convention.
In Lean we can state it formally.
Extracting IDs
def ids (todos : TodoList) : List Nat :=
todos.map (fun t => t.id)
Unique IDs Predicate
Lean already has List.Nodup.
It means:
this list contains no duplicates.
Now define:
def UniqueIds (todos : TodoList) : Prop :=
List.Nodup (ids todos)
This is our first specification.
Notice something subtle:
Prop
means:
a logical proposition.
Not a runtime boolean.
Proving Something
Let's prove:
an empty todo list has unique IDs.
theorem empty_has_unique_ids :
UniqueIds [] := by
unfold UniqueIds ids
simp
That tiny proof already demonstrates the core idea.
We encoded:
- a system property,
- mathematically,
- and mechanically verified it.
Safe Task Addition
Now we define safer insertion.
We only allow adding a task if its ID is fresh.
First:
def idExists (todos : TodoList) (id : Nat) : Bool :=
todos.any (fun t => t.id == id)
Then:
def addTaskSafe (todos : TodoList) (task : Task) : Option TodoList :=
if idExists todos task.id then
none
else
some (task :: todos)
This resembles production code more closely.
Proving Correctness of Safe Addition
Now the interesting part.
We want:
If the original list had unique IDs,
and insertion succeeds,
the resulting list also has unique IDs.
In theorem-prover land, this is the real API contract.
A simplified proof sketch:
theorem addTaskSafe_preserves_unique
(todos : TodoList)
(task : Task)
(h : UniqueIds todos)
(hadd : addTaskSafe todos task = some (task :: todos)) :
UniqueIds (task :: todos) := by
unfold addTaskSafe at hadd
unfold UniqueIds at *
simp at hadd
aesop
Do not worry if this feels strange initially.
The important conceptual shift is:
We are proving:
- state transitions preserve invariants.
That is the heart of formal methods.
Illegal States
Most application bugs reduce to:
invalid transitions between states.
For example:
{
completed: true,
completedAt: null
}
This is an illegal state.
Traditional systems allow it accidentally.
Lean encourages modeling state explicitly.
Encoding State in Types
Instead of:
structure Task where
completed : Bool
we can do:
inductive Status where
| active
| completed
Now:
structure Task where
id : Nat
title : String
status : Status
Already better.
But we can go further.
Dependent Thinking
Suppose completed tasks must contain a completion timestamp.
In mainstream languages:
completedAt?: Date
In Lean:
inductive TaskState where
| active
| completed (finishedAt : Nat)
Now the timestamp exists iff the task is completed.
The illegal state disappears entirely.
This is a recurring pattern in theorem proving:
move runtime checks into type structure.
Why This Matters
At first glance, this seems academic.
But think about real systems:
- payment processors,
- distributed databases,
- auth systems,
- CI pipelines,
- infrastructure tooling.
Most failures come from:
- invalid states,
- forgotten invariants,
- impossible transitions that became possible.
Lean lets you model systems where:
- assumptions are explicit,
- transitions are checked,
- proofs accompany implementations.
A More Interesting Direction
A todo app becomes genuinely interesting once you add:
- offline sync,
- collaboration,
- event sourcing,
- permissions,
- undo/redo,
- conflict resolution.
Then you start proving:
- merge convergence,
- replay determinism,
- permission safety,
- index consistency.
At that point, you are doing miniature distributed systems research.
Final Thoughts
The important lesson is not:
“we proved a todo app correct”.
It is:
ordinary software contains hidden formal structure.
Most systems already behave like:
- state machines,
- transition systems,
- protocol graphs,
- logical constraint engines.
Lean simply forces those assumptions into the open.
And once they are explicit:
they become provable.
*AI agents write code fast. They also silently remove logic, change behavior, and introduce bugs -- without telling you. You often find out in production.
git-lrc fixes this. It hooks into git commit and reviews every diff before it lands. 60-second setup. Completely free.*
Any feedback or contributors are welcome! It's online, source-available, and ready for anyone to use.
AI agents write code fast. They also silently remove logic, change behavior, and introduce bugs -- without telling you. You often find out in production.
git-lrc fixes this. It hooks into git commit and reviews every diff before it lands. 60-second setup. Completely free.
See It In Action
See git-lrc catch serious security issues such as leaked credentials, expensive cloud operations, and sensitive material in log statements
git-lrc-intro-60s.mp4
Why
- 🤖 AI agents silently break things. Code removed. Logic changed. Edge cases gone. You won't notice until production.
- 🔍 Catch it before it ships. AI-powered inline comments show you exactly what changed and what looks wrong.
- 🔁 Build a…