> NOTE!! i5h is now part of h5i, and the latest tutorial is available at https://medium.com/@Koukyosyumei/proving-rust-web-application-correctness-with-lean-4-8889583f1e15
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 Calcsupplies the types, tenant ID,transition, andapply.Store<Calc> for CalcStoreloads rows and persists the kernel's write set through the generated mapping.Api<Calc> for CalcStoreconverts between JSON and kernel commands, replies, and errors.ReplyCodec<Calc> for CalcStoresupplies 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 modeledusizebound.ht: the command succeeds, producing writewand reply valuev.hs: applyingwsucceeds and producess'.
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 uThe 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.