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.
50% 21 / 42 exports
repo @
b6a0546b1515 · rustc edition 2024 · leanprover/lean4:v4.32.0 · extracted 2026-07-14T12:12:36Z Projects
11
Exports
42
Specs
53
Proven specs
51
Verifications
51
Diagnostics
78
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 |
| 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 |