A Higher-Order Separation Logic for Verifying Liveness-Preserving Refinements of Distributed Systems

Distributed systems are notoriously difficult to design, implement, and reason about. This is especially true for liveness properties which state that a desired state of the system is guaranteed to eventually be reached. A lot of complexity is found in distributed system implementations as these often employ features such as higher-order constructions and concurrency. Such features are difficult to formally reason about even without the added complexity introduced by the asynchronous communication present in distributed systems, or considering liveness properties. In this paper we present Fairneris, the first higher-order concurrent program logic for formal and foundational verification of safety alongside liveness-preserving refinements for distributed system implementations. This work builds on the recent success of the Iris-based Trillium/Fairis program logic framework for liveness-preserving refinement reasoning about higher-order concurrent programs, and that of the Aneris program logic for reasoning about (only) safety properties of distributed systems. To demonstrate the capabilities of Fairneris we verify both safety and liveness properties of an implementation of a higher-order distributed RPC-like system on top of unreliable networking primitives, through a refinement to a live high-level model. All results presented in the paper are mechanized on top of the Rocq proof assistant.