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 = 101Lean 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 LeanThe 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 operationand decides:
allow / reject
+
new state
+
responseBecause 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-01The 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 configurationStep 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 definitionsThis 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 doand returns:
allowed:
database changes
+
responseFor 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::transitionWhen 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
│
▼
commitThe 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 extracth5i-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 checkOr, to re-extract the Rust code and verify everything together:
h5i app proveIf verification succeeds, the pipeline has checked:
Rust kernel
↓
translation to Lean via Aeneas
↓
the theorem you specified
↓
proof checking by the Lean kernelWhat 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