Verification progress
Wasm modules verified with Lean 4 — informal intent, formal spec, machine-checked proof, side-by-side.
Coverage = exports with at least one proven spec.
83% 19 / 23 exports
repo @
a054d8531f0c · rustc edition 2024 · leanprover/lean4:v4.32.0 · extracted 2026-07-14T11:02:01Z Projects
7
Exports
23
Specs
49
Proven specs
48
Verifications
48
Diagnostics
72
Projects
| Project | Exports | Specs | Proofs | Diagnostics | Coverage | Status |
|---|---|---|---|---|---|---|
| num_integer | 1 | 1 | 1 | 1 | 100% | verified |
| rust_array | 3 | 4 | 4 | 4 | 67% | verified |
| rust_array_tests | 4 | 8 | 8 | 8 | 100% | verified |
| rust_u64 | 13 | 12 | 12 | 12 | 85% | verified |
| rust_u64_tests | 0 | 22 | 22 | 44 | — | verified |
| swap_elements | 1 | 1 | 0 | 2 | 0% | 0/1 proven |
| total_variation | 1 | 1 | 1 | 1 | 100% | verified |