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.

Symbol	Unicode	Name	Meaning
*	—	Separating conjunction	Disjoint
-*	—	Magic wand	Separating implication
▷	U+25B7	Later	Step-indexed later
□	U+25A1	Persistent	Duplicable
\|={}=>	—	Fancy update	Resource update
WP	—	Weakest precondition	Program spec
Own	—	Ownership	Ghost resource
{P}^N	—	Invariant	Named invariant

Metatheory. Sound for concurrent operational semantics. Adequacy: WP implies actual behavior. Higher-order: full impredicativity. Expressive: encodes many logics. Mechanized in Coq. Extensible via custom RAs.

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

Limitations. Steep learning curve. Coq mechanization overhead. Ghost state design is an art. Step-indexing unfamiliar. Specifications can be complex. Proof effort still substantial.