33 unit/integration tests across the workspace (see crates' test files).
3 properties on arbitrary event journals (256 cases each per run): replay determinism (byte-identical), position = sum of distinct applied executions (independent recomputation), prefix+suffix = full replay.
cargo +nightly miri test -p ledger-core --lib → 18 passed
cargo +nightly miri test -p ledger-core --test reducer_invariants → 6 passed
Zero undefined behavior on all exercised paths (unsafe is forbidden
workspace-wide; Miri confirms the interpreter sees none).
Target: parse_journal_bytes(&[u8]) — the disk-facing attack surface.
Contract: arbitrary bytes never panic (Ok with recovery, or typed error).
Result: 17,461,635 runs in 121s, zero crashes, zero leaks.
Three proofs in crates/ledger-core/src/kani_proofs.rs — symbolic, exhaustive
within stated domains:
- P1
checked_addtotal & exact over ALL i64 pairs (checked vs i128) - P2 sequence successor law characterized over ALL u64
- 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.