arXiv:2609.14640v2 Announce Type: replace Abstract: PaxosLease is a protocol by which a quorum of acceptors grants time-bounded exclusive ownership with no durable acceptor lease state and no disk write on the lease acquisition path. This paper gives a precise, machine-checked statement of the protocol and of its standard use, electing a Multi-Paxos leader. Formalizing and model checking the orig
PaxosLease Revisited provides a machine-checked TLA+ model of the diskless PaxosLease protocol, uncovering three critical safety violations in the original 2012 specification. The analysis establishes that acceptor restart quarantine must equal the proposer attempt duration to prevent conflicting leases, and that starting the attempt timer at prepare-quorum receipt is unsafe, potentially allowing two simultaneous owners. Additionally, it proves that leftover messages from abandoned acquisition attempts can cause safety failures unless lease-open reports are scoped strictly to the active renewal of that exact lease.
PaxosLease Revisited presents a formal, machine-checked treatment of PaxosLease, a quorum-based protocol in which a coordinator obtains a time-bounded lease from a quorum of acceptors and thereby gains exclusive ownership for the lease interval. The setting is notable because the lease is not backed by durable acceptor lease state and its acquisition path avoids disk writes, making it attractive for low-latency coordination. The paper’s focus is not primarily a new protocol mechanism, but a precise specification of the lease protocol and of a canonical application: using the lease to elect a Multi-Paxos leader.
The main contribution is the checked model itself. By encoding the protocol’s message flow, quorum conditions, expiration behavior, and leader-election usage in a formal model, the authors can verify intended invariants and expose assumptions that are easy to miss in informal descriptions. In particular, the work clarifies how mutual exclusion is maintained across concurrent lease requests, how acceptor state and timing bounds interact with lease validity, and what conditions are needed for a lease to support safe leader election in a Multi-Paxos deployment.
This matters because diskless leases are a practical optimization for distributed systems that need fast leader selection or exclusive coordination without paying the cost of synchronous disk I/O on the critical path. However, such optimizations are only useful if their correctness is well understood under failure and timing assumptions. A machine-checked model provides a stronger basis for implementation, reasoning about edge cases, and extending the protocol, while also making the protocol’s guarantees explicit for designers of lease-based consensus systems.