Formal path
Every Lean theorem in the substrate bundle is pinned to its exact source bytes by a content-addressed anchor (vla_*) and attested by a signed verifier record (vlv_*). Records are signed by the Ed25519 key below; anyone can re-verify each record locally with vela lean verify-check.
One row per theorem. Anchor pins source bytes; verifier record signs an attestation that those bytes built cleanly. Click into any theorem for the full statement.
| T# | title | vla_* | vlv_* | status | module sha256 |
|---|
The substrate ships a CLI that re-derives every record from its preimage and verifies the signature against the published public key. No network, no trust in the build server: clone the source checkout, run the command, get yes/no.
git clone https://github.com/vela-science/vela cd vela cargo build --release --bin vela for f in theorems/T*.vlv.json; do base=$(basename "$f" .vlv.json) ./target/release/vela lean verify-check "$f" --anchor "theorems/$base.anchor.json" done
Each call returns vlv_… (T#) verifies under … when the signature, id derivation, anchor cross-check, and module sha256 all line up. Any tampering to the anchor, the record, or the source surfaces here.