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.
52% 23 / 44 exports
repo @
ee45cadd9455 · rustc edition 2024 · leanprover/lean4:v4.32.0 · extracted 2026-07-28T14:54:44Z Projects
13
Exports
44
Specs
56
Proven specs
53
Verifications
56
Diagnostics
86
Projects
| Project | Exports | Specs | Proofs | Diagnostics | Coverage | Status |
|---|---|---|---|---|---|---|
| float_minmax | 6 | 1 | 0 | 2 | 0% | 0/1 proven |
| float_reinterpret | 7 | 1 | 1 | 2 | 0% | verified |
| float_round | 3 | 1 | 1 | 1 | 33% | verified |
| float_trunc | 3 | 1 | 1 | 1 | 33% | verified |
| num_integer | 1 | 1 | 1 | 1 | 100% | verified |
| num_integer_opt3 | 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 | 3 | 4 | 9 | 100% | 1/3 proven |
| swap_elements_opt3 | 1 | 0 | 0 | 0 | 0% | no specs |
| total_variation | 1 | 1 | 1 | 1 | 100% | verified |