The audit instrument for the contract pre-registered in ee73dd1. No semantic change; the only kernel change is one new #[test]. scripts/p037_proof_boundary.py derives from source everything a hand-kept list would let drift: - the Kani inventory (23 #[kani::proof]); - the CI partition (15 fast in ci.yml formal-p037, 8 heavy in formal-p037-gate.yml; each loop must really run cargo kani); - the load-bearing assumptions of each harness, from the generators and predicates in its body. It then audits formal/p037-kernel/proof-boundary.json: - every harness has a claim, concrete kernel subjects, assumptions and a CI class; - every assumption has exactly one class, and a PRODUCTION_GUARANTOR names an existing mechanism with a production-seam control; - the bounded adapter matches lib.rs and claims no production bound; - A8 orders fin before select/collapse/lower; - A7 carries a fairness contract; - A11 reads NO_GUARDED_EVIDENCE. Two production-seam rules scan rust/, ownlang/ and frontend/: - no kernel-importing file calls solve_with / elect_with / lfp_chaotic (#368 option C, made executable); - none lowers or collapses cells outside apply (the F2 bypass). --selftest fires F1-F4 and F6-F10 as in-memory mutants. --mutants runs F5 on a temp copy of the crate: removing fin from apply or lower is killed by the k7_ twins. The #368 witness issue_368_unfair_schedule_returns_a_non_fixpoint pins Some(non-fixpoint) for solve_with and elect_with under a schedule that skips a live coordinate; #368 is not fixed. Wiring: - tests/test_p037_proof_boundary.py runs --check and --selftest in every tests/run_tests.py; - ci.yml formal-p037 gains a --mutants step; - the kernel README drops its stale hand-kept "22 harnesses" (the source has 23). docs/evidence/p037-b0-probes/ holds the three extractor probe programs and their observed bodies/sidecars (the A15 join cases). The dogfood scan covers frontend/roslyn/samples only, so they are inert for CI. Refs #304 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01KmiyfrkaG9sJruTcshM2oq

Commits

Commits on Sep 28, 2026

P-037 B0: pre-register the proof-boundary audit (question, conditions, falsifiers, KILL/PASS)

P-037 B0: the proof-boundary manifest, its checker, and the #368 witness

P-037 B0: RESULT PASS — proof boundary closed for Phase B shadow

P-037 B0: record the owner ruling on B0 and A14