Leanly, Lightly: Proving IsZero

Jan 25, 2026

What a tiny program can teach us about machines and correctness

Consider the smallest program that still does meaningful work:

isZero(x):
  return 1 if x == 0
  return 0 otherwise

No loops, no memory accesses, no algorithms to admire.

And yet, this tiny program quietly relies on almost everything we assume about machines: registers, flags, condition codes, and conventions that are rarely written down.

This post shows how to prove that such a program does what it claims to do — not in a high-level language, not by inspection, but at the level of machine instructions.

We’ll do it with the smallest possible spec, the simplest possible execution model, and a proof you can read end to end.

What are we actually proving?

Before we can prove anything, we need to be precise about what kind of claim we are making.

At first glance, the claim seems obvious: “this program returns 1 when the input is zero, and 0 otherwise.” But that sentence hides several decisions. What exactly is the input? Where does the output live? What does “returns” mean at the level of machine code? Which parts of the machine state matter, and which do not?

Formal methods begin by forcing these questions into the open.

A mathematical contract

We start with what is independent of machines: the intent.

We fix the input to be a 64-bit word and define a function that captures what we want, without mentioning registers or instructions.

abbrev Word64 := UInt64

def encodeBool (b : Bool) : Word64 :=
  if b then (1 : Word64) else (0 : Word64)

def isZeroSpec (x : Word64) : Word64 :=
  encodeBool (x == (0 : Word64))

Even without knowing Lean, the structure should be readable. Word64 names the kind of value we care about. encodeBool fixes how booleans are represented as machine words. isZeroSpec is the contract: it says exactly what the result should be.

This is not executable code. It is a statement of meaning.

Saying what cannot happen

At the machine level, correctness often includes ruling out nonsense. Here, that means stating that the output is always a valid boolean encoding.

def BoolWord (w : Word64) : Prop :=
  w = (0 : Word64) ∨ w = (1 : Word64)

This kind of predicate may look overly explicit, but it becomes a stable promise. Every implementation must produce one of these two values, no matter how it is written.

The core correctness claim

The main property we care about is best stated as an equivalence.

theorem isZeroSpec_correct (x : Word64) :
  isZeroSpec x = (1 : Word64) ↔ x = (0 : Word64)

Read it plainly: the result is 1 exactly when the input is zero. Nothing here mentions machines. That is deliberate. This statement is the anchor that all machine-level reasoning must refine to.

A brief note on all the symbols

If this is your first time seeing Lean, some of this may feel unfamiliar. There are symbols, arrows, and words like Prop and theorem that do not appear in everyday code.

That reaction is normal.

Proof languages compress ideas very aggressively. Where ordinary code relies on shared conventions and informal understanding, proof languages insist on writing everything down. As a result, they often look denser than they are.

For example, the theorem above is just saying “the output is 1 if and only if the input is 0.” You do not need to internalize Lean to follow this post. What matters is the structure of the reasoning, not the notation.

From intent to machines

So far, everything has been abstract. To connect the spec to real code, we need one simple idea: a machine program transforms a machine state into another machine state.

A machine state is just the collection of things we care about: registers, memory, and flags. A program does not “return” a value; it changes state.

Our goal is to show that after running the program, the resulting state reflects the intent captured by isZeroSpec.

Two machines, one idea

Here is a typical x86_64 implementation of isZero:

xor     rax, rax
cmp     rdi, 0
sete    al

And here is a typical AArch64 version:

cmp     x0, #0
cset    x0, eq

They look different, and they are. x86_64 relies on flags and partial registers, while AArch64 uses explicit conditional instructions.

But they share the same overall shape. They read an input register, compute condition codes, and produce a 0 or 1 in an output register.

The spec does not care how this is achieved. It only cares about the relationship between the input and the final state.

Walking through one machine: AArch64

Let’s walk through one architecture in detail. We’ll use AArch64, because for this program it is especially direct.

The entire program is two instructions:

cmp     x0, #0
cset    x0, eq

We make a minimal convention: the input value is in X0, and the output value is written back to X0. No stack, no calling convention, just enough structure to state the claim.

The proof follows the code, step by step. We start from a state where X0 = x. We execute cmp, which updates flags but not registers. We execute cset, which writes 1 or 0 into X0. Finally, we show that the resulting value of X0 equals isZeroSpec x.

Each instruction has a small, explicit semantic rule, and the proof composes those rules in order. Nothing global, nothing hidden. The structure of the proof mirrors the structure of the program.

Your turn: x86_64

The x86_64 version follows the same pattern:

xor     rax, rax
cmp     rdi, 0
sete    al

The details differ: partial registers, implicit zero-extension rules, and different flag conventions. But the proof strategy does not change.

Same spec. Same execution model. Different instruction semantics.

Once you understand one, the other becomes an exercise in careful translation.

What we didn’t model (and why that matters)

We intentionally did not model caches, speculation, branch predictors, out-of-order execution, calling conventions, stack layout, operating systems, or interrupts.

This is not an omission. It is a choice.

Formal methods are powerful not because they cover everything, but because they make assumptions explicit.

In Principia Mathematica, Whitehead and Russell spend hundreds of pages developing logical foundations before turning to arithmetic at all. The work is not in proving “1+1=2”, but in deciding what “number,” “addition,” and “proof” mean.

The final step is simple. The work is in deciding what you mean.

This proof of isZero is the same kind of exercise, just on a smaller scale. Once the foundations are clear, the proof itself becomes almost boring.

Why this is useful even if you never write a proof

You do not need to adopt formal methods wholesale for this way of thinking to be useful.

The habit of asking what exactly you are assuming, which parts of the system a claim depends on, and what would have to be false for the reasoning to break is valuable on its own.

Formal methods are not about pedantry. They are about honesty.

They force us to say what we usually leave implicit, and sometimes reveal that the system we thought we understood is not quite the system we are actually running. That is true for arithmetic, for machines, and especially for cryptographic code.