EPIC S2 standing: Provable Contracts (PVL-001) #2870

Spec: APR-EPIC-001 §2 · Epic: S2 · Train: standing · Successor at cut: —
Owner: aprender-w5382 (re-owned 2026-10-19 by aprender-triage-worker at the cop's word: previous owner session absent; picks up children only as batch constituents after its current timed task)

Theme

Provable Contracts (PVL-001)

done_when

Lean/Kani run in required contexts; bindings resolve; L4/L5 have one definition.

Budget

At most 3 open children (docs/roadmaps/epics.yaml). Repo-wide cap 100 open issues; andon at 95.

Absorbs

#2556, #4080, #4081, #4082, #4083, #4084, #4122, #4139, #4166, #4168, #4197, #4198, #4199, #4200, #4201, #4202, #4238, #4239, #4240, #4241, #4244, #4347, #4351

Prior body

Audit of the provable-contracts system in this tree together with its archived upstream
(paiml/provable-contracts). Full plan drafted as
docs/specifications/improve-provable-contracts.md (PV-IMPROVE-001, PR to follow); this
issue is the tracking ticket for it.

Reference HEAD: origin/main @ b1a6324b8 (v0.65.2, 2026-09-05). Every number below was
measured on a detached worktree of that commit with a pv 0.65.2 built from it by cargo
(scripts/pv_bin.sh doctrine) — not the pv on PATH.

The finding in one line

The measurement half (pv lint, pv score, pv proof-status, the README count) reports
PASS, a grade and a proof level for 1,807 YAML files. The enforcement half (build.rs →
#[contract], pv codegen → call sites, Kani, Lean) enforces almost nothing, and every
layer of it reports success while doing so. Most pieces are already filed (#2699, #2797,
#2557, #2648, #2704, #2630, #2530); what is missing is the ordering and the honest baseline.

Measured ledger

The upstream is archived and still being edited

• paiml/provable-contracts is archived on GitHub (last push 2026-04-06).
• The local clone at ../provable-contracts is on main @ 31791c3 with two commits dated after the archive (68a317d L5 binding fix, 31791c3 bashrs SEC002) plus an uncommitted 28-line edit to contracts/manzana/binding.yaml. None can be pushed. contracts/bashrs/safety-classifier-v1.yaml differs from our copy; contracts/manzana/ does not exist here.
• 47 of the 144 shared kernel contracts differ byte-wise; 58 library src/ files differ; ContractKind has 5 variants upstream vs 13 here.
• crates/aprender-contracts-staging/ is not a crate — it is a vendored snapshot (book/, mermaid.min.js 2.6 MB, generated/, proof-status.json) that also happens to hold the only Lean tree. proof_status.rs still falls back to ../provable-contracts/lean.
• 10 generated .pv/ cache files are tracked in git (Epic: pv / provable-contracts hardening — the tool that decides release soundness #2556 housekeeping).

Root cause (five whys, condensed)

The system was built to maximize a score (PMAT-082 mass generation, kaizen penetration, the
README count gate) and the score was allowed to be declared rather than derived. Every
row above follows: hand-typed proof counts are trusted, every silent path (option_env!,
COUNT missing ≡ 0, unparseable predicate ≡ skip, empty macro arm) was written to be
"graceful" for a crates.io stranger and is silent for us, and a count that a gate defends
gets inflated.

Proposed sequencing (detail in the spec)

Phase 0 — tell the truth (no shipped-code change). One ladder; pv validate errors on
summary-count drift; proof_status credits only resolving harnesses/theorems (expect
181 → 8 Lean, L4/L5 to single digits — this is the honest baseline); README headline
becomes three derived figures behind a floor (closes #2630); port the stranded upstream
edits, remove the ../provable-contracts fallback, untrack .pv/; pv lint becomes its own
CI step with a shrink-only warning baseline (1,082) and --min-score 0.48.

Phase 1 — enforcement that can fail. Close #2699 in full (exported contract_env_key,
generated registry include! instead of env vars, compile_error! on missing/unparseable,
explicit optional); repoint the 10 dangling #[contract] sites; codegen drops the
() => {{}} arm so the 329 empty call sites become compile errors; PV-ENF-003 vacuous-predicate
lint and no more !input.is_empty() auto-fix text; one scoped generated_contracts.rs per
crate (< 30 k lines total); one aprender registry, pv verify-bindings --both-ways in CI
(#2797), superseded + D5 "not measured" (#2704).

Phase 2 — proof credit only from receipts. PV-KANI-001 (every harness: must exist;
shrink-only baseline for the 1,115 dangling) + KaniStrategy::symbolic_float (#2530);
kani-nightly.yml writes receipts and D3 credits only receipts; pin mathlib, lean-nightly.yml
writes receipts, PV-LEAN-001 (delete the 631 inert refs in one PR); remove the registry: true
exemption (#2557) and add kind: descriptor for data-only YAML; test: must be executable
(prose → prediction:), so Gate 4 counts all refs instead of 26; then ratchet --min-score.

Phase 3 — corpus scope. contracts/work/ → .pmat-work/; delete/migrate
v1-legacy-skip/; fleet dirs → contracts/fleet/ (decision D-3); resolve the 48 baselined
duplicate stems; collapse the staging dir to lean/ and rewrite the spec copy for the
monorepo.

Phase 4. Course repo design-by-provable-contracts (installs aprender-contracts-cli
from crates.io) added to the release dogfood lane; fail-closed fixture suite for every gate.

Each item ships with a committed mutant that must be seen RED (FALSIFY-PVI-001..018 in the
spec), per the existing "guard's own case table must pass before it judges" convention.

Decisions needed

Ticket map

Repro

git worktree add --detach /tmp/apr-main origin/main && cd /tmp/apr-main
CARGO_TARGET_DIR=/tmp/apr-target cargo build --release -p aprender-contracts-cli --bin pv
PV=/tmp/apr-target/release/pv
$PV lint contracts/ | tail -4                                   # 0 errors, 1082 warnings, PASS
$PV score contracts/ --binding contracts/aprender/binding.yaml | grep Mean
$PV proof-status contracts/ --binding contracts/aprender/binding.yaml | grep -E '^Totals|^By kind'
grep -rhoE '^\s*#\[contract\("[^"]+"' crates --include='*.rs' --exclude-dir=target | sort | uniq -c
grep -c '() => {{}};' crates/aprender-core/src/generated_contracts.rs   # 1991
gh repo view paiml/provable-contracts --json isArchived                   # true

Refs #2556. Related: #2699 #2797 #2557 #2648 #2704 #2630 #2530 #2512 #1595 #673.

Parked

Closed over budget (APR-EPIC-001 rule 5). Reopen = pull (rule 7).

• aprender-contracts-macros: #[contract] fails open in four places, and the doc comment claims the opposite #2699 aprender-contracts-macros: #[contract] fails open in four places, and the doc co — over S2 budget (rank 4/38)
• P-0.4: honest headline: kernel · descriptive · fleet figures derived by pv status --headline; README checked as a floor (#2630) (FALSIFY-PVI-004) #2914 P-0.4: honest headline: kernel · descriptive · fleet figures derived by pv statu — over S2 budget (rank 31/38)
• P-0.5: freeze the archived upstream: port the two stranded commits + the dirty manzana binding; remove the ../provable-contracts/lean fallback; ARCHIVED-UPSTREAM.md; untrack the 10 .pv/ c #2915 P-0.5: freeze the archived upstream: port the two stranded commits + the dirty m — over S2 budget (rank 32/38)
• P-0.1: one proof ladder (upstream numbering: L4 Kani, L5 Lean; PVI-D-1) in proof_status.rs and the three docs; ladder_consistency test (FALSIFY-PVI-001) #2916 P-0.1: one proof ladder (upstream numbering: L4 Kani, L5 Lean; PVI-D-1) in proof — over S2 budget (rank 33/38)
• PVI-1.3-4.3: PV-IMPROVE phases 1.3-4.3 under #2556: empty macro arm, scoped codegen, PV-ENF-003, one binding registry, Kani/Lean nightly receipts, registry:true removed, prose test -> predictio #2978 PVI-1.3-4.3: PV-IMPROVE phases 1.3-4.3 under Epic: pv / provable-contracts hardening — the tool that decides release soundness #2556: empty macro arm, scoped code — over S2 budget (rank 34/38)
• PVL-F4: Kani in a required context for the L0-1 parity-chain kernels #3140 PVL-F4: Kani in a required context for the L0-1 parity-chain kernels — over S2 budget (rank 8/38)
• VERIFY-001: run the 132 Kani harnesses in CI (proof credit from runs, not declarations) and pilot Verus on one dequant/parser function #3495 VERIFY-001: run the 132 Kani harnesses in CI (proof credit from runs, not declar — over S2 budget (rank 35/38)
• a wide refactor of aprender-contracts made three unrelated PRs DIRTY on the same three files — the class needs a rebase sweep the moment such a merge lands #3628 a wide refactor of aprender-contracts made three unrelated PRs DIRTY on the same — over S2 budget (rank 36/38)
• apr_bin.sh / pv_bin.sh refuse a FOREIGN worktree's binary but accept an OWN-tree binary OLDER than the tree — HEAD sha matches while uncommitted edits differ (d4 #3634 apr; bf #3600 pv to confirm) #3635 apr_bin.sh / pv_bin.sh refuse a FOREIGN worktree's binary but accept an OWN-tree — over S2 budget (rank 5/38)
• 477 YAMLs live in crate-local contracts/ dirs that pv lint has never read — and a sample says some would fail if it did #3860 477 YAMLs live in crate-local contracts/ dirs that pv lint has never read — — over S2 budget (rank 6/38)
• tensor-layout-v1.yaml asserts a compile-time guarantee that is FALSE — and the copy that ships to crates.io carries it #3868 tensor-layout-v1.yaml asserts a compile-time guarantee that is FALSE — and the c — over S2 budget (rank 7/38)
• PROVABILITY-001 requires every kernel contract to declare kani_harnesses, and nothing in this repo runs kani — the schema mandates the declaration #3890 had to neutralise #3941 PROVABILITY-001 requires every kernel contract to declare kani_harnesses, and no — over S2 budget (rank 9/38)
• Enumerated conformance table: derive (qtype × op × backend) proof obligations from the dispatch registry — the test half of #3418 #3945 Enumerated conformance table: derive (qtype × op × backend) proof obligations fr — over S2 budget (rank 37/38)
• PVL-001 EV-8b — PVL-8b: L4 credit from the summary, not YAML; formalization.yaml #4082 PVL-001 EV-8b — PVL-8b: L4 credit from the summary, not YAML; formalization.yaml — over S2 budget (rank 19/38)
• PVL-001 EV-9 — PVL-9: provable-ladder required on main #4083 PVL-001 EV-9 — PVL-9: provable-ladder required on main — over S2 budget (rank 10/38)
• PVL-001 EV-12 — PVL-12: release aprender-contracts-cli with PVL-1..11 #4084 PVL-001 EV-12 — PVL-12: release aprender-contracts-cli with PVL-1..11 — over S2 budget (rank 20/38)
• Docs outside the PVL-001 EV-3 ladder copies still teach the old L4=Kani / L5=Lean mapping (9 files) #4106 Docs outside the PVL-001 EV-3 ladder copies still teach the old L4=Kani / L5=Lea — over S2 budget (rank 27/38)
• provable-contracts facades stuck at 0.4.0 (-> aprender-contracts ^0.64): tier-14 publishes nothing #4111 provable-contracts facades stuck at 0.4.0 (-> aprender-contracts ^0.64): tier-14 — over S2 budget (rank 28/38)
• PVL EV-5a orphan group ProvableContracts.Theorems: 55 module(s) outside the root import cone #4124 PVL EV-5a orphan group ProvableContracts.Theorems: 55 module(s) outside the root — over S2 budget (rank 29/38)
• PVL-001 EV-6a: pv discharge check — axiom subset pins; compiler-escape allowlist #4139 PVL-001 EV-6a: pv discharge check — axiom subset pins; compiler-escape allowlist — over S2 budget (rank 11/38)
• PVL-001 EV-11 — PVL-11: pv lint ratchets — theorem pairing and depends_on #4166 PVL-001 EV-11 — PVL-11: pv lint ratchets — theorem pairing and depends_on — over S2 budget (rank 21/38)
• PVL-001 EV-7a — PVL-7a: statement pinned apart from proof — pv challenge gen|check #4200 PVL-001 EV-7a — PVL-7a: statement pinned apart from proof — `pv challenge gen|ch — over S2 budget (rank 12/38)
• PVL-001 EV-7b — PVL-7b: comparator — the solution closes exactly the pinned statement #4201 PVL-001 EV-7b — PVL-7b: comparator — the solution closes exactly the pinned stat — over S2 budget (rank 13/38)
• PVL-001 EV-8a — PVL-8a: pv discharge run — one summary the tree can carry #4202 PVL-001 EV-8a — PVL-8a: pv discharge run — one summary the tree can carry — over S2 budget (rank 14/38)
• PVL: timeout on every lake call in pv discharge (comparator + elaborate) — a hang is RED, not a wait #4239 PVL: timeout on every lake call in pv discharge (comparator + elaborate) — a han — over S2 budget (rank 22/38)
• PVL: comparator rows must be cross-checked against EV-7a's Challenge roots — rowsOf's isInternal filter can drop a row silently #4240 PVL: comparator rows must be cross-checked against EV-7a's Challenge roots — row — over S2 budget (rank 23/38)
• PVL: comparator canon — escape Names, normalize universe-param names #4241 PVL: comparator canon — escape Names, normalize universe-param names — over S2 budget (rank 30/38)
• PVL-001 EV-6c — 59 Lean modules (85 bound roots) are unreachable from ProvableContracts.lean: never built, never leancheck'd #4244 PVL-001 EV-6c — 59 Lean modules (85 bound roots) are unreachable from ProvableCo — over S2 budget (rank 15/38)
• PVL: prove all 7 escape-allowlist axioms (DPO x3, f16 bound, NF4 x3) instead of confirming them #4347 PVL: prove all 7 escape-allowlist axioms (DPO x3, f16 bound, NF4 x3) instead of — over S2 budget (rank 24/38)
• proof_status Lean scan: 'sorry' in a doc comment, and the domain.file citation form, deny credit to sorry-free theorems #4351 proof_status Lean scan: 'sorry' in a doc comment, and the domain.file citation f — over S2 budget (rank 16/38)
• #[contract]: a registry sentinel — "no registry" is silent, "registry has no such contract" is a compile error (#2699 cause 2) #4368 #[contract]: a registry sentinel — "no registry" is silent, "registry has no suc — over S2 budget (rank 17/38)
• Migrate the 12 hand-rolled producer build.rs key builders onto build_helper::env_key (#2699 remainder) #4369 Migrate the 12 hand-rolled producer build.rs key builders onto build_helper::env — over S2 budget (rank 18/38)
• apr-cli: 65 #[contract] sites with no producer build.rs enforce nothing (#2699 remainder) #4370 apr-cli: 65 #[contract] sites with no producer build.rs enforce nothing (aprender-contracts-macros: #[contract] fails open in four places, and the doc comment claims the opposite #2699 r — over S2 budget (rank 38/38)
• Prose YAML pre/postconditions become compile_error! when wired — lint every emitted condition as a Rust expression (#2699 remainder) #4371 Prose YAML pre/postconditions become compile_error! when wired — lint every emit — over S2 budget (rank 26/38)
• build scripts still read the gone provable-contracts sibling path: serve codegen (arch-requirements, tensor-names), graph, verify, verify-ml (#4369 class) #4380 build scripts still read the gone provable-contracts sibling path: serve codegen — over S2 budget (rank 25/38)
• OXIDE-001 (0.68.3, fast-track): cuda-oxide pure-Rust #[kernel] → PTX — one GDN kernel ported and measured on lambda-labs, gx10, yoga and mini; every kernel an ont:Kernel with parity, timing and safety receipts per silicon under pv lint --gate shapes #3522 OXIDE-001 (0.68.3, fast-track): cuda-oxide pure-Rust #[kernel] → PTX — one GDN k — floor orphan, not linked over budget (rule 21 wins over rule 6, cop 18:08Z)

Superseded epics

• Epic: pv / provable-contracts hardening — the tool that decides release soundness #2556 Epic: pv / provable-contracts hardening — the tool that decides release soundnes — A4 pending close (waits apr lane); owner lines: owner: aprender-df

Children tracked here (REDUCE-1022)

• pv proof-status credits L3 for kani_harnesses whose harness fn does not exist, even with --verify-bindings #4531 — pv proof-status credits L3 for kani_harnesses whose harness fn does not exist, even with --verify-bindings (open)
• LAB: nightly pv census ratchet red (#4709) #5409 — LAB: nightly pv census ratchet red (CENSUS-RATCHET: entity-bound contracts never drop and rise every release #4709) (closed: not planned)
• pv shapes: give each nested node block its own IRI (#4994) #5501 — pv shapes: give each nested node block its own IRI (pv shapes: two nested node: blocks under one shape share one IRI (release-readiness-v1.host/node) #4994) (closed: not planned)
• Contract ids: sequential OPS-/PV- ids collided 3 times on 2026-10-19 (#5621, #5591, #5765); pick a scheme #5770 — Contract ids: sequential OPS-/PV- ids collided 3 times on 2026-10-19 (test: cover print_coverage_report in aprender-contracts-cli/src/commands/coverage.rs #5621, test: fold multinomial head + on_cuda_load_error + hex output_json_v2 coverage #5591, batch(manual-1615): fold 6 ready branches (#5735 #5592 #5586 #5657 #5672 #5762) #5765); pick a scheme (closed: not planned)
• pv extract walks outside its input dir (parent of <dir>): 9.9 s release / 56 s debug vs 0.00 s #5780 — pv extract walks outside its input dir (parent of ): 9.9 s release / 56 s debug vs 0.00 s (closed: not planned)
• pv lint --gate shapes: grade an external data graph (A-box) not built by pv extract #5892 — pv lint --gate shapes: grade an external data graph (A-box) not built by pv extract (closed: not planned)
• CUDA e2e for PP-LLAMA-001 row 8: .apr Q4K GPU serve enters the pool-allocator path under --features cuda #5831 — CUDA e2e for PP-LLAMA-001 row 8: .apr Q4K GPU serve enters the pool-allocator path under --features cuda (closed: not planned)