Everyone is talking about interactive theorem provers like Lean 4 and Coq right now. From formalizing frontier mathematics to verifying production code, the hype on social media is hard to miss. However, most people still treat these tools like magic boxes , and few actually know what happens under the hood when Lean 4 “proves” a theorem.

This post answers that question by implementing a toy Lean 4-style theorem prover from scratch. Walking through the core mechanics step by step will give you a deeper, more confident understanding of what modern theorem provers actually do, and why we can trust them.

The full source code written in Rust is available at https://github.com/h5i-dev/MiniLean4.

1. Propositions are types

At its core, a theorem prover has one job: deciding whether a proof is valid. Because a computer cannot directly verify a proof written in plain English, we need a formal bridge between mathematics and code. That bridge is the Curry–Howard correspondence, often summarized by a simple slogan: propositions are types, and proofs are programs.

In programming terms, think of a mathematical proposition as a type signature, and its proof as a program (or value) that satisfies that signature. If we can write a well-typed expression tof type A(written t: A), then the proposition Ais proven true. If no such program can be constructed, the proposition cannot be proven.

Consider logical implication: A → B( Aimplies B). To prove A → Bmathematically, we assume Ais true and use it to derive B. In programming, this is simply a function that takes an argument of type Aand returns a result of type B. If you can implement that function, you have proven the implication.

The same idea extends naturally to universal quantification (“for all x…”). Suppose we want to prove that “for every xof type A, the property B(x)holds. Just like implication, we prove this by writing a function that takes any input x: Aand returns a proof of B(x).

Notice the twist here: the return type B(x)actually changes depending on the value of the input x. In standard programming languages, return types can’t depend on runtime values, so we need a dependent function type (or Π-type), written as:

For example, let’s express the statement “every proposition implies itself.” In Lean’s type theory, the universe of all propositions is written as Sort 0(or Prop). Using a dependent type, we can write this statement as:

To prove it, we write a function that takes any proposition Pand returns the identity proof for that specific P:

This brings us to the central insight behind modern theorem provers: proving a theorem is just writing a program of the right type, and verifying a proof is just type-checking that program. A Lean-style kernel doesn’t need to “understand” mathematical truth , and it only needs to be a type checker.

2. Syntax

To build our minimal theorem prover, we don’t need a massive programming language. In fact, our entire core calculus consists of just five kinds of terms (we’ll add one more later):

Here, uis a natural number representing a universe level, and xis a variable name. Let’s break down what each construct does:

• Sort 𝑢: A universe containing types.
• 𝑥: A variable.
• Π(𝑥:𝐴). 𝐵: A Π-type (dependent function type), whose result type 𝐵 may depend on the input 𝑥.
• 𝜆(𝑥:𝐴). 𝑡: A 𝜆-abstraction, i.e. a function that takes 𝑥 : 𝐴 and returns 𝑡.
• 𝑡 𝑠: Function application.

#[derive(Clone, Debug, PartialEq, Eq)]
pub enum Term {
    Sort(u64),
    Var(String),
    Pi(String, Box<Term>, Box<Term>),
    Lam(String, Box<Term>, Box<Term>),
    App(Box<Term>, Box<Term>),
}

Everything is a Term

Notice that types and expressions share the exact same syntax. There is no separate grammar for “types” versus “values” or “proofs” versus “propositions”. Whether a given term Ais actually a valid type is decided dynamically by the type checker. For instance, our earlier theorem (“every proposition implies itself”) and its proof are both constructed from the exact same building blocks:

Associativity and Carring

As in functional languages like Haskell, Lean, and OCaml, function application associates to the left, while arrows associate to the right:

• f a b means (f a) b
• A -> B -> C means A -> (B -> C)

For example, 𝜆(𝑎:𝐴). 𝜆(𝑏:𝐵). 𝑎 has type 𝐴 → 𝐵 → 𝐴, and applied to 𝑥 : 𝐴 and 𝑦 : 𝐵 it is written (𝜆(𝑎:𝐴). 𝜆(𝑏:𝐵). 𝑎) 𝑥 𝑦, that is, ( (𝜆(𝑎:𝐴). 𝜆(𝑏:𝐵). 𝑎) 𝑥) 𝑦.

3. Typing Rules as Logical Inference

Now that we have our syntax, how does the kernel verify a proof? It checks types under a context Γ, which is an ordered list of assumptions:

It records the type of each variable in scope, and we write dom(Γ) for the set {𝑥_1, . . . , 𝑥_𝑛}. Since C-Ext below forbids repeated names, Γ can be used like a dictionary from names to types, and T-Var is simply a lookup. Unlike a plain dictionary, however, the order matters: 𝐴_𝑖 may mention 𝑥_1, . . . , 𝑥_𝑖−1, as in 𝑃 : Sort 0, ℎ : 𝑃. We use two judgments:

• ⊢ Γ ok: the context Γis well formed.
• Γ ⊢ 𝑡 : 𝐴 under the assumptions in Γ, the term𝑡has type𝐴.

Here,

 A
---
 B

means that A inducesB . B[x -> a] also denotes substituting x in B with a , and 𝐴 ≡ B denotes that the term A and B are equivalent (we’ll explain the definition of equivalence, later).

Seeing Curry–Howard in Action

To see just how directly these typing rules mirror formal logic, consider second-order propositional logic, where formulas are built from proposition variables P, 𝑄, . . . , implication (𝜑 → 𝜓 ), and universal quantification over propositions (∀𝑃 . 𝜑).

If we translate each logical formula 𝜑to its corresponding type 𝜑*, mapping 𝜑 → 𝜓to 𝜑* → 𝜓* and ∀𝑃 . 𝜑to Π(P : Sort 0). 𝜑* , then the standard rules of natural deduction match our kernel’s typing rules line for line (omitting well-formedness premises for readability):

Look closely at the two columns above: if you erase the program terms (h, 𝜆, t, f, a) from the right-hand side, you get the exact rules of logical deduction on the left! Every step of a logical proof corresponds to constructing a syntax tree node in our programming language.

What Do We Need to Implement This?

At first glance, turning these rules into a type-checking function seems almost trivial. However, there are some subtle details are hiding inside the rules above:

• T-App relies on substitution. How do we substitute terms inside dependent types without accidentally capturing bound variable names?
• T-Conv relies on equality (𝐴 ≡ B ): How do we evaluate terms and decide whether two different-looking types compute to the same normal form? For example, how does the kernel know that Π(P:Sort 0). P -> P and Π(Q:Sort 0). Q-> Q are the exact same type?

Section 5 in this article will cover those topics, while we can trete them as black box functions at this point.

What About Falsehood? (Consistency)

Translating every logical proof into a well-typed term guarantees that our type checker can verify any valid deduction. For the kernel to be trustworthy, however, we also need the opposite guarantee: it must never accept a term for a false proposition. In logic, falsehood (⊥) can be defined as ∀𝑃 . P, the absurd claim that “every proposition holds”. In our type theory, this translates to the type:

A type system in which no closed term inhabits Π(P:Sort 0). P is called consistent. Thus, the entire trustworthiness of our theorem prover boils down to a single property: ensuring that no closed program of type Π(P:Sort 0). Pcan ever pass the type checker.

4. Type Checker

Now we have some intuitive understanding of building blocks to create the type checker.

If you look back at our typing rules, you’ll notice a catch: the first five rules (T-Sort, T-Var, T-Pi, T-Lam, T-App) are triggered by the exact syntax of the expression we are looking at. The sixth rule, T-Conv (type conversion), has no syntax trigger, and it says we are allowed to simplify a type via computation at any time. If you are writing a program, how does the code know when to run T-Conv?

The Solution: infer vs. check The trick is that we never run T-Conv randomly. Instead, we split our type checker into two simple functions:

• infer(ctx, expr): Takes an expression and computes (infers) its type from the bottom up.
• check(ctx, expr, expected_type): Infers the type of expr, and then checks if it equals expected_type by normalizing both and comparing them based on alpha-equivalence (will explain what it is later).

In other words, T-Conv is no longer a separate step we have to guess when to apply, and it happens automatically inside check !

4.1 The Type Checker in 35 Lines of Code

Let’s look at the type checker first. Notice how the five match branches in infer map 1-to-1 to our five syntax constructs (Sort, Var, Pi, Lam, App):

impl Kernel {
    /// Infers the type of `t` and requires it to be a universe `Sort u`.
    /// Returns `u`.
    pub fn infer_sort(&self, ctx: &Context, t: &Term) -> Result<u64> {
        match self.whnf(&self.infer(ctx, t)?)? {
            Term::Sort(u) => Ok(u),
            other => Err(format!("expected a type, got {other:?}")),
        }
    }

    /// `Gamma |- t : ?`
    pub fn infer(&self, ctx: &Context, t: &Term) -> Result<Term> {
        match t {
            // T-Sort
            Term::Sort(u) => Ok(Term::Sort(u.checked_add(1).ok_or("universe overflow")?)),
            // T-Var
            Term::Var(x) => ctx
                .iter()
                .rev()
                .find(|(name, _)| name == x)
                .map(|(_, ty)| ty.clone())
                .ok_or_else(|| format!("unbound local: {x}")),
            // T-Pi: Sort 0 is impredicative.
            Term::Pi(x, domain, body) => {
                let domain_level = self.infer_sort(ctx, domain)?;
                let (x, body) = rename_binder_if_needed(ctx, x, body);
                let mut extended = ctx.clone();
                extended.push((x, (**domain).clone()));
                let body_level = self.infer_sort(&extended, &body)?;
                Ok(Term::Sort(if body_level == 0 {
                    0
                } else {
                    domain_level.max(body_level)
                }))
            }
            // T-Lam
            Term::Lam(x, domain, body) => {
                self.infer_sort(ctx, domain)?;
                let (x, body) = rename_binder_if_needed(ctx, x, body);
                let mut extended = ctx.clone();
                extended.push((x.clone(), (**domain).clone()));
                let body_type = self.infer(&extended, &body)?;
                Ok(Term::Pi(x, domain.clone(), Box::new(body_type)))
            }
            // T-App
            Term::App(f, a) => match self.whnf(&self.infer(ctx, f)?)? {
                Term::Pi(x, domain, codomain) => {
                    self.check(ctx, a, &domain)?;
                    Ok(subst(&codomain, &x, a))
                }
                ty => Err(format!("application of non-function: {ty:?}")),
            },
        }
    }

    /// `Gamma |- t : expected`, using T-Conv to compare the inferred type.
    pub fn check(&self, ctx: &Context, t: &Term, expected: &Term) -> Result<()> {
        self.infer_sort(ctx, expected)?;
        let actual = self.infer(ctx, t)?;
        if self.is_def_eq(&actual, expected)? {
            Ok(())
        } else {
            Err(format!(
                "type mismatch: actual {actual:?}, expected {expected:?}"
            ))
        }
    }
}

4.2 Watching the Kernel in Action

To verify a theorem TheoremType with a proof proof_term, the user calls check(empty_ctx, proof_term, TheoremType). Let's see how this handles three quick scenarios.

For example, suppose we want to verify our proof of “every proposition implies itself”:

• Theorem (expected type): Π(𝑃:Sort 0). 𝑃 → 𝑃 (which is shorthand for Π(𝑃:Sort 0). Π (_: 𝑃. 𝑃))
• Proof (expression): 𝜆(𝑃:Sort 0). 𝜆(ℎ:𝑃). ℎ

When check runs infer on our proof:

• The outer Lam puts 𝑃:Sort 0 into ctx.
• The inner Lam puts ℎ:𝑃 into ctx.
• The inner body Var(h) looks up ℎin ctx and returns its type: 𝑃.
• Wrapping those results back up in Πtypes, infer returns Π(𝑃:Sort 0). Π (h: 𝑃. 𝑃).
• Finally, check compares Π(𝑃:Sort 0). Π (h: 𝑃. 𝑃) with Π(𝑃:Sort 0). Π (_: 𝑃. 𝑃) using alpha_eq. They match, so the proof is accepted!

5. Inductive Types

So far, our theorem prover can verify proofs involving functions, implications, and universal quantification. But there is one obvious limitation: we cannot even define natural numbers yet!

In Lean 4, we can introduce new types using inductive declarations:

inductive Nat where
  | zero : Nat
  | succ : Nat → Nat

This declaration tells Lean that every natural number is constructed in one of two ways:

• zero represents zero.
• succ n represents the successor of a natural number n.

For example, the number two is represented as succ (succ zero) .

But there is a deeper question: How does the kernel know that mathematical induction is valid for this newly defined type? We never explicitly defined an induction principle. We only declared two constructors!

The answer is that the kernel automatically generates a recursor from the constructors. A recursor provides both the induction principle for proving properties and the computational rules for recursively processing values.

5.1 From Constructors to Mathematical Induction

Consider our Nat declaration again:

Nat.zero : Nat
Nat.succ : Nat → Nat

Suppose we want to prove some property P n for every natural number n.

Since every natural number is built using zero and succ, we only need to handle two cases.

(Case 1: zero) We must prove that the property holds for zero:

base : P zero

(Case 2: succ) Suppose the property already holds for some natural number n. We need to show that it also holds for succ n:

step : (n : Nat) → P n → P (succ n)

Notice that P n appears as an argument to step. This is the induction hypothesis.

Once we have both base and step, we can conclude that P n holds for any natural number n. In other words, we have derived the mathematical induction principle:

Nat.rec :
  (P : Nat → Prop) →
  P zero →
  ((n : Nat) → P n → P (succ n)) →
  (n : Nat) → P n

The remarkable part is that the kernel can generate this type automatically, using nothing more than the two constructor declarations. For each constructor, the kernel creates one case. Whenever a constructor contains a recursive field, the kernel adds an induction hypothesis for that field.

• For zero, there are no recursive fields, so we only need P zero.
• For succ, there is one recursive field n : Nat, so we need P n to construct P (succ n).

5.2 Mathematical Induction and Recursive Programming Are the Same Mechanism

There is something even more interesting about this construction: mathematical induction and recursive programming are two uses of exactly the same recursor.

To see why, let’s generalize the previous type. Instead of requiring P n to be a proposition, let M n be any type belonging to Sort u:

Nat.rec :
  (M : Nat → Sort u) →
  M zero →
  ((n : Nat) → M n → M (succ n)) →
  (n : Nat) → M n

The only difference is that the result type can now live in different universes.

(Case 1: Mathematical induction (u = 0)): When u = 0, we have:

M : Nat → Sort 0

Since Sort 0 is Prop, M n is a proposition. Therefore, the recursor constructs proofs:

Nat.rec :
  (P : Nat → Prop) →
  P zero →
  ((n : Nat) → P n → P (succ n)) →
  (n : Nat) → P n

This is precisely mathematical induction.

(Case 2: Recursive programming (u = 1)): Now suppose we want to implement a recursive function that doubles a natural number. Instead of a proposition, choose:

M : Nat → Sort 1
M n = Nat

Here, Nat is an ordinary data type living in Sort 1, not a proposition. Substituting this motive into the same recursor gives:

Nat.rec :
  Nat →
  ((n : Nat) → Nat → Nat) →
  Nat → Nat

The base case must return a Nat, and the successor case receives the previously computed result. We can now implement doubling:

def double (n : Nat) : Nat :=
  Nat.rec
    (motive := fun _ => Nat)
    0
    (fun _ result => Nat.succ (Nat.succ result))
    n

Its computation follows these equations:

double zero     ↦ zero
double (succ n) ↦ succ (succ (double n))

For example, the following result is 4:

double (succ (succ zero))
  ↦ succ (succ (double (succ zero)))
  ↦ succ (succ (succ (succ (double zero))))
  ↦ succ (succ (succ (succ zero)))

Notice that we did not introduce any new recursion mechanism. We simply used Nat.rec with a different motive. When M n : Sort 0, the result is a proof. When M n : Sort 1, the result is ordinary data. The kernel uses the same recursor, with different result types!!

Strictly speaking, this works whenever elimination into the chosen universe is permitted. For Nat, both propositional and computational elimination are allowed.

5.3 Generalizing Recursors: A Tree with Three Constructors

Natural numbers have only two constructors, and only one of them is recursive. Let’s consider a slightly more interesting inductive type:

inductive Tree where
  | leaf : Tree
  | node : Tree → Tree
  | branch : Tree → Tree → Tree

There are three ways to construct a tree:

Tree.leaf   : Tree
Tree.node   : Tree → Tree
Tree.branch : Tree → Tree → Tree

For example:

Tree.branch (Tree.node Tree.leaf) Tree.leaf

This represents a tree with four constructor occurrences. Now suppose we want to construct some result M t for every tree t, where:

M : Tree → Sort u

Just as with Nat, the recursor needs one case for each constructor.

(Case 1: leaf): leaf has no recursive fields, so we only need:

m_leaf : M leaf

(Case 2: node): node takes one subtree t : Tree. The recursor therefore provides an induction hypothesis M t:

m_node :
  (t : Tree) →
  M t →
  M (node t)

(Case 3: branch): branch takes two subtrees, l and r. Consequently, the recursor provides two induction hypotheses:

m_branch :
  (l : Tree) →
  (r : Tree) →
  M l →
  M r →
  M (branch l r)

Putting these cases together, the kernel generates:

Tree.rec :
  (M : Tree → Sort u) →
  M leaf →
  ((t : Tree) → M t → M (node t)) →
  ((l : Tree) → (r : Tree) →
    M l → M r → M (branch l r)) →
  (t : Tree) → M t

Compare this with Nat.rec. The mechanism is identical! The only differences are the number of constructors and the number of recursive fields in each constructor.

How Does MiniLean4 Generate These Types?

In our implementation, inductive declarations are represented by Rust structures:

pub struct InductiveSpec {
    pub name: String,
    pub params: Context,
    pub indices: Context,
    pub universe_level: u64,
    pub constructors: Vec<ConstructorSpec>,
}

pub struct ConstructorSpec {
    pub name: String,
    pub fields: Context,
    pub result_indices: Vec<Term>,
}

For Tree, both params and indices are empty, and we will explain why we need them later. The three constructors have zero, one, and two fields, respectively.

The recursor generator examines each constructor and adds induction hypotheses for its recursive fields. Conceptually, the code looks like this:

for constructor in &inductive.constructors {
    let mut binders = constructor.fields.clone();

    for recursive_field in &constructor.recursive_fields {
        let ih_type = /* motive applied to recursive field */;
        binders.push(("__ih".into(), ih_type));
    }
    let goa
l = /* motive applied to constructor result */;
    let minor_premise = telescope(&binders, goal);
}

Here, telescope builds nested dependent function types from a list of typed arguments. For branch, the kernel starts with:

l : Tree
r : Tree

Because both fields are recursive, it adds:

ih_l : M l
ih_r : M r

Finally, it produces:

(l : Tree) →
(r : Tree) →
M l →
M r →
M (branch l r)

This is exactly the branch case of Tree.rec.

5.4 How Does the Recursor Actually Compute? Iota Reduction

We have generated the type of Tree.rec, but we still need to explain how it computes. Let’s use the recursor to count the number of constructor occurrences in a tree. We want:

size(leaf)       = 1
size(node t)     = 1 + size(t)
size(branch l r) = 1 + size(l) + size(r)

Choose the motive:

M t = Nat

The three cases become:

m_leaf   = 1
m_node   = λ t ih. 1 + ih
m_branch = λ l r ih_l ih_r. 1 + ih_l + ih_r

Now consider:

size(branch (node leaf) leaf)

How does the kernel evaluate this expression? It inspects the constructor of the tree. Since the constructor is branch, it selects m_branch and recursively processes both subtrees.

More generally, Tree.rec follows three computation rules:

Tree.rec M m_leaf m_node m_branch leaf
  ↦ m_leaf

Tree.rec M m_leaf m_node m_branch (node t)
  ↦ m_node t
      (Tree.rec M m_leaf m_node m_branch t)

Tree.rec M m_leaf m_node m_branch (branch l r)
  ↦ m_branch l r
      (Tree.rec M m_leaf m_node m_branch l)
      (Tree.rec M m_leaf m_node m_branch r)

These are called ι-reduction (iota-reduction) rules. For our example:

size(branch (node leaf) leaf)
  ↦ 1 + size(node leaf) + size(leaf)
  ↦ 1 + (1 + size(leaf)) + 1
  ↦ 1 + (1 + 1) + 1
  = 4

The kernel does not need a hardcoded implementation of Tree.size. It only needs to know which constructor was used, which case to select, and which recursive fields need to be processed.

5.5 Strict Positivity: Why Some Constructors Are Forbidden

One of the importnat thing about inductive types is that not every constructor type is safe. Consider this declaration:

inductive Bad where
  | mk : (Bad → False) → Bad

At first glance, it looks similar to our recursive Tree constructors. But there is a crucial difference. Compare:

Tree → Tree           -- Allowed
(Bad → False) → Bad   -- Rejected

In the first case, the constructor directly receives a value of the inductive type. In the second case, the constructor receives a function that takes the inductive type as an argument.

Why does this matter? Suppose we allowed the second constructor and generated an unrestricted recursor. We could define:

f : Bad → False
f (Bad.mk g) = g (Bad.mk g)

Here, g : Bad → False, and Bad.mk g : Bad, so the right-hand side has type False. Now substitute f for g:

f (Bad.mk f)
  ↦ f (Bad.mk f)
  ↦ f (Bad.mk f)
  ↦ ...

The computation never terminates, and the unrestricted recursor would allow us to construct a closed term of type False. This would make the logic inconsistent.

To prevent this, inductive declarations must satisfy strict positivity. In our simplified kernel, recursive fields must have one of the following forms:

I
B → I
B₁ → B₂ → I
...

Here, I is the inductive type being defined, and none of the argument types B, B₁, B₂, etc. may contain I. For example:

Tree                 -- Allowed
Nat → Tree           -- Allowed
Tree → Nat           -- Not a valid recursive field
(Tree → Nat) → Tree  -- Rejected

Why is Nat → Tree allowed? Because the function produces a Tree. We can recursively process every tree returned by that function. Suppose a constructor contains:

f : Nat → Tree

Then its induction hypothesis has type:

ih : (n : Nat) → M (f n)

In contrast, a field of type Tree → Nat consumes trees rather than producing them. It does not provide the recursive subtrees needed by this recursor construction.

5.6 Parameters and Indices: From Lists to Length-Indexed Vectors

Our Nat and Tree examples had no parameters or indices. Let’s now consider a polymorphic list:

inductive List (A : Type) where
  | nil : List A
  | cons : A → List A → List A

Here, A is a parameter. It determines the type of the elements stored in the list. For example:

List Nat
List Bool

are different types, but within a particular list, the element type remains fixed.

The constructors have types:

nil  : List A
cons : A → List A → List A

The recursor can therefore use the following cases:

m_nil : M nil

m_cons :
  (a : A) →
  (xs : List A) →
  M xs →
  M (cons a xs)

This is exactly the same mechanism we used for Nat and Tree. But ordinary lists do not encode their lengths in their types. Both an empty list and a list of three natural numbers have type List Nat.

What if we want the length to be part of the type? We can define a length-indexed vector:

inductive Vec (A : Type) : Nat → Type where
  | nil : Vec A 0
  | cons : (n : Nat) → A → Vec A n → Vec A (Nat.succ n)

Now:

Vec Nat 0
Vec Nat 2

are different types.

The distinction is:

• A is a parameter, fixed throughout the recursive computation.
• n is an index, which may change depending on the constructor.

The constructors make this explicit:

nil  : Vec A 0

cons : (n : Nat) →
       A →
       Vec A n →
       Vec A (succ n)

The cons constructor receives a vector of length n and produces one of length succ n. This information changes the recursor’s motive.

For ordinary lists:

M : List A → Sort u

For vectors:

M : (n : Nat) → Vec A n → Sort u

The motive must now depend on both the vector and its length. In particular, the cons case becomes:

m_cons :
  (n : Nat) →
  (a : A) →
  (xs : Vec A n) →
  M n xs →
  M (succ n) (cons n a xs)

Notice that the induction hypothesis concerns a vector of length n, while the result concerns a vector of length succ n.

Indices allow the kernel to express and verify how type-level information changes across constructors. In our implementation, parameters and indices are stored separately in InductiveSpec. Each constructor also stores its result_indices.

During recursor generation, the kernel uses the recursive field’s indices to construct the induction hypothesis and the constructor’s result indices to construct the goal. Parameters are fixed before introducing the motive, while indices become arguments to the motive itself.

5.7 Equality Is Also an Inductive Type!

So far, we have used inductive types to represent data such as natural numbers, trees, and lists. But here is something surprising: even mathematical equality can be defined as an inductive type!

In Lean 4, equality is defined essentially as follows:

inductive Eq (A : Type) (a : A) : A → Prop where
  | refl : Eq A a a

Let’s unpack this definition. Eq A a b represents the proposition that a equals b. It has two parameters, A and a, and one index, b. Unlike Nat or Tree, equality has only one constructor:

Eq.refl : (A : Type) → (a : A) → Eq A a a

In other words, the only way to construct an equality proof directly is to show that something equals itself. But how can this single constructor justify rewriting an expression using an equality proof? The answer, once again, is the recursor!

Deriving Eq.rec

Just as we generated Nat.rec and Tree.rec, the kernel generates a recursor for Eq. Suppose we want to establish a property M b h for any value b and equality proof h : Eq A a b. Our motive has type:

M : (b : A) → Eq A a b → Sort u

Since equality has only one constructor, refl, we only need to handle one case:

base : M a (Eq.refl A a)

From this, the recursor allows us to construct the property for any equality proof:

Eq.rec :
  (A : Type) →
  (a : A) →
  (M : (b : A) → Eq A a b → Sort u) →
  M a (Eq.refl A a) →
  (b : A) →
  (h : Eq A a b) →
  M b h

This may look complicated, but the meaning is simple: If a property holds when two values are identical, it also holds whenever we have a proof that those values are equal.

Equality Gives Us Rewriting

For example, suppose we have:

h : Eq Nat a b
P : Nat → Prop
pa : P a

We want to construct a proof of P b. Choose the motive:

M b h = P b

The base case is simply pa : P a. Therefore, Eq.rec gives us:

Eq.rec Nat a M pa b h : P b

This is exactly the logical principle behind rewriting with equality. The computation rule is also straightforward:

Eq.rec A a M base a (Eq.refl A a)
  ↦ base

When the equality proof is refl, the recursor simply returns the base case. This is another example of ι-reduction, using precisely the same general mechanism as Nat.rec and Tree.rec.

Why Is Eq Different from Nat?

There is one important difference: Eq A a b lives in Prop, or Sort 0, while Nat lives in Sort 1.

Lean generally restricts eliminating arbitrary proofs in Prop into computational data types. However, equality is a special case: it has only one constructor, with no fields, so its recursor may eliminate into larger universes. Our implementation checks this restriction when registering inductive declarations.

The important takeaway is that equality does not need to be a primitive logical rule hardcoded into the kernel. Its elimination principle can be generated from an inductive declaration, just like the induction principle for natural numbers.

6. Tactics: Building an Interactive Theorem Prover

We now have a kernel capable of checking proof terms, defining inductive types, and evaluating recursive computations. In principle, this is already enough to prove many theorems. But there is a usability problem.

Consider our very first theorem:

(P : Prop) → P → P

We can prove it by writing a lambda expression directly:

fun (P : Prop) (h : P) => h

For this simple theorem, writing a proof term is easy. But for larger theorems, manually constructing deeply nested lambda expressions, function applications, and recursors quickly becomes painful.

This is where tactics come in. Instead of writing the complete proof term ourselves, we can interactively transform a theorem into smaller goals using commands such as intro, apply, rw, and induction.

For example:

theorem identity (P : Prop) : P → P := by
  intro h
  exact h

Although this looks very different from a lambda expression, both proofs ultimately represent the same term:

fun (h : P) => h

The crucial point is that tactics do not introduce new logical rules. They construct proof terms that are checked by the same kernel we already implemented.

6.1 What Is a Goal?

Suppose we want to prove:

P → P

In tactic mode, Lean displays something like:

P : Prop
⊢ P → P

The symbol ⊢ separates the local context from the proposition we want to prove. We can represent a goal as two pieces of information:

struct Goal {
    context: Context,
    target: Term,
}

Here, context contains the available variables and hypotheses, while target is the type of the proof term we need to construct.

For example:

Context:
  P : Prop

Target:
  P → P

corresponds to a goal whose context contains P : Prop and whose target is P → P. Mathematically, this is the typing judgment:

P : Prop ⊢ ?proof : P → P

The question mark means that the proof term has not been constructed yet. We call such an unfinished term a metavariable or hole.

For now, imagine that every goal represents a missing part of a proof. A tactic either fills that missing part or replaces it with smaller holes.

Let’s implement two of the most basic tactics in the next few subsections.

6.2. `intro`: Turn an Implication into an Assumption

Suppose our goal is:

P : Prop
⊢ P → P

We execute:

intro h

The goal changes to:

P : Prop
h : P
⊢ P

What happened? We were trying to construct a function of type P → P. The intro tactic introduced its argument h : P, leaving us to construct the function body. This is exactly the same operation as constructing a lambda expression.

Before:

?proof : P → P

After:

?proof = fun (h : P) => ?body

where:

h : P ⊢ ?body : P

We have not completed the proof. We have only replaced one hole with another, smaller hole. More generally, if the goal is:

Γ ⊢ (x : A) → B

then intro x transforms it into:

Γ, x : A ⊢ B

The resulting proof term will be:

fun (x : A) => body

This corresponds directly to the T-Lam typing rule from Section 3.

6.3. `exact`: Fill the Hole with a Proof Term

We now have:

P : Prop
h : P
⊢ P

Execute:

exact h

The tactic checks that h has the expected type P.

Since:

h : P

the goal is solved.

The generated proof term is simply:

h

Combining the two tactics, we obtain:

fun (h : P) => h

which the kernel can verify using the ordinary typing rules. This also suggests a straightforward implementation for exact. Conceptually, the tactic needs to do little more than:

fn exact(kernel: &Kernel, goal: &Goal, term: &Term) -> Result<()> {
    kernel.check(&goal.context, term, &goal.target)
}

This simplified function checks whether a term solves the goal. A complete tactic engine must also store the term in the corresponding proof hole.

Notice that exact does not decide whether a proposition is mathematically true. It delegates type checking to the kernel.

6.3 apply: Proving a Goal Backwards

Now consider a slightly more interesting theorem:

theorem compose (P Q R : Prop)
    (f : P → Q) (g : Q → R) (p : P) : R := by
  apply g
  apply f
  exact p

The initial goal is:

f : P → Q
g : Q → R
p : P
⊢ R

We have a function g : Q → R. If we can construct a proof of Q, applying g will give us a proof of R.

Therefore, executing:

apply g

changes the goal to:

⊢ Q

Similarly, since f : P → Q, executing:

apply f

changes the goal to:

⊢ P

Finally:

exact p

closes the proof. The complete proof term is:

g (f p)

This is an important distinction between apply and exact.

• exact g fails because g has type Q → R, not R.
• apply g succeeds because it creates a new goal for the missing argument of g.

apply can also generate multiple goals Suppose we have:

f : P → Q → R
⊢ R

Applying f requires two arguments:

?p : P
?q : Q

The tactic generates two goals:

Goal 1:
⊢ P

Goal 2:
⊢ Q

The partially constructed proof term is:

f ?p ?q

Once both holes are filled, the proof is complete. This is why an interactive theorem prover needs to manage multiple goals rather than only a single target. A simple tactic state might look like:

struct TacticState {
    goals: Vec<Goal>,
}

However, this is not yet sufficient to reconstruct the complete proof term. We also need to remember how the goals fit together. That leads us to metavariables.

6.4 Metavariables: How the Kernel Gets a Complete Proof

So far, we have described tactics as transforming goals. But there is a subtle problem. Suppose we start with:

⊢ P → P

and execute:

intro h

We now have:

h : P
⊢ P

If we only store the new goal, we have forgotten that its solution must be wrapped in a lambda expression.

Similarly, after apply g, we need to remember that the eventual proof must be an application of g. In other words, a list of goals is not enough. We must also track the partially constructed proof term.

We can extend our expression language with a metavariable:

enum Term {
    // Existing term constructors...
    MetaVar(usize),
}

This is an illustration of the tactic layer’s internal representation. Unlike ordinary kernel terms, metavariables are not accepted as unfinished proofs by the trusted kernel.

We can maintain a mapping from metavariable IDs to their assignments. For example, start with:

?0 : P → P

After intro h, assign:

?0 := fun (h : P) => ?1

where:

?1 : P

After exact h, assign:

?1 := h

Substituting the assignments gives:

?0 = fun (h : P) => h

No holes remain.

The tactic engine can now send the complete term to the kernel:

kernel.check(&empty_context, &proof, &theorem_type)?;

This final check is essential. A tactic implementation may have bugs. It might introduce an incorrect substitution, generate malformed applications, or make invalid assumptions while manipulating goals. But as long as every resulting proof is independently checked by a sound kernel, a bug in a tactic cannot make an invalid theorem pass verification.

6.5 rw: Rewriting with Equality

In Section 5, we defined equality as an inductive type and generated its recursor. Recall that an equality proof has type:

h : Eq A a b

Intuitively, h tells us that a and b are equal. The rw tactic uses this proof to replace one expression with another.

Consider:

theorem rewrite_example
    (P : Nat → Prop) (a b : Nat)
    (h : a = b) (pa : P a) : P b := by
  rw [← h]
  exact pa

Initially, the goal is:

P : Nat → Prop
a b : Nat
h : a = b
pa : P a
⊢ P b

The command:

rw [← h]

rewrites the target using the equality in the reverse direction, from b to a. The new goal is:

⊢ P a

Now exact pa solves it.

But why is this logically sound? Because the rw tactic can construct a proof using the equality recursor from Section 5. Recall the general idea of Eq.rec:

Eq.rec :
  (M : (b : A) → Eq A a b → Sort u) →
  M a (refl a) →
  (b : A) →
  (h : Eq A a b) →
  M b h

For our example, choose:

M b h = P b

Then the base case requires a proof of P a, which we already have. Applying Eq.rec transports this proof along h : a = b and produces a proof of P b. Conceptually, the completed proof is:

Eq.rec (M := fun b _ => P b) pa b h

The precise Lean 4 elaboration may use specialized equality-transport constants and additional implicit arguments, but the logical mechanism is the same.

6.6 induction: Using the Recursor as a Tactic

Now we can connect the tactic system to the inductive types we implemented in Section 5.

Recall that Nat.rec has the type:

Nat.rec :
  (M : Nat → Sort u) →
  M zero →
  ((n : Nat) → M n → M (succ n)) →
  (n : Nat) → M n

When M n is a proposition, this is exactly mathematical induction. Therefore, an induction tactic does not need to introduce another logical principle. It only needs to construct an application of Nat.rec.

Suppose our goal is:

n : Nat
⊢ P n

where:

P : Nat → Prop

Execute:

induction n with
| zero => ...
| succ k ih => ...

The tactic creates two goals.

Base case:

⊢ P zero

Inductive step:

k : Nat
ih : P k
⊢ P (succ k)

These are precisely the two arguments required by Nat.rec. The proof term being constructed has the form:

Nat.rec
  (M := P)
  ?base
  (fun k ih => ?step)
  n

Here, ?base and ?step are metavariables that the remaining tactics must fill.

Let’s think about a concrete exmaple of proving n + 0 = n. Consider:

theorem add_zero (n : Nat) : n + 0 = n := by
  induction n with
  | zero =>
      rfl
  | succ n ih =>
      rw [Nat.succ_add, ih]

The initial goal is:

n : Nat
⊢ n + 0 = n

After induction n, we obtain:

Case zero:
⊢ 0 + 0 = 0

and:

Case succ:
n : Nat
ih : n + 0 = n
⊢ (succ n) + 0 = succ n

In the base case, both sides compute to the same value, so rfl succeeds.

In the successor case, Nat.succ_add rewrites the left-hand side using the recursive definition of addition, and ih completes the proof. The generated proof has the same essential structure as:

Nat.rec
  (M := fun n => n + 0 = n)
  base_proof
  (fun n ih => step_proof)
  n

This is a direct application of the recursor we already generated from the Nat constructors.

Note that the exact rewriting steps depend on how addition is defined. In Lean 4, a simpler proof of n + 0 = n is also available by computation, but the induction-based version makes the generated recursor explicit.

Generalizing induction Beyond Nat

For the Tree type from Section 5:

inductive Tree where
  | leaf : Tree
  | node : Tree → Tree
  | branch : Tree → Tree → Tree

the tactic:

induction t with
| leaf => ...
| node child ih => ...
| branch left right ih_left ih_right => ...

generates three goals instead of two.

The node case receives one induction hypothesis, while the branch case receives two. This is not special logic implemented for trees. The tactic simply uses the constructor cases required by Tree.rec. The general principle is:

An induction tactic turns a goal into the constructor cases required by the inductive type’s recursor, then assembles their proofs into a recursor application.

That is why the inductive type machinery from Section 5 is so useful: we can build a generic induction tactic rather than implementing a separate induction rule for every type.

6.7 Implementing a Minimal Tactic Engine in Rust

We now have enough pieces to sketch a small tactic engine. The kernel already provides trusted operations such as:

kernel.infer(...)
kernel.check(...)
kernel.is_def_eq(...)

The tactic engine adds a separate layer that manages unfinished proofs. A possible minimal design is:

struct ProofGoal {
    context: Context,
    target: Term,
    metavariable_id: usize,
}

struct TacticState {
    goals: Vec<ProofGoal>,
    assignments: HashMap<usize, Term>,
    next_metavariable_id: usize,
}

The responsibilities of the main tactics can then be summarized as follows:

A tactic is therefore just a program that reads the current proof state, creates or assigns metavariables, and updates the remaining goals.

For example, the essence of intro is:

fn intro(state: &mut TacticState, name: &str) -> Result<()> {
    let goal = state.pop_goal()?;

    let (binder, domain, body) = expect_pi(&goal.target)?;
    let new_target = rename_binder_body(&body, &binder, name);
    let new_goal = state.fresh_goal(
        extend_context(&goal.context, name, &domain),
        new_target,
    );
    state.assign(
        goal.metavariable_id,
        lam(name, domain, new_goal.as_term()),
    )?;
    state.push_goal(new_goal);
    Ok(())
}

intro does not prove anything by itself. It replaces a hole with a lambda expression containing another hole. Likewise, apply replaces a hole with a function application containing holes for the missing arguments.

7. The Machinery Under the Hood: Substitution, 𝛼-Equivalence, and Conversion

The above type checker internally calles various functional operations to compare and normalize expressions: capture-avoiding substitution (for T-App and function evaluation), 𝛼-equivalence (for comparing types up to bound variable names), and conversion (for T-Conv).

7.1 Free Variables and Capture-Avoiding Substitution

In our syntax, Π (x: A). Band 𝜆(x: A), tact as binders: any occurrence of xinside the body Bor trefers to the bound parameter. Crucially, the binder’s scope covers only the body , and xis not bound inside the type annotation A. Variables that are not bound by any enclosing Πor 𝜆are called free variables, written FT(x):

/// The free variables `FV(t)`.
pub fn fv(t: &Term) -> HashSet<String> {
    match t {
        Term::Sort(_) => HashSet::new(),
        Term::Var(x) => HashSet::from([x.clone()]),
        Term::App(f, a) => {
            let mut names = fv(f);
            names.extend(fv(a));
            names
        }
        Term::Pi(x, a, b) | Term::Lam(x, a, b) => {
            let mut names = fv(a);
            let mut body_names = fv(b);
            body_names.remove(x);
            names.extend(body_names);
            names
        }
    }
}

Suppose we want to compute (𝜆 (y: A). x) [x -> y]. The original function (𝜆 (y: A). x)ignores its argument yand returns the outer free variable x. If we naively replace xwith y, we get (𝜆 (y: A). y) , which is the identity function! The free variable yhas been accidentally “captured” by the 𝜆 (y: A) binder, completely changing the meaning of the program.

To prevent this, substitution must be capture-avoiding: whenever a binder’s variable yappears free in the replacement terms (y \in FV(s)), we must first rename the binder to a fresh variable zbefore descending into the body.

pub fn subst(t: &Term, x: &str, replacement: &Term) -> Term {
    match t {
        Term::Sort(_) => t.clone(),
        Term::Var(y) => {
            if y == x {
                replacement.clone()
            } else {
                t.clone()
            }
        }
        Term::App(f, a) => app(subst(f, x, replacement), subst(a, x, replacement)),
        Term::Pi(y, domain, body) | Term::Lam(y, domain, body) => {
            let substituted_domain = subst(domain, x, replacement);
            let (renamed_binder, substituted_body) = if y == x || !fv(body).contains(x) {
                (y.clone(), (**body).clone())
            } else if !fv(replacement).contains(y) {
                (y.clone(), subst(body, x, replacement))
            } else {
                let mut avoid = all_names(body);
                avoid.extend(all_names(domain));
                avoid.extend(all_names(replacement));
                avoid.insert(x.to_string());
                let z = fresh(y, &avoid);
                let body_with_z = subst(body, y, &var(&z));
                (z, subst(&body_with_z, x, replacement))
            };
            let domain = Box::new(substituted_domain);
            let body = Box::new(substituted_body);
            if matches!(t, Term::Pi(..)) {
                Term::Pi(renamed_binder, domain, body)
            } else {
                Term::Lam(renamed_binder, domain, body)
            }
        }
    }
}

7.2 alpha-Equivalence: Variable Names Don’t Matte

In any programming language, renaming a function’s parameter doesn’t change what the function does. For example, fun (x: A) => x is the exact same function as fun (y: A) => y .

Similarly, in our theorem prover, Π(𝑃:Sort 0). 𝑃 → 𝑃and Π(𝑄:Sort 0). 𝑄 → Q express the exact same proposition. Terms that are identical except for the names of their bound variables are called 𝛼-equivalent (written as =𝛼).

When the kernel checks whether two types are equal, a simple string or AST equality check (s == t) won't work because P and Q are different variable names. On the other hand, repeatedly renaming variables in the AST to make them match is slow and messy, how do we know which fresh names to pick?

While the detailed mechanism is out of the scope of this article, alpha-equivalence check usually compare binder positions instead of variable names, and the kernel walks both ASTs side-by-side and compares how many binders outward each variable points.

For example, suppose we want to check whether these two nested functions are alpha-equivalent:

• 𝜆(𝑥:𝐴). 𝜆(𝑦:𝐵). x
• 𝜆(𝑎:𝐴). 𝜆(𝑏:𝐵). a

As the algorithm steps inside the binders on both sides, it records the parameter names in two lists (stacks), E1 and E2:

• Pass the first binder: E1 = [x] and E2 = [a].
• Pass the second binder: E1 = [x, y]and E2 = [a, b].

We then look up how far back each variable appears in its respective list (counting from the innermost binder at index 0).

• In E1 = [x, y], x is at distance 1 from the right.
• In E2 = [a, b], a is also at distance 1 from the right.

pub fn alpha(a: &Term, b: &Term) -> bool {
    fn binder_distance(bound: &[String], x: &str) -> Option<usize> {
        bound.iter().rev().position(|name| name == x)
    }
    fn go(a: &Term, b: &Term, bound_a: &mut Vec<String>, bound_b: &mut Vec<String>) -> bool {
        match (a, b) {
            (Term::Sort(u), Term::Sort(v)) => u == v,
            (Term::Var(x), Term::Var(y)) => {
                match (binder_distance(bound_a, x), binder_distance(bound_b, y)) {
                    (Some(i), Some(j)) => i == j,
                    (None, None) => x == y,
                    _ => false,
                }
            }
            (Term::App(f, a), Term::App(g, b)) => {
                go(f, g, bound_a, bound_b) && go(a, b, bound_a, bound_b)
            }
            (Term::Pi(x, a, b), Term::Pi(y, c, d)) | (Term::Lam(x, a, b), Term::Lam(y, c, d)) => {
                if !go(a, c, bound_a, bound_b) {
                    return false;
                }
                bound_a.push(x.clone());
                bound_b.push(y.clone());
                let bodies_equal = go(b, d, bound_a, bound_b);
                bound_a.pop();
                bound_b.pop();
                bodies_equal
            }
            _ => false,
        }
    }
    go(a, b, &mut vec![], &mut vec![])
}

7.3 beta-Reduction: Simplyfing the dependent types

In languages like Rust, TypeScript, or Java, type checking is purely static: the compiler never has to run your functions just to check if two types match.

In a dependent type theory like Lean, however, types can contain ordinary function calls. And that means two types that look completely different on the surface might actually be the same type once you evaluate them!

For example, let Id = 𝜆(𝑋:Sort 0). X be the identity function on propositions. Consider these two types:

• Type A: (𝜆(𝑋:Sort 0). X) P(i.e., Id P )
• Type B: P

Syntactically, Type A is a function application while Type B is a single variable, so they are not alpha-equivalent. Yet if we actually run the function application in Type A by plugging P into X, it evaluates directly to P. Thus, any proof of Id Pmust also be accepted as a valid proof of P.

More formally, evaluating a function application by substituting the argument into the function body is called 𝛽-reduction:

When we repeatedly apply 𝛽-reduction everywhere inside a term until no more function applications can be simplified, the resulting expression is in normal form.

                Term::Lam(x, _, body) if !args.is_empty() => Some(apps(
                    subst(&body, &x, &args[0]),
                    args[1..].iter().cloned(),
                )),

7.4 Conversion

To decide 𝑠 ≡ 𝑡, the kernel normalizes both terms and compares the results with =𝛼 . This procedure relies on two facts. First, 𝛽-reduction is confluent: different reduction orders cannot lead to different normal forms, so 𝑠 ≡ 𝑡 holds exactly when the normal forms of 𝑠 and 𝑡 are 𝛼-equivalent. Second, every well-typed term has a normal form, so normalization terminates.

8. Conclusion

We started with a simple question: What actually happens when Lean 4 verifies a mathematical proof?

By building a miniature theorem prover from scratch, we have seen that the answer is surprisingly elegant. At its core, a theorem prover is a type checker. Thanks to the Curry–Howard correspondence, propositions can be represented as types, proofs as programs, and proof verification as ordinary type checking.

Of course, MiniLean4 is far from a complete implementation of Lean 4. The real system includes sophisticated elaboration, universe polymorphism, type classes, powerful metaprogramming facilities, and many other features. Our implementation also deliberately simplifies several aspects of inductive types and tactics.

Nevertheless, the fundamental architecture is already there. Once you understand how a few typing rules, reduction rules, and recursors fit together, interactive theorem proving starts to look much less like magic and much more like a carefully designed programming language.

You can explore the complete implementation, run the examples, and experiment with your own extensions in the MiniLean4 GitHub repository.

Reimplementing LiteLLM with Rust with h5i-app, optimizing streaming and database operations, and formally verifying core logic with Lean 4.

As applications increasingly rely on multiple LLM providers, developers need a way to manage API keys, route requests, enforce rate limits, track usage, and control costs through a unified interface. This is why AI gateways, services that unify various LLM inference APIs, are becoming an essential part of modern AI infrastructure.

One of the most popoular open-source AI gateways is LiteLLM, a Python-based AI gateway that supports a wide range of LLM providers.

Last weekend, one simple question came to my mind: “What if we rebuilt an AI gateway in Rust? How much performance could we gain?” .

To find out, I built h5i-ai-gateway, an open-source Rust implementation of an AI gateway inspired by LiteLLM, using the Rust web framework, h5i-app which is a Axum-based framework backed with Lean 4 formal verification.

The results was quite promising:

• 41.4× higher throughput for standard chat completions
• 40.5× higher throughput for streaming responses
• 30.1× higher throughput for embeddings
• 65× lower memory usage, from 4.4 GB to just 68 MB
• More than 100× improvement in p99 latency, from 346 ms to 3.08 ms

h5i-app framework also alloed me to formally verify important properties like the correctness of authentication with Lean 4.

What Is an AI Gateway?

An AI gateway sits between your application and LLM providers such as OpenAI, Anthropic, and Google. Instead of integrating each provider independently, applications send requests through a single gateway.

              Application
                   |
                   v
               AI Gateway
                   |
          +--------+--------+
          |        |        |
          v        v        v
        OpenAI  Anthropic  Gemini

An AI gateway typically handles several responsibilities:

• Authentication: Validate API keys and control access to models.
• Routing: Forward requests to the appropriate LLM provider.
• Rate limiting: Prevent excessive requests from individual users or teams.
• Budget management: Track token usage and enforce spending limits.
• Streaming: Relay responses using Server-Sent Events (SSE).

While his additional infrastructure is worthwhile for many applications because it centralizes important operational concerns, the gateway itself can become a significant source of overhead as AI agents begin generating hundreds or thousands of LLM requests,

(Re-) Building the Gateway in Rust

I re-implemented the LiteLLM gateway in Rust, using h5i-app, a Rust web framework built on top of Axum.

One of the central design principles of h5i-app is to separate application logic from HTTP infrastructure. Instead of embedding authorization, budgeting, and routing decisions directly into HTTP handlers, the gateway implements these operations in a separate Rust kernel. This architecture also allows the core logic to be translated into Lean 4 for formal verification.

The overall structure looks like this:

               HTTP Request
                   |
                   v
              Gateway Server
                   |
                   v
               Rust Kernel
                   |
            +------+------+
            |             |
          Admit         Settle
            |             ^
            v             |
        Provider API -----+
                   |
                   v
              HTTP Response

Each request goes through two important stages.

1. Admit: Validate and reserve

Before forwarding a request, the gateway checks:

• Whether the API key is valid
• Whether the requested model is allowed
• Whether the request satisfies rate limits
• Whether sufficient budget is available

If the request is accepted, the gateway reserves the estimated cost.

2. Settle: Finalize usage

After the provider returns a response, the gateway calculates the actual cost using token usage information and updates the corresponding budget.

This separation makes it easier to reason about the correctness of accounting operations, especially when multiple requests execute concurrently. The gateway also supports chat completions, embeddings, streaming responses, and routing across multiple providers.

Benchmark: Rust vs. Python LiteLLM

To make the performance comparison meaningful, I wanted to measure the gateway itself rather than the speed of the underlying LLM. Specifically, I compared the original Python implementation of LiteLLM and my Rust re-implementation, using 8 CPUs and 64 concurrent connections.

Throughput

The Rust implementation achieved more than 40 times the throughput for both standard chat completions and streaming.

However, the PostgreSQL-backed workload showed a much smaller improvement, showing that a faster language does not automatically eliminate database bottlenecks.

Memory Usage

The difference in memory consumption was equally significant.

The Rust implementation used approximately 65 times less memory in this benchmark configuration. This can become particularly important when deploying gateways across multiple replicas or operating resource-constrained infrastructure.

Latency

For the chat completion benchmark, the latency results were:

The improvement in tail latency was particularly impressive. At p99, latency decreased from 346 ms to just 3.08 ms. Of course, real LLM requests often spend much longer waiting for inference. To explore this, I also benchmarked the gateways with an artificial 50 ms upstream delay.

At 256 concurrent connections:

• Python LiteLLM: 657 req/s
• Rust gateway: 4,887 req/s

The Rust implementation still achieved approximately 7.4× higher throughput. These results suggest that gateway overhead can remain significant even when upstream requests involve network delays.

What Actually Made It Faster?

The performance improvement was not simply the result of replacing Python with Rust, and several optimizations made a substantial difference.

1. Optimizing TCP for Streaming Responses

LLM streaming typically uses Server-Sent Events (SSE), where the server continuously sends small chunks of data to the client. Unlike a conventional HTTP response, which might return a single large payload, an SSE connection can involve many small writes. These writes can interact with TCP buffering and delayed acknowledgments, introducing unnecessary latency.

One important optimization was enabling TCP_NODELAY on accepted TCP sockets. This disables Nagle’s algorithm, allowing small TCP segments to be transmitted without waiting for additional data to accumulate.

In the streaming benchmark with 64 concurrent connections, enabling this option improved throughput from approximately: 1,550 req/s → 11,600 req/s (roughly a 7.5x improvement).

2. Batching PostgreSQL Operations with Group Commit

AI gateways often need to maintain accurate accounting information. For example, a request may reserve part of a user’s remaining budget before execution, then settle the final amount after the response is received.

In a PostgreSQL-backed implementation, these operations typically require transactions to preserve consistency. However, issuing an independent transaction for every individual update can become expensive under high concurrency.

To address this, I implemented Group Commit. Instead of committing every update independently, the gateway groups multiple updates from the same tenant into a batch. It also coalesces multiple modifications to the same database row when possible. This significantly reduces the overhead associated with database round trips and repeated updates.

With 64 concurrent connections, PostgreSQL-backed throughput improved from approximately: 70 req/s → 877 req/s (12.5× improvement) .

Formal Verification with Lean 4

Making infrastructure faster is useful, but an AI gateway also needs to be correct. This becomes especially important when the gateway handles authentication, authorization, and financial accounting.

For example, consider the following requirements:

• A request must not be admitted if it violates the budget policy.
• An API key without administrative permissions must not be allowed to modify restricted limits.
• An optimized batch operation must preserve the semantics of the corresponding sequential operations.

These are not merely performance considerations. They are correctness properties. Traditional unit tests can check specific examples, but they cannot generally establish that a property holds for all possible inputs and states. This is where formal verification comes in.

Rust Kernels and Lean 4

One of the motivations behind h5i-app is to make formal verification more practical for real web applications. The framework encourages developers to implement important business logic as a separate Rust kernel. That kernel can then be translated into Lean 4, where mathematical properties of its behavior can be specified and proven.

For the AI gateway, this includes reasoning about admission decisions, permissions, and budget accounting. I also verified properties related to the batching optimization, including equivalence between optimized batched operations and their sequential counterparts under the modeled assumptions.

Try It Yourself

I have open-sourced both the AI gateway and its benchmark.

• AI Gateway: h5i-dev/h5i-ai-gateway
• Benchmark Scripts and Results: h5i-ai-gateway/bench
• Rust Web Framework: h5i-dev/h5i

I tried building a benchmark for formally verifying popular Rust OSS. Along the way, I ended up finding real security vulnerabilities.

In my previous article, I introduced h5i, an Axum-based Rust web framework that allows developers to translate application logic into Lean 4 and formally verify properties such as authorization, data isolation, and business rules.

The core idea of h5i is pretty simple: instead of relying on unit tests alone to check whether an application behaves correctly, we want to mathematically prove that real implementations satisfy specific properties. To achieve this, h5i adopts a kernel-based architecture that allows security-critical application logic to be automatically translated into Lean 4 (see my previous article for details).

To find out whether this approach works for real-world systems, I started building h5i-app-bench, a benchmark that takes existing Axum-based Rust open-source projects, ports their core implementations to h5i, and attempts to formally verify their correctness using Lean 4. Since h5i itself is built on Axum, porting existing Axum applications to h5i was relatively straightforward.

Although I was able to prove most of the selected security properties, I also encountered several properties that I couldn’t prove in Lean 4. Investigating these failed proof attempts revealed bugs in the original Rust implementations, which I then confirmed with concrete tests against the upstream projects.

Some turned out to be real security vulnerabilities, including cross-user data deletion, access-control bypasses, information disclosure, and denial of service in widely used open-source projects.

Here are a few findings that have already been fixed and publicly disclosed. Some of the corresponding benchmark cases, including RustiCal, are still being prepared and have not yet been published.

1. RustiCal: One User Could Delete Another User’s Data

The first example is RustiCal (GHSA-9cp5–7crm-9cf7), a Rust-based CalDAV and CardDAV server.

The bug was surprisingly simple. RustiCal stores calendar objects using three identifiers:

(principal, calendar_id, object_id)

Here, principal identifies the owner. Suppose Alice and Bob both have a calendar named work, containing an event named meeting.ics. These are two completely different objects belonging to different users. However, the hard-delete path executed a database query equivalent to:

DELETE FROM calendarobjects
WHERE cal_id = ? AND id = ?;

Notice what is missing? The owner’s identity. The application correctly checked that Alice was authorized to delete her own event. But the resulting SQL operation could also delete Bob’s event if the calendar and object identifiers matched.

In a reproduction against the original application:

Alice deletes Bob's event directly
    -> 401 Unauthorized

Alice deletes her own matching event
    -> 200 OK

Bob tries to read his event
    -> 404 Not Found

The authorization check worked at the HTTP layer, but the database operation affected a larger set of objects than the authorization decision permitted.

2. OxiCloud: File Metadata Leaked Through Music Playlists

The next example comes from OxiCloud PR #796, a Rust-based file management and sharing platform.

OxiCloud has an authorization system that controls which files a user can access. The interesting part was its music playlist functionality.

A user could create a playlist and add file identifiers to it. However, the application checked whether the user could modify the playlist without sufficiently checking whether the user could access the referenced files.

The resulting behavior was roughly:

Alice owns a playlist
        |
        v
Alice adds Bob's file ID
        |
        v
Playlist accepts the reference
        |
        v
Alice requests playlist tracks
        |
        v
Bob's private file metadata is returned

The leaked information included file names, sizes, MIME types, and audio metadata. The underlying issue was that permission to modify a playlist was being confused with permission to read the files referenced by that playlist.

3. RustFS: A Policy Evaluation That Could Loop Forever

Not every interesting finding involved authorization. While working with RustFS, an S3-compatible object storage system written in Rust, I also encountered a non-termination bug in its policy-variable resolution logic, which was published as GHSA-9wgh-5r68–49p7.

Specifically, RustFS supports variables in access-control policies, such as:

${aws:AccountId}
${aws:username}

These variables are substituted with values from the request context.

The implementation already had a maximum iteration count intended to prevent unbounded expansion. However, the limit was enforced only in the outer resolution loop. A nested substitution routine could repeatedly reconstruct a variable expression and expand it again without returning to that outer loop.

As a result, a tiny input could trigger more than 100,000 resolver calls, while an ordinary input required just one. In certain configurations, this could lead to a denial of service.

4. Why Did Building a Verification Benchmark Reveal Bugs?

One lesson from this experiment was that formal verification changes how we inspect software.

When conducting ordinary security testing, we often start by looking for suspicious endpoints, missing checks, or known vulnerability patterns.

When formalizing an application, we start with a different question: What property is this code supposed to guarantee?

For example:

• Can one user ever modify another user’s data?
• Does every successful operation satisfy the declared access policy?
• Can an API response reveal an object that the caller cannot read?
• Does a recursive or iterative operation always terminate?

To prove these properties, we need to understand the relevant behavior precisely. That process often exposes assumptions that were never explicitly enforced.

• In RustiCal, authorization was checked, but the final database operation was insufficiently scoped.
• In OxiCloud, playlist permissions did not imply permissions on the referenced files.
• In RustFS, an iteration bound did not actually bound the inner computation.

Of course, an unsuccessful proof is not automatically evidence of a vulnerability. It may simply mean that the proof is incomplete, the model is incorrect, or the translation does not support some language feature.

But when a property cannot be proved, investigating why can sometimes reveal a real bug. And that is exactly what made this experiment interesting.

5. What’s Next?

I am continuing to develop h5i-app-bench to understand how formal verification with Lean 4 can scale to real Rust applications.

The benchmark currently includes six published application ports and 101 selected specifications, covering real-world authorization, identity management, file sharing, policy evaluation, and event visibility logic.

AI coding agents are making it dramatically easier to generate large amounts of application code. But generating more code does not automatically make it correct or secure.

We need better ways to check what that code actually guarantees. My original goal was simply to benchmark a framework for proving Rust application correctness. But along the way, I learned that formal verification isn’t just about proving software correct. It can also help us discover where our assumptions about correctness break down.

Links

• h5i — Build, Verify, and Hack Web Applications
• h5i-app-bench — Formal Verification Benchmark
• Benchmark Dashboard
• Previous Article: Proving Rust Web Application Correctness with Lean 4

AI coding agents such as Claude Code and Codex are making it possible to build surprisingly large web applications in a very short amount of time.

But as the speed of writing code increases, another problem becomes increasingly important: “How do we know that the generated code actually behaves the way we intended?”

Of course, we can write unit tests. But tests usually tell us something like “For the inputs we tried, the program behaved correctly.”

Sometimes, however, we want much stronger guarantees like

• One user must never be able to modify another user’s data.
• A balance must never become negative.
• An unauthorized user must never be able to perform an administrative operation.
• A database invariant must remain true after every valid operation.

These are properties we would ideally like to guarantee for all possible inputs, rather than for a finite collection of test cases.

This is where formal verification becomes useful. In this article, I’ll show how we can write the core logic of a web application in Rust, automatically translate that logic into Lean 4, and prove properties about the actual program.

We’ll use h5i-app, a Rust framework built as part of the h5i web security project (repository: https://github.com/h5i-dev/h5i).

What Is Lean 4?

Lean 4 is both a programming language and a interactive proof assistan systemt, where we can write mathematical statements and machine-checkable proofs.

Suppose we are testing a simple function. With ordinary tests, we might check examples such as:

1 + 1 = 2
100 + 1 = 101

Lean lets us state something much stronger:

For every natural number n,
n + 1 is greater than n.

Instead of checking a handful of concrete values, we state a proposition that quantifies over every possible value, and Lean verifies that the proof is logically correct.

For a web application, we might want to prove something like:

For every pair of users A and B,
an operation performed by A cannot modify B's data.

If Lean’s kernel accepts the proof, then, under the assumptions encoded in the model , that property has been mechanically verified.

However, one of the practical problems is how we can ensure the equivalence between the actual Rust implementatino and Lean4 model. To reduce this gap, h5i-app uses Aeneas, which translates Rust programs into Lean.

The entire workflow therefore looks like this:

Write application logic in Rust
            ↓
Automatically translate it to Lean 4
            ↓
State the desired properties as theorems
            ↓
Prove them in Lean

The important point is that the proof is connected to the Rust implementation itself, rather than to a separately maintained model.

What Is h5i-app?

h5i-app is part of h5i, an agent-native web security workspace. h5i approaches web security from two complementary directions; 1) find bugs like a professional red-team, and 2) prove that properties via formal verification.

h5i-app handles the second part, is designed around Axum, which is one of the most popular web framework in Rust, and lets developers isolate security-critical application logic in Rust and verify that logic in Lean 4.

The goal is not to rewrite an entire web application in Lean. You still write your application in Rust as usual. Instead, you separate out the parts where correctness matters most , authorization, state transitions, business rules, and database writes, and make those parts amenable to verification.

Conceptually, the architecture looks like this:

HTTP request
     │
     ▼
┌──────────────┐
│ Axum / HTTP  │
│  transport   │
└──────┬───────┘
       │
       ▼
┌──────────────────────┐
│     Rust kernel      │
│                      │
│ authorization        │
│ business logic       │
│ state transitions    │
└──────┬───────────────┘
       │
       │ Aeneas
       ▼
┌──────────────────────┐
│        Lean 4        │
│                      │
│ theorem / proof      │
└──────────────────────┘
       │
       ▼
┌──────────────────────┐
│ storage / PostgreSQL │
└──────────────────────┘

The central idea is the kernel that receives:

current state
+
the user performing the operation
+
the requested operation

and decides:

allow / reject
+
new state
+
response

Because the kernel is written as relatively pure Rust, separated from HTTP and SQL, Aeneas can translate it into Lean.

Typical things worth verifying include:

• application state transitions
• authorization rules
• business invariants
• construction of database writes
• correspondence between application snapshots and database representations

Building a Tiny Verified Web Application

Let’s build a small example. We’ll create a very simple application that behaves like calculator memory.

Each user owns one number. A user can:

• set the number,
• apply arithmetic operations to it,
• or read the current value.

Create the project:

h5i app new calculator
cd calculator-01

The generated structure looks roughly like this:

calculator/
├── h5i-app.toml
├── kernel/
│   └── src/
│       └── lib.rs
└── proofs/
    ├── Theorems.lean
    └── generated/

The important parts are:

kernel/src/lib.rs
    Application logic written in Rust
proofs/Theorems.lean
    Properties we want to prove
proofs/generated/
    Lean code automatically generated from Rust
h5i-app.toml
    Extraction, verification, and mutation-testing configuration

Step 1: Define Who Is Performing the Operation

First, modify kernel/src/lib.rs, and define a Principal representing the authenticated user:

#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub struct Principal {
    pub org: u64,
    pub user: u64,
}

Here we can interpret that org is the organization ID, and user is the user ID inside that organization..

Step 2: Define the Application State

Next, we define the data stored by the application. h5i-app provides a schema! macro that describes the schema in a form shared between Rust, Lean, and PostgreSQL.

h5i_app_schema::schema! {
    mapping calc_tables for calculator_kernel,
        lean "../proofs/generated/Schema.lean";

    #[derive(Clone, Debug, Default, PartialEq, Eq)]
    pub struct Snapshot {
        memories: Vec<Memory>,
    }
    #[derive(Clone, Copy, Debug, PartialEq, Eq)]
    pub struct Memory in "memories" {
        key { user: u64 }
        value: u64
    }
}

You can think of Snapshot as the current relevant database state. Each Memory represents one user’s calculator value. The schema definition is also used to generate machinery for things such as:

Rust row operations
database conversions
SQL write representations
Lean schema definitions

This is useful because otherwise we would have to maintain separate descriptions of the data model for Rust, SQL, and Lean.

Step 3: Put the Application Decisions in the Kernel

Now we write the core application logic. Conceptually, the kernel exposes a function like:

fn transition(
    actor: &Principal,
    snap: &Snapshot,
    cmd: &Command,
) -> Result<(WriteSet, Reply), Error>

It receives:

who is acting
+
the current state
+
what they want to do

and returns:

allowed:
    database changes
    +
    response

For our calculator application:

pub fn transition(
    actor: &Principal,
    snap: &Snapshot,
    cmd: &Command,
) -> Result<(Option<Memory>, Reply), Error> {
    match cmd {
        Command::Set { value } => Ok((
            Some(Memory {
                user: actor.user,
                value: *value,
            }),
            Reply::Value(*value),
        )),

　　　　　Command::Apply { op, arg } => {
            let m = memory_of(&snap.memories, actor.user);
            match compute(*op, m, *arg) {
                Ok(v) => Ok((
                    Some(Memory {
                        user: actor.user,
                        value: v,
                    }),
                    Reply::Value(v),
                )),
                Err(e) => Err(e),
            }
        }
        Command::Get => Ok((
            None,
            Reply::Value(memory_of(&snap.memories, actor.user)),
        )),
    }
}

The actual arithmetic lives in compute:

pub fn compute(
    op: Op,
    a: u64,
    b: u64,
) -> Result<u64, Error> {
    match op {
        Op::Add => {
            if a > u64::MAX - b {
                Err(Error::Overflow)
            } else {
                Ok(a + b)
            }
        }

　　　　　Op::Sub => {
            if a < b {
                Err(Error::Underflow)
            } else {
                Ok(a - b)
            }
        }
        Op::Mul => {
            if b != 0 && a > u64::MAX / b {
                Err(Error::Overflow)
            } else {
                Ok(a * b)
            }
        }
        Op::Div => {
            if b == 0 {
                Err(Error::DivByZero)
            } else {
                Ok(a / b)
            }
        }
    }
}

Notice that this is still completely ordinary Rust. We have not written any Lean yet.

Step 4: Connect the Kernel to the Web Server

The kernel itself does not know anything about HTTP. On the server side, we connect it to h5i-app’s Kernel interface:

pub struct Calc;

impl Kernel for Calc {
    type Principal = k::Principal;
    type Snapshot = k::Snapshot;
    type Command = k::Command;
    type WriteSet = Option<k::Memory>;
    type Reply = k::Reply;
    type Error = k::Error;
    fn tenant(actor: &k::Principal) -> TenantId {
        TenantId(actor.org)
    }
    fn transition(
        actor: &k::Principal,
        snap: &k::Snapshot,
        cmd: &k::Command,
    ) -> Result<(Option<k::Memory>, k::Reply), k::Error> {
        k::transition(actor, snap, cmd)
    }
    fn apply(
        snap: &k::Snapshot,
        w: &Option<k::Memory>,
    ) -> k::Snapshot {
        k::apply(snap, w)
    }
}

This may look complicated at first, but it is mostly wiring:

Axum
 ↓
h5i-app Engine
 ↓
Calc::transition
 ↓
calculator_kernel::transition

When a request is processed, the runtime roughly performs the following sequence:

HTTP request
     │
     ▼
Authenticate the user
     │
     ▼
Begin PostgreSQL transaction
     │
     ▼
Load the tenant state as a Snapshot
     │
     ▼
kernel::transition(actor, snapshot, command)
     │
     ├── Error
     │     └── rollback
     │
     └── Success
           │
           ▼
       apply writes
           │
           ▼
         commit

The important security decisions therefore happen inside a small piece of logic that we can reason about independently.

Step 5: Translate the Rust Kernel to Lean

Now comes the interesting part. We want to prove properties about the transition function that the application is actually running.

Run:

h5i app extract

h5i-app invokes Aeneas and generates Lean code under proofs/generated . We now have a Lean representation derived from our Rust implementation.

Step 6: Define the Lean4 specifications.

Formal verification does not magically determine what your application should do. You still need to specify the desired properties. That is actually one of the most important aspects of formal verification.

For example, we can state that the transition function is total: for every actor, application state, and command, evaluating the kernel returns a well-defined result instead of encountering an invalid execution such as an unchecked overflow or bad index.

A theorem may look like this:

/--
The kernel never fails:
no panic, overflow or bad index, for any input.
-/
theorem transition_total
    (a : Principal)
    (s : Snapshot)
    (c : Command) :
    ∃ r, transition a s c = ok r := by
  ...

Here, variables like Principle, Snapshot, and Command, are arbitrary, and we are claiming something about every possible combination of actor, state, and command.

Step 7: Prove It

We then provide the proof:

theorem transition_total
    (a : Principal)
    (s : Snapshot)
    (c : Command) :
    ∃ r, transition a s c = ok r := by
  have h : transition a s c ⦃ _ => True ⦄ := by
    unfold transition
    cases c <;> step*
  obtain ⟨r, hr, _⟩ :=
    (WP.spec_equiv_exists _ _).1 h
  exact ⟨r, hr⟩

Finally:

h5i app check

Or, to re-extract the Rust code and verify everything together:

h5i app prove

If verification succeeds, the pipeline has checked:

Rust kernel
    ↓
translation to Lean via Aeneas
    ↓
the theorem you specified
    ↓
proof checking by the Lean kernel

What Kinds of Properties Can We Prove?

h5i-app works particularly well for properties that can be expressed in terms of state transitions.

Authorization

For example:

A user from another organization
cannot modify this resource.

This is stronger than testing a few authorization endpoints. The theorem can quantify over arbitrary users, organizations, resources, and application states.

Data invariants

Suppose an application handles balances. We could prove:

If the balance is non-negative before an operation,
it remains non-negative afterward.

Workflow rules

For a payment workflow:

A request that has not been approved
cannot transition to the paid state.

Ownership

For a resource-transfer system:

resource.owner may change only when
a transfer operation succeeds.

These are exactly the kinds of properties where ordinary test suites tend to grow into enormous collections of edge cases.

Formal verification lets us instead reason about the underlying rule.

Tests and Formal Verification Solve Different Problems

This does not mean formal verification replaces ordinary testing. A unit test is excellent for checking “given this concrete input, do I get this concrete output?”

A theorem is better suited to questions like “for every possible user, state, and command, can this security invariant ever be violated?”

Similarly, formal verification does not eliminate the need for security testing. You can only prove properties that you thought to specify. An attacker, on the other hand, may discover an entirely different weakness that never appeared in your specification.

Conclusion: Why This Matters More in the Age of AI-Generated Code

As AI agents become capable of generating increasingly large amounts of production code, reviewing every generated line manually becomes less realistic.

Today, we often rely on arguments such as “I read the code and it looks correct.” or “The tests pass, so it is probably fine.” Those approaches remain useful, but they become increasingly difficult to scale as the amount of generated software grows.

For important properties, I think we will increasingly want a stronger statement: “Lean checked that this property holds for every possible input covered by the model.”

That does not mean the entire web application has somehow been mathematically proven perfect. The assumptions still matter., the specification still matters, and the boundary between the verified kernel and the rest of the system still matters. But it gives us a much stronger foundation for reasoning about particularly security-sensitive core application logic.

If you want to experiment with this approach, h5i is available on GitHub: https://github.com/h5i-dev/h5i

A Formally verify the correctness of Web App written in Axum via Lean4.

AI Agents such as Claude Code and Codex has made it easy for anybody to implement web applications that “work”. However, it’s still quite difficult to verify whether those softwares are correctly implemented or not.

One potential approach is writting as many unit tests as possible and increasing their coeverage, though it does not provide any theoretical gurantee.

One of the better solution that gives us formally verified gurantee is using a theorme prover like Lean 4, where we can state a property such as “a successful command leaves every other user’s memory unchanged” and supply a mathematical proof checked by Lean.

However, verifying the correctness of Web Applications with Lean 4 is still quite difficult, since Lean 4 has been mostly used in mathematical research or softwares in limited domains like crypto, and there is no standard way to model basic comonents of web app like authentication, DB, or resource management.

This is why I’m building i5h, pronounced “icefish.” It lets developers prove properties of their Rust application logic in Lean 4 while serving the application through Axum. This walkthrough follows its calculator example. The code excerpts come from that example; the complete project includes the imports, adapters, and proof bodies omitted here.

Example: Calculator

Let’s build a web API for a calculator with memory. Each user gets one stored number, initially zero. They can set it, apply an arithmetic operation, or read it back. The server saves the numbers in PostgreSQL between requests.

Here is how the finished API will behave. Alice and Bob are two users in the same organization. $ALICE and $BOB hold their respective authentication tokens, so the server can tell who is making each request. The example below shows the expected responses from a fresh database.

The helper sends a JSON command to POST /rpc:

rpc() {
  curl -s \
    -H "Authorization: Bearer $1" \
    -H 'content-type: application/json' \
    -d "$2" http://127.0.0.1:8080/rpc
  echo
}

rpc "$ALICE" '{"cmd":"set","value":6}'
# {"value":6}
rpc "$ALICE" '{"cmd":"apply","op":"mul","arg":7}'
# {"value":42}
rpc "$ALICE" '{"cmd":"get"}'
# {"value":42}
rpc "$BOB" '{"cmd":"get"}'
# {"value":0}

Alice stores 6, multiplies it by 7, and reads back 42. Bob still reads 0 because Alice’s commands affect only her own stored number. The token selects the caller; the JSON body selects the operation.

We want to establish three properties of this behavior: arithmetic produces the specified result or error, a successful update can be read back, and a user’s command leaves other users’ numbers unchanged.

Axum handles HTTP; Lean checks proofs

We will implement the calculator in Rust and then examine the Lean theorems that express these properties.

Axum provides HTTP routing and request handling for Rust applications. We use it to expose the calculator as a JSON API.

Aeneas connects Rust and Lean 4. Together with Charon, it translates supported Rust code into Lean definitions. We then prove theorems about those extracted definitions.

To make this practical, i5h separates application decisions from I/O. A pure Rust function decides what a command does. The surrounding server loads data, calls the function, and persists the result.

Define the calculator’s state and commands

The authentication tokens in the opening example identify Alice and Bob. Inside the application, that authenticated identity is represented by a Principal: an organization ID plus a user ID. We will use organization 1, with user 1 for Alice and user 2 for Bob.

An organization is called a tenant in i5h. It is a group whose stored data is kept separate from other groups. Alice and Bob belong to the same tenant but have separate calculator memories within it.

Start in kernel/src/lib.rs:

#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub struct Principal {
    pub org: u64,
    pub user: u64,
}

For Alice, this value is Principal { org: 1, user: 1 }; for Bob, it is Principal { org: 1, user: 2 }.

The kernel is the Rust code that decides what a command does. It receives a snapshot, the loaded calculator rows for the caller’s organization. In our example, those rows contain Alice’s and Bob’s stored numbers. We declare the snapshot and table together:

i5h_schema::schema! {
    mapping calc_tables for calculator_kernel, lean "../proofs/generated/Schema.lean";

/// One tenant's state: every user's memory.
    #[derive(Clone, Debug, Default, PartialEq, Eq)]
    pub struct Snapshot {
        memories: Vec<Memory>,
    }
    #[derive(Clone, Copy, Debug, PartialEq, Eq)]
    pub struct Memory in "memories" {
        key { user: u64 }
        value: u64,
    }
}

A Memory row holds one user's stored number as an unsigned 64-bit value, keyed by that user's ID. schema! generates the row operations and table mapping, as well as a Lean schema file used by the proofs.

The API supports three commands:

#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub enum Op {
    Add,
    Sub,
    Mul,
    Div,
}

#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub enum Command {
    /// Store `value` in my memory.
    Set { value: u64 },
    /// Replace my memory `m` with `m op arg`.
    Apply { op: Op, arg: u64 },
    /// Read my memory.
    Get,
}
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub enum Reply {
    Value(u64),
}
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub enum Error {
    Overflow,
    Underflow,
    DivByZero,
}

Set replaces the caller's value, Apply performs arithmetic on it, and Get reads it. A user who has never stored a value starts at zero. The helper memory_of implements that rule by searching the snapshot for the first matching user row.

Implement arithmetic and the state transition

The arithmetic function computes the operations, while checking whether an operation has a valid u64 result:

pub fn compute(op: Op, a: u64, b: u64) -> Result<u64, Error> {
    match op {
        Op::Add => {
            if a > u64::MAX - b {
                Err(Error::Overflow)
            } else {
                Ok(a + b)
            }
        }
        Op::Sub => {
            if a < b {
                Err(Error::Underflow)
            } else {
                Ok(a - b)
            }
        }
        Op::Mul => {
            if b != 0 && a > u64::MAX / b {
                Err(Error::Overflow)
            } else {
                Ok(a * b)
            }
        }
        Op::Div => {
            if b == 0 {
                Err(Error::DivByZero)
            } else {
                Ok(a / b)
            }
        }
    }
}

For multiplication, the guard checks whether the result would exceed u64::MAX without first computing the potentially overflowing product. Subtraction rejects a negative result, and division uses integer division.

Now connect arithmetic to the user’s memory:

pub fn transition(
    actor: &Principal,
    snap: &Snapshot,
    cmd: &Command,
) -> Result<(Option<Memory>, Reply), Error> {
    match cmd {
        Command::Set { value } => Ok((
            Some(Memory { user: actor.user, value: *value }),
            Reply::Value(*value),
        )),
        Command::Apply { op, arg } => {
            let m = memory_of(&snap.memories, actor.user);
            match compute(*op, m, *arg) {
                Ok(v) => Ok((
                    Some(Memory { user: actor.user, value: v }),
                    Reply::Value(v),
                )),
                Err(e) => Err(e),
            }
        }
        Command::Get => Ok((
            None,
            Reply::Value(memory_of(&snap.memories, actor.user)),
        )),
    }
}

The result contains a proposed write and a reply. Some(Memory { ... }) means to insert or replace a row; None means there is no write. An error refuses the command.

Notice that both write-producing branches construct the row using actor.user. The request does not supply a different user to write to. We will make this ownership property explicit in the proofs.

The function apply defines what applying a proposed write means for an in-memory snapshot:

pub fn apply(snap: &Snapshot, w: &Option<Memory>) -> Snapshot {
    let mut s = snap.clone();
    match w {
        Some(m) => Memory::put(&mut s.memories, *m),
        None => {}
    }
    s
}

The generated Memory::put replaces the matching user's row or appends a new one. Keeping this operation explicit lets us prove properties involving both the decision and its resulting state.

None of these functions queries PostgreSQL. Their inputs contain everything they need. The kernel uses the Rust subset supported by the extraction toolchain; the example uses indexed while loops and explicit match expressions.

Expose the calculator through Axum

The server adapter in server/src/lib.rs connects the kernel to i5h:

• Kernel for Calc supplies the types, tenant ID, transition, and apply.
• Store<Calc> for CalcStore loads rows and persists the kernel's write set through the generated mapping.
• Api<Calc> for CalcStore converts between JSON and kernel commands, replies, and errors.
• ReplyCodec<Calc> for CalcStore supplies encoding and request identity for idempotency support.

For example, the kernel adapter calls the function we just wrote:

fn transition(
    actor: &k::Principal,
    snap: &k::Snapshot,
    cmd: &k::Command,
) -> Result<(Option<k::Memory>, k::Reply), k::Error> {
    k::transition(actor, snap, cmd)
}

The server’s main function constructs the engine and merges i5h's RPC route into an Axum router. Here is its central setup, with formatting expanded:

let engine = Arc::new(Engine::<Calc, CalcStore>::new(
    pool(&i5h_pg::with_schema(&url, "calculator")?, 8)?,
    EngineConfig::default(),
));
engine.install_schema().await?;

let app = I5h::new(engine, auth);
let router = Router::new()
    .route("/healthz", get(|| async { "ok" }))
    .merge(rpc_router(app));
let listener = tokio::net::TcpListener::bind(&addr).await?;
axum::serve(listener, router).await?;

For an RPC request, the engine loads the tenant’s state, runs transition, persists the resulting writes, and commits within a PostgreSQL SERIALIZABLE transaction. A retry starts again from a newly loaded snapshot.

Extract the Rust code and write its specification

Charon extracts an intermediate representation from the Rust kernel, and Aeneas translates it into proofs/generated/CalculatorKernel.lean. We do not edit that generated file. It represents the implementation whose behavior we want to establish.

Our specification lives separately in proofs/Spec.lean:

def eval : Op → Nat → Nat → Except Error Nat
  | .Add, a, b => if a + b < 2 ^ 64 then .ok (a + b) else .error .Overflow
  | .Sub, a, b => if b ≤ a then .ok (a - b) else .error .Underflow
  | .Mul, a, b => if a * b < 2 ^ 64 then .ok (a * b) else .error .Overflow
  | .Div, a, b => if b = 0 then .error .DivByZero else .ok (a / b)

Nat means natural numbers, so multiplication here has no machine-integer overflow. The specification computes the mathematical result and checks whether it fits below 2^64.

That gives us two independently readable descriptions. Rust implements multiplication using a division-based overflow guard. Lean’s eval describes the intended answer directly. The proof must show that they agree, including which operations return errors.

State what the implementation must guarantee

The following declarations are from proofs/Proofs.lean. Only the theorem statements are shown; their existing proof bodies are omitted from the article.

Arithmetic matches the specification

theorem compute_spec (op : Op) (a b : U64) :
    compute op a b ⦃ r => match r with
      | .Ok v => eval op a.val b.val = .ok v.val
      | .Err e => eval op a.val b.val = .error e ⦄

This means that for every operation and every pair of 64-bit inputs, compute completes without an extracted runtime failure, and its result agrees with eval.

If Rust returns a value v, the specification returns the same value. If Rust returns an application error e, the specification returns that same error. The .val fields expose machine integers as natural numbers.

The notation ⦃ r => ... ⦄ expresses successful execution of the extracted computation together with a property of its result. A deliberate Error::Overflow is a valid application result; it is different from the implementation unexpectedly overflowing or panicking.

Reading after an update returns its result

theorem get_after (a : Principal) (s s' : Snapshot) (c : Command) (w : Option Memory) (v : U64)
    (hroom : s.memories.length < Usize.max)
    (ht : transition a s c = ok (.Ok (w, .Value v))) (hs : apply s w = ok s') :
    transition a s' .Get = ok (.Ok (none, .Value v))

The parameters are an actor a, an initial snapshot s, a resulting snapshot s', and any command c. Its hypotheses say:

• hroom: the memory vector has room below the modeled usize bound.
• ht: the command succeeds, producing write w and reply value v.
• hs: applying w succeeds and produces s'.

The conclusion says that Get in s', by the same actor, returns v and produces no write.

This covers Alice setting 6 or multiplying it by 7, but it is not restricted to Alice or those numbers. It quantifies over all values satisfying the hypotheses. It describes the state immediately after this modeled update, with no intervening command.

There are two success layers in ok (.Ok ...): the outer ok means the extracted computation completes successfully; the inner .Ok is the Rust application's Result::Ok.

Other users’ memory stays unchanged

theorem others_unchanged (a : Principal) (s s' : Snapshot) (c : Command) (w : Option Memory) (reply : Reply)
    (hroom : s.memories.length < Usize.max)
    (ht : transition a s c = ok (.Ok (w, reply))) (hs : apply s w = ok s')
    (u : Nat) (hu : u ≠ a.user.val) :
    memOf s'.memories.val u = memOf s.memories.val u

The setup is similar, but now we choose any user u different from the caller. memOf is the specification's lookup function: it returns that user's stored value, or zero if the row is absent.

The conclusion is an equality between the value before and after applying the command. Whatever successful command Alice executes, Bob’s memory stays the same. This is a property of users within the supplied tenant snapshot; the framework’s separate storage machinery handles tenant separation.

The file also proves writes_own_memory, which establishes that any returned write names the caller, and transition_total, which establishes that the extracted transition completes for every input. The latter still permits intentional application errors such as division by zero.

What happens if we introduce a bug?

Lean checks the proof bodies supplied in the repository against the extracted implementation. To see why that connection matters, consider a one-character change to the Rust code.

To see the connection to Rust, change the subtraction condition in compute:

// Incorrect: equal operands should produce zero.
if a <= b {
    Err(Error::Underflow)
} else {
    Ok(a - b)
}

The original guard was a < b. With <=, the implementation rejects 5 - 5, while eval requires zero.

After the changed Rust is translated into Lean, the existing arithmetic proof fails in the subtraction case. At equal operands, the implementation returns Underflow, but compute_spec requires it to agree with eval, which returns zero. The repository's tutorial demonstrates this failure.

The proof is tied to the extracted code. If we changed Rust but kept checking an old Lean translation, we would still be checking the old implementation. The repository’s CI regenerates the translation and checks that it matches the committed Lean code.

What connects these proofs to the running server?

get_after and others_unchanged are about the extracted kernel and its modeled state update. A running server also needs to store and reload that state correctly.

The calculator’s Storage.lean connects the generated row operations, writes, and decoding to a shared storage theorem. i5h also contains SQL compilation proofs against a model of PostgreSQL statements.

PostgreSQL’s actual statement semantics and serializable execution remain assumptions, as does the engine’s implementation of its transaction protocol. The HTTP and authentication layers must supply the intended command and caller. The translation tools and proof checker are also trusted. These boundaries are documented in docs/TRUST.md.

For this calculator, we have concrete statements to inspect: arithmetic agrees with eval, successful updates can be read back in the resulting state, and other users' values remain unchanged. Each statement refers to the extracted implementation and spells out the conditions under which it holds.

Reference

• https://github.com/h5i-dev/i5h
• https://github.com/AeneasVerif/aeneas
• https://docs.rs/axum/latest/axum/

When you log in to an application, how does it recognize you on the next request? One common answer is a JSON Web Token, or JWT. To put it simply, it’s a token issued by a server, and the client presents it later. The service that receives it from the client checks whether it should trust that token or not.

What is JWT?

In a conventional server-side session, an application stores session state and gives the browser a session identifier, often in a cookie. On a later request, the application looks up the identifier.

JWT-based design instead allows the client to present a singed token, often as Authorization: Bearer <token> or through a cookie. Then, the service verifies the token and checks its claims before deciding what the request may do.

One of the advantages of tihs JWT-based authentication is that asigned JWT can reduce the need for a central session lookup on every request. Ofcourse, it does not mean the application has no other state. Account status, permissions, revocation, and business rules may still require a database or another service.

Also, JWT is a format, not a login protocol. A JWT may serve as an ID token or an access token, depending on the system. Those tokens have different intended recipients and must not be treated as interchangeable.

What is inside a signed JWT?

The common compact form has three Base64url-encoded segments separated by dots:

base64url(header).base64url(payload).base64url(signature)

The header describes how the token is protected. For example:

{"alg":"HS256","typ":"JWT"}

The payload contains claims (the bellow is a simplified example with illustrative values):

{
  "iss": "https://login.example.test",
  "sub": "user-123",
  "aud": "https://api.example.test",
  "exp": 1893456000
}

iss identifies the issuer; sub identifies the subject; aud names the intended recipient; and exp is an expiration time expressed as a Unix timestamp. Systems may add claims such as scopes or roles, but a claim is only useful if the receiving service interprets and enforces it correctly.

The signature protects the encoded header and payload against undetected changes. For an HS256 token, the issuer computes an HMAC over the first two segments using a shared secret, then Base64url-encodes the result.

Note that Base64url is encoding, and not encryption. Anyone holding an ordinary signed JWT can decode its header and payload.

Verification process?

Suppose someone changes sub from user-123 to admin-1. The first two encoded segments change, but the old signature remains tied to the original bytes. Thus, averifier with the correct key detects the mismatch.

The receiving service should also check that the token is unexpired, comes from the expected issuer, is meant for this service, and is of the expected token type. It should enforce the permissions needed for the specific operation. The application must choose which signing algorithms and keys it accepts; it must not let an attacker-controlled header expand that policy.

In short, the signature says that the protected bytes were issued by a party with the signing key. It does not by itself say that this token is suitable for this API request.

Flow 1: the application issues and checks its own token

Imagine an application that uses HS256, and it keeps a strong shared secret on the server.

1. The user submits login credentials to the application.
2. The application authenticates the user and creates a short-lived JWT with appropriate claims.
3. It computes the HMAC with its secret and returns the token to the client.
4. On a later request, the client presents the token.
5. The application verifies the HMAC and checks the claims and the requested operation before responding.

The client never needs the signing secret. Every service that verifies an HS256 token, however, also has the secret needed to create one. Note that it is important to securely design and implement secret distribution when multiple services are involved.

Flow 2: an identity provider issues the token

Now separate the issuer from the application. An identity provider signs a token with its private key; the application verifies it with the corresponding public key. The application can check the token without receiving the issuer’s private key.

1. The user authenticates with the identity provider through the appropriate login flow.
2. The provider issues a signed token intended for a particular client or resource.
3. The client presents the appropriate token to the intended recipient.
4. The recipient obtains the provider’s trusted public keys, commonly through a published key set that it can cache.
5. The recipient verifies the signature and the relevant claims before granting access.

The distinction in step 3 matters, where in OpenID Connect, an ID token tells the client application about the user’s authentication and is addressed to that client. An access token is what a client typically presents to a resource API. Being signed by a familiar provider does not make an arbitrary ID token a valid access token for your API. Likewise, social login can establish identity, but the application may still need to create a local account or session and apply its own authorization rules.

A small security checklist

• Verify the signature using a configured algorithm and trusted key.
• Check iss, aud, exp, and any other claims required by your protocol.
• Keep tokens short-lived where practical and plan how logout or revocation works.
• Treat roles and scopes as authorization inputs, then check the requested resource and action.
• Do not put secrets in a readable payload or expose bearer tokens in logs and shared screenshots.

Exploring JWT-protected requests with h5i

h5i is a red-teaming workspace that lets an agent browse the app and inspect the HTTP requests it produces. You can easily capture an authenticated request, inspect its Authorization header or cookie, replay it with a controlled change, and compare the response. For example, you can check whether an expired JWT token is rejected or whether an endpoint enforces the permissions represented by a valid token.

Further reading

• RFC 7519: JSON Web Token
• RFC 8725: JWT Best Current Practices
• OpenID Connect Core
• JWT Attacks

V8, Google’s JavaScript engine, has become the dominant choice for practical browsers and many embedded runtimes. However, it has also been one of the main source of browser vulnerabilities. Typically, many involve memory-safety problems, such as CVE-2026–78910, a buffer overflow that could be triggered by a malicious HTML page.

Many people then are trying to implement a JavaScript engine in memory safe language such as Rust. One example is Boa, a JavaScript engine written in Rust. While Rust does not completely eliminate memory bugs, especially when unsafe code is involved, it still removes large classes of them by default.

For example, Cloudflare recently released Kitesurf, a new browser built largely with Rust components. Yet its main page scripts still run in V8 isolates. Boa is used only for the occasional eval() that Cloudflare Workers cannot execute natively.

This question has been particularly interesting to me because I have been developing h5i, a CLI-based red-teaming browser that treats both page automation and HTTP traffic capture as first-class capabilities.

Security teams routinely open unknown or deliberately malicious web pages. For that use case, the safety of the browser itself matters a lot. I therefore decided to use Boa as h5i’s primary JavaScript engine rather than embedding V8.

So, did it work? Yes, but only after sharply defining what “a practical browser” meant.げｎ

What worked

Boa is capable enough to run JavaScript used by many ordinary pages. In h5i, scripts can modify the DOM, register event handlers, use promises and timers, call fetch(), load ES modules, and communicate through WebSockets and EventSource. Forms, redirects, cookies, and script-triggered navigation also work.

This was enough to let h5i interact with pages whose contents are created or changed by JavaScript, maintain a session, click elements, submit forms, and inspect the resulting page and network traffic.

Boa also gives us a big resource efficiency. In our simple benchmark, h5i loaded a 22 KB documentation page in 59 ms with 65.6 MB of peak memory. Chromium’s headless_shell took 176 ms and 461.5 MB on the same test.

Removing V8 also means removing its JIT compiler from the attack surface. That is relevant for a browser designed to process hostile pages. It does not prove that h5i is secure, but it avoids one of the most complex and historically vulnerable components found in mainstream browsers.

Web compatibility was better than I initially expected. h5i currently passes 88,199 of 116,471 subtests, or 75.7%, in its selected core Web Platform Tests (WPT) suite.

What broke

However, we also encounter various problems.

For example, Boa does not have V8’s optimizing JIT, and can be slow in a large script-heavy page. In our script-built test page, h5i took 248 ms while Chromium headless_shell took 176 ms.

The second problem was compatibility. Running JavaScript is not the same as running the modern Web. Applications assume the presence of an enormous collection of browser APIs surrounding the engine. h5i supports the subset needed by the pages we currently target, but it has not yet cleared a production React application.

As a result, h5i works best for content-heavy sites, common web interactions, scraping, and HTTP-oriented security testing. However, highly interactive applications may still require Chromium.

Rust did not automatically make the browser secure

Using Rust and removing V8 reduced memory corruption in the JavaScript engine and JIT, although it did not solve browser security as a whole.

For instance, after implementing fetch(), we found a policy bug involving loopback access. A hostile page could request a local development service, read the response through JavaScript, and send it to another allowed destination. Although the code was memory-safe, the security model was wrong. We fixed it by checking both the destination and the document that initiated the request.

Was it worth it?

For h5i, yes.

The goal of h5i was not to replace Chrome for everyday browsing, but to build a lightweight browser for automated and security-sensitive red-teaming tasks, where lower memory use, a smaller attack surface, and control over the full browser stack can matter more than perfect compatibility.

Boa was practical for that scope, because it runs enough JavaScript to make h5i a real interactive browser, while keeping the project in Rust and avoiding a V8 dependency.

The answer would be different for a general-purpose browser. If the requirement is to run every major web application exactly as Chrome does, using V8 or another mature engine such as SpiderMonkey or JavaScriptCore remains the realistic choice.

Reference

• https://h5i.dev/
• https://github.com/h5i-dev/h5i
• Think Like an Attacker: CI/CD Security in the AI Era
• I Built h5i, a Headless Browser for AI Agents Entirely in Rust. No Chromium, No V8

AI has made it much easier to find potential vulnerabilities, inspect application code, mutate HTTP requests, and assemble proof-of-concept attacks.

However, finding a vulnerability is only half the job. A bug may be fixed today and quietly reintroduced during a refactor six months later (it often happenes to me when I use Claude or Codex). A new endpoint may repeat the same authorization mistake.

Thus, it is significantly important to implement the attack as a regression test that runs in CI/CD, rather than just fixing a bug.

In this article, I will show how to encode a confirmed attack flow with h5i and replay it in GitHub Actions.

Example Scenario

Suppose an application exposes this endpoint:

GET /api/documents/{documentId}

During testing, we discover an IDOR vulnerability: after logging in as Alice, changing the document ID in the URL may return a document owned by Bob. Here, the security property that we want to satisfy is “Alice must not be able to read Bob’s document.”

Hence, we want CI to perform the following steps on every pull request:

1. Log in as Alice.
2. Request a document that belongs to Bob.
3. Verify that the application denies access.
4. Verify that Bob’s data does not appear in the response body.

You could express this in an application-specific integration test. But preserving the actual HTTP attack flow gives us a useful black-box property: we test what an external attacker can observe, rather than only the internal function that was patched.

What h5i does in CI

h5i is a lightweight browser and HTTP testing tool for red-team. While h5i is quite useful for interactive red-teaming, we can also easily integrate it with CI/CD pipeline like GitHub Actions.

repository-owned attack flow
            ↓
     structured evidence
            ↓
application-owned oracle

h5i replays the requests and records the responses. A repository-owned program, called an oracle, decides whether the evidence satisfies the application’s security property.

Repository layout

For this example, we add four files:

.
├── .github/
│   └── workflows/
│       └── security.yml
├── .h5i-tests/
│   ├── oracles/
│   │   └── document-isolation.sh
│   └── tests/
│       └── document-isolation.yaml
└── openapi.yaml

• document-isolation.yaml describes the HTTP requests and their order.
• document-isolation.sh decides whether the observed responses are secure.
• security.yml starts the application and runs the test in GitHub Actions.
• openapi.yaml is optional and provides a denominator for API-operation coverage.

1. Describe the attack flow

Create .h5i-tests/tests/document-isolation.yaml:

version: h5i.test/v1
id: document-isolation
name: Alice cannot read Bob's document

actors:
  alice: {}
requests:
  login:
    method: POST
    path: /api/session
    headers:
      content-type: application/json
    json:
      username: alice
      password: "${env.H5I_ALICE_PASSWORD}"
  other-users-document:
    method: GET
    path: "/api/documents/${env.H5I_OTHER_DOCUMENT_ID}"
    headers:
      accept: application/json
flow:
  - send: login
    as: alice
    save: login_result
  - send: other-users-document
    as: alice
    save: attack
    covers:
      operation: getDocument
      mutation: identifier-substitution
oracle:
  command: [../oracles/document-isolation.sh]
  inputs: [login_result, attack]
  timeout_seconds: 10

An actor owns an isolated cookie jar, so the second request uses the session established by the first request.

Values such as the password and Bob’s document ID come from environment variables through ${env.NAME}. The CI job should use seeded, non-production fixtures. Production credentials and production customer data do not belong in this test.

The covers block records that this flow exercises the OpenAPI operation getDocument using an identifier-substitution attack. We will use that metadata later for coverage reporting.

2. Define what “the attack failed” means

Now create .h5i-tests/oracles/document-isolation.sh:

#!/bin/sh
set -eu

login_status="$(jq -r '.responses.login_result.status' "$H5I_TEST_RESULT")"
attack_status="$(jq -r '.responses.attack.status' "$H5I_TEST_RESULT")"
attack_body="$(jq -r '.responses.attack.body' "$H5I_TEST_RESULT")"
forbidden_marker="${H5I_FORBIDDEN_MARKER:?set H5I_FORBIDDEN_MARKER}"
# If login failed, the security property was not actually tested.
case "$login_status" in
  200|204) ;;
  *) exit 2 ;;
esac
# Alice's request for Bob's document must be denied.
case "$attack_status" in
  403|404) ;;
  *) exit 1 ;;
esac
# Bob's data must not appear in the response body either.
if grep -Fq "$forbidden_marker" "$H5I_TEST_ARTIFACTS/$attack_body"; then
  exit 1
fi

h5i provides the oracle with three relevant environment variables:

• H5I_TEST_RESULT points to a JSON evidence bundle containing response metadata.
• H5I_TEST_ARTIFACTS points to the owner-only directory containing response bodies and related evidence.
• H5I_TEST_INPUTS contains the saved response names declared in oracle.inputs.

In h5i, the oracle contract is intentionally small:

• Exit 0: the security property held.
• Exit 1: the security property was violated.
• Any other exit code or a timeout: the test could not reach a conclusion.

3. Replay it in GitHub Actions

Add .github/workflows/security.yml:

name: Security regression tests

on:
  pull_request:
  push:
    branches: [main]
permissions:
  contents: read
jobs:
  security-regression:
    runs-on: ubuntu-latest
    timeout-minutes: 15
    steps:
      - uses: actions/checkout@v4
      - name: Start application
        run: docker compose up -d --wait
      - name: Replay security regression tests
        uses: h5i-dev/h5i@v1
        env:
          # Seeded, non-production CI fixtures
          H5I_ALICE_PASSWORD: alice-ci-password
          H5I_OTHER_DOCUMENT_ID: "2"
          H5I_FORBIDDEN_MARKER: bob@example.test
        with:
          target: http://localhost:3000
          tests: .h5i-tests/tests
          openapi: openapi.yaml
          output: h5i-test-results
      - name: Upload h5i evidence
        if: always()
        uses: actions/upload-artifact@v4
        with:
          name: h5i-test-results
          path: h5i-test-results/
          if-no-files-found: warn

This example assumes that docker compose up -d --wait starts the application at http://localhost:3000. Replace that command with however your project starts its integration-test environment.

The h5i action writes:

• result.json for structured processing,
• junit.xml for CI test reporting, and
• per-response artifacts for investigation when a test fails.

Response evidence may contain sensitive application data. Treat the uploaded directory accordingly: restrict access, choose an appropriate retention period, and avoid using production data.

For stricter supply-chain controls, pin h5i-dev/h5i@v1 and other third-party actions to reviewed commit SHAs rather than moving tags.

4. Measure attack coverage

As the suite grows, a simple test count becomes less informative. Ten passing attacks might cover ten different API operations, or the same operation ten times.

h5i can compare each test’s covers.operation field with the operationId values in an OpenAPI document. It then reports the proportion of API operations for which an attack flow reached a conclusive oracle result.

A minimal openapi.yaml could look like this:

openapi: 3.0.0
info:
  title: Example document API
  version: 1.0.0
paths:
  /api/documents/{documentId}:
    get:
      operationId: getDocument
      responses:
        "200":
          description: Document
        "403":
          description: Forbidden
  /api/profile:
    get:
      operationId: getProfile
      responses:
        "200":
          description: Current user profile

This metric is not code coverage, and it is certainly not the probability that the application is vulnerability-free. It answers how many declared API operations do we have at least one attack flow whose evidence was checked by an oracle.

Summary

AI can accelerate the exploratory side of security testing: reading code, identifying suspicious flows, enumerating endpoints, mutating requests, and proposing exploit chains.

But asking an agent to rediscover every vulnerability from scratch on every pull request is neither deterministic nor efficient. Even a capable model may take a different path, overlook a previously known bug, or stop before reproducing the exact condition that matters.

A better division of labor is:

• Explore: A human or AI discovers an unknown vulnerability.
• Freeze: The confirmed request sequence and expected defense become reviewable repository files.
• Regress: CI replays the attack deterministically on every relevant change.

As vulnerability discovery gets cheaper, retaining what we learn becomes more important. The final step after fixing a security bug should be to make the exploit fail forever.

Links

• h5i on GitHub
• Complete security regression CI example
• Design of portable h5i security tests

However, in 2026, AI agent can now sit above them, choose the next action, interpret and summarize the result, revise its hypothesis, and continue, just like professional human ethical hackers.

As a consequence, a lot of agent-native solutions and tools have poped up this year. Some try to automate and connect the existing softwares like Burp or ZAP with general-purpose agents, while others provides the agent-native solutions that are mostly headless CLI tools.

This article maps that landscape as it stands in September 2026. Note that this blog is not a ranking or recommendation, solely aiming to explain what each category is for, where representative tools fit, and what still remains unsolved.

Category — 1: Automated pentesting

There are many services that try to provide the end-to-end process of pentesting as automated services. It typically includes defining a target and scope, lettting the system test it, and receiving validated findings, attack paths, or counter-examples.

1. XBOW

XBOW is a AI-native offsec platform that emulates hacker behaviors to find, chain, and validate critical vulnerabilities in software. XBOW has startted a lot of attentino after it achieved the top of HackerOne’s US leaderboard in 20205. It runs without a human supervision, and returns vulnerabilities with concrete evidences.

2. Horizon3.ai NodeZero

NodeZero focuses on autonomous pentesting across a broader situations, such as internal and external infrastructure, Active Directory, cloud, Kubernetes, and web applications. It tries to identify realistic attack paths that show how an attacker could exploit target environment and reach valuable assets, rather than just returring isolated lists of potential bugs.

3. Pentera

Pentera, one of the most popular automated seucirty tools, has been also shifting to AI-driven approach. Like NodeZero, it covers internal/external, cloud, identity, and application exposure.

4. Hadrian Nova

Hadrian combines external attack-surface discovery with continuous validation. It’s agentic pentesting feature lets AI agents analyze exposed assets, exuecute tests, and explore potential attack path.

5. Escape

Escape tests APIs, including GraphQL, and discovers endpoints without needing a schema uploaded first. It runs inside the software-delivery lifecycle

6. Aikido

Aikido Security also incorporates autonomous pentesting into a broader developer security platform. It positiones itself as all-in-one application security platform, and provides AI-driven pentesting, secrets and malware detection, and automatic bug fix.

7. Terra

Terra Security takes an explicitly human-supervised position within the commercial segment. Its agents run continuous, business-context-aware tests across web apps, APIs, mobile, internal applications, networks, and cloud.

2. Open-source autonomous agents

Open-source community on agentic security has been also evolving significantly.

8. Strix

Strix is an open-source application-security agent that fully automates the pentesting and bug fix worlflows. It dynamically runs code, tests applications, and attempts to validate findings with working proofs of concept. It can be also integrated with multiple agents, CLI and CI/CD workflows.

9. Shannon

Shannon is also an autonomous pentester for web applications and APIs. It combines source-code analysis with live exploitation, using the code to identify candidate attack paths and the running target to prove whether they are real.

10. PentAGI

PentAGI is a self-hosted multi-agent system for complex penetration-testing tasks. It gives agents access to security tooling and web search, separates roles, stores operational context, and provides an interface for supervising runs.

11. PentestGPT

PentestGPT first begans as an LLM-assisted penetration-testing workflow and has evolved toward a more agentic framework capable of planning and executing security and CTF tasks.

12. Nebula

Nebula deliberately takes a more human-led position. It combines a terminal, browser, editor, files, notes, findings, reports, and AI assistance in one engagement workspace. The operator defines scope and decides what runs.

13. CAI

CAI is an open-source framework for building your own security agents rather than a finished product. It provides agents, tools, handoffs, multi-agent patterns, and optional human-in-the-loop supervision, and it connects to the tooling a team already runs, such as Nmap or Burp.

Note that CAI has been archived, though it’s source code is still available.

3. General-purpose agents connected to security tools

A second open-source movement starts with Claude Code, Codex, Cursor, or another general-purpose agent and gives it security capabilities. Model Context Protocol, or MCP, has become a common integration layer.

14. HexStrike AI

HexStrike AI is an MCP server that exposes a large collection of offensive-security tools to AI agents. Instead of building a proprietary reasoning system, it lets the user bring an agent and equips that agent to invoke scanners, recon tools, web-testing utilities, and exploitation frameworks.

15. Burp Suite’s MCP server and Burp AT

PortSwigger provides an official Burp Suite MCP Server extension, allowing AI clients to analyze traffic and interact with Burp programmatically. PortSwigger has also introduced Burp AT, an agentic capability inside Burp Suite Professional. It takes a human-led approach: the agent receives Burp’s project context and specialist tools, while the tester retains control of scope, tasks, and conclusions.

16. Caido

Caido is following a similar path with an AI skill and MCP-backed access to proxy traffic and testing operations. A general-purpose agent can inspect requests, send modified versions to replay, examine automation results, and work within the proxy context.

17. AutoPentest

AutoPentest packages web-testing workflows behind MCP, drawing on the OWASP Web Security Testing Guide and PortSwigger’s educational material. Many smaller projects expose Nmap, Nuclei, SQLMap, Metasploit, or custom recon pipelines in the same way.

4. Agent-native execution primitives

There are also many tools designed to give an agent a better way to observe or act.

18. h5i

h5i is an open-source, security-oriented headless browser for AI-driven red-teaming. It combines automated browsing with direct access to its own HTTP traffic. An agent can browse an application, capture requests, edit and replay them, compare responses, and run bounded recon through one command-line interface. It also provides several tiers of sandboxes to make the workflow safer.

19. Nuclei

Nuclei remains one of the most useful deterministic engines beneath an agent. Its YAML templates provide fast, reproducible checks across applications, infrastructure, and cloud services. An agent can use Nuclei for broad coverage, interpret the results, select follow-up tests, or generate a regression template after confirming a new issue.

20. OWASP ZAP

OWASP ZAP remains relevant because it provides a mature proxy, scanner, API, daemon mode, and YAML-based Automation Framework. Those are exactly the kinds of stable, inspectable capabilities an agent can orchestrate.

5. What is still unsolved

Triage came back. Autonomous validation was supposed to remove the false-positive problem. In practice a platform that produces hundreds of findings still hands the sorting work to a team that was already behind on alerts, and validation quality varies enough that the sorting cannot be skipped.

Chaining and business logic still favor humans. In the December 2025 ARTEMIS study on a live 8,000-host network, the best autonomous agent beat 9 of 10 OSCP-certified testers but lost to the top human, 9 findings to 13, and it lost on creative chaining and business logic. That gap is the difference between a scan and a pentest.

Reference

• https://strobes.co/blog/open-source-agentic-pentesting-tools/
• https://www.reddit.com/r/cybersecurity/comments/1usbadf/best_platforms_for_continuous_security_validation/

Use all offensive-security tools only against systems you own or are explicitly authorized to test.

Burp was first released in 2003, and ZAP was built around 2010. Caido is much more recent, built in 2022, but still before the coding-agent era. Both were designed for humans, while the web security landscape has shifted dramatically toward AI agents in recent years.

Today, an AI agent in a terminal can use command-line tools to browse an application, inspect HTTP traffic, write scripts to replay requests, research relevant vulnerabilities, and choose its next test based on the results, without opening any GUI-based systems like Burp.

Of course, Burp remains useful for automated scanning, interactive investigation, and reviewing an agent’s work. It also recently relreased MCP-based support for AI agents. Whether to use it depends on the tests you need to run and how you want to inspect the results.

Agents can combine CLI tools to run the entire worlflow of web security tests

An agent can use Nmap for port and service discovery, rustbuster for web content discovery, curl for HTTP requests, ffuf for fuzzing, and Nuclei for existing vulnerability checks. mitmdump captures and modifies traffic, Playwright scripts automate full browsers, and h5i combines headless browsing with HTTP inspection, replay, and modification.

Disclosure: I’ve been an active user of Burp for several years, and also am the maintainer of h5i (600+ GitHub stars), an open-source security-first headless browser with built-in HTTP traffic capturing and modification. I admit that my preference for Burp Suite, along with my optimism regarding human-AI collaboration, might introduce some bias in this article.

AI agents tend to be very good at connecting these tools with bash scripts, such as repeating a request under different sessions, comparing responses, and saving a working reproduction. I really consider Burp Suite one of the best tools for web security testing, but agents can already complete many of these tasks using CLI tools alone, without Burp or its MCP integration.

Agents can solve most challenges in these benchmarks using only CLI tools

Thesedays, many researches have shown that AI agents can solve suprisingly massive areas of security tasks with only CLI tools.

“LLM Agents can Autonomously Hack Websites” gaves agents a Playwright headless browser, basic CLI tools like curl, and a Python interpreter. The agents use them to test sandboxed websites and execute multistep attacks, including database schema extraction and SQL injection.

Their follow-up, LLM Agents can Autonomously Exploit One-day Vulnerabilities, gave agents browser operations, a terminal, web search results, file editing, and a code interpreter. In one case, the agent navigated a checkout flow, collected the required fields, wrote a Python script to exploit a race condition, and executed it through the terminal. GPT-4 exploited 87% of the 15 vulnerabilities when supplied with CVE descriptions, compared with 7% without them.

Both studies used terminal commands and programmatic browser tools to execute attacks. They support testing without a human operating a security GUI, although neither was a CLI-only evaluation.

I also confirmed the agents’ security-related problem solving power with only CLI tools. In my own h5i-benchmark experiment, a general-purpose agent like the normal Opus 5.0 model solved 100 of 104 XBOW validation challenges and 54 of 60 Argus validation challenges through h5i, python script, and other basic CLIs like curl. There are also some teams who have already shown that stronger agents or domain-specific agents can solve more challenges.

Caution: other teams had already published writeups of XBOW and Argus before our experiment. While the agent in my experiment did not directly access or observe those solutions during the run, there is a possibility that those writeups might have been included in its training data. These results only demonstrate that h5i supported the interactions needed to solve most challenges in the two corpora, and they do not show the agents’U performance on unseen vulnerabilities.

Burp still helps testers review agent findings

A GUI-based workspace of Burp is quite helpful for humanto inspect traffic and review uncertain findings. This process is still necessary when we want to check whether AI-generated report is valid or not. There are also relatively modern alternatives such as Caido or ZAP.

These tools can also work with agents. For example, both of Burp and Caido supports MCP integration with AI agents, so that human testers can automate the workflow with agents.

I think Burp, Caido, or ZKP are still necessary for exploratory testing and manual follow-up, while agents using CLI tools would defenitely make the entire workflow more efficient.

Model providers can block authorized testing

An agent may be capable of a test that its provider blocks. Anthropic’s cyber safeguards documentation describes default blocks on certain high-risk dual-use activities, including activities with legitimate defensive applications. It offers a verification process for eligible users and acknowledges that approved users can still encounter blocks on legitimate work.

These restrictions aim to prevent abuse, but they can also interrupt an authorized assessment. Permission from the application owner does not guarantee access to the model capabilities needed for a test.

Save reviewed reproduction scripts, captured traffic, and explicit assertions so the team can verify findings without asking the model to repeat the investigation. A reproduction script can also become a regression test after the vulnerability is fixed.

We human still need the skills to verify agent findings

I would keep practicing manual testing and bug discovery even if AI agents can handle most workflows. Reviewing theiir output requires understanding HTTP, sessions, access controls, and the application’s intended behavior. Model providers like OpenAI and Anthropic may also downgrade the security-related capabilities of agents (which they already do).

Agents can make the bug discovery and report writing process dramatically more efficient, but human testers still need to inspect the evidence, reproduce findings, and continue the assessment when the model fails or refuses a task. Burp and other interactive tools remain useful for that work.