Repository navigation
[Epic][Audit 2026-10-21] Formal decision verification, documentation truth and advisory proof gates #674
Description
Baseline main@66648081fbd7b4642f38ba0b273417a8891026ba (2026-10-21). Prior audit epic #657 and JEV fixes #658–#664 are closed; do not reopen or duplicate completed functionality. Existing draft source-pinned docs #662 merged. This epic covers newly discovered residual proof/maintenance gaps under Thermo-Nuclear Review and Thermo-Nuclear Code Quality Review principles.
Deliverables and execution graph
- Verification maintenance: update existing Codex
verify-decision-contractskill + bounded real-code state-space checker, 135-case exhaustive scope and one mutation negative control, independent canonical source capture requirements, durable proof semantics; no second orchestrator or role registry. - Documentation truth: distinguish completed changes from frozen prior audit findings, clarify adapter/profile/schema/role boundaries, correct synthetic fast-role cost/latency and broken local
file://links. - Calibrated evidence authority: require independently reviewable provenance for any
acceptedevidence, distinguish fixture/declared metrics from real calibration, and prevent checked-in metadata from self-authorizing live routing. - Paid provider budget: enforce a real cap or explicitly limit promises and disable unsupported paid dispatch. Current cumulative accounting occurs only after decided response with fabricated fallback
$0.001, no per-call reservation/concurrency limit. - Verification acceptance gate: Swarm independent spec/code/tool/proof checks, Arena baseline vs minimal maintenance vs new model tooling tradeoff, Interrogate mutant/privacy/budget/false-PASS review. Only label actual distinct execution runs when witnessed; otherwise BLOCKED.
Order: (1)+(2) independent; (3)+(4) separately scoped runtime follow-ups; final native/opt-in admission gate depends on (3)+(4) and independently observed receipts. No JEV live calls or paid credentials in this audit. CI smoke is offline evidence, not proof of unrestricted code correctness.
Recursive GitHub execution DAG (2026-10-21)
- [Verification][P1] Maintain Jev formal verification skill with code-level bounded proof and mutation controls #675 existing formal-verification skill and executable bounded invariant suite → draft PR #679 (CI/independent review pending).
- [Docs][P2] Refresh JEV implementation map and label simulated role-fit benchmarks #678 truthful current docs/benchmark qualifications → included in verify(docs): maintain Jev bounded invariants and current adapter truth #679; no retroactive rewriting of historical simulated results.
- [JEV][P1] Require provenance-backed calibration instead of preaccepted in-repo fixture #676 calibration source/provenance and human-approved receipts → runtime follow-up; blocks real advisory promotion until genuine proof.
- [JEV][P1] Paid System One spend ceiling is estimated postresponse, not enforceable #677 paid provider hard spend control → runtime follow-up; blocks promises of capped paid dispatch.
- Final Swarm/Arena/Interrogate acceptance gate → independent reviewer or model receipts with actual run/model IDs and exact code SHA; mark BLOCKED when unavailable. Strict failure-first PASS/UNTESTED/BLOCKED/FAIL semantics.
#675 bounded source-level check ─┐
#678 honest docs + simulated labels ├─→ #679 verification/doc gate
#676 provable calibration ───────┐
#677 enforceable paid budget ───┴─→ opt-in JEV advisory/payment promotion gate
Do not reopen #657/#658–#664 or claim the prior offline fixes are absent. Source inspection/reviewer prompts alone are not native Swarm/Arena/Interrogate execution.
Final exact-head offline evidence (2026-10-21)
-
PR HEAD
7049ecd09f02d82a99fc4851ff30a8eb6eea0903— Portable offline contracts #39556769859 SUCCESS. Original offline Python contracts: 811 passed/28 skipped; added docs, JEV and bounded suite: 134 passed/1 skipped. The maintained verification skill's ownlaunchanddoctorran successfully: 135 finite combinations and bypass mutation test covered by its 2 pytest tests, plus 87 contract regressions passed/1 skipped. -
openspecCLI is missing in the job and is explicitly UNTESTED. Independent official commit/tree source-capturedrive, native harness invocations, provider authentication, paid spend caps, and real Swarm/Arena/Interrogate runs were not executed. They are NOT PASS. -
Source-level Thermo-Nuclear changed-file and Code Quality review recorded as a COMMENT on PR verify(docs): maintain Jev bounded invariants and current adapter truth #679, distinct from independent model reviews. 13 changed files, production runtime unchanged, existing gaps tracked under [JEV][P1] Require provenance-backed calibration instead of preaccepted in-repo fixture #676/[JEV][P1] Paid System One spend ceiling is estimated postresponse, not enforceable #677.
-
[Formal][P2] Model-check atomic paid budget reservation and crash/timeout settlement once designed #680 formal interleaving model of budget reservation/settlement (Quint/FizzBee/TLA+ evaluation after [JEV][P1] Paid System One spend ceiling is estimated postresponse, not enforceable #677 design), with runnable bounded counterexample and code action mapping; optional proof lane, not a pretext to call estimated spend a hard cap. If no provider-bounded charge can be guaranteed, paid JEV must stay OFF.
Activity
tommy-ca commentedon Oct 21, 2026
Progress Update (2026-10-21)
103a466):feat/jev-calibration-and-spend-guardtommy-ca commentedon Oct 21, 2026
Epic Completion & Full DAG Reconciliation (2026-10-21)
All deliverables and child issues under Epic #674 have been fully resolved, audited, verified across the gauntlet, merged into
main, and shipped.1. Reconciled Execution DAG & Shipped PRs
103a466):tests/test_decision_bounded_invariants.py).676275f):specimen_fixture. Enforced non-synthetic evaluator run IDs, immutable dataset digest, and verified reviewer checks before any live advisory route promotion is authorized.SpendLedgerinscripts/decision_adapter.pywith atomic preflight reservation before provider egress, and mandatory conservative settlement infinallyblocks.tests/test_paid_budget_concurrency.py) verifying the safety invariant0 <= spent + reserved <= capacross concurrent race windows, network errors, and timeouts.2. Architectural Boundaries Preserved
pstackstandard library (threading.Lock,urllib,dataclasses).3. Exact Head Verification
bash .codex/skills/verify-decision-contract/scripts/driver.sh doctor:Portable offline contract verification (no-secret push / PR): All checks green in CI.openspec validate --changes --strict: 3 passed, 0 failed.All sub-issues (#675, #676, #677, #678, #680) are closed. Closing epic #674.
refactor(jev): apply thermo-nuclear code judo to spend ledger and obs…
tommy-ca commentedon Oct 21, 2026
Thermo-Nuclear Code Quality Review & Code Judo Polish (PR #684)
Following the completion of PR #679 and PR #681, an exhaustive Thermo-Nuclear Code Quality Review was conducted across the entire stack against the eight non-negotiable standards. The full 6-part layered report is recorded in
docs/audit/thermo-nuclear-674/.1. Code Judo & Structural Simplifications (PR #684, merged as
5f649c6)reset()andset_cumulative_spend()methods toSpendLedger. Eliminated direct external access tospend_ledger._lockinJevDecisionAdapterproperty setters._obs(status, confidence)helper toJevDecisionAdapter, replacing 8 repetitive boilerplate blocks in_invoke_providerand reducing 36 lines of duplicated construction logic.is_fixture_evidence_allowed()inscripts/evidence_receipts.pysupporting bothPSTACK_JEV_ALLOW_FIXTURE_EVIDENCEandPSTACK_JEV_ALLOW_FIXTURE_PROMOTION, removing ad-hoc environment parsing fromscripts/route_resolver.py.CalibratedEvidenceReceipt.provenancein__post_init__to eliminate unstructured metadata fallbacks.2. Non-Negotiable Standards Verification
scripts/decision_adapter.py) is 656 lines.pstackstandard library (threading.Lock,urllib,math).tests/test_paid_budget_concurrency.pyverifies safety invariant0 <= spent + reserved <= capin 50ms with negative mutation protection.3. Exact Head Evidence
bash .codex/skills/verify-decision-contract/scripts/driver.sh doctor: PASS (2 router invariants, 5 concurrency model checks, 91 regressions, OpenSpec valid).python -m scripts.model_role_policy: PASS.openspec validate --changes --strict: 3 passed, 0 failed.