i5h/ benchmark GitHub

i5h 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 i5h 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 i5h

i5h is a Rust web framework whose application logic can be proved correct in Lean 4.

  1. Rust

    Build

    Handlers and state changes are written in a subset of Rust, served with axum and PostgreSQL transactions.

  2. Aeneas

    Extract

    Aeneas translates that Rust into Lean 4 definitions, so the Lean is the code that runs, not a model of it.

  3. 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 i5h.

Method

How a task is made, and what counts as solving it.

  1. Rust

    Upstream code

    Access control, input validation and parsing code of an open-source application, at a pinned commit.

  2. Rust

    i5h port

    Ported function by function. Strings become byte slices, iterators become loops; each change is listed in the port's deviations file.

  3. Lean 4

    Extracted model

    Aeneas extracts the ported code. A hand-written spec states the property as a theorem.

  4. Agent

    Proof attempt

    No network; the i5h Lean library and skill; 40 minutes, resumed once if it stops early.

  5. Grader

    Accepted?

    The proof builds, the statement is unchanged, and only propext, Classical.choice and Quot.sound are used.

Differential test. Upstream and the i5h port run on the same random inputs and must return the same result. A deliberately mutated port must fail.

Not given to the agent. The benchmark's own reference proofs. Proofs the models wrote and the grader accepted are shown under each task.

Applications

Upstream lines are counted without blanks, comments and attributes.

ApplicationUpstreamPorted lines PropertiesProperties 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 Rust line is the spend at list prices on those tasks, divided by the upstream lines of the operations those properties are about.

ModelHarnessSolvedMinutes per solveCost per Rust line

Tasks

One row per task. solved not solved not run