Gate formal-verification jobs and complete Lean Ed25519 (sorry placeholders, unwired)

[avrabe]

Expected standard (the "full circle"): a formal-verification asset should be (1) wired into CI, (2) gating — not continue-on-error — so a regression actually blocks the merge, and (3) complete — no sorry/axioms standing in for proofs. When any link is missing, the proof exists but cannot stop a regression, so the loop is open. Maybe there is a reason here; if so it should be documented — otherwise it should follow the standard.

Found (.github/workflows/formal-verification.yml): verus-proofs (lines 39, 43), kani-proofs (line 64), and rocq-proofs all run continue-on-error: true. Separately, lean/Ed25519.lean has 6 sorry + an axiom and is not built by any job (the workflow triggers on lean/** but no job checks it).

Recommend: (1) drop continue-on-error on the Verus/Kani/Rocq jobs so SMT/BMC/translation regressions block; (2) complete Ed25519.lean (remove the sorry) and add a lake/Lean CI job that gates. If the proof tooling is too unstable to gate today, note that explicitly.

Noticed during a kiln verification-corpus audit.

[avrabe]

Investigated for the release campaign. The continue-on-error flags are not unexplained oversights — they're load-bearing and documented:

• Verus (formal-verification.yml:51,55): continue-on-error: true # WIP — see audit C-1. The job comment notes the theorem_* functions in src/lib/src/verus_proofs/ are incomplete; the masking is what keeps the job green.
• Rocq (:173): # WIP — see audit C-3: verification/rocq/ is a translation-pipeline stub, not a real Rocq proof. continue-on-error stays until a real .v proof exists.
• Kani (:144): already a refined gate — continue-on-error: ${{ matrix.tolerate_failure }}, tolerating only specific harnesses that hit #[kani::unwind] limits, not a blanket pass.

So dropping continue-on-error now would gate the merge queue on genuinely incomplete proofs (Verus C-1, Rocq C-3 stub) and block all PRs — strictly worse than the open-loop state. The correct sequencing is the inverse of the issue's first bullet: complete the proof first, then flip its gate, per item:

1. Verus C-1 — finish the theorem_* Merkle proofs → then drop continue-on-error on those two steps.
2. Rocq C-3 — produce a real .v proof (not the translation stub) → then gate.
3. Lean Ed25519 — discharge the 6 sorry + the axiom, wire a job that builds lean/Ed25519.lean → then gate.

Each is a proof-completion task (feature-loop + proof-synthesis), not a CI toggle. Recommend relabeling this as a tracking/epic issue with those three as the actual work items, and keeping the gates as-is until each proof is real. The Kani matrix is already at the right standard.