Formal-verification map — the invariant–model–proof correspondence

Navigation: ↑ Persistence architecture · Durability & recovery · Concurrency model · Formal-verification tree

The durability and concurrency claims made throughout this corpus are not asserted — they are machine-checked. This page is the correspondence index: for each persistence invariant, it names the TLA⁺ model that model-checks it and the Rocq proof that establishes it, and links the doc that relies on it. It does not restate the proofs; the authoritative source is formal-verification/ and its VERIFICATION_RESULTS.md.

The two-pronged strategy

Verification divides the obligation space cleanly between two tools, tied to the running Rust by an executable correspondence harness:

The map is drawn as two companion figures — one per prong — so each fits the prose column; both prongs tie to the same implementation-under-test and correspondence harness.

Prong	Tool	Establishes	Scope
① Model checking	TLA⁺ / TLC	temporal safety + liveness under concurrency and crashes	bounded instances, all interleavings
② Theorem proving	Rocq / Coq	functional correctness + abstract-data-type (ADT) refinement	all inputs, machine-checked Qed.

Aggregate: 72 Rocq .v files, 1,348 propositions (1,027 Theorem + 313 Lemma + 8 Corollary), 0 Admitted / 0 Axiom / 0 Parameter; 57 TLA⁺ modules, 69 .cfg TLC configs, all SANY-clean (SANY = the TLA⁺ syntactic analyzer). Many models ship a paired _Unsafe.cfg negative control that must violate the named invariant, proving the checker has teeth. The correspondence harness gives every TLC invocation a distinct on-disk state directory. A negative control succeeds only when TLC returns status 12 and the diagnostic names the required invariant (or, for the liveness control, status 13 and a temporal-property violation). Parser failures, resource failures, timeouts, and state-directory collisions therefore fail the gate instead of masquerading as successful negative controls.

Correspondence by concern

Lock-free overlay (CAS, values, removal)

Invariant	TLA⁺ model	Rocq proof	Doc
Root-CAS linearizability (duplicate-insert, insert-vs-contains)	LockFreeARTrieLinearizability.tla	Spec/ARTrieSpec.v, Proofs/MapRefinement.v	lock-free-overlay
Indexed-overlay counter accumulation + vocab index uniqueness	LockFreeIndexedOverlay.tla	Spec/LockFreeCounterMergeSpec.v	lock-free-overlay
Arbitrary-V value-CAS + remove-CAS correctness	LockFreeOverlayValueCas.tla, LockFreeOverlayRemoveCas.tla (+ _Unsafe)	Spec/ARTrieSpec.v	lock-free-overlay
Counter-merge no-lost-update, order-independent	LockFreeCounterMergeAtomicity.tla	Spec/LockFreeCounterMergeSpec.v	lock-free-overlay

Durability, watermark & checkpoint

Invariant	TLA⁺ model	Rocq proof	Doc
acknowledged $\implies$ durable; checkpoint_lsn = committed prefix; no truncation loss	LockFreeDurableCheckpoint.tla (+ _Unsafe), SharedPersistentConcurrency.tla	Spec/PublicDurabilityPolicySpec.v, Spec/PersistentWalAtomicitySpec.v	durability-and-recovery
Checkpoint snapshot $\subseteq$ visible; publication serialized by CK	ConcurrentCheckpointPublication.tla, ConcurrentCheckpointSerialization.tla (+ _Unsafe NoTornDescriptor)	Spec/PersistentCheckpointRetentionSpec.v, Spec/PersistentDirtyCheckpointSpec.v	durability-and-recovery
Durable checkpoint under eviction	LockFreeDurableCheckpointEviction.tla (+ _Unsafe)	Spec/PersistentDirtyCheckpointSpec.v	durability-and-recovery

Recovery & crash-safety

Invariant	TLA⁺ model	Rocq proof	Doc
Reopen replay reproduces exactly the visible state; drop uncommitted	LockFreeOverlayDurableReplay.tla (+ _Unsafe), CrashRecovery.tla	Spec/PersistentRecoveryPlannerSpec.v, Spec/PersistentRecoveryReplayCompletenessSpec.v	durability-and-recovery
Epoch accounting + recovery	EpochCheckpoint.tla, EpochCheckpointRecovery.tla	Spec/PersistentWalSegmentLifecycleSpec.v	durability-and-recovery
End-to-end refinement across checkpoint/compaction/crash/vocab	—	Spec/PersistentEndToEndTraceSpec.v	durability-and-recovery

Concurrency & the F4 lock hierarchy

Invariant	TLA⁺ model	Rocq / test	Doc
Shared-handle linearizability (byte + char + vocab), reads observe completed visible state	SharedPersistentConcurrency.tla, ConcurrentVocabLinearizability.tla	Spec/SharedPersistentConcurrencySpec.v	concurrency-model
F4 deadlock-freedom (CK > merge_lock > EC, drop-before-join)	—	tests/persistent_lockfree_f4_lock_hierarchy_loom.rs, tests/vocab_lockfree_f4_lock_hierarchy_loom.rs	concurrency-model

Eviction & epoch reclamation

Invariant	TLA⁺ model	Rocq proof	Doc
Eviction-CAS overwrite-race + stale-image safety (serial_disk_ptr stamp)	OverlayEvictionCas.tla, OverlayEvictionStale.tla (+ _Unsafe each)	—	eviction, concurrency-model
Eviction-walk epoch reclamation + registry publish	EvictionWalkEBR.tla, EvictionRegistryPublication.tla	Spec/PersistentCharEpochReclamationSpec.v	eviction
Version-GC reader-guard reclaim safety	VersionLifecycle.tla	—	concurrency-model

WAL, storage & group commit

Invariant	TLA⁺ model	Rocq proof	Doc
WAL-before-mutation ordering, fail-closed on WAL error	WAL.tla, WAL_FileSystem.tla	Spec/PersistentWalAtomicitySpec.v, Spec/PersistentVocabWalAtomicitySpec.v	wal-format
Fail-closed write/sync durability boundary	StorageSyscallOutcome.tla	—	durability-and-recovery
Backend contracts (mmap block storage, io_uring SQE/CQE + fixed-buffer ownership)	MmapBlockStorage.tla, IoUringSqeCqeLifecycle.tla, IoUringFixedBufferOwnership.tla	—	storage-backends
Buffer-page lease exclusion; raw-child-pointer ownership	BufferPageLease.tla, PointerOwnership.tla	—	storage-backends
Group-commit frontier: no early ack; ordered FIFO / returned-LSN	DurabilityFrontier.tla, AsyncWalGroupCommit.tla	—	group-commit
Vocab reopen bijection ownership	VocabPersistenceOwnership.tla	Spec/PersistentVocabCheckpointSpec.v	families

ABI resource layer (vt.dictionary.v1 producer)

The language-binding boundary joined the correspondence program in wave W2 of the family ABI plan. Its registry is formal-verification/ABI_INVARIANTS.tsv (checked by scripts/check-abi-invariants.py inside this gate), and its artifacts follow the same spec ↔ test convention as every concern above:

Model	Checks	Executable mirror
formal-verification/tla+/AbiProducerSnapshot.tla (+_Unsafe.cfg negative control)	immutable-capture law, fresh-capture visibility, content-preserving maintenance publishes [LDICT-SNAP-1..3]	tests/ffi_snapshot_law.rs, tests/ffi_crud_model_correspondence.rs, torn-capture regression in tests/ffi_concurrent_snapshot_stress.rs
formal-verification/rocq/Spec/AbiTraversalSnapshotSpec.v	ABI-local node-id arena laws: stable, append-only, unambiguous, write-once memoization, well-formedness preservation [LDICT-ARENA-1..5]	src/bindings.rs node-id unit tests
formal-verification/rocq/Spec/AbiPagingProducerSpec.v	paging bounds, out_total stability, lossless page decomposition [LDICT-PAGE-1..2]	tests/ffi_resource_paging_proptest.rs
formal-verification/rocq/Spec/AbiStatusMappingSpec.v	status-table bijections and the deliberate project/interop divergence (raw-integer reuse provably misroutes) [LDICT-STAT-1..2]	tests/ffi_status_matrix.rs

Lifecycle (retain/release) is deliberately NOT re-modeled here: the protocol is owned by the interop lifecycle model in the liblevenshtein-rust repo (docs/verification/tla/AbiResourceLifecycle.tla, invariants VT-LIFE-1..6); this repo realizes it and pins the realization with the abi-owned-resource-release-once unsafe-contract row plus the balance and cross-thread teardown tests [LDICT-LIFE-1..2].

The negative-control methodology

A model that only checks the safe configuration proves nothing if its invariant is vacuous. Most durability/eviction models therefore ship an _Unsafe.cfg that deliberately breaks the mechanism (e.g. a frontier-bounded reclaim instead of the watermark, or eviction without the stamp) and asserts the checker finds the violation. The pair "safe cfg passes $\land$ _Unsafe cfg fails" is what makes the safe result meaningful — a falsifiable experiment in the scientific sense.

The CI correspondence gate

The two prongs are tied to the running code by scripts/verify-formal-correspondence.sh: it runs the Rust trace-correspondence tests (the code's observable trace matches the spec), the Rocq make (asserting 0 Admitted/Axiom/Parameter), TLA⁺ SANY parsing (and, under RUN_TLC, model checking), and the unsafe-inventory gate (every unsafe block in src/ must be reconciled row-for-row against formal-verification/UNSAFE_INVENTORY.tsv

• UNSAFE_CONTRACTS.tsv, by set-equality). A drifted proof, a new unreconciled unsafe, or a stale count fails CI.

Running it locally

# Rocq proofs (resource-limited, per CLAUDE.md guidance):
systemd-run --user --scope -p MemoryMax=32G -p CPUQuota=1800% \
  make -C formal-verification/rocq -j1

# TLA+ model checking (bounded):
RUN_TLC=1 scripts/verify-formal-correspondence.sh

See also

• formal-verification/README.md — the properties table and theorem list.
• formal-verification/VERIFICATION_RESULTS.md — the full model-checking + proof results and the spec $\leftrightarrow$ Rust correspondence tables.
• formal-verification/GAP_LEDGER.md — the tracked verification gaps and footguns (e.g. the #41 watermark hazard).