h5i-app benchmark
Can a coding agent formally verify what real-world Rust code does, in Lean 4?
Each task is one property of an open-source Rust application whose security-relevant logic (access control, input validation, parsing) was ported to h5i-app and extracted to Lean 4. The agent gets the ported Rust, the extracted Lean and a spec, and has to prove the property. Click any task to see the upstream Rust, the port, how the two are checked against each other, the Lean, and the proofs the models wrote.
Work in progress
The benchmark is still being measured. The results below are an interim snapshot: not every model has been run on every task yet, and the numbers will change.
What is h5i-app
h5i-app, the application framework of h5i, is a Rust web framework whose application logic can be proved correct in Lean 4.
- Rust
Build
Handlers and state changes are written in a subset of Rust, served with axum and PostgreSQL transactions.
- Aeneas
Extract
Aeneas translates that Rust into Lean 4 definitions, so the Lean is the code that runs, not a model of it.
- Lean 4
Prove
Authorization, tenant isolation and other invariants become theorems about those definitions.
This benchmark asks whether a coding agent can do the last step on real code: the logic of existing open-source applications, ported to h5i-app.
Method
How a task is made, and what counts as solving it.
- Rust
Upstream code
Access control, input validation and parsing code of an open-source application, at a pinned commit.
- Rust
h5i-app port
Ported function by function. Strings become byte slices, iterators become loops; each change is listed in the port's deviations file.
- Lean 4
Extracted model
Aeneas extracts the ported code. A hand-written spec states the property as a theorem.
- Agent
Proof attempt
No network; the h5i-app Lean library and skill; 40 minutes, resumed once if it stops early.
- Grader
Accepted?
The proof builds, the statement is unchanged, and only
propext,Classical.choiceandQuot.soundare used.
Differential test. Upstream and the h5i-app port run on the same random inputs and must return the same result. A deliberately mutated port must fail.
Applications
Upstream lines are counted without blanks, comments and attributes.
| Application | Upstream | Ported lines | Properties | Properties proved by at least one model |
|---|
Models
Share of attempted tasks solved. Models were not all run on the same tasks; the count is next to each bar. Minutes and cost count only the tasks a model solved. Cost per property-line is the spend at list prices on those tasks, divided by the upstream lines of the operation each solved property is about, summed over the properties. A line counts once for every property about it, and a property proves one aspect of that code, so this compares models; it is not the cost of verifying a codebase.
| Model | Harness | Solved | Minutes per solve | Cost per property-line |
|---|
Tasks
One row per task. solved not solved not run