Verifying a high-performance distributed transaction system using permissioned state machines
The permissioned state machine (PSM) approach, which extends TLA-style protocol reasoning with ideas from concurrent separation logic, enables the developer to specify and verify complex protocols, such as Tulip, by breaking them down into smaller modules.