Compositional Verification of Composite Byzantine Protocols
Qiyuan Zhao

George Pîrlea

National University of Singapore
Singapore, Singapore
qiyuanz@comp.nus.edu.sg

National University of Singapore
Singapore, Singapore
gpirlea@comp.nus.edu.sg

Karolina Grzeszkiewicz
Yale-NUS College
Singapore, Singapore
karolina.grzeszkiewicz@u.yale-nus.edu.sg

Seth Gilbert

Ilya Sergey

National University of Singapore
Singapore, Singapore
seth.gilbert@comp.nus.edu.sg

National University of Singapore
Singapore, Singapore
ilya@nus.edu.sg

Abstract1

Byzantine Fault-Tolerant (BFT) protocols are known to be difficult todesign and to reason about. To address this challenge, on one hand,several approaches have been developed recently for computeraided formal verification of the desired correctness properties, both
safety and liveness, of standalone BFT protocols. On the other
hand, the distributed computing community has made attempts
to reduce the conceptual complexity of constructing new suchprotocols by showing how to assemble them from simpler “building
blocks”. No methodology to date combines these two approaches
for foundational verification of arbitrary BFT protocols.
We present Bythos, the first foundational framework for compositional mechanised verification of both safety and liveness ofcomposite BFT protocols. Bythos is implemented on top of the Coq
proof assistant and uses Coq’s higher-order logic to reuse proofsof common facts about knowledge and trust in BFT protocols. It
allows for compact liveness specifications in the style of TLA+, andfor their proofs using an embedding of TLA into Coq. Most importantly, Bythos provides a family of higher-order definitions thatallow building composite BFT protocols from simpler ones, with
their correctness proofs derived. We showcase Bythos by verifying
in it safety and liveness properties of three basic BFT protocols:
Reliable Broadcast, Provable Broadcast, and the recently proposed
Accountable Byzantine Confirmer, as well as their compositions.

In the evolving landscape of distributed computing, Byzantine Fault
Tolerance (BFT) protocols have emerged as a cornerstone for ensuring the reliability and integrity of Internet services in the presenceof malicious adversaries and arbitrary faults [37]. In particular, BFT
protocols have proven invaluable in critical infrastructure systems
and blockchain technologies [6, 16, 19, 43, 65].
After more than two decades of research on BFT protocols,
computer scientists’ understanding of them is relatively mature.
Nonetheless, new proposals of such protocols are still intricate andimplementation is difficult and prone to bugs [49], which, given thecritical applications of the technology, could prove disastrous.
One approach to reducing the risk of bugs in BFT protocols is
computer-aided formal verification. Protocols and their implementations can be encoded in the language of a software tool such asa proof assistant and shown from first principles to satisfy their
desired properties [26, 30, 39, 54, 57, 61–63].
These proofs can often be made fully foundational [8], in thesense that they are expressed in terms of a small set of accepted
axioms, and machine-checked, providing a very high degree ofconfidence that the verified systems indeed satisfy the properties.
Practically speaking, however, most of these efforts cannot bereused. The issue is that BFT protocols, at least for a long time, havegenerally been described monolithically, without a clear separation
into sub-protocols with logically distinct roles of each such protocol
and its effect on the overall correctness properties of the wholeconstruction. The issue is not with formal verification itself, butwith how the protocols are described in the first place, which makes
it difficult to recognise reusable design components that could be
used for constructing new protocols and proofs about them.

CCS Concepts• Networks → Protocol testing and verification.

Keywords
Byzantine fault tolerance, distributed protocols, formal verification

Introduction

Motivating example: verifying iterated provable broadcast. Protocol
designers have recognised the issue that BFT protocols are complicated to understand and have sought to provide simpler, more
modular descriptions. An example of this is a series of blog posts byAbraham et al. [1–3] explaining how a basic Provable Broadcast (PB)
protocol [55] can be iterated to obtain progressively stronger properties. In a single instance of PB, a sender broadcasts a value 𝑣 andan associated proof to all 𝑛 parties, which validate the first 𝑣 theyreceive using the proof and an external validity function EV, sign 𝑣
with their own keys and echo the signed 𝑣 to the sender, whichcollates signatures from 𝑛 − 𝑓 parties into a delivery certificate for 𝑣.
As Abraham et al. observe [4], an iterated version of PB forms themain loop of Tendermint [15], Casper [17], and HotStuff [65]. The

ACM Reference Format:
Qiyuan Zhao, George Pîrlea, Karolina Grzeszkiewicz, Seth Gilbert, and Ilya
Sergey. 2024. Compositional Verification of Composite Byzantine Protocols.
In Proceedings of the 2024 ACM SIGSAC Conference on Computer and Communications Security (CCS ’24), October 14–18, 2024, Salt Lake City, UT, USA.
ACM, New York, NY, USA, 15 pages. https://doi.org/10.1145/3658644.3690355

This work is licensed under a Creative Commons AttributionShareAlike International 4.0 License.
CCS ’24, October 14–18, 2024, Salt Lake City, UT, USA© 2024 Copyright held by the owner/author(s).
ACM ISBN 979-8-4007-0636-3/24/10
https://doi.org/10.1145/3658644.3690355
1

CCS ’24, October 14–18, 2024, Salt Lake City, UT, USA

Qiyuan Zhao, George Pîrlea, Karolina Grzeszkiewicz, Seth Gilbert, and Ilya Sergey

first iteration (if it terminates) proves that 𝑛 − 𝑓 parties know andhave validated 𝑣; the second proves that 𝑛 − 𝑓 parties know that𝑛 − 𝑓 parties know and validated 𝑣, and so on.
Following Lamport’s classification [35], a protocol’s correctness
specification can be divided into safety properties, which assert that“bad states” cannot be reached, and liveness properties, which assertthat “good states” are eventually reached. Typically, the satisfactionof these properties is conditioned on the number of faults the system
experiences. In a Byzantine consensus protocol, for instance, data
integrity can be guaranteed in an asynchronous setting with 𝑓faulty nodes only if at least 2𝑓 + 1 nodes are non-faulty (i.e., 𝑛 > 3𝑓 );eventual termination can be guaranteed as well when assuming
certain fairness condition. Provable Broadcast satisfies three safety
properties and one liveness property:

that formally address both liveness properties and Byzantine fault
tolerance either focus on a concrete monolithic blockchain system
in a synchronous network [61] or lack the ability to compose proofs
across protocols [10, 42, 53]. The only approach to date we are awareof that is capable of the desired proof decomposition [32], requires
encoding a system as a threshold automaton suitable for model
checking [33], thus giving up on the expressivity of the specification
formalism and on the foundational verification guarantees.
The goal of this work is to provide a framework for machineassisted verification of BFT protocols, which supports proofs of theirsafety and liveness, that are both compositional (i.e., are constructed
out of properties of sub-protocols) and foundational (i.e., do not
require a bespoke trusted encoding of the system).
This work. In our quest, we are taking forward the ideas fromearlier efforts on encoding and verifying distributed systems ininteractive proof assistants based on higher-order logic [50, 54, 57,63], enhancing them with the following new aspects:• Knowledge lemmas. For each verified basic BFT protocol, we
identify and prove a family of lemmas, which provide a succinct
summary of the knowledge derivable from any execution historyof a protocol, facilitating the proofs of safety and liveness. Whilethe lemmas have to be stated in terms of the data types specificto a protocol’s definition, their shapes are generic, making theirstatements easy to formulate for any BFT construction.
• A functor for protocol composition. We provide a higher-orderfunctor to build composite protocols from basic sub-protocols.
This structure allows for the safety and liveness properties of acomposite protocol to be derived from those of its sub-protocols.
The result of these enhancements is Bythos, a new framework
embedded in the Coq proof assistant [60] for the compositionalverification of both safety and liveness properties of BFT protocols.
Contributions. Our work makes the following contributions:(1) Weak Availability (S): if a delivery certificate exists for 𝑣, thenat least 𝑛 − 2𝑓 honest parties hold and echoed the value 𝑣;(2) Uniqueness (S): at most one value obtains a delivery certificate;(3) External Validity (S): if there is a delivery certificate for a value 𝑣,
then 𝑣 is externally valid;(4) Termination (L): an honest sender that has an externally valid
input 𝑣 will eventually obtain a delivery certificate for 𝑣.
Weak availability follows from the construction of the protocol.
Uniqueness follows from quorum intersection, by contradiction:
having two delivery certificates for different values 𝑣 ≠ 𝑣 ′ implies
there are two sets of 𝑛 − 𝑓 parties who have signed 𝑣 and 𝑣 ′ , respectively. But if 𝑛 > 3𝑓 , these two sets intersect in at least 𝑓 + 1
parties, and thus one honest party signed different values, which is
impossible for honest nodes. External validity follows from weak
availability and the fact that all honest parties validate the echoedvalue. Finally, termination follows under the fairness condition thatpackets between honest nodes are eventually delivered.
Iterated versions of PB, in which 𝑣 and the delivery certificate
from iteration 𝑖 become the value and the proof respectively initeration 𝑖 + 1, provide increasingly stronger guarantees. Concretely,
by combining the weak availability of iteration 𝑖 +1 with the uniqueness of iteration 𝑖, we prove properties of the form “a quorum knowsthat a quorum knows 𝑣”, with increasing depth. This “locks” values
such that nodes cannot later renege them. Such guarantees are thebasic logical building block of BFT consensus protocols.

• We present a methodology for compositional verification of BFT
protocols based on modular proofs of inductive invariants andtemporal reasoning, that applies to a wide range of basic protocol
constructions and their combinations.
• We introduce the idea of knowledge lemmas: building blocks of
inductive invariants that concisely encapsulate the causality ofthe system execution, facilitating its safety and liveness proofs.
• We propose the systematic decomposition of composite BFT protocols and verification of their properties, especially liveness ones,
by modularising the protocol implementations and specifications
using the mechanism of Coq modules and functors.
• We implement our methodology as Bythos, a domain-specificlanguage and library of lemmas in the Coq proof assistant [60]. To
the best of our knowledge, this is the first verification frameworkthat (1) is foundational, (2) allows reasoning about Byzantine
faults, (3) supports both safety and liveness proofs, and (4) allows
for effective proof reuse for composite BFT protocols.
• We showcase Bythos and its compositional nature by verifying
the Provable Broadcast (PB) protocol [55] and two of its iterated
versions [2], Bracha’s Reliable Broadcast (RB) protocol [14], andthe recent Accountable Confirmer (AC) protocol [22], as wellas the composition of RB and AC. Ours are the first machinechecked formalisations of any of these protocols.

Problem statement. Assume one would like to establish a stronger
property for the PB protocol iterated two times, a composition
known as Locked Broadcast (LB). For example, consider Unique Lock
Availability: if a delivery certificate exists for 𝑣 then it implies there
exists a lock certificate for 𝑣, which no other value 𝑣 ′ can have, andthere are at least 𝑛 − 2𝑓 honest parties that hold this lock certificate;
the lock certificate implies that at least 𝑛 − 2𝑓 honest parties holdthe value 𝑣. This property follows from uniqueness (2) of PB run in
LB’s first stage and weak availability (1) of LB’s second stage.
While intuitive and simple, a compositional proof of this property
out of the already established facts (1) and (2) cannot be obtained inmost of the modern frameworks for verifying distributed protocols.
While some existing approaches allow for deriving properties ofcomposite distributed protocols from their sub-parts, they either
lack support for liveness proofs [54, 62] or do not allow reasoning
about Byzantine behaviours [29, 30], or both [57, 63]. Recent works
2Compositional Verification of Composite Byzantine Protocols
1
2
3
4
5
6
7
8
9
10
11
12
13

CCS ’24, October 14–18, 2024, Salt Lake City, UT, USA

Record State := Node {id : Address;(* sender state *)sent : Round -> bool;counter : Round -> list (Address * PartialSignature);
output : Round -> option CombinedSignature;(* receiver state *)echoed : Address * Round -> option (Value * Proof) }.
Inductive InternalEvent :=| SendAction (r : Round).
Inductive Message :=| Init (r : Round) (v : Value) (pf : Proof)| Echo (r : Round) (ps : PartialSignature).

1
2
3
4
5
6
7
8
9
10
11
12
13

Definition procMsg st src msg : State * list Packet :=let: Node q _ cnt output _ := st inmatch msg with| Echo r ps => if (output r == None) &&(partial_verify (r, proposal q r) ps src) &&(src ∉ (map fst (cnt r))) thenlet: cnt' := {cnt[r] ↦→ (src, ps) :: cnt r} in
let: st' := if length (cnt' r) == n - f thenlet: cs := partialsig_combine (map snd (cnt' r)) in
st <| output := {output[r] ↦→ Some cs}, cnt := cnt' |>else st <| cnt := cnt' |> in (st', [])else (st, [])| Init r v pf => (* processing the Init message *)(b) Condensed version of the message handler, procMsg. We use{mp[a] ↦→ b} to denote a map update and r <| f := ... |> to denote a record field update.

(a) Local state defined as a record, with internal event and message
defined as algebraic datatypes, where Round, Value and Proof are all
declared as Parameters.

Fig. 1: Highlights from the Bythos encoding of Provable Broadcast.
Paper outline. Sec. 2 gives a tour of Bythos from the user’s perspective, demonstrating its features by following the formalisation of Provable Broadcast, its correctness proofs, and the verification of two of its iterated versions, outlining the conceptualidea of knowledge-driven proofs of safety and liveness in Sec. 2.2
and Sec. 2.3, respectively. Subsequently, Sec. 3 presents the implementation of Bythos on top of Coq, focusing on the components
the user must instantiate to define a working system (Sec. 3.1), thesupport for liveness specifications and proofs (Sec. 3.2) and the functor for composing protocols (Sec. 3.3). Sec. 4 describes more casestudies: verification of Reliable Broadcast (RB, Sec. 4.1), Accountable
Confirmer (AC, Sec. 4.2), and Accountable Reliable Broadcast—thecomposition of RB and AC (ARB, Sec. 4.3). Sec. 5 discusses the proof
efforts of this work and the limitations of Bythos. Sec. 6 compares
Bythos with related frameworks for mechanised verification ofsafety and liveness of distributed protocols.

2

messages that contain signatures (line 13). Unlike the simplified
description [1–3], in scenarios where PB is used as a sub-protocol(e.g., consensus protocols like [4]), each node acting as the sender
can initiate and concurrently execute multiple rounds of PB, and all
messages thereby contain Round tags for disambiguation (lines 12–13). When echoing, nodes sign a round-value pair rather than justthe value. Because a node can be part of multiple concurrent rounds,
acting in different capacities in each, nodes maintain state both for
acting as a sender (lines 4–6) and acting as a receiver (line 8).
Every node has a fixed unique address (id on line 2), i.e., a cryptographic public key that for simplicity also doubles as a network
identifier to which packets can be sent. For each round, the senderkeeps track of whether it broadcast a value in that round (sent online 4), of which signed echoes it received (counter on line 5), andwhether it output a delivery certificate (output on line 6). Receivers
keep track of what they have echoed to whom and at which round(echoed on line 8). We model the values to broadcast as taken fromproposal (used on line 5 in Fig. 1b), an oracle we take as a parameterof the protocol, defining what value node 𝑞 proposes at round 𝑟 .

Overview

In this section, we take the Provable Broadcast protocol as a running
example to showcase the process of implementing BFT protocols
and verifying their safety and liveness in Bythos, and highlight
how to compose protocols to obtain strengthened guarantees.

2.1

2.1.1 Specification of Cryptographic Primitives. In Bythos, wework in the Dolev-Yao model [24]. Specifically, we assume ideal
cryptographic primitives from the threshold signature scheme [41],with the following standard axioms, often assumed in hand-written
distributed protocol proofs [4]:• A partial signature1 ps can be verified wrt. the pair (𝑟, 𝑣) andthe public key 𝑞 if and only if ps is signed for (𝑟, 𝑣) using thecorresponding private key of 𝑞.
• A combined signature cs can be verified wrt. the pair (𝑟, 𝑣) if andonly if cs is obtained from collating 𝑛 − 𝑓 partial signatures, wherefor each partial signature ps, there must exist a public key 𝑞 suchthat ps can be verified with respect to (𝑟, 𝑣) and 𝑞, and these 𝑞
are different for each partial signature.
• The signing function is injective. That is, any given partial signature ps can only be verified with respect to a single input (𝑟, 𝑣).
The PartialSignature and CombinedSignature types (cf. lines 5, 6,
and 13 of Fig. 1a), which abstract partial signatures and combined
signatures respectively, are predefined as Parameters in Bythos.
Their associated methods including partial_sign, partial_verify

Provable Broadcast, Formally

In Bythos, a protocol is defined in terms of two handlers, implemented as pure functional programs:• procInt, which handles internal events within a node, e.g. thedecision of the sender in PB to broadcast a value;• procMsg, which defines the effect of receiving a message.
Each of them takes as input the local state of a node and, respectively, the internal event or message to be handled, and returns the
updated state and a list of packets (i.e., messages decorated withsender’s and receiver’s identities) to be sent in response.
We start implementing the Provable Broadcast protocol by defining a node’s local state, the kinds of internal events that can occur,and the type of messages, as shown in Fig. 1a. The only internal event in PB is the initiation of a broadcast (line 10), where asender sends to all nodes Init messages, each of which contains
a value and a proof (line 12). The receivers echo by sending Echo

1 Also called signature share [4]. Here, we follow the terminology by Civit et al. [22].

3CCS ’24, October 14–18, 2024, Salt Lake City, UT, USA

Qiyuan Zhao, George Pîrlea, Karolina Grzeszkiewicz, Seth Gilbert, and Ilya Sergey(line 5 in Fig. 1b), partialsig_combine (line 9), and combined_verify
are also declared as Parameters satisfying the axioms listed above.

1
2
3

2.1.2 Protocol Definition. With these preliminaries, we can define
the two handlers. In the interest of space, in Fig. 1b we show only acondensed version of the Echo message handler at the sender, which
receives (line 4), verifies (line 5), and records (line 7) signatures fromthe protocol parties, and when the threshold of 𝑛 − 𝑓 ≥ 2𝑓 + 1 valid
partial signatures received from distinct parties is reached (line 8),builds the combined delivery certificate (line 9). In particular, online 5, the sender (with identifier 𝑞) verifies that the value signed
is indeed the value that it originally proposed. The Init message
handler at the receiver is defined similarly: if the attached value
and proof are validated by the external validity function EV, thenthe receiver records them into the echoed field, uses partial_sign
to sign the round-value pair and attaches the signature to the Echothat is then sent back. The procInt handler for SendAction uses
proposal to choose a value and broadcasts it by returning a list of
packets rather than [], as procMsg does on line 12.

2.2

4
5
6
7
8
9
10
11

Definition producible p r v (cs : CombinedSignature)(w : SystemState) : Prop :=forall (pss : list PartialSignature),cs = partialsig_combine pss ->forall (q : Address) (ps : PartialSignature),ps ∈ pss ->(* q is honest *) ->partial_verify (r, v) ps q = true ->exists pkt : Packet,(* pkt is in the packet soup, is sent by node q,
and carries the message (Echo r ps) *).

Fig. 2: Predicate constraining any producible delivery certificate cs by node p for round r and value v, in system state w.
as mediators that induce causal relationships: the fact that a packet
was sent (i.e., it is in the packet soup) implies something about
the local state of the sender 𝑠, and similarly, a packet’s receipt
has implications for the state of the receiver 𝑟 . Put together, theexistence of a received packet lets us relate the states of 𝑠 and 𝑟 ,which would be difficult if we were unable to determine whether the
packet was received; an instance of such correlation is property (5a)in Sec. 2.2.5. Such discrimination over packets is widely used inother verification frameworks [30, 46, 57].

Proving Safety Properties

With a full implementation of the protocol, we proceed to verify that
our implementation satisfies the four properties listed in Sec. 1. But
first we must understand how to formally express these properties
and, more fundamentally, what it means for a protocol to satisfy aproperty. Both aspects are tied to the system model of Bythos.

2.2.2 Modelling Byzantine Faults. We model the Byzantine adversary as controlling the asynchronous network, having the ability toobserve all packets and indefinitely delay packets. However, the adversary cannot tamper with the contents of packets between honest
nodes and cannot forge messages to appear as coming from honest
nodes. Moreover, the adversary is constrained in terms of whatvalues it can produce, regardless of whether these values become
externally visible via messages or not.
To state the assumption that Byzantine nodes do not possess
unbounded computing power and thus cannot forge the signaturesof non-faulty nodes, we follow the Dolev-Yao approach [24] andstate that the only way Byzantine nodes can acquire signaturessigned with the private keys of non-faulty nodes is by intercepting
packets transmitted over the network. In the context of Provable
Broadcast, the adversary is constrained in terms of which delivery
certificates (i.e., combined signatures) it can produce. We formalise
this as shown in Fig. 2. The producible predicate says that if cs
is a producible certificate in the system state w obtained by combining a list of partial signatures pss (which is the only way toform a combined signature that can be verified as per the axiom
in Sec. 2.1.1), then all valid signatures in pss from honest nodes
were seen in the history of w (i.e., in its packet soup) as part of Echo
messages. Intuitively, this predicate captures all the possible ways a
Byzantine adversary could combine partial signatures into delivery
certificates—the existence of any other delivery certificate implies abreak of the cryptography. Taking this constraint as premise in the
proof of uniqueness (2) suffices to establish the safety and livenessof the system, without additional constraints on which messages
can be sent. Consequently, the byzConstraints predicate is simply
True for Provable Broadcast.

2.2.1 System Model. In Bythos, the entire distributed system, including all nodes and the network, is modelled as a state-transition
system. The SystemState consists of a mapping from each node’s
Address to its local (protocol-specific) State, as well as a collectionof all the packets that have been ever sent, called the packet soup.
In the packet soup, packets that have been received (i.e., deliveredby the network) are distinguished from those that have not, which
are referred to as being fresh. The system has four different kinds oftransitions, or steps, which define how a system state can change:• Stuttering, which leaves the system state unchanged. The existence of such a step is essential for compositionally reasoning
about composite protocols (cf. Sec. 4.3).
• Delivery, where a non-faulty node receives some packet in thepacket soup. As mentioned in Sec. 2.1, procMsg is for handling thepacket and defines what the node’s local state should be updated
to, as well as the packets that should be added to the packet soup.
• Internal, where a non-faulty node spontaneously triggers aninternal event, without input from the network. The procInt
handler specifies how the internal event should update the node’s
local state and which, if any, freshly produced packets should be
added to the packet soup.
• Byzantine, where a Byzantine node adds a single fresh packet tothe packet soup. The packet’s source must be one of the Byzantine nodes (i.e., packets cannot be forged), and the message contained within the packet must satisfy a protocol-specific predicate
byzConstraints, which specifies the messages that the adversary
can produce in a given system state (more details in Sec. 3.1.5).
Packets are never removed from the packet soup. Moreover, thefact that we distinguish between fresh and received packets plays
an important role in our proofs. The intuition is that packets serve

2.2.3 Safety Properties. Having defined the system model, we can
now state what a property is and what it means for a system to4Compositional Verification of Composite Byzantine Protocols

CCS ’24, October 14–18, 2024, Salt Lake City, UT, USA

satisfy a property. A safety property is a predicate on SystemStates.
A system satisfies a safety property 𝑆 if every system state 𝑤 reachable via valid system steps from an initial system state satisfies 𝑆.
The standard approach to prove safety properties is to establish
an inductive invariant, a property 𝐼 which is closed under (i.e. preserved by) system transitions. Once we find an inductive invariant
𝐼 such that ∀𝑤, 𝐼 (𝑤) ⇒ 𝑆 (𝑤) and show that 𝐼 holds on the initialsystem state, we can establish that the system satisfies 𝑆.

have its echoed field set for 𝑝 and 𝑟 (𝑞 may not have echoed
to the same Init message, though, since 𝑝 can be Byzantine and have sent multiple such Init messages); these two
represent receipt-sensitive knowledge propagation, requiring that the described message be received, while thosein (4a) are receipt-insensitive, which hold regardless ofwhether the message is received;(5) Implications of knowledge:(a) Echoed implies proposed: if an honest node 𝑎 echoed toanother honest node 𝑏, then it echoed what 𝑏 proposed;(b) Counted implies echoed: if an honest node 𝑎 has a partial
signature from another honest node 𝑏 in its (counter r),then 𝑏 must have echoed the same value that 𝑎 initially
proposed for round 𝑟 , and that value is externally valid;(c) Honest output: if an honest node output a delivery certificate
for 𝑣, then the certificate can be verified and at least 𝑛 − 2𝑓
honest nodes echoed 𝑣; moreover, 𝑣 is externally valid;(d) Uniqueness: in any instance of Provable Broadcast (determined by the sender and the round), every producible certificate is for the same value.
The knowledge lemmas from categories (1)–(4) capture the lowlevel properties of the protocol, which directly follow from theprotocol design and the system model. Specifically, the first three
categories of knowledge lemmas focus solely on the local statesof honest nodes, derived from the “delta” between the local state
updated by procInt or procMsg and the original one. On the other
hand, knowledge lemmas from category (4) describe the mutual
effect between the local states of honest nodes and packets sentfrom or to them.
By composing existing knowledge, we can then incrementallydevise higher-level guarantees, as those listed in category (5). For
example, property (5a) can be derived by composing the first property in (4b) and the second one in (4a). Moreover, property (5a)itself can be used in proving property (5b), which, in turn, aidsin proving other properties. In this way, we establish the safetyof Provable Broadcast: property (5c) implies weak availability andexternal validity, and property (5d) directly is uniqueness.

2.2.4 Knowledge Lemmas as Incremental Invariants. However, it isusually difficult to come up with an inductive invariant all at once.
As a rough intuition, an inductive invariant reflects some knowledge
about the protocol execution “contained” within a system stateand preserved under transitions. If the invariant is to imply any
interesting safety property, it must capture a lot of information
about the protocol’s execution. But protocols themselves are notmonolithic, and the properties they guarantee do not “fall from thesky”. Rather, protocols are designed in a gradual fashion, such thathigh-level guarantees are built progressively on top of low-level
guarantees. This is a form of logical composition within a single
protocol, and arises naturally in well-designed systems. And weought to verify protocols in the same way they are designed. Thisis the intuition behind our idea of knowledge lemmas: we want toincrementally capture the knowledge within a distributed execution
following the way this knowledge is generated in the first place.
2.2.5 Knowledge-Driven Proof of Safety. This process of incremental construction of an inductive invariant is best understood witha worked example at hand. We build our inductive invariant as
the conjunction of knowledge lemmas from each of the following
categories, with representative knowledge lemmas shown for eachcategory (please refer to the definitions in Fig. 1a):(1) Data representation: every list of collected signatures stored
in counter does not contain duplicates, and every included signature verifies; every value-proof pair collected in echoed passes
the external validity function;(2) Data persistence: the echoed field, once set for an address andround, is never overwritten; similarly for the output field; thecounter field only grows; the id field remains constant;(3) Knowledge propagation within a node: if (output r) is set
for some round r, then (counter r) has length exactly 𝑛 − 𝑓and (output r) is obtained by combining the partial signaturesin (counter r); if it is not set, then the length is less than 𝑛 − 𝑓 ;(4) Knowledge propagation through packets, where there are
two independent attributes:(a) Direction: if a node 𝑞 records that it initiated round 𝑟 , thenthere is an Init message for 𝑟 sent by 𝑞 to every node in thepacket soup, and symmetrically, if there is an Init message
from node 𝑞, then 𝑞’s local state has (sent r) being true
and that message carries 𝑞’s proposal for round 𝑟 ; these two
represent knowledge propagation in the local-to-packet
and packet-to-local directions, respectively;(b) Receipt-sensitivity: if a node 𝑞 records in echoed that it
echoed to node 𝑝 for round 𝑟 , then there is a received Init
message for 𝑟 sent by 𝑝 in the packet soup; conversely, if
there is a received Init message containing an externallyvalid value for 𝑟 sent by 𝑝 to an honest node 𝑞, then 𝑞 must

2.3

Reasoning about Liveness2.3.1 Liveness Properties. Whereas safety properties are predicatesover states, liveness properties are predicates over infinite execution
traces of system states, usually expressed in temporal logic [52]. To
encode and prove liveness properties in Coq using temporal logic,
we employ the CoqTLA library [20]. While it is straightforward to
define how a system satisfies a safety property (cf. Sec. 2.2.3), it ismuch trickier to do so for a liveness property. If we require thatany possible execution satisfies the property, then effectively nonon-trivial properties could be satisfied by a system: an execution
consisting of only stuttering steps does not do anything interesting.
Rather, the properties we want to prove hold only over “reasonable”
executions. In the literature, this concept of reasonableness is described in terms of fairness conditions, restrictions over executions.
A system satisfies a liveness property if all fair executions of thesystem satisfy the property.
2.3.2 Fair Delivery. Our fairness assumption cannot be related toclocks or Byzantine nodes due to the presence of asynchrony and5

CCS ’24, October 14–18, 2024, Salt Lake City, UT, USA

Qiyuan Zhao, George Pîrlea, Karolina Grzeszkiewicz, Seth Gilbert, and Ilya Sergey

the Byzantine adversary. Therefore, the fairness assumption we
adopt as default throughout Bythos is fair delivery, which statesthat all packets between honest nodes are eventually delivered.

2.4

Verifying Protocol Composition

We conclude our overview by demonstrating how to verify thesafety of iterated versions of the Provable Broadcast protocol, in avery simple way. For composable liveness proofs, see Sec. 4.3.1.
If we run two iterations of Provable Broadcast one after theother, taking the output of the first as the input of the second, we
obtain a stronger safety property called Unique Lock Availability,
cf. Sec. 1. Very interestingly, we can prove the safety of the iterated
protocol in only 5 lines of Coq, by creating two instances of the
Coq Module that defines Provable Broadcast, and simply adding ahypothesis that states that both instances propose the same value
and the proof used in the second (cf. line 12 in Fig. 1a) is the delivery
certificate output at the end of the first instance. The proof thenconsists simply of directly applying the safety properties of theindividual instances. We can then add yet another iteration of PB,
and obtain an even stronger guarantee with the same ease.

2.3.3 Knowledge-Driven Proofs of Liveness. We prove liveness by
first identifying, for the sake of modularising the proof, a decomposition of the protocol into phases. These phases arise naturally
in asynchronous protocols, resembling “rounds” in synchronous
protocols. Then, proving liveness amounts to showing that under
the fair delivery assumption, these phases are guaranteed to happen
consecutively, with the start of the first phase “leading to” the endof the last phase (a formal notion of “leading-to” is given in Sec. 3.2).
Consider an instance of Provable Broadcast initiated by an honest node 𝑞 for round 𝑟 , where 𝑞 is going to propose an externallyvalid value 𝑣. The natural decomposition is into two phases: an “initial” phase in which Init messages circulate, and an “echo” phasein which Echo messages circulate. This intuitive description is notquite fit for formalisation, however. We need to be more precise.
Concretely, we define the start and end of each phase to be predicates over system states: (1) the “initial” phase starts when 𝑞 locallysets (sent r) to true; (2) the “initial” phase ends, as well as the“echo” phase starts, when all honest nodes echoed for 𝑞 and 𝑟 ; (3)the “echo” phase ends when 𝑞 produces a delivery certificate for 𝑣.
To show that both phases will eventually conclude, we conduct thefollowing reasoning, utilising the fairness assumption and a seriesof knowledge lemmas established in Sec. 2.2.5:

3

Bythos Under the Hood

We implemented Bythos as a shallow embedding into the language
and logic of the Coq proof assistant [60]. The framework comeswith a set of reusable definitions for Byzantine network semantics,
generic shape of system state, helper lemmas for discharging common safety and liveness proof obligations, as well as a functor (i.e.,a higher-order Coq module) for constructing composite protocols,
which we will outline in Sec. 3.3. To keep things simple for the
purpose of protocol modelling, Bythos does not support advanced
language features, such as concurrency, exceptions, or advanced
control operators, unlike some existing program logics for safety
verification of distributed systems [34, 57, 58]. In particular nodes inprotocols defined in Bythos do not feature any additional mutablestate besides what is explicitly declared in their local state data type(e.g., the sent field in Fig. 1a for the case of Provable Broadcast).
In this section, we will elaborate on the components of Bythosthat a user needs to instantiate to define a complete distributed
system acting in a Byzantine environment in a way that is amenable
for safety proofs (Sec. 3.1), enables stating and proving livenessproperties (Sec. 3.2), and allows for composing individually defined
protocols into composite systems (Sec. 3.3). We will also briefly illustrate how to make protocol models in Bythos executable (Sec. 3.4).

(i) By the first knowledge lemma from (4a), when the “initial”
phase starts, 𝑞 has sent to all nodes Init messages that carry 𝑣
and which can be found in the packet soup;(ii) By the fair delivery assumption, all honest nodes will eventually receive these Init messages;(iii) At that time, by the second knowledge lemma from (4b), allhonest nodes will have their echoed fields set for 𝑞 and 𝑟 ;(iv) Moreover, by property (5a), all honest nodes will have echoed
to the Init messages carrying 𝑣, indicating the end of the“initial” phase and the start of the “echo” phase;(v) By a local-to-packet receipt-insensitive knowledge lemma andthe fair delivery assumption, 𝑞 will eventually receive Echo
messages from all honest nodes in response to its previously
sent Init messages;(vi) At that time, by a packet-to-local receipt-sensitive knowledge
lemma, 𝑞 will have collected all partial signatures on those
Echo messages to its (counter r);(vii) Finally, by the knowledge lemmas from (3) and property (5c),since the number of honest nodes is larger than 𝑛 − 𝑓 , 𝑞 will
have produced a delivery certificate for 𝑣 by that time.

3.1

Instantiating a Byzantine System in Bythos

3.1.1 Basic Data Types. As demonstrated by the example in Fig. 1a,every user-defined protocol in Bythos is expected to provide two
concrete data types: Address and Message, both used to instantiate
the parametric definition of the network semantics, which we willshow in Sec. 3.1.6. To facilitate the proofs, Bythos requires Address
to be inhabited and finite, which matches the real-world scenario
where the set of nodes in a protocol is not empty but is nonethelessfinite. The derived datatype of packets, Packet is defined as a Coq
Record parameterised by Address and Message:

The termination property is then proved by following the reasoning
steps above. (Its formal statement is shown in Fig. 4 and will be
explained in Sec. 3.2.)
We note that the key element in the liveness proof is the application of packet-to-local receipt-sensitive knowledge lemmas insteps (iii) and (vi). Intuitively, those lemmas state that honest nodes
will not “reject” well-formed messages delivered to them; without
such a guarantee, we cannot apply further knowledge propagation.

Record Packet := mkP { src : Address; dst : Address;
msg : Message; received : bool }.

This definition decorates its wrapped message msg with sender src
and receiver dst identities, as well as a Boolean tag received indicating whether this packet has been delivered.
6Compositional Verification of Composite Byzantine Protocols

CCS ’24, October 14–18, 2024, Salt Lake City, UT, USA

Bythos also provides abstractions of ideal cryptographic primitives, with their interfaces specified and their guarantees axiomatised (e.g., those listed in Sec. 2.1.1).

StutteringS(Σ, PS) −→ (Σ, PS)

3.1.2 Byzantine Resilience Threshold. As the next parameter ofthe system, the user needs to specify the maximum number of
Byzantine nodes f that the protocol can tolerate as a function of
its number of nodes 𝑛. Bythos requires that f be smaller than 𝑛,
imposing a (typically trivial) proof obligation on the user. For instance, for many protocols, f is ⌊(𝑛 − 1)/3⌋. To account for this very
common scenario, Bythos provides a pre-defined system template,where f is fixed to be ⌊(𝑛 − 1)/3⌋ and some useful lemmas (e.g.,properties about quorums of size 𝑛 − 𝑓 ). This template is useful forverifying protocols with the optimal resilience [14].

Internal

isByz 𝑝 = false

procInt Σ(𝑝) ev = (st, pkts)

I(𝑝,ev)(Σ, PS) −→ (Σ[𝑝 ↦→ st], sendout(pkts, PS))
Delivery𝑝 = pkt.dst
isByz 𝑝 = false
pkt ∈ PS
procMsg Σ(𝑝) pkt.src pkt.msg = (st, pkts)
D(pkt )

(Σ, PS) −→ (Σ[𝑝 ↦→ st], sendout(pkts, consume(pkt, PS)))

3.1.3 Protocol. With the basic data types and the Byzantine resilience threshold given, the next step is to define the actual protocol. This is achieved by instantiating the local state datatype State,
the kinds of internal events InternalEvent and the two handlers
procInt and procMsg, as demonstrated in the example from Fig. 1(although most protocols have more complex definitions).

Byzantine

isByz 𝑝 = true
pkt.received = false
byzConstraints pkt.msg (Σ, PS)
B(pkt )

(Σ, PS) −→ (Σ, sendout([pkt], PS))
where

3.1.4 System State. Recall from Sec. 2.2.1 that the system stateincludes a mapping of each node’s identity to its local state, alongwith a packet soup. Bythos represents SystemState naturally as arecord type, with the user having to provide the definition initStateof individual nodes’ initial local states to instantiate the initial
overall system state initSystemState, as shown below:defΣ[𝑝 ↦→ st] (𝑞) =

(

st,
Σ(𝑞),

if 𝑞 = 𝑝otherwise∀pkt, pkt ∈ sendout(pkts, PS) ⇐⇒ pkt ∈ pkts ∨ pkt ∈ PS
∀pkt, pkt ∈ consume(pkt ′, PS) ⇐⇒ pkt = markRcv pkt ′ ∨(pkt ∈ PS ∧ pkt ≠ pkt ′ ).

Record SystemState := mkW { localState : Address -> State;packetSoup : list Packet }.
Definition initSystemState : SystemState := mkW initState [].

Fig. 3: System semantics. A system state is a pair (Σ, PS) of
localState and packetSoup, respectively. A transition step from
(Σ, PS) to (Σ′, PS ′ ) is represented as (Σ, PS) −→ (Σ′, PS ′ ). Eachstep is associated with a tag (e.g., D(pkt), B(pkt)), that carries
additional information about the step (e.g., which packet isdelivered) and indicates which type of transition is taken.
The function markRcv pkt returns pkt <| received := true |>.

For simplicity, in Bythos the packet soup is defined as a list of
packets, which is initially empty. Whether a packet in the packet
soup is received can be determined via its received field.
3.1.5 Byzantine Nodes and Their Behaviour. Defining the semantics of the entire system requires specifying which nodes are acting
in a Byzantine fashion and precisely modelling their behaviour. We
specify which nodes are malicious through the isByz system parameter of type Address -> bool, which returns true if the argument
is a Byzantine node. Unlike previous system components (e.g., theMessage data type or the initState value), isByz does not have to
be instantiated, and is instead treated as a universally quantified
variable in all proofs about the system, since the system’s properties
should hold under any setting of Byzantine nodes. Naturally, unlike
other parameters, isByz must not be instantiated when extracting
executable system implementations, as implementations have nocontrol over the number and identities of Byzantine parties.
A key aspect of describing the behaviour of Byzantine nodes
is specifying what messages they can send, which is determinedby the adversary’s capability. To model this capability, Bythos
requires the user to instantiate

possible adversary, one that is able to send any messages during
the protocol’s execution. This is exactly the assumption made in
the proofs of the Reliable Broadcast protocol discussed further inSec. 4.1. In particular such an adversary can send a message thatbreaks the security guarantees of cryptographic primitives (e.g., amessage with a signature that requires the private key of a nonfaulty node), and thus the adversary can be viewed as possessing
unbounded computational power and even the knowledge of thelocal states and private keys of non-faulty nodes. More commonly,
we instantiate byzConstraints to model a more realistic adversary
following the Dolev-Yao model [24], allowing a Byzantine node to
produce a message based solely on the knowledge obtained fromintercepting packets in the packet soup.
In some proofs, we also need to constrain Byzantine nodes interms of what values they can produce (potentially not visible via
messages), as in Sec. 2.2.2. Such constraints are expressed in thesame way as byzConstraints and typically taken as premises in thestatements of key protocol properties.

Parameter byzConstraints : Message -> SystemState -> Prop.

which constrains the messages that can be sent by a Byzantine node
during executions of the system. Although this predicate has a simple type, we can model adversaries with varying degrees of powerby instantiating it differently. For example, by instantiating thepredicate to be (fun _ _ => True) in Coq, we model the strongest
7

CCS ’24, October 14–18, 2024, Salt Lake City, UT, USA

Qiyuan Zhao, George Pîrlea, Karolina Grzeszkiewicz, Seth Gilbert, and Ilya Sergey

Definition pb_termination : Prop := forall q r v,
isByz q = false -> v = proposal q r ->(* v is externally valid *) ->⌜ init ⌝ ∧ □ ⟨ next ⟩ ∧ WFDelivery ⊢⌜ initiated q r ⌝ { ⌜ has_certificate_for q r v ⌝.

3.1.6 System Semantics. With the definitions and parameters fromSec. 3.1.1–3.1.5, we can instantiate the system semantics of Bythos
for a particular protocol. The generic definition of the semantics
parametrised over those definitions is given in Fig. 3; in our Coq
implementation, we model it as a functor taking a set of modules
defining the above described components as input. The functor
defines an inductive relation with four constructors, replicating the
logic of the semantic rules from Fig. 3, which we detail below.
The rules for Stuttering and Internal steps are straightforward. In the case of the Delivery step, the packet soup after transitioning must contain the packets produced by the protocol’s
procMsg, and also mark the packet delivered at this step as received.
To this end, we use the combination of two functions, sendout andconsume, to achieve this: informally, sendout(pkts, PS) adds thepackets pkts to the packet soup PS, and consume(pkt ′, PS) marks
the packet pkt ′ inside PS to be received. The Byzantine step adds
an arbitrary packet to the packet soup, ensuring that its contents
do not violate the restrictions imposed by byzConstraints. Since
Byzantine nodes may not conform to the protocol, we do not specify how their local states change. Additionally, we do not consider
whether packets will be received by Byzantine nodes, as reflectedin the isByz 𝑝 = false premise of the Delivery step.
The generic definition of the system semantics in Fig. 3 accurately captures our basic assumptions. For instance, we assume
the network model to be asynchronous, since there is no internal
constraint on when a Delivery step will be taken, which captures
the scenario of packets being arbitrarily rearranged or delayed by
the adversary. The semantics also allows the network to deliver
the same packet multiple times by not requiring pkt.received to
be false in the pkt ∈ PS premise of the Delivery step rule. Thismodels the assumption that packets may duplicate. Our semantics
does not encode tampering or loss of packets explicitly, as those canbe modelled by a suitable choice of an adversary in combination
with the non-deterministic nature of our semantics.
Lastly, we note that despite its conceptual simplicity the semantics in Fig. 3 still allows us to prove several generic facts that we canuse in reasoning about execution properties of arbitrary protocols.
One example of such property is step locality, which follows fromthe fact that the system semantics treats the execution of handlers
or the step of a Byzantine node as being atomic: for the Internalor the Delivery step, only one node will be executing procInt or
procMsg, and its execution is completed in one transition step; for
the Byzantine step, only one Byzantine node is allowed to send apacket in a transition step. Therefore, at most one node will have its
local state changed after transition. Another useful generic property
is soup growth monotonicity, which has been observed and used inprior works on formal verification [5]: if a received packet is in thesoup, then that packet will remain in it after any transition, which
implies that the packet soup only grows.

3.2

Fig. 4: PB termination statement in Bythos via CoqTLA.

that takes a module implementing a system instance (assembled as
outlined in Sec. 3.1) as an argument and adapts its definitions to
the TLA notation and semantics.
With the help of the LTL notations provided by CoqTLA, we can
express the same properties in Bythos in a manner almost identicalto the expressions of liveness properties in TLA, allowing us tostate liveness properties in an intuitive way. As an example, consider the termination property of the Provable Broadcast protocol(Sec. 1) stating that if an honest node 𝑞 broadcasts some externallyvalid value 𝑣 at round 𝑟 , then eventually it will output a delivery
certificate for 𝑣. Its statement in Bythos is shown in Fig. 4, withsome definitional details omitted for brevity.
The embedding of Bythos system semantics into CoqTLA is
made possible thanks to the polymorphic nature of the definitions in
CoqTLA, which allows the logical connectives to work immediately
for predicates on traces of system states produced by Bythos. To
understand the notations from Fig. 4, recall that in TLA, a trace 𝜎 ofsystem states is defined as a function from natural numbers (representing timestamps) to system states. For a predicate 𝑃 over system
states, 𝜎 ⊨ ⌜𝑃⌝ if 𝑃 (𝜎 (0)) holds; for a binary predicate 𝐴 over system states (so-called action in TLA), 𝜎 ⊨ ⟨𝐴⟩ if 𝐴(𝜎 (0), 𝜎 (1)) holds.
Furthermore, by the semantics of the always temporal operator,𝜎 ⊨ □⟨𝐴⟩ if for any 𝑖 ∈ N, 𝐴(𝜎 (𝑖), 𝜎 (𝑖 + 1)) holds. Therefore, we
can encode the fact that 𝜎 is indeed a trace produced via consecutive system transitions by requiring 𝜎 ⊨ ⌜init⌝ ∧ □⟨next⟩, wheredefinit(𝑤) = (𝑤 = initSystemState) and the transition relationdefnext is defined as next(𝑤, 𝑤 ′ ) = 𝑤 −→ 𝑤 ′ (cf. Fig. 3).
In addition to basic definitions like init and next, the Bythos
functor for enabling temporal specifications also provides a tailored notion of fairness, denoted as WFDelivery. As we will show
below, under certain conditions, WFDelivery is logically equivalent
to the common eventual delivery assumption (Sec. 2.3.2) used in
our liveness proofs. Formally, WFDelivery is defined asdef

WFDelivery = ∀pkt, goodPkt(pkt) ⇒ WF(dlvSteppkt )where goodPkt(pkt) states that pkt is sent between honest nodes:
def

goodPkt(pkt) = isByz pkt.src = false ∧ isByz pkt.dst = false
In this definition, WF is the weak fairness combinator [36] anddlvSteppkt is a TLA action stating that the system takes a Delivery
step tagged with D(pkt), given that pkt is fresh in the packet soup:Specifying and Proving Livenessdef

dlvSteppkt (𝑤, 𝑤 ′ ) = pkt ∈ 𝑤 .packetSoup ∧One of the main features of Bythos is the ability to express liveness properties using the connectives from Linear Temporal Logic(LTL) [52] and prove them using the rules of Lamport’s Temporal
Logic of Actions (TLA) [36]. To achieve that, we have incorporated
the CoqTLA library [20] into Bythos by developing a Coq functor

D(pkt )

pkt.received = false ⇒ 𝑤 −→ 𝑤 ′To justify the definition of WFDelivery given above, we prove thatfor any trace 𝜎 such that 𝜎 ⊨ □⟨next⟩, 𝜎 ⊨ WFDelivery if and only
8Compositional Verification of Composite Byzantine Protocols

CCS ’24, October 14–18, 2024, Salt Lake City, UT, USA

Parameter trigger_procMsg :P_A.State (* local state before executing P_A.procMsg *) ->P_A.State (* local state after executing P_A.procMsg *) ->option P_B.InternalEvent.
Parameter trigger_procInt : (* the same type as above *)if the following predicate holds on 𝜎:
defeventualDelivery(𝜎) =∀pkt, 𝑛 ∈ N, goodPkt(pkt) ∧ pkt ∈ 𝜎 (𝑛).packetSoup ∧D(pkt )

pkt.received = false ⇒ ∃𝑘 ∈ N, 𝜎 (𝑛 + 𝑘) −→ 𝜎 (𝑛 + 𝑘 + 1)

The functor then constructs the composite protocol by setting its
local state to be the pair of those of 𝑃𝐴 and 𝑃𝐵 , and making its
message type be the sum type of those of 𝑃𝐴 and 𝑃𝐵 . The procMsg
handler of the composite protocol works by checking whether theincoming message is for 𝑃𝐴 or 𝑃𝐵 and calling the procMsg of thecorresponding protocol accordingly, whereas the procInt of thecomposite protocol only handles the internal events of 𝑃𝐴 . Whenthe triggers of these two handlers instruct that 𝑃𝐵 should also start
executing, they will additionally call 𝑃𝐵 ’s procInt.
We note that the composite protocol instance produced by thefunctor is on its own a protocol which can be plugged back into thefunctor, thereby enabling iterated sequential composition. Moreover, the system instance of the composite protocol is obtainedby following the same steps as other protocols (Sec. 3.1.4–3.1.6),
with its byzConstraints defined simply using those of 𝑃𝐴 and 𝑃𝐵 .
Consequently, the utilities for reasoning about liveness introducedin Sec. 3.2 are also applicable to the composite protocol.
The composition functor also provides relevant lemmas that “lift”
the safety and liveness properties of sub-protocols to the composite
protocol. This lifting is feasible because each transition step of thecomposite protocol can be “projected” into a valid transition step ofeach sub-protocol, facilitated by the presence of Stuttering steps.
For example, an Internal step of the composite protocol where
the trigger is not enabled can be projected into an Internal stepof 𝑃𝐴 and a Stuttering step of 𝑃𝐵 (or an Internal step of 𝑃𝐵 if
the trigger is enabled instead). In this way, execution traces of thecomposite protocol can be projected into those of sub-protocols,
ensuring that their safety and liveness properties are preserved by
the composite protocol’s execution. Thanks to the transitivity of
the leads-to connective (Leadsto-Trans), we can even compose
the liveness properties of 𝑃𝐴 and 𝑃𝐵 to derive liveness properties of
the composite protocol which cannot be derived from any of theindividual sub-protocols in isolation (cf. Sec. 4.3).

This predicate can be viewed as a “finer-grained” version of theeventual delivery assumption, stating that every packet sent between honest nodes at timestamp 𝑛 will eventually be deliveredat timestamp 𝑛 + 𝑘, where 𝑘 is an unknown natural number but isguaranteed to exist.
Apart from the symbols explained above, in CoqTLA, an entailment 𝑃 ⊢ 𝑄 holds if for any 𝜎, 𝜎 ⊨ 𝑃 implies 𝜎 ⊨ 𝑄. It allows for
liveness specifications to be expressed in the form of⌜init⌝ ∧ □⟨next⟩ ∧ WFDelivery ⊢ ⌜𝑃𝑏 ⌝ { ⌜𝑃𝑒 ⌝where the leads-to connective 𝑃 { 𝑄 is defined as □(𝑃 ⇒ ^𝑄) in
LTL (^ is the eventual operator). This entailment can be interpreted
as: during the execution of a system, under the eventual delivery
assumption (equivalent to WFDelivery), whenever the system enters
the state described by 𝑃𝑏 , it is guaranteed to eventually reach thestate described by 𝑃𝑒 . The entailment in Fig. 4 is then obtained byproperly instantiating the 𝑃𝑏 and 𝑃𝑒 above.
One important lemma involved in translating the informal proof
from Sec. 2.3.3 into formal proof scripts is the transitivity of {:∀𝑃, 𝑄, 𝑅, 𝑃 { 𝑄 ∧ 𝑄 { 𝑅 ⊢ 𝑃 { 𝑅(Leadsto-Trans)

This lemma is indispensable for achieving modular liveness proofs.
Recall that in the informal proof, the protocol is divided into the“initial” phase and the “echo” phase. By allowing us to reason about
these two phases independently (i.e., show 𝑃 { 𝑄 and 𝑄 { 𝑅separately), this lemma bridges these phases and completes the
final step towards the desired termination property (i.e., 𝑃 { 𝑅).

3.3

A Functor for Protocol Composition

As the final ingredient of Bythos, we describe one of its key innovations: a functor for combining two verified BFT protocol instances,along with their safety and liveness. Our construction is motivatedby Abraham et al.’s observation [1–3] that sequentially executing
the logic of the same or different BFT protocols may help to increase
the amount of knowledge that a node has about the preceding execution of the system and the amount of trust in other nodes. To
reflect this observation, Bythos provides a mechanism for sequential composition of protocol instances, such that when executing theprotocol composed of 𝑃𝐴 and 𝑃𝐵 , an honest node will execute theactions of the protocol 𝑃𝐴 first, and upon reaching a certain stage(for example, when 𝑃𝐴 outputs a value), it starts the execution ofanother protocol, 𝑃𝐵 . This sequential composition can be iterated.
Specifically, we allow users to sequentially compose protocols
implemented in Bythos by providing a functor that takes two
protocol instances 𝑃𝐴 , 𝑃𝐵 , defined by following the steps fromSec. 3.1.1–3.1.3, as inputs and provides the construction of thecomposite protocol in which each honest node runs the logic of
𝑃𝐴 and 𝑃𝐵 sequentially. To determine the starting conditions for
𝑃𝐵 , the user only needs to specify two triggers, which determine
when a node should start to run 𝑃𝐵 , based on the node’s local states
before and after executing the procInt or procMsg of 𝑃𝐴 :3.4

Extracting an Executable Implementation

The definitions of the protocol components outlined in Sec. 3.1.1–
3.1.3 are sufficient to derive executable reference implementations.
We use the standard mechanism of extracting OCaml code from
Coq [40], which turns Coq data types into corresponding ones in
OCaml, and converts handler functions procInt and procMsg into
the respective OCaml definitions. No additional effort is required to
extract a composite protocol, since the extraction works on protocol
instances, and composite protocols are also “first-class” protocol
instances (cf. Sec. 3.3). The working reference implementation is
obtained by linking the extracted protocol code to the trusted (i.e.,unverified) network shim [48], which is assumed to correctly capture the network behaviour as per the semantics from Sec. 3.1.6, as
well as the trusted concrete implementations of the cryptographic
primitives used by the protocol’s handlers.2
2 In our artefact [66], the threshold signature scheme is, for simplicity, implemented

assuming public-key infrastructure, avoiding the need for key distribution.
9

CCS ’24, October 14–18, 2024, Salt Lake City, UT, USA

Qiyuan Zhao, George Pîrlea, Karolina Grzeszkiewicz, Seth Gilbert, and Ilya Sergey

Algorithm 1 Reliable Broadcast (for node 𝑝)

an honest node
voted for v⇓≥ n − 2f

1: action RBcast(Round r, Value v):
2:send Init(𝑟, 𝑣) to all nodes

honest nodes
voted for v

3: upon receiving Init(𝑟, 𝑣) from node 𝑞:
4:
if 𝑝 has never sent Echo(𝑞, 𝑟, 𝑣 ′ ) before for any 𝑣 ′ :5:send Echo(𝑞, 𝑟, 𝑣) to all nodes
q reliably↝
broadcast v

6: upon receiving Echo(𝑞, 𝑟, 𝑣) from ≥ 𝑛 − 𝑓 different senders
7:
8:
9:

or receiving Vote(𝑞, 𝑟, 𝑣) from ≥ 𝑓 + 1 different senders:if 𝑝 has never sent Vote(𝑞, 𝑟, 𝑣 ′ ) before for any 𝑣 ′ :send Vote(𝑞, 𝑟, 𝑣) to all nodes

10: upon receiving Vote(𝑞, 𝑟, 𝑣) from ≥ 𝑛 − 𝑓 different senders:
11:

output (𝑞, 𝑟, 𝑣)

4

More Case Studies⇓

all honest nodes
echoed v≥ n − 2f(q, r, v)⇓

all honest nodes
voted for v⇑↝

all honest nodes
received≥n−f(q, r, v)

Proof of global liveness(two phases)

all honest nodes
received↝≥n−f(q, r, v)⇓

all honest nodes
output v
Proof of validity(three phases)

Fig. 5: Phase decomposition for the liveness proofs of Reliable Broadcast. A box represents the start or end of a phase,and a { symbol indicates the proof goal that a phase progresses from start to end. The area enclosed by dotted lines
corresponds to the proof of global liveness, while the area
enclosed by dashed lines corresponds to the proof of validity.
𝖨𝗇𝗂𝗍
𝖤𝖼𝗁𝗈
𝖵𝗈𝗍𝖾

In this section, we showcase more of the distributed protocols wehave verified in Bythos wrt. their safety and liveness specifications.

4.1

all honest nodes
received(r, v) from q↝

all honest nodes
received

The message type is an algebraic data type with three constructors
corresponding to Init, Echo, and Vote respectively. The handlers
are straightforward translations from the pseudocode (procInt corresponds to RBcast at line 1, while upon checks are performed
in procMsg). Since no cryptographic primitive is involved in RB,
byzConstraints is set to (fun _ _ => True).

Reliable Broadcast

We begin with Bracha’s Reliable Broadcast (RB) [13, 14], a classic BFT broadcast protocol in the asynchronous setting with at
most 𝑓 adversaries and at least 2𝑓 + 1 honest nodes. The protocol assumes the existence of authenticated channels, no message
loss or tampering, and no public-key infrastructure (PKI), i.e., no
cryptographic signatures. We consider the multi-shot version ofthis protocol [9, 44], shown in Algorithm 1. Similar to the Provable Broadcast in Sec. 2, this variant allows an arbitrary sender 𝑝
to broadcast different values in distinct rounds. All messages are
implicitly decorated with the sender’s identity, provided by the authenticated channel. The protocol has three types of messages: Init,
Echo and Vote. A node 𝑝 reliably broadcasts a value 𝑣 at round 𝑟 bysending Init(𝑟, 𝑣) to all nodes (line 2). The Echo and Vote messages
are for securing the broadcast in the presence of the Byzantine adversary. Once a node sees 𝑛 − 𝑓 votes for the same value in a round,
it outputs that value, acknowledging its receipt from 𝑞 (line 11).
Reliable Broadcast is expected to satisfy the following specification comprising two safety and two liveness properties:• Integrity (S): For any two honest nodes 𝑝 and 𝑞, if 𝑝 outputs(𝑞, 𝑟, 𝑣), then 𝑞 must have reliably broadcast 𝑣 at round 𝑟 .
• Agreement (S): For any two honest nodes 𝑝 1 and 𝑝 2 , if 𝑝 1 outputs(𝑞, 𝑟, 𝑣 1 ) and 𝑝 2 outputs (𝑞, 𝑟, 𝑣 2 ), then 𝑣 1 = 𝑣 2 .
• Global liveness (L): If an honest node 𝑝 outputs (𝑞, 𝑟, 𝑣), then every
honest node will eventually output (𝑞, 𝑟, 𝑣).
• Validity (L): If an honest node 𝑞 reliably broadcast 𝑣 at round 𝑟 ,then every honest node will eventually output (𝑞, 𝑟, 𝑣).
Intuitively, the agreement and validity properties mean that RB canserve as a reliable broadcast primitive for honest (i.e., non-faulty)
nodes. Global liveness guarantees that all honest nodes eventually
have the same behaviour even if the sender is Byzantine: they either
all output the same value, or none output at all.
We encoded Reliable Broadcast in Bythos, in the same manneras Provable Broadcast. Specifically, a node’s local state is defined asa Record, with each field capturing information such as the values
the node has echoed, voted for or output, the list of nodes fromwhich it has received certain Echo or Vote messages, and so on.

4.1.1 Knowledge-Driven Proofs of Safety. We prove the safety properties in the same fashion as Sec. 2.2.5, incrementally establishing an
inductive invariant that implies both safety properties by devisingknowledge lemmas of different categories. For RB, the knowledge
lemmas in the categories (1)–(4) in Sec. 2.2.5 closely resemble thoseused in the safety proof of PB. As an example, the data persistence
properties in RB can be summarised as: a field in the local state ofan honest node is never overwritten or evolves monotonically (e.g.,
set of received messages only grows). Therefore, for brevity, we
omit the statements of those knowledge lemmas and instead only
list representative implications of knowledge as follows (fixing 𝑞
as the broadcast initiator and 𝑟 as the round):(1) Echo before vote: if an honest node has voted for 𝑣, there is atleast one honest node that echoed 𝑣;(2) Vote integrity: if an honest node voted for 𝑣 and 𝑞 is honest, 𝑞
did reliably broadcast 𝑣 at round 𝑟 ;(3) Integrity: if an honest node output a value 𝑣 and 𝑞 is honest, 𝑞
did reliably broadcast 𝑣 at round 𝑟 ;(4) Agreement: if two honest nodes output, they must output thesame value, regardless of whether 𝑞 is honest.
The properties (3) and (4) are exactly RB’s two safety properties.
4.1.2 Knowledge-Driven Proofs of Liveness. We prove liveness inthe same fashion as Sec. 2.3.3. For each liveness property, we firstdecompose the protocol execution into several phases, so that the
liveness property can be formulated as “the start of the first phaseleads to the end of the last phase”.
For conciseness, we only depict the phase decomposition in Fig. 5
without going into details. As we have done in Sec. 2.3.3, at thestart of each phase, we use local-to-packet knowledge lemmas toinfer which packets appear in the packet soup. Based on the fairdelivery assumption, we know that they will eventually be received.
10

Compositional Verification of Composite Byzantine Protocols

CCS ’24, October 14–18, 2024, Salt Lake City, UT, USA

Algorithm 2 Accountable Confirmer (for node 𝑝)

We then apply knowledge lemmas–especially the packet-to-local
receipt-sensitive ones–for reasoning at the end of the current phase(represented by short arrows in Fig. 5). After dealing with all phases,
we finally bridge them using (Leadsto-Trans). Remarkably, bothglobal liveness and validity share the same last phase. Thanks to theproof modularity via phase decomposition and (Leadsto-Trans),
the proof for this last phase is reused across both properties.

4.2

1: on initialisation:2:

set buffer, fromset, psset, nsset, lcertset, certset to ∅;set acval to ⊥; set confirmed to false

3: action ACSubmit(Value 𝑣):

Accountable Byzantine Confirmer

Our next case study is the Accountable Confirmer (AC) protocol [22], which can be attached to an arbitrary non-synchronous
BFT consensus protocol, via the Accountable Byzantine Consensus (ABC) transformation, to add accountability when the number of Byzantine nodes 𝑓 ′ exceeds the threshold 𝑓 . AC requires
both threshold signature scheme and public-key infrastructure; toavoid ambiguity, we refer to the PKI-based signatures as standard
ones. Given a BFT consensus protocol that satisfies the standard
agreement, validity, and termination properties (statement omitted), ABC produces an accountable BFT consensus protocol that stillsatisfies those properties when 𝑓 ′ ≤ 𝑓 , and additionally satisfies
the accountability (L): if two honest nodes decide different values,
then every honest node eventually detects at least 𝑛 − 2𝑓 Byzantine
nodes and obtains a proof of their culpability. The accountability,
essentially provided by AC, says that if the Byzantine adversary
has compromised the safety of the consensus (which, for a correct protocol, can only happen if 𝑓 ′ > 𝑓 ), then every honest node
will eventually detect this, and moreover, identify the culprits andproduce a cryptographically verifiable proof of their misbehaviour.
It is surprising that accountability can be added to an arbitrary
underlying protocol–regardless of the concrete value of 𝑓 –without
any knowledge of its internals, and moreover, without increasing
overall communication complexity in the normal case. The intuition
behind AC (outlined in Algorithm 2) and the ABC transformation,
however, is simple. Basically, the accountable protocol produced by
ABC can be regarded as the sequential composition of its underlying consensus protocol and AC. Whenever a node decides a value
𝑣 in the underlying consensus, the node submits 𝑣 in AC (line 3)
by broadcasting 𝑣 along with a partial signature and a standard
signature for 𝑣 (line 5). When a node receives a Submit message
containing the node’s submitted value and valid signatures, it willrecord the sender and the signatures (lines 10–11). Once the numberof collected senders reaches 𝑛 − 𝑓 , a node confirms its submitted
value (a confirmation in AC is the decision in the transformed
accountable protocol), combines the previously recorded partial
signatures into a light certificate and broadcasts it (lines 12–14). If a
confirmed node sees light certificates for conflicting values—whichsuggests that safety might be violated in the underlying consensus—
it broadcasts a full certificate consisting of all recorded senders andstandard signatures from them (lines 15–18). Since the thresholdof confirmation is 𝑛 − 𝑓 , two full certificates for conflicting values
must intersect in at least 𝑛 − 2𝑓 nodes which signed different values,
and the associated standard signatures can be used as positive proofof misbehaviour, thus providing accountability (line 22).
We note that two different signature schemes are used here
to control communication complexity and accommodate different
axioms on cryptographic primitives. Interested readers can find thefull details in the original paper [22].

⊲ called only once4:

acval := 𝑣

5:send Submit(𝑣, partial_sign𝑝 (𝑣), sign𝑝 (𝑣)) to all nodes

6:

for each Submit message msg in buffer:process msg according to line 8

7:

8: upon receiving Submit(𝑣, ps, 𝑠) from node 𝑞:

if acval is ⊥: add this Submit message to buffer
else if ps and 𝑠 can be verified wrt. 𝑣 with 𝑞’s public key,acval = 𝑣, confirmed = false and 𝑞 ∉ fromset:
add 𝑞 to fromset; add ps to psset; add (𝑞, 𝑠) to nsset
11:
9:

10:

12: upon | fromset | ≥ 𝑛 − 𝑓 :13:

confirmed := true

14:

send LightCert(acval, combine(psset)) to all nodes

15: upon receiving LightCert(𝑣, cs):
16:

if cs can be verified wrt. 𝑣: add (𝑣, cs) to lcertset

17: upon confirmed = true and ∃(𝑣, cs), (𝑣 ′ , cs ′ ) ∈ lcertset, 𝑣 ≠ 𝑣 ′ :18:send Cert(𝑣, nsset) to all nodes

19: upon receiving Cert(𝑣, nss):
20:

if |nss| ≥ 𝑛 − 𝑓 and for any (𝑞, 𝑠) ∈ nss, 𝑠 can be verified
wrt. 𝑣 with 𝑞’s public key: add (𝑣, nss) to certset

21: upon ∃(𝑣, nss), (𝑣 ′ , nss ′ ) ∈ certset, 𝑣 ≠ 𝑣 ′ :22:detect {𝑞 : ∃𝑠, 𝑠 ′, (𝑞, 𝑠) ∈ nss ∧ (𝑞, 𝑠 ′ ) ∈ nss′ }4.2.1 Uncovering Implicit Assumptions. In the process of formalising AC, we discovered an implicit assumption required for the
protocol to be live. Concretely, to ensure that the transformed accountable protocol satisfies termination and agreement, AC has
to satisfy terminating convergence, a liveness property: if 𝑓 ′ ≤ 𝑓
and all honest nodes submit the same value 𝑣, then 𝑣 is eventuallyconfirmed by every honest node. In the original formulation of AC(i.e., Algorithm 2 excluding grey parts), this property may nothold due to asynchrony, even if we assume fair delivery. To see
that, consider a “slow” node that submits only after all the othernodes have submitted. Before it submits, when receiving Submit
messages from other nodes, the slow node would do nothing due
to the check on line 10. Consequently, the poor slow node may nothave a chance to reach the required 𝑛 − 𝑓 threshold and confirm,
since it may not receive enough Submit messages after it submits.
To address this issue, nodes that have not yet submitted must
buffer (i.e., store) received Submit messages until they submit andcan thus examine the messages to discern whether to accept themor not. This buffering introduces extra complexity in both the implementation and knowledge lemma proofs, requiring that the procInt
handler that processes the ACSubmit event (line 3) call procMsg ina loop over all received and buffered messages.
4.2.2 Liveness Proof. With the buffering in place, the liveness proof
proceeds similarly to that for Reliable Broadcast, by a decomposition into phases. Terminating convergence is proven in a single
11

CCS ’24, October 14–18, 2024, Salt Lake City, UT, USA

Qiyuan Zhao, George Pîrlea, Karolina Grzeszkiewicz, Seth Gilbert, and Ilya Sergey

Table 1: Statistics of the formal development, including
Bythos and all formalised protocols, in lines of Coq code.

phase: the “submit” phase starts once all honest nodes submit thesame value, and hence broadcast Submit messages with signatures,and ends when these messages are received by all honest nodes.
At that point, every honest node will confirm since 𝑛 − 𝑓 ′ ≥ 𝑛 − 𝑓 .
Accountability is proven in two phases: (1) a “confirm” phase thatstarts once two honest nodes confirmed different values and hence
broadcast conflicting light certificates, and (2) a “detect” phase thatstarts once the two honest nodes received conflicting light certificates and hence broadcast their full certificates. Once the second
phase ends, all honest nodes will have received two conflicting fullcertificates and be able to detect at least 𝑛 − 2𝑓 culprits (line 22).

4.3

Accountable Reliable Broadcast

The Accountable Byzantine Consensus paper [22] also defines a generalised ABC transformation that can be applied to any agreement
protocol, including Reliable Broadcast. In this section, we demonstrate our composition of the Accountable Confirmer from Sec. 4.2
with the Reliable Broadcast instance we formalised in Sec. 4.1. The
definition of the novel composed protocol, which we call ARB, isstraightforward conceptually. The formalisation of the composition
is more involved, as we have already detailed in Sec. 3.3. The connection between RB and AC is done by trigger_procMsg (cf. Sec. 3.3),
which fires the ACSubmit event in AC once RB outputs.
4.3.1 Compositional Liveness Proof. Based on the validity of RB(cf. Sec. 4.1) and the terminating convergence of AC (cf. Sec. 4.2.1), wewant to prove the overall validity of the ARB composition, whichstates that if an honest node 𝑞 reliably broadcast 𝑣, then 𝑣 is eventually confirmed by every honest node, under the assumption thatthe threshold 𝑓 is not breached. This proof follows the same technique of decomposition into phases described earlier, except now
the phases are the two different protocols, RB and AC. Similar tothe previous proofs, the most involved part is showing that the endof one phase (in this case, when all honest nodes output a value 𝑣 inRB) corresponds to the beginning of the next phase (all honest nodes
in AC submitted 𝑣). We prove this correspondence by propagatingknowledge across the protocol boundary via specialised invariants,
which follow from the implementation of trigger_procMsg and theinvariants of RB and AC. One of those invariants in particular,
which we refer to as the connector, ensures that AC will proceed
as expected following RB; it states that if an honest node output avalue 𝑣 in RB, then it submitted 𝑣 in AC. By reusing the livenessproofs of RB validity and AC terminating convergence, and integrating them with the connector and (Leadsto-Trans), the Coq
proof of overall validity is condensed to merely 7 lines.

5

Library

Component

Spec

Proof

Total

Bythos(Sec. 3)

System (Sec. 3.1)
Liveness (Sec. 3.2)
Composition (Sec. 3.3)
Utilities
Total

729
160
329
184
1402

465
181
255
157
1058

1194
341
584
341
2460

Provable
Broadcast(Sec. 2)

Implementation (Sec. 2.1)
Safety (Sec. 2.2)
Liveness (Sec. 2.3)
Composition (Sec. 2.4)
Total

121
404
92
85
702

6
320
67
10†
403

127
724
159
95
1105

Reliable
Broadcast(Sec. 4.1)

Implementation
Safety (Sec. 4.1.1)
Liveness (Sec. 4.1.2)
Total

130
448
144
722

6
432
161
599

136
880
305
1321

Accountable
Confirmer(Sec. 4.2)

Implementation
SafetyLiveness (Sec. 4.2.2)
Total

237
619
172
1028

109
709
200
1018

346
1328
372
2046

Accountable
Reliable
Broadcast(Sec. 4.3)

Implementation
Connector (Sec. 4.3.1)
Liveness (Sec. 4.3.1)
Total

33
48
3
84

0
92
7
99

33
140
10
183

† For both twice-iterated and thrice-iterated PB, each one is 5 lines.

them. To ensure this function’s correctness, after implementing it,
we immediately prove that its implementation satisfies a certain
specification, which is later used in the proof of accountability.
The total size of our Coq development is around 7100 lines ofcode. The trusted shim layer in OCaml (cf. Sec. 3.4), not included
into the statistics, contains around 200 lines of code.
Both the Provable Broadcast and Reliable Broadcast requireroughly 1000 lines of Coq proof each. The proof of Accountable
Confirmer, however, is almost twice as long. The fundamental reason for this is that, because of the buffering (explained in Sec. 4.2.1),
procInt may invoke procMsg an indefinite number of times (determined by the size of buffer). Therefore, in the safety proof, wemust first prove that the inductive invariant is preserved under any
Delivery step, and then do the same for any Internal step. This
two-step process leads to the inflation of the proof size.
Limitations. The major limitation of Bythos is its scalability, inthe sense that it might require substantial human efforts to verify acomplex Byzantine protocol in Bythos. When verifying the protocols listed in Tab. 1, all knowledge lemmas were discovered manually through trial and error, and the proofs showing that they form
inductive invariants were also manually created (by typing proof
scripts). Each of these protocols has 10 to 20 knowledge lemmas; accordingly, for more complex protocols, our knowledge-driven proof
methodology will necessitate a more challenging knowledge discovery process and longer proofs. Moreover, some protocols may
involve advanced features such as probabilistic termination [4],which Bythos is unable to help reason about.

Discussion

In this section, we discuss both the quantitative and qualitative
aspects of our verification work from a user’s perspective.
Proof effort. We summarise our verification efforts in Tab. 1. Notably, the number of Proof lines in protocol implementation may be
non-zero, since some definitions are constructed using tactics in the
proof mode, and we might reason about some definitions as soon
as defining them. For example, the implementation of Accountable
Confirmer requires a detecting function (cf. line 22 in Algorithm 2),
which, given a list of full certificates, returns all culprits within
12

Compositional Verification of Composite Byzantine Protocols

6

CCS ’24, October 14–18, 2024, Salt Lake City, UT, USA

Table 2: Comparison with existing frameworks for machineassisted verification of distributed protocols on the groundsof supporting proofs of Safety, Liveness, Byzantine network, allowing for horizontal protocol Composition, being
Foundational, and capable of generating Executable code.

Related Work

Computer-aided verification of distributed protocols, both interactive and automated, has been a very active research area for the last
decade. Tab. 2 summarises the related approaches and frameworks.
Frameworks for foundational verification. The seminal work on
IronFleet [30] has presented the first framework for deductive verification of both safety and liveness properties of real-world executable distributed systems. IronFleet is implemented on top of
the deductive Dafny verifier [38], which was also used for embedding the specifications in the style of Lamport’s TLA [36] and therespective rules of Linear Temporal Logic (LTL), similarly to the
TLA+ embedding into Coq employed by Bythos. IronFleet did notencode Byzantine network semantics and, thus, did not allow for
verification of BFT protocols in the respective environment. It also
did not consider verification of composite protocols. While thelogic of IronFleet and the semantics of protocol verified in it has
been encoded in terms of Dafny language, Dafny itself relies on an
Z3 SMT solver [23] to discharge the verification conditions (VCs).
Therefore, verification in IronFleet can be considered foundationalwith the reservation that one trusts the correctness of Dafny VC
generator and the underlying SMT solver (hence ✓SMT in Tab. 2).
Developed concurrently with IronFleet, Verdi [63] is a foundational framework embedded into Coq aiming to reduce the trusted
code base down to the implementation of Coq proof checker. Usedto verify the safety specification of Raft consensus protocol [64],Verdi allows for a limited form of proof composition with the mechanism of verified system transformers that allow for strengthening
assumptions about (non-Byzantine) network semantics.
Toychain [50] was the first attempt to formalise the safety ofa BFT blockchain protocol in a foundational proof assistant (alsoCoq), executable via code extraction to OCaml, although its network
semantics did not account for the Byzantine behaviours. Thanks to
its simplicity, the Toychain approach to formulate the semantics
of blockchain protocols has inspired a number of follow-up safety
verification efforts on Algorand [7], Casper [47], HotStuff [18], as
well as a proof of safety and liveness of Nakamoto Proof of Stakeblockchain consensus in a synchronous network [61].
Disel [57] was the first framework to tackle compositional foundational verification of composite protocols by implementing a
version of Separation Logic [56] and allowing its logical assertions
to quantify over the network state spanning different sub-protocol
instances. Disel’s verification capabilities have been later enhancedin the works on Aneris [34] and Grove [58], both implemented on
top of Coq-based Iris separation logic embedding [31] and allowing
for node-local concurrency and crash recovery, respectively. Neither Aneris nor Grove support reasoning about Byzantine systems,
nor do they allow to verify liveness properties.
TLC (Temporal Logic of Components) [29] is a Coq-based framework that features a temporal program logic and offers inference
rules to reason about safety and liveness of vertically-composed
distributed system stacks. We conjecture that TLC should be able
to accommodate proofs about horizontally composed protocols as
well, yet the TLC paper does not showcase it in that capacity. TLC
does not support proofs about Byzantine fault tolerance.
Velisarios [54] and Asphalion [62] are two verification frameworks embedded into Coq that aim specifically at reasoning about

Framework

Safe Live Byz Comp Found Exec

IronFleet [30]2015
Verdi [63]2015
PSync [26]2016
Ivy [46]
2016
Toychain [50]2018
Disel [57]2018
Padon et al. [45]2018
Taube et al. [59]2018
Velisarios [54]2018
Asphalion [62]2019
Aneris [34]2020
TLC [29]2020
Losa & Dodds [42]2020
Thomsen & Spitters [61] 2021
Carr et al. [18]2022
ByMC [32]2023Grove [58]2023
LiDO [53]2024
Bythos (this work)
2024

✓
✓
✓
✓
✓
✓
✓
✓
✓
✓
✓
✓
✓
✓
✓
✓
✓
✓
✓

✓P

✓SMT
✓

✓
✓
✓

✓

✓
✓

✓
✓

✓
✓
✓

✓
✓
✓
✓

✓P

✓A
✓
✓
✓P
✓A
✓S
✓A

✓
✓
✓
✓

✓P
✓A

✓
✓

✓
✓
✓
✓

✓
✓
✓
✓
✓

✓
✓
✓

✓
✓
✓

safety specification of BFT consensus protocols and are based on
Logic of Events [12]. Stating properties and reasoning in the Logicof Events is quite different in flavour from the state-based inductive
proofs conducted in Bythos. That said, the knowledge lemmas wephrase in our proofs are reminiscent to the rules of the knowledge
calculus employed by Asphalion. Both Velisarios and Asphalion
leave reasoning about liveness properties for the future work.
Finally, LiDO [53] is a recent verification framework, whichallows one to verify BFT protocols for both safety and liveness, yetwhose take on composition is quite different from ours. Specifically,
LiDO achieves vertical composition via refinement, allowing one
to verify validity of optimisations within the same protocol. In
contrast, Bythos allows for horizontal composition, i.e., reusing
proofs when assembling multi-stage protocols from basic ones.
Tools for automated verification. Concurrently with foundationalverification frameworks, a number of domain-specific tools for distributed protocol verification have been proposed, each exploiting
certain assumptions about the systems being verified. Those approaches typically sacrifice foundational guarantees, axiomatising
the semantics of their programming language, as well as the ability
to compose specifications, for the sake of proof automation.
PSync [26] is a domain-specific language based on the heard-ofmodel [21], which allows the user to implement and automaticallyverify their protocols that assume round-based communication ina partially synchronous model. It supports checking of both safety
and liveness properties that are expressible in a specialised fragmentof first-order logic and can be proved using SMT solvers [25].
Ivy [46] is an automated verification tool that expects the protocols, their specifications, and the inductive invariants provided by
the user as quantified formulas to produce verification conditions
13

CCS ’24, October 14–18, 2024, Salt Lake City, UT, USA

Qiyuan Zhao, George Pîrlea, Karolina Grzeszkiewicz, Seth Gilbert, and Ilya Sergey

that fit into a specific decidable fragment of the first-order logic [51].
Ivy has been later demonstrated to be able to encode and prove
liveness specifications by reducing them to safety properties [45]; it
was also extended to produce executable C++ code from the model
definitions [59] and used to verify both safety and liveness of a simplified Stellar Consensus Protocol [42]. Due to the first-order natureof the Ivy logic, it does not allow for specification composition andreuse of proofs about independently verified protocols.
ByMC [32] is a symbolic model checker that automates safety
and liveness proofs for BFT protocols [11]. The proof is done via
the decomposition similar to what is offered by Bythos. That said,
for the verification, ByMC relies on an unverified translation ofan protocol’s pseudo-code to a threshold automaton. Similarly toother automated tools, ByMC imposes restrictions on the shapesof properties it can express, requiring them to be for the form
∀𝑅 ∈ N, 𝜙 [𝑅], where 𝜙 is a quantifier-free formula in LTL. It means,in particular, that ByMC would not be able to directly encode andprove the property (1) of Reliable Broadcast from Sec. 4.1.1.

7Conclusion

The Bythos framework, together with its methodology, streamlines the verification of Byzantine Fault-Tolerant protocols and theircompositions. Bythos allows users to encode protocols in a way
closely aligned with their informal specifications in pseudocode
and to reason about them using a standard toolset of invariantbased safety reasoning and TLA-based liveness proofs. Throughsystematic decomposition, correctness proofs, especially the liveness ones, can be reused within a standalone protocol or acrosscomponents of a composite protocol. Beyond these aspects, ournovel knowledge-driven proof methodology clarifies causal relations within a protocol and structures its correctness proof in an
incremental fashion, thereby rendering the proof more tractable.

Acknowledgments
We thank Ittai Abraham for his comments. We also thank the anonymous CCS’24 reviewers for their feedback. This work was partially
supported by a Singapore Ministry of Education (MoE) Tier 3 grant“Automated Program Repair” MOE-MOET32021-0001, MoE Tier 1
grant T1 251RES2108 “Automated Proof Evolution for Verified Software Systems”, and by Sui Academic Research Award.

Liveness and synchrony. We conclude with a brief discussion on
the nature of liveness proofs supported by approaches from Tab. 2.
Due to the famous FLP impossibility result [28], one would needto make certain assumptions about synchrony in the network toestablish a desired termination property of any fault-tolerant consensus protocol. To wit, the work by Thomsen and Spitters proves
liveness of Nakamoto-style blockchain consensus assuming strong
synchrony [61], where an upper bound on the time it takes to deliver
a message is statically determined—hence the mark ✓S in Tab. 2.
With the same rationale, IronFleet [30], PSync [26], TLC [29],and LiDO [53] assume partially synchronous network (✓P ) [27], inwhich the message delivery latency has a fixed bound that is guaranteed to hold after certain unspecified moment a.k.a. global synchronisation time (GST). Each of those frameworks encodes partial
synchrony differently: IronFleet imposes additional assumptions on
the considered executions of the specific protocol in question [30,§5.1.4]; PSync adds the GST existence to the axiomatisation of the
network semantics in the first-order logic [26, §5.3]; TLC features
an explicit logical rule postulating the existence of GST [29, Fig. 11];
LiDO’s handling of GST is done semantically at the level of system
traces [53, §2.4], similarly to that of PSync. Despite being the closest in its expressive power to Bythos, LiDO does not offer a proof
system (i.e., logic) for liveness proofs (e.g., by means of TLA-stylerules): all its liveness proofs are in terms of explicit execution traces.
Similarly to Ivy [42, 45] and ByMC [11], Bythos is geared towards proofs of eventual liveness in an asynchronous network undera fairness assumption (✓A ), which is sufficient to state many usefulspecifications (as we have shown in Sec. 2 and Sec. 4)—though someproblems (like deterministic fault-tolerant consensus), are impossible in an asynchronous network. Adopting the weakest form ofsynchrony in Bythos has allowed for very short liveness proofs
via TLA-style logic rules (as compared to much more intricate formalism of TLC [29]), as well as compositional liveness verification.
Moreover, proving protocol liveness in asynchrony immediately
implies protocol liveness in synchrony and partial synchrony. Thatsaid, we recognise the advantage of supporting partial synchrony
assumptions, and consider it our future work.

Data Availability
The artefact with a snapshot of the Coq development accompanying
this paper is available online [66]. It contains Bythos source codeand the implementation of all case studies from Sec. 2 and Sec. 4.

References[1] Ittai Abraham. 2022.
Linear PBFT: a gentle introduction to Practical Byzantine Fault Tolerance.
https://decentralizedthoughts.github.io/
2022-11-20-pbft-via-locked-braodcast/[2] Ittai Abraham. 2022. Provable Broadcast. https://decentralizedthoughts.github.
io/2022-09-10-provable-broadcast/[3] Ittai Abraham. 2022. Two Round HotStuff. https://decentralizedthoughts.github.
io/2022-11-24-two-round-HS/[4] Ittai Abraham, Dahlia Malkhi, and Alexander Spiegelman. 2019. Asymptotically
Optimal Validated Asynchronous Byzantine Agreement. In PODC. ACM. https://doi.org/10.1145/3293611.3331612[5] Danel Ahman, Cédric Fournet, Catalin Hritcu, Kenji Maillard, Aseem Rastogi,
and Nikhil Swamy. 2018. Recalling a witness: foundations and applications ofmonotonic state. Proc. ACM Program. Lang. 2, POPL (2018). https://doi.org/10.
1145/3158153[6] Mustafa Al-Bassam, Alberto Sonnino, Shehar Bano, Dave Hrycyszyn, and George
Danezis. 2018. Chainspace: A Sharded Smart Contracts Platform. In NDSS. The
Internet Society. https://www.ndss-symposium.org/wp-content/uploads/2018/02/ndss2018_09-2_Al-Bassam_paper.pdf[7] Musab A. Alturki, Jing Chen, Victor Luchangco, Brandon M. Moore, Karl Palmskog, Lucas Peña, and Grigore Rosu. 2019. Towards a Verified Model of the Algorand Consensus Protocol in Coq. In FM Workshops (LNCS, Vol. 12232). Springer.
https://doi.org/10.1007/978-3-030-54994-7_27[8] Andrew W Appel. 2001. Foundational Proof-Carrying Code. In LICS. IEEE Computer Society. https://doi.org/10.1109/LICS.2001.932501[9] Hagit Attiya and Jennifer L. Welch. 2004. Distributed computing - fundamentals,
simulations, and advanced topics (2. ed.). Wiley.
[10] Idan Berkovits, Marijana Lazic, Giuliano Losa, Oded Padon, and Sharon Shoham.
2019. Verification of Threshold-Based Distributed Algorithms by Decomposition
to Decidable Logics. In CAV (LNCS, Vol. 11562). Springer. https://doi.org/10.1007/
978-3-030-25543-5_15[11] Nathalie Bertrand, Vincent Gramoli, Igor Konnov, Marijana Lazic, Pierre Tholoniat, and Josef Widder. 2022. Holistic Verification of Blockchain Consensus.
In DISC (LIPIcs, Vol. 246). Schloss Dagstuhl - Leibniz-Zentrum für Informatik.
https://doi.org/10.4230/LIPICS.DISC.2022.10[12] Mark Bickford, Robert Constable, and Vincent Rahli. 2012. The Logic of Events,a framework to reason about distributed systems. In Languages for Distributed
Algorithms (LADA) workshop.
14

Compositional Verification of Composite Byzantine Protocols

CCS ’24, October 14–18, 2024, Salt Lake City, UT, USA[40] Pierre Letouzey. 2008. Extraction in Coq: An Overview. In CiE (LNCS, Vol. 5028).
Springer. https://doi.org/10.1007/978-3-540-69407-6_39[41] Benoît Libert, Marc Joye, and Moti Yung. 2014. Born and raised distributively:
fully distributed non-interactive adaptively-secure threshold signatures withshort shares. In PODC. ACM. https://doi.org/10.1145/2611462.2611498[42] Giuliano Losa and Mike Dodds. 2020. On the Formal Verification of the Stellar Consensus Protocol. In 2nd Workshop on Formal Methods for Blockchains,
FMBC@CAV (OASIcs, Vol. 84). Schloss Dagstuhl - Leibniz-Zentrum für Informatik.
https://doi.org/10.4230/OASICS.FMBC.2020.9[43] Loi Luu, Viswesh Narayanan, Chaodong Zheng, Kunal Baweja, Seth Gilbert, andPrateek Saxena. 2016. A Secure Sharding Protocol For Open Blockchains. In CCS.
ACM. https://doi.org/10.1145/2976749.2978389[44] Hammurabi Mendes, Maurice Herlihy, Nitin Vaidya, and Vijay K Garg. 2015.
Multidimensional agreement in byzantine systems. Distributed Computing 28, 6(2015). https://doi.org/10.1007/S00446-014-0240-5[45] Oded Padon, Jochen Hoenicke, Giuliano Losa, Andreas Podelski, Mooly Sagiv,
and Sharon Shoham. 2018. Reducing liveness to safety in first-order logic. Proc.
ACM Program. Lang. 2, POPL (2018). https://doi.org/10.1145/3158114[46] Oded Padon, Kenneth L. McMillan, Aurojit Panda, Mooly Sagiv, and Sharon
Shoham. 2016. Ivy: safety verification by interactive generalization. In PLDI.
ACM. https://doi.org/10.1145/2908080.2908118[47] Karl Palmskog, Milos Gligoric, Lucas Pena, Brandon Moore, and Grigore Roşu.
2018. Verification of Casper in the Coq proof assistant. (2018). https://core.ac.
uk/download/pdf/161954227.pdf.
[48] George Pîrlea. 2019. Toychain: Formally Verified Blockchain Consensus. Master’s
thesis. University College London.
[49] George Pîrlea. 2021. Errors Found in Distributed Protocols. https://github.com/
dranov/protocol-bugs-list Online; last accessed 29 April 2024.
[50] George Pîrlea and Ilya Sergey. 2018. Mechanising Blockchain Consensus. In CPP.
ACM. https://doi.org/10.1145/3167086[51] Ruzica Piskac, Leonardo Mendonça de Moura, and Nikolaj Bjørner. 2010. Deciding
Effectively Propositional Logic Using DPLL and Substitution Sets. J. Autom.
Reason. 44, 4 (2010). https://doi.org/10.1007/S10817-009-9161-6[52] Amir Pnueli. 1977. The Temporal Logic of Programs. In FOCS. IEEE Computer
Society. https://doi.org/10.1109/SFCS.1977.32[53] Longfei Qiu, Yoonseung Kim, Ji-Yong Shin, Jieung Kim, Wolf Honore, and Zhong
Shao. 2024. LiDO: Linearizable Byzantine Distributed Objects with RefinementBased Liveness Proofs. PACMPL 8, PLDI (2024). https://doi.org/10.1145/3656423[54] Vincent Rahli, Ivana Vukotic, Marcus Völp, and Paulo Jorge Esteves Veríssimo.
2018. Velisarios: Byzantine Fault-Tolerant Protocols Powered by Coq. In ESOP
(LNCS, Vol. 10801). Springer. https://doi.org/10.1007/978-3-319-89884-1_22[55] Michael K. Reiter. 1994. Secure Agreement Protocols: Reliable and Atomic GroupMulticast in Rampart. In CCS. ACM. https://doi.org/10.1145/191177.191194[56] John C. Reynolds. 2002. Separation Logic: A Logic for Shared Mutable Data
Structures. In LICS. IEEE. https://doi.org/10.1109/LICS.2002.1029817[57] Ilya Sergey, James R. Wilcox, and Zachary Tatlock. 2018. Programming andProving with Distributed Protocols. PACMPL 2, POPL (2018). https://doi.org/10.
1145/3158116[58] Upamanyu Sharma, Ralf Jung, Joseph Tassarotti, M. Frans Kaashoek, and Nickolai
Zeldovich. 2023. Grove: a Separation-Logic Library for Verifying Distributed
Systems. In SOSP. ACM. https://doi.org/10.1145/3600006.3613172[59] Marcelo Taube, Giuliano Losa, Kenneth L. McMillan, Oded Padon, Mooly Sagiv,
Sharon Shoham, James R. Wilcox, and Doug Woos. 2018. Modularity for decidability of deductive verification with applications to distributed systems. In PLDI.
ACM. https://doi.org/10.1145/3192366.3192414[60] The Coq Development Team. 2024. The Coq Reference Manual – Release 8.19.0.
https://coq.inria.fr/doc/V8.19.0/refman.
[61] Søren Eller Thomsen and Bas Spitters. 2021. Formalizing Nakamoto-Style Proofof Stake. In CSF. IEEE. https://doi.org/10.1109/CSF51468.2021.00042[62] Ivana Vukotic, Vincent Rahli, and Paulo Jorge Esteves Veríssimo. 2019. Asphalion:
trustworthy shielding against Byzantine faults. Proc. ACM Program. Lang. 3,
OOPSLA (2019). https://doi.org/10.1145/3360564[63] James R. Wilcox, Doug Woos, Pavel Panchekha, Zachary Tatlock, Xi Wang,
Michael D. Ernst, and Thomas E. Anderson. 2015. Verdi: a framework for implementing and formally verifying distributed systems. In PLDI. ACM. https://doi.org/10.1145/2737924.2737958[64] Doug Woos, James R. Wilcox, Steve Anton, Zachary Tatlock, Michael D. Ernst,
and Thomas E. Anderson. 2016. Planning for change in a formal verification of theRaft consensus protocol. In CPP. ACM. https://doi.org/10.1145/2854065.2854081[65] Maofan Yin, Dahlia Malkhi, Michael K Reiter, Guy Golan Gueta, and Ittai Abraham. 2019. HotStuff: BFT Consensus with Linearity and Responsiveness. In
PODC. ACM. https://doi.org/10.1145/3293611.3331591[66] Qiyuan Zhao, George Pîrlea, Karolina Grzeszkiewicz, Seth Gilbert, and Ilya Sergey.
2024. Bythos: Compositional Verification of Composite Byzantine Protocols. Software
Artefact. https://doi.org/10.5281/zenodo.12787570[13] Gabriel Bracha. 1984. An Asynchronou [(n-1)/3]-Resilient Consensus Protocol.
In PODC. ACM. https://doi.org/10.1145/800222.806743[14] Gabriel Bracha. 1987. Asynchronous Byzantine Agreement Protocols. Inf. Comput.
75, 2 (1987). https://doi.org/10.1016/0890-5401(87)90054-X[15] Ethan Buchman. 2016. Tendermint: Byzantine Fault Tolerance in the Age ofBlockchains. Master’s thesis. University of Guelph.
[16] Ethan Buchman, Jae Kwon, and Zarko Milosevic. 2018. The latest gossip on BFT
consensus. CoRR abs/1807.04938 (2018). arXiv:1807.04938 http://arxiv.org/abs/
1807.04938[17] Vitalik Buterin and Virgil Griffith. 2017. Casper the Friendly Finality Gadget.
CoRR abs/1710.09437 (2017). http://arxiv.org/abs/1710.09437[18] Harold Carr, Christa Jenkins, Mark Moir, Victor Cacciari Miraldo, and Lisandra
Silva. 2022. Towards Formal Verification of HotStuff-Based Byzantine Fault
Tolerant Consensus in Agda. In NASA Formal Methods (LNCS, Vol. 13260). Springer.
https://doi.org/10.1007/978-3-031-06773-0_33[19] Miguel Castro and Barbara Liskov. 1999. Practical Byzantine Fault Tolerance. In
OSDI. USENIX Association. https://dl.acm.org/citation.cfm?id=296824[20] Tej Chajed. 2024. TLA in Coq. https://github.com/tchajed/coq-tla.
[21] Bernadette Charron-Bost and André Schiper. 2009. The Heard-Of model: computing in distributed systems with benign faults. Distributed Comput. 22, 1 (2009).
https://doi.org/10.1007/S00446-009-0084-6[22] Pierre Civit, Seth Gilbert, Vincent Gramoli, Rachid Guerraoui, and Jovan Komatovic. 2022. As easy as ABC: Optimal (A)ccountable (B)yzantine (C)onsensus iseasy!. In IPDPS. IEEE. https://doi.org/10.1109/IPDPS53621.2022.00061[23] Leonardo Mendonça de Moura and Nikolaj S. Bjørner. 2008. Z3: An Efficient
SMT Solver. In TACAS (LNCS, Vol. 4963). Springer. https://doi.org/10.1007/
978-3-540-78800-3_24[24] Danny Dolev and Andrew Chi-Chih Yao. 1983. On the security of public key
protocols. IEEE Trans. Inf. Theory 29, 2 (1983). https://doi.org/10.1109/TIT.1983.
1056650[25] Cezara Dragoi, Thomas A. Henzinger, Helmut Veith, Josef Widder, and Damien
Zufferey. 2014. A Logic-Based Framework for Verifying Consensus Algorithms. In
VMCAI (LNCS, Vol. 8318). Springer. https://doi.org/10.1007/978-3-642-54013-4_
10[26] Cezara Dragoi, Thomas A. Henzinger, and Damien Zufferey. 2016. PSync: apartially synchronous language for fault-tolerant distributed algorithms. In POPL.
ACM. https://doi.org/10.1145/2837614.2837650[27] Cynthia Dwork, Nancy A. Lynch, and Larry J. Stockmeyer. 1988. Consensus in
the presence of partial synchrony. J. ACM 35, 2 (1988). https://doi.org/10.1145/
42282.42283[28] Michael J. Fischer, Nancy A. Lynch, and Mike Paterson. 1985. Impossibility ofDistributed Consensus with One Faulty Process. J. ACM 32, 2 (1985). https://doi.org/10.1145/3149.214121[29] Jeremiah Griffin, Mohsen Lesani, Narges Shadab, and Xizhe Yin. 2020. TLC:
temporal logic of distributed components. Proc. ACM Program. Lang. 4, ICFP
(2020). https://doi.org/10.1145/3409005[30] Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R. Lorch, Bryan Parno,
Michael L. Roberts, Srinath T. V. Setty, and Brian Zill. 2015. IronFleet: proving
practical distributed systems correct. In SOSP. ACM. https://doi.org/10.1145/
2815400.2815428[31] The Iris Project. 2022. Iris: a Higher-Order Concurrent Separation Logic
Framework, implemented and verified in the Coq proof assistant.
https://iris-project.org/ Online; last accessed 29 April 2024.
[32] Igor Konnov, Marijana Lazic, Ilina Stoilkovska, and Josef Widder. 2023. Survey on
Parameterized Verification with Threshold Automata and the Byzantine Model
Checker. Log. Methods Comput. Sci. 19, 1 (2023). https://doi.org/10.46298/
LMCS-19(1:5)2023[33] Igor V. Konnov, Marijana Lazic, Helmut Veith, and Josef Widder. 2017. A shortcounterexample property for safety and liveness verification of fault-tolerant
distributed algorithms. In POPL. ACM. https://doi.org/10.1145/3009837.3009860[34] Morten Krogh-Jespersen, Amin Timany, Marit Edna Ohlenbusch, Simon Oddershede Gregersen, and Lars Birkedal. 2020. Aneris: A Mechanised Logic for Modular Reasoning about Distributed Systems. In ESOP (LNCS, Vol. 12075). Springer.
https://doi.org/10.1007/978-3-030-44914-8_13[35] Leslie Lamport. 1977. Proving the Correctness of Multiprocess Programs. IEEE
Trans. Software Eng. 3, 2 (1977). https://doi.org/10.1109/TSE.1977.229904[36] Leslie Lamport. 2002. Specifying Systems, The TLA+ Language and Tools for
Hardware and Software Engineers. Addison-Wesley. http://research.microsoft.
com/users/lamport/tla/book.html[37] Leslie Lamport, Robert E. Shostak, and Marshall C. Pease. 1982. The Byzantine
Generals Problem. ACM Trans. Program. Lang. Syst. 4, 3 (1982). https://doi.org/
10.1145/357172.357176[38] K. Rustan M. Leino. 2010. Dafny: An Automatic Program Verifier for Functional Correctness. In LPAR (LNCS, Vol. 6355). Springer. https://doi.org/10.1007/
978-3-642-17511-4_20[39] Mohsen Lesani, Christian J. Bell, and Adam Chlipala. 2016. Chapar: certified
causally consistent distributed key-value stores. In POPL. ACM. https://doi.org/
10.1145/2837614.2837622
15