Declarative distributed algorithms as axiomatic theories in three-valued modal logic over semitopologies
Murdoch J. Gabbay
cs.LO
Dec 24, 2025 · v1
TL;DR
Correctness proofs for declarative axiomatic specifications of distributed protocols are formalised in Lean 4.
Abstract
We illustrate how to formally specify distributed algorithms as declarative axiomatic theories in a modal logic, using as illustrative examples a simple voting protocol, a simple broadcast protocol (Bracha Broadcast), and a simple agreement protocol (Crusader Agreement). The methods scale well and have been used to find errors in a proposed industrial protocol. The key novelty is to use modal logic to capture a declarative, high-level representation of essential system properties -- the logical essence of the algorithm -- while abstracting away from explicit state transitions of an abstract machine that implements it. It is like the difference between specifying code in a functional or logic programming language, versus specifying code in an imperative one. Thus we present axiomatisations of Declarative Bracha Broacast and Declarative Crusader Agreement. A logical axiomatisation in the style we propose provides a precise, compact, human-readable specification that abstractly captures essential system properties, while eliding low-level implementation details; it is more precise than a natural language description, yet more abstract than source code or a logical specification thereof. This creates new opportunities for reasoning about correctness, resilience, and failure, and could serve as a foundation for human- and machine verification efforts, design improvements, and even alternative protocol implementations. The proofs in this paper have been formalised in Lean 4.
Problem
Specifying distributed algorithms typically requires explicit state-transition models, which mix essential protocol logic with low-level implementation details, making formal verification cumbersome.
Approach
The authors specify distributed algorithms as declarative axiomatic theories in a three-valued modal logic over semitopologies, where nonempty open sets represent quorums. The middle truth value captures uncertainty in message delivery. They demonstrate the approach on a voting protocol, Bracha Broadcast, and Crusader Agreement, capturing the logical essence of each algorithm without explicit state machines. Proofs are formalized in Lean 4.
Results
Declarative axiomatizations of Bracha Broadcast and Crusader Agreement are presented and formally verified in Lean 4. The methods have been used to find errors in a proposed industrial protocol.
