Verus: proofs are model-only (no refinement link) and 2/4 aren't CI-run

[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: Verus is the only formal method gating kiln CI (job verus_verification in ci.yml), but: (1) it proves an abstract model (VerifiedStaticVec in kiln-foundation/src/verus_proofs/static_vec_proofs.rs) with no refinement link to the production StaticVec — "mirrors the production logic but lives entirely in the proof world"; (2) static_string_verify and the safe_memory proof have Bazel targets but are not in the CI job (only static_vec + static_queue run).

So the proven model isn't tied to shipped code, and 2 of 4 written proofs don't gate.

Recommend: add the two missing targets to verus_verification, and add a refinement obligation (or explicitly document the model↔impl gap). Relates to #237 (disabled Kani/Miri — kiln's 22 Kani harnesses don't run in CI).

From a verification-corpus audit across the toolchain.

[avrabe]

Progress: static_string_verify is now wired into the gating verus_verification CI job (PR up). It existed and passed but wasn't run — verified locally (bazel test → PASSED in 5.2s) before wiring, so no CI-breakage risk. The Verus proof count gating kiln goes 2 → 3 of 3 verus_test targets.

Note: there is no separate safe_memory verus_test target in the BUILD — only a verus_library; the three gating proofs are StaticVec / StaticQueue / StaticString. The substantive remaining gap from this issue — the proofs verify an abstract model with no refinement link to the production StaticVec/etc. — stays open; that needs a refinement obligation (or an explicit documented model↔impl gap), which is the harder, separate piece.

[avrabe]

Progress (the second half of this issue): rivet validate open errors are now closed.

#292 takes rivet validate from 16 error-severity diagnostics → 0. This gate had been RED since v0.3.1 (never historically enforced at release time); the release-execution skill treats it as a hard step-4 blocker before tagging.

All 16 closed with honest V-model links (the status-gated rule is: an implemented requirement must trace to both a feature AND a design-decision):

• 23 requirement→parent links to existing features/design-decisions
• 3 new design-decisions documenting real decisions: AD-EXEC-001 (stackless/resumable), AD-QUALITY-001 (defense-in-depth verification), AD-DEBUG-001 (WIT-aware DWARF)
• CTRL-BUILTINS STPA controller added (6 orphaned UCA-BI-* resolved)

Still open (the first half of this issue): the Verus proofs verify an abstract model of the bounded collections, with no refinement link to the production StaticVec/StaticQueue/StaticString types. That refinement obligation (or a documented model↔impl gap) is unchanged and remains the substantive work here.

Residual non-error gate noise (tracked separately, not blocking): 87 undeclared-schema-field warnings + 33 kiln:-prefixed cross-refs originating in synth/meld externals.

[avrabe]

Triage sweep (2026-06-13). First half (CI wiring) is done: all 3 verus_test targets now gate (static_string_verify wired in #291), and the rivet validate gate was closed 16→0 in #292.

Remaining half — the refinement link (the Verus proofs verify an abstract VerifiedStaticVec model with no proven connection to the production StaticVec) — is still open and is the substantive part. Note a relevant unblock: the Charon→Aeneas Rust→Lean pipeline that was risk R3 is now wired (rules_lean#1), so a production-code refinement is reachable through that path as well as via Verus-internal refinement. Kept open as the tracked refinement work.