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.