Iris Logic

Origin. Jung, Krebbers, Jourdan, Bizjak, Birkedal, Dreyer developed Iris (2015-present). Higher-order concurrent separation logic in Coq. Unifies many verification techniques. Ghost state, invariants, protocols. State-of-the-art program verification framework.

Models. Modular concurrent verification. Higher-order: quantify over predicates. Impredicative invariants: invariants can mention themselves. Ghost state: logical resources tracking protocol state. Step-indexed: handles recursion and impredicativity.

Formalism.

Resource algebra (RA): Commutative monoid (M, ·, ε) with validity ✓.

• Ghost state: own logical resources
• Frame-preserving updates: change resources consistently

Ownership: Own(a): own resource a. Own(a) * Own(b) ≡ Own(a · b): ownership composition.

Invariants: {P}^N: invariant named N protecting P. Invariant accessible via masks and fancy updates.

Fancy update: |={E₁, E₂}=> P: update from mask E₁ to E₂, yielding P. E: set of enabled invariants.

Weakest precondition: WP e {Φ}: executing e yields value v with Φ(v). Program logic integrated with type system.

Later modality: ▷P: P holds "one step later." Handles recursion: recursive specs unfold under ▷.

Protocols (ghost state): Define state machine via ghost state. Transitions: update ghost state with frame-preserving updates.

Symbols.

Metatheory. The theorem that matters is adequacy: if ⊢ WP e {Φ} is provable with Φ a pure postcondition, then no execution of e in the given operational semantics gets stuck, and every value it returns satisfies Φ — so a purely logical derivation implies a property of the real reduction relation. Jung, Krebbers, Jourdan, Bizjak, Birkedal, and Dreyer ("Iris from the ground up", 2018) reduced the whole framework to a small base logic: ownership of elements of a camera, invariants, and the later modality, with the weakest precondition defined as a guarded fixpoint rather than taken as primitive. Cameras are step-indexed partial commutative monoids, and frame-preserving update is the only sound way to change ghost state, since it must respect every frame another thread might hold. Impredicativity requires the later modality: opening an invariant yields ▷P and not P, which is exactly what blocks the self-reference paradox, and Löb induction — from ▷P ⊢ P conclude ⊢ P — is what makes recursive specifications well-founded. Concurrent separation logic, rely-guarantee, CAP, logical atomicity, and RustBelt's lifetime logic are all derived inside Iris rather than added as axioms, and the entire development is machine-checked in Coq.

Applies to. Rust verification (RustBelt). Concurrent data structures. Language semantics. Lock-free algorithms. Type system soundness. Operating systems (CertiKOS).

Limitations. Iris is an affine separation logic — resources may be discarded, so P * Q ⊢ P holds and the absence of memory leaks is not expressible; what adequacy delivers is safety, not resource exhaustion bounds. Adequacy says nothing about termination or liveness either: a proved program may diverge or deadlock, and total correctness requires added machinery such as time credits. The later modality is what impredicative invariants require, and it appears on every invariant access; an assertion obtained as ▷P can be stripped only by taking a physical reduction step, so reasoning that must conclude P without executing anything is blocked. Step-indexing likewise restricts the model to assertions that are non-expansive in the index. The base logic is higher-order and its entailment is undecidable, so proof search is interactive and no complete automation exists. Soundness is relative to Coq's consistency and to the accuracy of the supplied operational semantics; the memory model is a parameter, and relaxed-memory instantiations are separate developments.

© 2026 Lingenic LLC