17. From checked claims to guarded execution

A certificate establishes a derivation; an action changes a state. Their connection requires a claim interpretation, sound starting observations, and a command bound to the same program and context used by the proof.