An Iris invariant invN P says that P holds, of resources no one owns, between every two steps of the program. It is persistent, so every thread may know it; a thread opens it for one atomic step, takes P out under a laterlater modality IrisIris's propositions hold or fail at each step index, a budget of program steps still to run, and ▷ P ("later P") holds at n + 1 when P holds at n. Stored propositions, in invariants or ghost state, come back only under a ▷, and each program step lets a proof remove one. Löb induction, (▷ P → P) ⊢ P, proves P while assuming it one step later; loops, recursion and the weakest precondition itself are proved or defined that way., and puts P back before the step ends. Masks record which invariants are open, so none opens twice at once. Since Iris 3 it is defined in the logic from ghost stateghost state IrisGhost state exists only in the proof. own γ a owns the piece a of the ghost location γ, where a belongs to a camera; it is allocated and changed by updates, never by the program. It records what the program's memory does not: shares, histories, a protocol's phase, or a whole map that the state interpretation ties to the real heap. and fancy updatesupdate modality IrisAn update modality says a proposition holds after a change the proof makes on its own, with no program step. The basic update |==> P changes ghost state by frame-preserving updates and allocates new ghost locations. The fancy update |={E1,E2}=> P may also open and close invariants, from the mask E1 of closed invariants to E2; P ={E}=∗ Q is P -∗ |={E}=> Q..

• It is not the global invariant of never_panics_by_invariant, which is one Rocq predicate on whole configurations that the proof must reestablish at every step. An Iris invariant is a resource that names only what is shared.

• nanofil's planned logic does not need one yet: its model has one thread, and the runtimeruntime Fil-CThe runtime is what Fil-C does around one thread's program, natively libpizlo.so with FUGC: where a new object goes, what free does, and what the collector may change while the program waits at a safepoint. The model does not define it; it states it as one page of axioms, Module Type Runtime (Runtime), each with a native test in tests/c/prog/axiom-*.c. at a safepoint is a premise, not a party sharing an invariant.

See How Iris works, Invariants.