I02 Failure Workbook #

Baseline:

• I02Lease.tla
• I02Lease.cfg

Bug scenarios:

• I02DuplicateClaimBug.tla
• I02StaleActorBug.tla

Main insights #

1. Claim is an exclusivity contract #

• bug: more than one owner can be active
• catches: AtMostOneOwner
• lesson: lease/claim truth must reject a second owner at the data layer

2. Lease expiry is not enough; stale actors must be fenced #

• bug: an actor can still Use with an old epoch
• catches: UseMustUseCurrentEpoch
• lesson: authority must be proven by the current epoch, not merely by past ownership