diff --git a/doc/execution-semantics.md b/doc/execution-semantics.md
index 735c88a6e08..f22e49dbf91 100644
--- a/doc/execution-semantics.md
+++ b/doc/execution-semantics.md
@@ -1,7 +1,7 @@
 # Execution Semantics
 
 Status: Current implementation guide
-Date: 2026-04-26
+Date: 2026-06-10
 Audience: Product and engineering
 
 This document explains how Paperclip interprets issue assignment, issue status, execution runs, wakeups, parent/sub-issue structure, and blocker relationships.
@@ -121,6 +121,17 @@ These are related but not identical:
 
 Paperclip already clears stale execution locks and can adopt some stale checkout locks when the original run is gone.
 
+The active-lock lifecycle is part of the checkout contract:
+
+- a run owns `checkoutRunId` only while that run is non-terminal
+- when a run reaches `succeeded`, `failed`, `cancelled`, or `timed_out`, finalization must compare-and-clear lock columns that still point at that run
+- finalization must not clear a lock already reacquired by a successor run
+- process-loss retry handoff must not leave `checkoutRunId` pinned to the failed run when `executionRunId` moves to the retry run
+- checkout and checkout-owner checks may self-heal lock columns that point at terminal or missing runs before evaluating conflicts
+- the recovery sweeper may clear rows whose checkout and execution locks all point at terminal or missing runs
+
+Stale-lock recovery is crash recovery, not a retry loop. Paperclip must not clear or adopt locks held by non-terminal runs. After stale cleanup, a checkout `409` should mean a real live owner, status/assignee mismatch, unresolved blocker, or active gate still prevents checkout. Agents must treat that `409` as an ownership conflict and stop rather than retrying the same checkout.
+
 ## 6. Parent/Sub-Issue vs Blockers
 
 Paperclip uses two different relationships for different jobs.