Building a Verifiable Web Framework in Rust

The problem with proving a handler helper

An Axum handler can authenticate, authorize, query PostgreSQL, update rows, and render a response in one place. You can prove a helper function correct and still accidentally bypass it in another route. You can also authorize one object and issue a database write that touches more objects. The architecture has to constrain the path from request to committed change.

The kernel is a decision surface, not an HTTP framework hidden inside Lean. Axum still handles transport. The engine loads the snapshot, invokes the kernel, and applies its proposed write. The table shows why a theorem about kernel logic must be stated with a trust boundary.

A concrete Rust decision

The calculator kernel stores one value per user. Its transition matches commands; these two branches show the essential distinction:

Command::Set { value } => Ok((
    Some(Memory { user: actor.user, value: *value }),
    Reply::Value(*value),
)),
Command::Get => Ok((
    None,
    Reply::Value(memory_of(&snap.memories, actor.user)),
)),

Set proposes a write to actor.user; Get proposes no write. Neither branch takes a database handle or an HTTP request. That restricted shape lets the same Rust implementation become a Lean definition. The full kernel also handles arithmetic errors and an Apply command.

Extractability is a tradeoff. The kernel uses the Rust subset and framework crates supported by Charon and Aeneas; I/O stays in the application shell. This restriction makes the proof surface reviewable, but a handler that bypasses the engine would undermine the intended path. The framework and code review both matter.

What the Lean theorem actually says

After extraction, the calculator proof states that every successful write belongs to the caller:

theorem writes_own_memory (a : Principal) (s : Snapshot) (c : Command) :
    transition a s c ⦃ r => ∀ w reply, r = .Ok (w, reply) →
      ∀ m, w = some m → m.user = a.user ⦄ := by
  unfold transition
  cases c <;> step* <;> (try split) <;> simp_all

The quantified command matters: this is a claim over all successful kernel commands under the model, not a handful of sample requests. It still says nothing by itself about whether an HTTP route supplied the right principal, whether a separate read route skipped the kernel, or whether a GPU executes equivalent code.

Kernel proofs describe a proposed write. Storage proofs address the modeled effect of applying and compiling writes. For tenant isolation, both are needed: a kernel unable to name another tenant would not excuse an SQL statement that omitted its tenant scope. The trust model

Returning to the running web app

The server connects that decision path to Axum. In the calculator example, the application engine is passed to H5iApp, and the resulting router is merged with the ordinary health route:

let app = H5iApp::new(engine, auth);
let router = Router::new()
    .route("/healthz", get(|| async { "ok" }))
    .merge(rpc_router(app));

This bridge is where the proof meets a running service. Authentication, snapshot loading, transaction behavior, external dependencies, and PostgreSQL behavior still have to satisfy their documented assumptions. Integration tests and red-teaming examine those running boundaries. The build and verify guide covers the commands for creating and checking a project.

A proof can pass for the wrong reason

Proving that Get writes nothing is useful, but it does not check whether Apply writes the correct user's row. Proof validation asks whether the specification covers the risky behavior. A deliberate mutation that redirects a write should break a relevant ownership theorem; if it does not, the missing sensitivity deserves investigation. Mutation testing gives feedback about the proof suite, not a new theorem about the whole deployment.

The result is a Rust web app with a deliberately narrow formal core. The strength of this design is that a reviewer can point to the exact implementation, theorem, storage semantics, and remaining trust boundary instead of calling the entire server “verified.”