Nine TLA+ specifications of a calculus for the runtime governance of action authority, together with configuration files, a one-command reproduction script covering every reported configuration, and run records. Eight model families are included: the single-agent calculus; a federated instance under communications partition; a human-machine handoff instance with a bounded reversion deadline; a vehicle instance whose safe behaviour consumes the resource it protects; trust-anchor recovery across four provenance and reach architectures; an integrated instance composing those constraints on one platform; a lease instance in which authority expires rather than being revoked; and a gate evaluated on measured rather than true evidence. Results are exhaustive for the bounded configurations reported. Sixteen configurations are deliberately negative and are labelled as such, including a sub-majority quorum admitting two simultaneously acting components, an unguarded reversion deadline, an unguarded return budget, dependent recovery anchors, a safe behaviour placed under the same authorization as the mission, a de-rating margin below the measurement error bound, and a lease outlived by clock skew. No operational validation is claimed.