Projects · Agent control · Research prototype · PROVEN
compositional-temporal-safety
What this 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 this 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.
Trusted base
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.
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.
Result
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.
Negative controls. Four Lean controls: dropping a budget or acquire guard breaks the bound or mutual exclusion; dropping a cross-agent assumption breaks the guarded action.
Reproduce
make check- Toolchain
- Lean 4 leanprover/lean4:v4.32.0 (mathlib-free); TLA+ Tools v1.7.4 / TLC2 2.19; Python 3
- Verified at
- repowazdogz-droid/compositional-temporal-safety@7a812bdb (2026-07-20)
This pass. Re-verified this pass for the Lean layer (lake build and the axiom audit) and the Python differential; the TLA+/TLC model was confirmed by source read at 7a812bdb, not re-run this pass.
Independent reproduction
None known. The Lean build and Python differential were reproduced from a fresh clone during the evidence inventory.
Prior art and positioning
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.