fold(B3): contracts / ONT / PVL / docs onto main — replaces #4317

.gitattributes

@@ -23,3 +23,8 @@
 #
 # scripts/check_append_only_ledgers.sh holds that distinction as a case table.
 docs/audits/*.jsonl merge=union
+# Append-only ledgers one level down. `docs/audits/*.jsonl` does not cross a `/`,
+# so these two resolved no merge driver (check_append_only_ledgers, after the
+# main merge into #4431). Named file by file: the scope rule above still holds.
+docs/audits/review-corpus/corpus-v1.jsonl merge=union
+docs/audits/rex-001/rex-04-admission.jsonl merge=union

.github/workflows/conleche-nightly.yml

@@ -0,0 +1,79 @@
+# conleche-nightly.yml -- PVL-F7 (#3142): an independent kernel re-checks the Lean tree once a day. ADVISORY.
+#
+# Every other verdict on crates/aprender-contracts-staging/lean comes from Lean's own C++ kernel (lake build,
+# leanchecker via `pv discharge check`). con-leche is a second checker that shares no code with it or with pv,
+# and it rejects every axiom beyond propext / Classical.choice / Quot.sound -- so it also re-proves that the
+# escape allowlist is empty (#4347). The whole procedure, its pins and its controls live in conleche.sh; this
+# file only provisions elan and runs it.
+#
+# ADVISORY. Nothing requires this job; a red run blocks no PR and no release. It is a finding to file, not a
+# gate: exit 1 = RED (a rejected declaration or an escape axiom), exit 2 = NOT A VERDICT (unsupported feature,
+# OOM, unpinned toolchain, or a control that failed). Both turn the run red, with an annotation naming which --
+# "not a verdict" is never shown green.
+#
+# Measured on lambda 2026-09-25 at 9018366cf (warm pins): controls ok, 402163 declarations accepted, 7:11 wall,
+# 5.7 GB max RSS. Cold adds the con-leche build (395 s) and two toolchain downloads.
+#
+# RUNNER. [self-hosted, Linux, X64, clean-room] -- the sovereign-ci pool, never a hosted runner (operator rule,
+# 2026-09-10). elan is not part of the pool image, so the job installs a PINNED, sha256-checked elan into its
+# own directory and touches nothing else on the host. Toolchains, pins and the Mathlib cache persist there
+# between runs; the concurrency group keeps two runs from sharing them at once.
+name: conleche-nightly
+
+on:
+  schedule:
+    # 21:23 UTC -> lands ~02:23 UTC. GitHub dispatches schedules ~5h late on this account (#3292); the slot is
+    # free and clear of guards-nightly (21:47) and cuda-nightly (20:30).
+    - cron: '23 21 * * *'
+  workflow_dispatch:
+
+concurrency:
+  group: conleche-nightly
+  cancel-in-progress: false
+
+permissions:
+  contents: read
+
+jobs:
+  conleche:
+    runs-on: [self-hosted, Linux, X64, clean-room]
+    # 90: BSE-05 T = max(15, ceil(1.5*p99), p99+20) with p99 taken as a cold ~45 min (no history yet: con-leche
+    # build 6.6 min, toolchains + Mathlib cache, a from-scratch ProvableContracts build, export 4 min, check
+    # 2.6 min) -> T = max(15, 68, 65) = 68, rounded up for a shared host. The first three runs replace this basis.
+    timeout-minutes: 90
+    env:
+      CI_CACHE: /mnt/nvme-raid0/ci-cache/pvl-conleche
+      ELAN_VERSION: v4.2.4
+      ELAN_SHA256: 42b94d4244e8353142c456ec0e4ca6528fd898a6c604d4059f494e706e431f63
+      LEAN_NUM_THREADS: '8'
+    steps:
+      - uses: actions/checkout@v7
+        with:
+          fetch-depth: 1
+      - name: Verdict case table (the classifier this job trusts)
+        run: bash crates/aprender-contracts-staging/lean/conleche.sh --self-test
+      - name: Pinned elan in the job's own directory (sha256-checked, never a host install)
+        run: |
+          set -euo pipefail
+          export ELAN_HOME="$CI_CACHE/elan"
+          mkdir -p "$CI_CACHE"
+          if [ ! -x "$ELAN_HOME/bin/elan" ] || ! "$ELAN_HOME/bin/elan" --version | grep -q "${ELAN_VERSION#v}"; then
+            tgz="$RUNNER_TEMP/elan.tgz"
+            curl -fsSL -o "$tgz" "https://github.com/leanprover/elan/releases/download/$ELAN_VERSION/elan-x86_64-unknown-linux-gnu.tar.gz"
+            echo "$ELAN_SHA256  $tgz" | sha256sum -c -
+            tar xzf "$tgz" -C "$RUNNER_TEMP"
+            "$RUNNER_TEMP/elan-init" -y --no-modify-path --default-toolchain none
+          fi
+          echo "ELAN_HOME=$ELAN_HOME" >> "$GITHUB_ENV"
+          echo "$ELAN_HOME/bin" >> "$GITHUB_PATH"
+      - name: con-leche re-check (advisory)
+        run: |
+          set -uo pipefail
+          rc=0
+          PVL_CONLECHE_CACHE="$CI_CACHE/pins" bash crates/aprender-contracts-staging/lean/conleche.sh || rc=$?
+          case "$rc" in
+            0) ;;
+            1) echo "::error title=con-leche RED::a declaration was rejected or an escape axiom is present -- file it against #3142" ;;
+            *) echo "::warning title=con-leche NOT A VERDICT::exit $rc -- the tree was not checked (see the log above); not a pass" ;;
+          esac
+          exit "$rc"

.gitignore

@@ -131,3 +131,7 @@ docs/roadmaps/*.lock
 # The VERDICT artifact (quorum-*.json) is committed; its .lanes/ working
 # directory is transient and a lane review correctly refused a PR carrying it.
 docs/audits/quorum-*.json.lanes/
+
+# PVL-001 EV-8a (#4202): `pv discharge run`'s full log. The tracked summary is its sibling
+# crates/aprender-contracts-staging/discharge-summary.json, outside the tree it hashes.
+crates/aprender-contracts-staging/lean/discharge.json

Cargo.toml

@@ -79,6 +79,8 @@ members = [
     "crates/aprender-zram-adaptive",
     "crates/aprender-zram-cli",
     "crates/aprender-zram-generator",
+    # --- REX-001 (#4354): review-lane experiment harness + frozen analysis ---
+    "crates/aprender-review-experiment",
     # --- APR-MONO Phase 3b: presentar sub-crates (enabled) ---
     "crates/aprender-present-core",
     "crates/aprender-present-terminal",

Makefile

@@ -577,6 +577,7 @@ readme-sync-check: ## Fail if README.md is not what the generator produces
 # merge-tree measurement READS A FILE ON DISK must turn the hand-edited rows
 # GREEN, which is what makes their RED load-bearing rather than incidental.
 # `--class complexity` and `--class satd` are stubs and exit 3, never 0.
+.PHONY: oracle-owl oracle-owl-check
 .PHONY: roadmap-aggregate roadmap-aggregate-check
 roadmap-aggregate: ## Regenerate docs/roadmaps/roadmap.yaml from docs/roadmaps/entries/ (#3296)
 	@python3 scripts/lib/roadmap_fragments.py aggregate --write
@@ -594,6 +595,12 @@ ratchet-semantics-test: ## BSE-03: D2 ratchet polarity rows (--class readme)
 # enforces COV_FLOOR, so this is a name, not a new policy.
 coverage-check: coverage
 
+# PVL-001 EV-6a (#4139): the ONLY writer of the Lean label ratchet. `pv discharge check` never writes
+# unresolved-labels.json; this rewrites it DOWNWARD (a label that resolves now leaves; a new one is never added).
+.PHONY: label-ratchet
+label-ratchet:
+	@. scripts/pv_bin.sh && "$$PV" discharge label-ratchet crates/aprender-contracts-staging/lean --contracts contracts
+
 # Ditto for `contracts`. The provable-contract tier is a HARD release gate per
 # CLAUDE.md, and the dogfood protocol looked for a target that did not exist, so
 # it WARNed instead of checking. `pv lint` runs validate + audit + score across
@@ -612,7 +619,10 @@ contracts:
 	@. scripts/pv_bin.sh && "$$PV" census contracts --format json > contracts/census.json
 	@git diff --exit-code contracts/census.json || { echo "FAIL: the tracked census differs from a fresh one — commit the regenerated contracts/census.json"; exit 1; }
 	@echo "== graph: tracked contracts/contracts.nt + shapes.ttl == a fresh extraction (ONT-001 ONT-4b, R-18) =="
-	@. scripts/pv_bin.sh && "$$PV" extract contracts --check >/dev/null
+	@. scripts/pv_bin.sh && "$$PV" extract contracts --check >/dev/null || exit 1
+	@echo "== consistency: pv-sat writes the witness, pv lint re-checks it (ONT-001 ONT-5, R-1); refines is Liskov (ONT-4e, R-20); bindings resolve (ONT-3a) =="
+	@. scripts/pv_bin.sh && { [ -x "$$PV_SAT" ] || { echo "FAIL: no pv-sat beside $$PV -- a PV_BIN override must ship its pv-sat too"; exit 1; }; } && "$$PV_SAT" contracts && "$$PV" lint contracts/ --gate ont-consistency >/dev/null && "$$PV" lint contracts/ --gate refines >/dev/null && "$$PV" lint contracts/ --gate bindings >/dev/null || exit 1
+	@test -z "$$(git status --porcelain -- contracts/witness)" || { git status --short -- contracts/witness; echo "FAIL: contracts/witness/ differs from what pv-sat writes -- commit it"; exit 1; }
 	@echo "== README states the censused count =="
 	@bash scripts/readme_sync.sh --check
 	@echo "== provenance marks, interim (ONT-001 R-10) =="
@@ -1398,6 +1408,16 @@ ont-ratchet:
 ont-ratchet-check:
 	@bash scripts/check_ont_ratchet.sh --check
 
+# PVL-001 EV-11 (PMAT-4166): the two `pv lint` ratchets (theorem-pairing, depends-on-present) move ONLY
+# through this target, and only DOWN. The gates read contracts/lint-baseline.json and never write it.
+# NEVER in CI: a CI job that could rewrite the baseline is a ratchet that turns both ways.
+.PHONY: lint-ratchet lint-ratchet-self-test
+lint-ratchet:
+	@bash scripts/lint_ratchet.sh
+
+lint-ratchet-self-test:
+	@bash scripts/lint_ratchet.sh --self-test
+
 # ONT-001 §5 ONT-4b2 / R-13 — the out-of-gate SHACL differential oracle.
 #
 # NOT a PR check, by the rule that puts it here: `shacl` is 316 crates and pinned at ONE version (ONT-0's
@@ -1417,3 +1437,22 @@ oracle:
 oracle-check: oracle
 	@git diff --exit-code tests/oracle/differential.json \
 	  || { echo "FAIL: tests/oracle/differential.json differs from a fresh run — commit it"; exit 1; }
+
+# ONT-001 §3.8 / ONT-2c — the OWL oracle (release gate only, R-13; never per PR). Three arms:
+# horned-owl re-parses the fixture's written .ofn and must equal the HAND-WRITTEN axiom list; every live
+# axiom must be a told-closure-admitted kind; ELK 0.4.3 (pinned by sha256, needs a JVM) must agree with
+# contracts/tbox-report.json, with a planted positive control turning it RED every run. No JVM exits 2 with
+# `decline: NOT MEASURED`, which is RED at the release gate and never a skip. The crate is detached from the
+# workspace AND from tests/oracle's SHACL crate (feature unification breaks horned-owl there).
+oracle-owl:
+	@echo "== OWL oracle: horned-owl round-trip + admitted kinds + ELK TBox differential (out of gate) =="
+	@. scripts/pv_bin.sh && "$$PV" ontology export --owl tests/fixtures/ont/owl/ontology.yaml > "$${TMPDIR:-/tmp}/ont2c-fixture.ofn"
+	@cargo build --release --quiet --manifest-path tests/oracle/owl/Cargo.toml
+	@O="$$(cargo metadata --no-deps --format-version 1 --manifest-path tests/oracle/owl/Cargo.toml | sed -n 's/.*"target_directory":"\([^"]*\)".*/\1/p')/release/owl-oracle"; \
+	"$$O" roundtrip "$${TMPDIR:-/tmp}/ont2c-fixture.ofn" tests/fixtures/ont/owl/axioms.txt && \
+	"$$O" kinds contracts/ontology.ofn && \
+	"$$O" elk .
+
+oracle-owl-check: oracle-owl
+	@git diff --exit-code tests/oracle/tbox-differential.json \
+	  || { echo "FAIL: tests/oracle/tbox-differential.json differs from a fresh run — commit it"; exit 1; }

README.md

@@ -41,7 +41,7 @@ publishing — all backed by YAML provable contracts that fail CI on drift.
 | Metric | Count | Source of truth |
 |-------:|------:|---|
 | Workspace crates | **79** workspace crates | `cargo metadata --no-deps` (NOT `ls crates/` — 4 are `exclude`d, 1 has no Cargo.toml) |
-| Provable contracts | **<!-- CONTRACT_COUNT_START -->1837<!-- CONTRACT_COUNT_END -->** provable contracts | `contracts/census.json` `.n_files` — the set `pv lint` walks (`pv census`, ONT-001 ONT-1; regenerated by `make contracts`, written by `make readme-sync`, guarded by `scripts/check_readme_claims.sh`) |
+| Provable contracts | **<!-- CONTRACT_COUNT_START -->1851<!-- CONTRACT_COUNT_END -->** provable contracts | `contracts/census.json` `.n_files` — the set `pv lint` walks (`pv census`, ONT-001 ONT-1; regenerated by `make contracts`, written by `make readme-sync`, guarded by `scripts/check_readme_claims.sh`) |
 | CLI commands | **111** CLI commands | `contracts/apr-cli-commands-v1.yaml` §`commands` (parse the list; `apr --help` prints 112 because it lists `help` itself, and `grep -c '^  - name:'` gives 117 — other same-indent `name:` keys exist in the file) |
 | Book CLI chapters | **113** chapters | `ls book/src/cli/*.md` |
 | Book lib chapters | **72** chapters | `ls book/src/lib/*.md` (parity with `pub mod`) |
@@ -321,7 +321,7 @@ falsification_tests:
   prediction: apr validate bad-model.apr exits non-zero
 ```
 
-The tree carries <!-- CONTRACT_COUNT_START -->1837<!-- CONTRACT_COUNT_END --> contracts across inference, training, quantization, attention, FFN,
+The tree carries <!-- CONTRACT_COUNT_START -->1851<!-- CONTRACT_COUNT_END --> contracts across inference, training, quantization, attention, FFN,
 tokenization, model formats, CLI safety — and this README itself.
 
 ## Migration from old crates

ci/explicit-test-commands.d/456-aprender-contracts-cli-ev11-lint-ratchets.cmd

@@ -0,0 +1 @@
+cargo test -p aprender-contracts-cli --test ev11_lint_ratchets

ci/explicit-test-commands.d/457-aprender-contracts-cli-ont8-evidence-gate.cmd

@@ -0,0 +1 @@
+cargo test -p aprender-contracts-cli --test ont8_evidence_gate

ci/explicit-test-commands.d/461-aprender-contracts-cli-pvl-discharge-check.cmd

@@ -0,0 +1 @@
+cargo test -p aprender-contracts-cli --test pvl_discharge_check

ci/explicit-test-commands.d/462-aprender-contracts-cli-pvl-obligations-golden.cmd

@@ -0,0 +1 @@
+cargo test -p aprender-contracts-cli --test pvl_obligations_golden

ci/explicit-test-commands.d/463-aprender-contracts-cli-ont2c-owl-tbox.cmd

@@ -0,0 +1 @@
+cargo test -p aprender-contracts-cli --test ont2c_owl_tbox

ci/explicit-test-commands.d/471-aprender-contracts-cli-pvl-discharge-leanchecker.cmd

@@ -0,0 +1 @@
+cargo test -p aprender-contracts-cli --test pvl_discharge_leanchecker

ci/explicit-test-commands.d/472-aprender-contracts-cli-ont4d-subsumption.cmd

@@ -0,0 +1 @@
+cargo test -p aprender-contracts-cli --test ont4d_subsumption

ci/explicit-test-commands.d/480-aprender-contracts-cli-pvl-challenge.cmd

@@ -0,0 +1 @@
+cargo test -p aprender-contracts-cli --test pvl_challenge

ci/explicit-test-commands.d/481-aprender-contracts-cli-pvl-comparator.cmd

@@ -0,0 +1 @@
+cargo test -p aprender-contracts-cli --test pvl_comparator

ci/explicit-test-commands.d/490-aprender-contracts-cli-pvl-ghost-binding.cmd

@@ -0,0 +1,3 @@
+# PVL-001 EV-2 (#4080): pv proof-status --binding resolves bindings; a ghost binding is a reject.
+# Reads tests/fixtures/pvl/ and contracts/ from the workspace root (the resolver is CWD-sensitive).
+cargo test -p aprender-contracts-cli --test pvl_ghost_binding

ci/explicit-test-commands.d/510-aprender-contracts-cli-ont5-consistency-gate.cmd

@@ -0,0 +1 @@
+cargo test -p aprender-contracts-cli --test ont5_consistency_gate

ci/explicit-test-commands.d/520-aprender-contracts-cli-pv-sat-bin.cmd

@@ -0,0 +1 @@
+cargo test -p aprender-contracts-cli --bin pv-sat

ci/explicit-test-commands.d/575-aprender-contracts-cli-ont9-self-contract.cmd

@@ -0,0 +1 @@
+cargo test -p aprender-contracts-cli --test ont9_self_contract

ci/explicit-test-commands.d/580-aprender-contracts-cli-ont4f-github-entities.cmd

@@ -0,0 +1 @@
+cargo test -p aprender-contracts-cli --test ont4f_github_entities

ci/explicit-test-commands.d/600-aprender-contracts-cli-ont4e-refines-gate.cmd

@@ -0,0 +1 @@
+cargo test -p aprender-contracts-cli --test ont4e_refines_gate

contracts/alibi-slopes-v1.yaml

@@ -55,7 +55,7 @@ proof_obligations:
     mathlib_imports:
     - Mathlib.Analysis.SpecialFunctions.Pow.Real
     notes: 'Exponent -8(h+1)/n < 0 for h >= 0, n > 0; base 2 > 1 so 2^(neg) < 1.
-      Companion alibi_slope_pos proves 0 < m[h] (strictly positive geometric sequence).'
+      Companion alibi_slope_real_pos proves 0 < m[h] (strictly positive geometric sequence).'
 - id: AS-EQ-003
   type: equivalence
   property: Matches ggml reference exponent
@@ -89,15 +89,15 @@ verification_summary:
     theorem: Alibi.alibi_slope_lt_one
     file: ProvableContracts/Theorems/Alibi/Slopes.lean
     note: 'exponent -8(h+1)/n < 0 for h>=0, n>0, and base 2>1, so 2^(neg) < 1
-      (Real.rpow_lt_one_of_one_lt_of_neg). alibi_slope_pos additionally proves 0 < m[h].'
+      (Real.rpow_lt_one_of_one_lt_of_neg). alibi_slope_real_pos additionally proves 0 < m[h].'
   - obligation: Matches ggml reference exponent
     theorem: Alibi.alibi_slope_ggml
     file: ProvableContracts/Theorems/Alibi/Slopes.lean
     note: 'alibiSlope n h = (alibiM0 n)^(h+1) via (x^y)^z = x^(y*z) (Real.rpow_mul),
       matching llama.cpp soft_max_ext.'
   notes: 'All 3 obligations proved sorry-free in Lean 4 over the reals (Mathlib
     Real.rpow). Zero N/A — the contract is fully analytic. Slopes are a positive,
-    strictly-decreasing geometric sequence: alibi_slope_pos (m[h]>0) and
+    strictly-decreasing geometric sequence: alibi_slope_real_pos (m[h]>0) and
     alibi_slope_strict_anti (m[0]>m[1]>...>m[n-1]) additionally proved. Verified via
     lake env lean ProvableContracts/Theorems/Alibi/Slopes.lean (exit 0, 0 sorry).'
 kernel_structure:

contracts/apr-cli-commands-v1.yaml

@@ -786,7 +786,7 @@ commands:
     description: "Provable-contracts CLI (also ships as the standalone pv binary)"
     requires_model: false
     side_effects: [filesystem]
-    subcommands: [audit, book, census, certify, check-parity, codegen, coq, coverage, diff, equations, explain, extract, extract-pytorch, flux, fuzz, generate, graph, infer, invariants, kaizen, kani, lean, lean-status, lint, migrate, mirai, pipeline, probar, proof-status, query, roofline, scaffold, score, status, tla, unlock, validate, verify-bindings, verify-pipeline, verify-structure]
+    subcommands: [audit, book, census, certify, challenge, check-parity, codegen, coq, coverage, diff, discharge, equations, explain, extract, extract-pytorch, flux, fuzz, generate, graph, infer, invariants, kaizen, kani, lean, lean-status, lint, migrate, mirai, obligations, ontology, pipeline, probar, proof-status, query, roofline, scaffold, score, status, tla, unlock, validate, verify-bindings, verify-pipeline, verify-structure]
 
 # ── Falsification Conditions ──
 

contracts/apr-cli-coverage-v1.yaml

@@ -44,7 +44,7 @@ falsification_tests:
   if_fails: "apr-cli coverage below 95%"
 
 verification_summary:
-  total_obligations: 1
+  total_obligations: 0
   proven: 0
   tested: 0
   status: pending

contracts/apr-cli-dep-migration-v1.yaml

@@ -58,7 +58,7 @@ kani_harnesses:
   bound: 4
 
 verification_summary:
-  total_obligations: 2
+  total_obligations: 1
   proven: 0
   tested: 0
   status: pending

contracts/apr-cli-publish-v1.yaml

@@ -88,7 +88,7 @@ kani_harnesses:
   bound: 4
 
 verification_summary:
-  total_obligations: 4
+  total_obligations: 1
   proven: 0
   tested: 0
   status: pending

contracts/apr-cli-qa-v1.yaml

@@ -254,7 +254,7 @@ kani_harnesses:
   bound: 4
 
 verification_summary:
-  total_obligations: 11
+  total_obligations: 5
   proven: 0
   tested: 11
   status: tested

contracts/apr-cli-safety-v1.yaml

@@ -88,8 +88,8 @@ qa_gate:
   - falsification
   pass_criteria: All 5 falsification tests + 4 proof obligations pass
 verification_summary:
-  total_obligations: 4
-  l2_property_tested: 4
+  total_obligations: 1
+  l2_property_tested: 1
   l3_kani_proved: 0
   l4_lean_proved: 0
   l4_sorry_count: 0

contracts/apr-cpu-vs-gpu-output-parity-v1.yaml

@@ -607,7 +607,7 @@ proof_obligations:
   property: "on Blackwell (cc>=120) default apr run --gpu decode throughput for a 1.5B Q4_K_M model is >= 100 tok/s (on-GPU resident path, no silent CPU/wgpu fallback); ~10 tok/s falsifies it as an F2 false-fallback / stale binary (PMAT-885)"
 
 verification_summary:
-  total_obligations: 11
+  total_obligations: 10
   proven: 0
   tested: 1
   status: pending

contracts/apr-docs-v1.yaml

@@ -159,7 +159,7 @@ kani_harnesses:
   bound: 4
 
 verification_summary:
-  total_obligations: 9
+  total_obligations: 3
   proven: 0
   tested: 9
   status: tested

contracts/apr-dogfood-coverage-v1.yaml

@@ -62,6 +62,13 @@ metadata:
     # crates/apr-cli/src/commands_enum.rs. All 64 citations of that file in 55 rows
     # were re-derived: 42 at lines >= 139 shifted by +4, 22 at <= 138 unchanged, and
     # every cited line's text was checked identical between 79a3af79d and the batch.
+    # PARTIAL RE-AUDIT, PVL-001 EV-2 / #4095 (G2.1). Same rule: `measured_commit` does not
+    # move. #4095 rewrites one doc comment in crates/aprender-contracts-cli/src/cli.rs
+    # line-for-line (4 for 4, no shift), but re-deriving the 76 `pv`/`apr pv` rows that
+    # cite it found 54 ALREADY stale on main (+6 from `Coverage` on, +12 from `Lint` on --
+    # variants inserted since 2026-08-22, never re-audited). Every row now cites the line of
+    # its own `Commands::<Variant>` declaration, checked by reading that line back; 22 were
+    # already exact. `pv census` and `pv extract` ship with no row at all -- not added here.
     ledger: docs/audits/surface_audit.csv
 
     overall:
@@ -842,7 +849,7 @@ qa_gate:
   pass_criteria: "F-DOGCOV-{001..016} all PASS; any one FAIL is NO-GO"
 
 verification_summary:
-  total_obligations: 16
+  total_obligations: 9
   proven: 0
   tested: 16
   status: proposed

contracts/apr-pretrain-from-init-v1.yaml

@@ -313,7 +313,7 @@ kani_harnesses:
   bound: 8  # 4 failure modes × 2 mode values
 
 verification_summary:
-  total_obligations: 6
+  total_obligations: 7
   proven: 0
   tested: 0
   status: pending