Build and Verify a Web App

Tests can show what happened for chosen inputs. A theorem can state a rule over every input covered by its model. For a web app, that rule might say a user can only change their own record, a balance cannot become negative, or a state transition preserves an invariant. The proof is useful only when it describes the Rust that actually runs and when its assumptions are understood.

1. Put application decisions in a Rust kernel

h5i-app uses Axum for HTTP and a separate kernel for application decisions. The handler authenticates a request and passes the actor, current state, and command to the kernel. The kernel returns a proposed write and reply, or a refusal. Keeping HTTP and database access out of this function gives the translation toolchain a focused Rust program to model in Lean 4.

HTTP request → Axum handler → Rust kernel(actor, snapshot, command)
                                  ↓
                       write + reply, or refusal

The calculator example stores one memory value per user. Its transition function decides whether an operation is valid and which row may change. The same shape works for authorization, tenant isolation, and business workflows.

// From the calculator kernel's transition match:
Command::Set { value } => Ok((
    Some(Memory { user: actor.user, value: *value }),
    Reply::Value(*value),
)),

This branch constructs a write for actor.user. The caller's identity comes from the handler, while the command supplies only the new value. The full transition also handles arithmetic and reads.

2. Scaffold a project

h5i app new counter
cd counter
h5i app doctor

The new project has a Rust kernel, a proofs/ directory, and h5i-app.toml to describe extraction and proof targets. doctor checks the pinned Charon, Aeneas, and Lean toolchain. If you already have a Rust project, cargo add h5i-app adds the framework, but you still need a kernel and proof project; the app manual describes that layout.

3. State the property before proving it

Decide which rule must hold. In the calculator, a useful property is that a successful command writes only the caller's memory. Another is that an arithmetic operation either returns its mathematical result or the specified refusal. Write the rule in the Lean specification, then prove it about the extracted kernel. A proof of the wrong rule is still a valid proof, so review the specification as carefully as the Rust code.

For example, the Rust kernel refuses subtraction that would underflow:

// From the calculator kernel's compute match:
Op::Sub => {
    if a < b {
        Err(Error::Underflow)
    } else {
        Ok(a - b)
    }
}

The handwritten Lean specification expresses the same rule over natural numbers. It is deliberately simpler than the implementation, so a reviewer can check what the proof is supposed to establish.

-- proofs/Spec.lean: the intended arithmetic
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)

Charon extracts the Rust kernel into an intermediate form and Aeneas emits Lean definitions under proofs/generated/. Keep handwritten theorems outside that generated directory. This avoids maintaining a second handwritten implementation that could drift from Rust.

4. Extract and check the proofs

h5i app extract
h5i app prove

extract refreshes the Lean model. prove runs extraction and checks the configured proof targets. One theorem in the calculator connects the extracted transition to the ownership rule:

-- proofs/Proofs.lean: a successful command writes only the caller's row
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 theorem covers every command case in this model, including the arithmetic branch. In CI, h5i app extract --check verifies that committed generated files match the current Rust kernel without rewriting them. Run the application's ordinary tests too: they exercise adapters and deployments that a kernel proof does not cover.

5. Make the proof fail on purpose

h5i app lint
h5i app mutate

lint checks route authentication structure. mutate changes the kernel in a temporary copy and rebuilds the proofs. A mutation that survives identifies behavior the present specification has not pinned down. For example, changing a subtraction boundary from a < b to a <= b should break a theorem that specifies the equal case. Review a surviving mutation before adding a property; it may also be irrelevant to the intended contract.

What the proof covers

Lean checks stated properties of the extracted kernel under explicit assumptions. It does not automatically prove authentication adapters, the PostgreSQL implementation, deployment configuration, or GPU execution. Read the verification trust model and test the running application as a separate step. The optional GPU backend is checked with CPU/GPU differential tests, not by the Lean kernel proof.

Go deeper

This guide follows the workflow in the author's Japanese h5i-app walkthrough. For runnable source and complete Lean theorems, continue with the calculator tutorial and the framework README.