docs: clarify verification scope and evidence

README.md

@@ -13,10 +13,9 @@ This is not an execution engine and connects to no broker. It is the
 correctness core such an engine would sit on.
 
 A companion C++20 project, [execution-journal](https://github.com/ddehanne/execution-journal),
-carries the same contract into live-execution engineering — durable
-journaling with an fsync dispatch-eligibility barrier, broker
-reconciliation, real-process fault injection, IBKR TWS API adapter
-exercised against a live paper gateway.
+explores related execution-integrity mechanisms in C++20, including
+durable journaling, dispatch eligibility, reconciliation and fault
+injection. Its verification scope is documented separately.
 
 ## Design laws
 
@@ -67,16 +66,18 @@ its torn-tail repair is deliberately not exposed by this CLI.
 
 | Level | Tool | Claim | Reproduce |
 |---|---|---|---|
-| 1 | `cargo test` | 32 example tests | `cargo test --workspace` |
+| 1 | `cargo test` | 33 example tests | `cargo test --workspace` |
 | 2 | proptest | 3 properties on arbitrary journals | same |
 | 3 | Miri | zero UB on all exercised paths | `cargo +nightly miri test -p ledger-core --lib` |
 | 4 | libFuzzer+ASAN | 17.4M runs, 0 crashes on `parse_journal_bytes` | `cargo +nightly fuzz run fuzz_target_1 -- -max_total_time=120` |
 | 5 | Kani (CBMC) | 3 bounded proofs, exhaustive in-domain | `cargo kani -p ledger-core` |
 
 Kani proofs: money arithmetic total & exact over **all** `i64` pairs
 (`i128` oracle); sequence successor law over **all** `u64`; transition
-table over the **full** state×event product — never panics,
-no-mutation-on-error.
+table across all nine modeled states and six event variants, with
+bounded symbolic quantities. The harness checks transition behavior
+within those bounds; it is not a proof over unrestricted quantities
+or of mutation behavior outside the pure transition interface.
 
 Details: [`docs/VERIFICATION.md`](docs/VERIFICATION.md).
 

docs/VERIFICATION.md

@@ -1,7 +1,7 @@
 # Verification Evidence
 
 ## Level 1 — Example tests
-32 unit/integration tests across the workspace (see crates' test files).
+33 unit/integration tests across the workspace (see crates' test files).
 
 ## Level 2 — Property tests (proptest)
 3 properties on arbitrary event journals (256 cases each per run):
@@ -20,10 +20,15 @@ Contract: arbitrary bytes never panic (Ok with recovery, or typed error).
 Result: 17,461,635 runs in 121s, zero crashes, zero leaks.
 
 ## Level 5 — Bounded model checking (Kani v0.67 / CBMC)
-Three proofs in `ledger-core/src/kani_proofs.rs` — symbolic, exhaustive
+Three proofs in `crates/ledger-core/src/kani_proofs.rs` — symbolic, exhaustive
 within stated domains:
 - P1 `checked_add` total & exact over ALL i64 pairs (checked vs i128)
 - P2 sequence successor law characterized over ALL u64
-- P3 transition table: full state×event product — never panics,
-  no-mutation-on-error proven exhaustively (INV-17)
+- P3 transition table: all nine modeled states and six event variants,
+  with symbolic quantities restricted by harness assumptions.
+  The harness checks its assertions exhaustively within these bounds;
+  it does not establish unrestricted quantity coverage. Because the
+  transition interface borrows the input immutably, its equality check
+  on error is not an independent proof of mutation safety throughout
+  the authoritative reducer (INV-17).
 Result: `Complete - 3 successfully verified harnesses, 0 failures.`