capctl-iris

That a capability meter never exceeds its cap over every concurrent interleaving of charge operations, in Iris concurrent separation logic, for any cap and any finite operation list.

It is terminal-observation safety, the value the driver reads is within the cap, not an all-intermediate-state invariant, and carries no liveness or wait-freedom. Floor E shows per-key safety does not certify a tighter cross-key aggregate bound. There is no machine-checked link to the TLA+ model or the Lean parent.

The concurrent driver forks one compare-and-swap charge thread per element onto a single shared cell; safety is stated as adequacy, which quantifies over every reachable configuration, that is, every thread schedule.

The headline theorem conc_meter_never_exceeds_cap closes with Qed; the assumptions audit reports 29 theorems each closed under the global context at the released version v0.1.3 (40 at the current untagged head); a live search finds no admitted goals. The kernel was not re-run in the evidence pass, so axiom-freedom rests on the committed audit.

The Rocq kernel (rocq-core 9.2.0). The 29 audited theorems of the released version are each closed under the global context: no user axioms and no foundational axioms, which is stronger than 'no added axioms'. The proofs are stated over a few Iris and heap_lang definitions, the operational semantics and the adequacy bridge, which are kernel-checked, not axiomatic.

Iris concurrent separation logic and its adequacy theorem; capability and authority bounds. The contribution is the concurrent meter bound and the audited axiom-free trusted base.

eval $(opam env --switch=capctl-iris) && make verify

Findings drawn from this artifact are on the evidence ledger.