Artifact
compositional-temporal-safety
A compositional safety invariant holds for all finite N, machine-checked.
What it establishes
That a composed safety invariant, aggregate spend within cap, and mutual exclusion, holds over all reachable states for any finite roster of agents, proved in Lean by composing an isolated per-agent guarantee.
What it does not establish
Only the sound non-circular fragment of assume-guarantee; the full circular Abadi-Lamport form is not claimed. Lean proves safety only, with no liveness, which is a bounded TLA+ property at one configuration. No machine-checked refinement connects the Lean, TLA+ and Python layers; the roster is static; it is not propext-free.
Method
An isolated per-agent guarantee is composed by a step lemma into an invariant over all reachable states; a TLA+ model and a Python differential exercise the bounded state space, with four Lean negative controls.
Results
The Lean theorems build green and the axiom audit reports at most propext and Quot.sound; the TLA+ model checks the invariant over 200 distinct states at one configuration, and a Python differential reaches the same count as a bounded agreement, not a refinement.
What has to be trusted
Lean 4 (v4.32.0), mathlib-free; the axioms propext and Quot.sound, with some theorems using none; and the transition system being a faithful abstraction, argued not machine-proved. The TLA+ side adds TLC and the JVM, bounded.
Prior work
Assume-guarantee reasoning (Abadi-Lamport, Misra-Chandy) and compositional temporal safety. The contribution is the machine-checked non-circular composition with load-bearing negative controls and an honest bounded-agreement account of its cross-checks.