WPe {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 interpretationstate interpretation IrisThe state interpretation is the proposition a language instance ties to the machine's real state. The WP receives it before every step and must give it back for the new state, so it is an invariant of every run; a proof never sees the state itself, only what owning fragments and the interpretation together imply. For heap_lang it is the authoritative ghost heap, which equals the real heap. of any state, e can step (when stuckness is NotStuck), and after every step it can take, one 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. on, the new state's interpretation and the WP of what e became hold. Hoare triplesHoare triple IrisA Hoare triple {P} c {Q} says that if P holds when c starts and c finishes, Q holds when it does. Hoare logic gives one rule per construct: assignment substitutes into the postcondition, sequencing chains triples, a loop needs an invariant each iteration keeps. It is partial correctness: a run that never finishes satisfies every triple. and specifications are wands into it.

• In nanofil's Iris language a configuration that fails cannot step, so a NotStuck WP of the entry call says no reachable configuration fails, and Iris's 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. makes that never_panics. The spike's wpc is the WP with postcondition True, and wp_never_panics is that adequacy.

See How Iris works, Weakest preconditions.