Repository navigation
EPIC: Proofs reach code — PVB-001 proof↔code bridge #6452
Description
Lean theorems prove properties of models; 0/3133 bindings resolve, so no proof reaches shipped code. Spec docs/specifications/PVB-001-proof-code-bridge.md v1.3 defines L5 = discharge ∧ binding ∧ Kani ∧ differential-oracle evidence, held in a tracked content-addressed bridge-summary.json, nested under ONT-001 proof:.
Pilot: five existing computable exact Lean models, then an authored computable Q4_K scale/min unpacker.
Consumer surface: pv proof-status --format json and pv bridge fresh (pvb-fresh/1), used by pmat via PVB-PMAT-001.
Depends on: PVL-001 EV-1, EV-2, EV-3, EV-5a, EV-6a, EV-6b, EV-7a, EV-7b, EV-8a, EV-8b, EV-9 (D-4: the worker lands missing rows first).
Rulings 2026-10-27: D-1 L5 = four legs, no legacy label · D-2 changed-only PR checks + full nightly · D-3 ≥ 20 % kernel-kind · D-4 PVL rows first · D-5 train N+1, L1 slot, one worker.
Exit: proof-status → .l5_source=="bridge" and .l5_bridged>=6; planted bit-flip mutant RED in provable-ladder; BR-9 at ≥ 20 %; 0 open spec-weakness findings.
🤖 Generated with Claude Code
Activity