h5i-app/ bench / prove
GitHub

$ h5i app prove ports/*

How much real-world Rust can h5i-app verify?

Security logic from six open-source Rust servers, ported to h5i-app and stated as 356 Lean 4 properties. We measure how many are proved, how much upstream code they cover, and how fast the port runs.

Verified

Proved specs, the upstream code they cover, and project checks. A theorem proves one property of a function, not all of its behavior.

Application Specs accepted Of security kernel Of kernel ceiling Extract Diff test Gate
Specs accepted
Per application, the larger of the benchmark task set and the source-matched project gate set; the two sets are not added together. Project properties pass h5i app check; benchmark proofs are re-checked in a clean workspace. Only propext, Classical.choice and Quot.sound are allowed.
Of security kernel
Reached lines over the kernel-eligible lines whose module or name is about authentication, authorization, tokens, credentials, sessions, validation or visibility. Keyword-based; every selected spec is a security property.
Of kernel ceiling
Upstream lines in functions that accepted theorems are about, over the module's kernel ceiling: the lines that could be a kernel at all (pure, synchronous, no I/O, clock, randomness or locks, transitively). A static estimate; see harness/kernel_ceiling.py.
Gate
h5i app check. Passes once every spec is proved.

Kernel cost

Kernel time ÷ upstream time on the same inputs, release builds on one host. Below 1× the port is faster. Only measurements where both sides do the same work are plotted.

Show the measurements as a table
ApplicationBenchmarkUpstream nsKernel nsRatioBoundary
Excluded measurements

One side does work the other does not (HTTP request construction, database round trips, input cloning), so the ratio does not compare the kernels. Kept as a record until matched runs replace them.

ApplicationBenchmarkRatioWhy not comparable

Effort

Extracted Lean is generated. Spec and proof lines are written by hand; proof lines exclude the statement.

Application Ported Rust Extracted Lean Lean / Rust Spec Proof lines Median per spec

One mark per accepted benchmark task. Log scales.

Specs

Project properties and the original 101 timed benchmark tasks. Open a task for its statement, code, Lean and proof.

Spec Property Status Upstream lines Proof lines Prover

Method

How specs are built and checked.

  1. Rust

    Upstream code

    Security code of an open-source server, at a pinned commit.

  2. Rust

    h5i-app port

    Ported function by function. Each change is listed in DEVIATIONS.md.

  3. Lean 4

    Extracted model

    Aeneas turns the port into Lean. A spec states each property.

  4. Prover

    Proof

    Agents in an offline sandbox, 30 minutes per try, or by hand.

  5. Checker

    Accepted?

    Re-checked in isolation, then gated by h5i app check.

Differential tests. Upstream and port must agree on random inputs. Testing, not proof.

Corrections. A false spec gets a recorded precondition, never a silent change.