Iris is a higher-order concurrent separation logicconcurrent separation logic IrisConcurrent separation logic carries ownership across threads: threads that own disjoint resources run in parallel without interfering, and a lock guards a resource invariant that the thread taking the lock receives and must restore before releasing it. The decade after it produced a logic per sharing pattern (RGSep, CAP, iCAP, TaDA and more), each with its own soundness proof; Iris reduced them to ghost state and invariants. framework in Rocq. Its propositions describe owned resources, may quantify over propositions, and are shared through invariantsIris invariant IrisAn Iris invariant inv N 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 later, 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 state and fancy updates.; user-defined 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. expresses protocols. A language joins it by giving its step relation, and adequacyadequacy nanofilAdequacy is the one theorem that ties a program logic to the machine: if a program's proof in the logic can be derived, then no state any of its runs reaches fails. It is proved once; after it, proving a program never panics is deriving its proof, with no reasoning about runs. turns a weakest preconditionweakest precondition IrisWP e {{ v, Φ v }} says that running e is safe and that, if it ends in a value v, Φ v holds. Iris defines it once for every language by guarded recursion: unless e is a value, given the state interpretation of any state, e can step (when stuckness is NotStuck), and after every step it can take, one later on, the new state's interpretation and the WP of what e became hold. Hoare triples and specifications are wands into it. proved in the logic into a fact about every run.

• nanofil's machine is an Iris language in the spike IrisLang.v (prim_step, wp_never_panics), built so that a configuration that fails has no step; Iris's adequacy then proves never_panics itself. logic.md recommends Iris for the never_panics campaign.

See How Iris works.