Formal path
Every kernel guarantee that can be proved is proved. The 0 theorems below live in lean/Vela/, build with lake build Vela.CoreTheorems, and verify against Mathlib v4.29.1. Each carries an Ed25519-signed kernel-verification record (vlv_*).
| T# | title | module | decl | module sha256 | kernel |
|---|
git clone https://github.com/vela-science/vela cd vela/lean lake exe cache get lake build Vela.CoreTheorems
The build is deterministic: same Lean toolchain (v4.29.1), same Mathlib pin (v4.29.1), same proofs. Each module also has a fast no-toolchain check at scripts/test-lean-bundle.sh.