From Permissioned to Proof-of-Stake Consensus

The main result of this paper is indeed a “compiler” of the above type, but certain compromises are, or appear to be, unavoidable. First, “sufficiently permissionless” protocols inherently suffer from provable limitations that are not shared by permissioned protocols, and for this reason we focus on the quasi-permissionless setting. In more detail, Lewis-Pye and Roughgarden [62] classify the “permissionlessness of a protocol” – or more accurately, the maximum permissionlessness under which a protocol functions as intended – via a hierarchy with several levels. The permissioned setting is one extreme point of the hierarchy. The next-most restrictive setting is the quasi-permissionless (QP) setting; the assumption here, when specialized to proof-of-stake protocols, is that correct processes with a positive amount of locked-up stake are always active. (But unlike the permissioned setting, the set of such processes can be ever-changing, and correct processes without locked-up stake can be periodically inactive.) The next level in the hierarchy is the dynamically available (DA) setting in which, similar to the sleepy setting of [74], correct processes (including those with locked-up stake) may be periodically offline. Protocols that have even minimal consistency and liveness guarantees in the DA setting cannot, for example, be consistent under asynchrony, or accountable (even in synchrony), or optimistically responsive (even in synchrony) [70, 62, 69]. If the assumptions on the setting are strengthened from DA to QP, all of the properties are achievable [62]. As we are interested in a compiler that preserves properties like consistency and responsiveness, we confine our analysis of permissionless protocols to the QP setting.

The strongest-possible assertion that the compiler’s (permissionless) output protocol shares all the desired properties of its (permissioned) input protocol would be some type of homomorphism between executions (in the spirit of e.g. [32]). Such a homomorphism would map an execution of the permissionless protocol to one or more executions of the permissioned protocol showing that, intuitively, whatever could go wrong in a permissionless execution could have already gone wrong in a permissioned execution. There are several seemingly insurmountable obstacles to achieving this goal. To spell out one just example, such a homomorphism would presumably establish a relationship between the units of participation in the permissionless protocol (e.g., staked coins in a PoS protocol) and those in the original permissioned protocol (e.g., individual processes). But in an execution of the permissionless protocol, coins might well be transferred back and forth between correct and Byzantine processes (even if “locked” for certain durations of the execution), which would seem to translate to an execution of the permissioned protocol with a mobile adversary. Such a homomorphism cannot hope to preserve any property that is achievable with a static adversary but unachievable with a mobile adversary.

Because of the seeming impossibility of a property-preserving mapping between executions of the permissioned and permissionless protocols, we instead prove that our compiler preserves (a long list of) specific properties using direct, property-specific arguments.

Because the set of processes in a permissioned protocol is fixed while that of a permissionless protocol must update periodically (e.g., to reflect changes in processes’ stakes), and because the permissioned protocol is given only as a closed box, any implementation of the desired compiler must presumably execute the permissioned protocol repeatedly, updating the process set appropriately each time. We refer to each execution of the permissioned protocol as an epoch, and this approach to the compiler’s design as epoch-based. The naive hope would then be that the assumed properties of the permissioned protocol hold in each epoch of the permissionless protocol’s execution, and thus also for the overall execution of that protocol.

Neither part of this hope can be carried out without restrictions on the properties we aim to preserve. The first part of the hope breaks down for, for example, properties of the form “eventually, the execution satisfies some predicate $\phi$.” The issue here is that while every (infinite) execution of a permissioned protocol might eventually satisfy $\phi$, there may be no finite epoch length for which subexecutions of the protocol are guaranteed to satisfy $\phi$. The second part of the hope breaks down for properties that are not preserved by the “concatenation” of the executions of two consecutive epochs. For a trivial example, the property that “at most $n$ distinct identifiers ever vote” will be true for a PBFT-style permissioned protocol with a fixed set of $n$ processes, but will not generally be true for any corresponding permissionless protocol (for which there is an unbounded number of identifiers, any of which may acquire stake and vote at some point in an execution).

The hope, then, is that an epoch-based compiler might still be capable of preserving all of the specific properties that one would be interested in preserving. This brings us to the main result of the paper.

Several blockchain systems in practice – such as Sui, Aptos, Cosmos, and Celo – already employ partially synchronous, quasi-permissionless consensus protocols. These systems typically adapt or build upon well-known permissioned protocols like HotStuff [84] (in the case of Aptos and Celo), Tendermint [18] (in the case of Cosmos), or Mysticeti [9] (in the case of Sui). While these protocols achieve significant practical performance and are deployed at scale, they rely on protocol-specific modifications and often embed ad-hoc reconfiguration mechanisms to work in PoS/QP settings. In particular, they are designed and analyzed in a bespoke manner – each new protocol or setting requires revisiting core design choices, reestablishing safety and liveness guarantees, and adapting reconfiguration logic to ensure correctness. To date, there exists no general-purpose method for converting an arbitrary permissioned protocol into a quasi-permissionless PoS protocol with well-defined theoretical guarantees.

Prior theoretical work has investigated how to adapt specific permissioned consensus protocols to PoS or quasi-permissionless settings. However, these approaches, like their practical counterparts, are fundamentally protocol-specific and rely on tightly coupled mechanisms that are not general. For example, Lewis-Pye and Roughgarden [62] construct a quasi-permissionless, PoS version of HotStuff [84] by embedding specialized reconfiguration mechanisms directly into the protocol. Budish et al. [19] similarly transform Tendermint [18] into a quasi-permissionless, PoS protocol, but again this requires bespoke changes tailored to that specific protocol. Sui Lutris [16] is yet another protocol-specific design, featuring a custom hybrid architecture with partial and total ordering, and an ad-hoc epoch-based reconfiguration mechanism. Other systems, such as Hybrid Consensus [73] and PaLa [26], proceed in epochs and incorporate reconfiguration, but are built from the ground up with specific assumptions and analysis for a given protocol architecture. More broadly, reconfiguration – the task of updating the set of validators – has been widely studied [40, 39, 72, 14], but existing solutions embed reconfiguration logic deeply within the protocol’s internal machinery. None of these approaches offer a generic, reusable method for reconfiguration mechanisms or for achieving quasi-permissionless PoS protocols.

This disconnect – between theory, which mainly focuses on permissioned consensus, and practice, which needs permissionless consensus – is precisely what motivates our work. We present the first generic, closed-box transformation that converts any partially synchronous permissioned protocol into a quasi-permissionless PoS protocol, while preserving a rich set of properties: consistency, liveness, optimistic responsiveness, accountability, and all composable log-specific safety properties. Our transformation separates the consensus core from reconfiguration logic, enabling a clean and composable analysis. This modularity provides two key benefits:

• $\mathrm{■}$

  For theorists, it allows continued focus on designing and analyzing permissioned protocols, while ensuring their results can be lifted automatically to the permissionless world.

• $\mathrm{■}$

  For practitioners, it offers a principled and reusable path to deploying proven permissioned protocols in permissionless environments, without redesigning reconfiguration or re-establishing correctness from scratch.

Our transformation acts as a “bridge lemma” between permissioned and permissionless worlds, making decades of theoretical work directly applicable to modern PoS systems.

Naively running an arbitrary permissioned protocol as a subroutine within a PoS protocol – restarting it periodically with a new set of processes reflecting the latest stake amounts – fails to preserve even the most basic properties. Next, we highlight key technical challenges in designing and analyzing our generic compiler, along with the ideas that contribute to our solution.

To address this challenge, we proceed as follows: (1) we extend the interface of Tendermint – though the idea applies to any permissioned protocol – to allow correct processes to stop participating, and (2) we analyze the guarantees provided by this extended protocol. We refer to these enriched versions of permissioned protocols as quit-enhanced permissioned protocols. Given any standard permissioned protocol, in which correct processes are expected to participate forever, the quit-enhanced version behaves identically in terms of internal logic but explicitly permits correct processes to stop executing the protocol. Thus, quit-enhancing a standard permissioned protocol constitutes a closed-box transformation: only the interface is extended, while the internal mechanisms remain unchanged (and untouched). Importantly, quit-enhanced permissioned protocols integrate naturally with our epoch-based structure: the properties of quit-enhanced permissioned protocols extend directly to our setting. With this in mind, we prove that quit-enhanced versions of arbitrary permissioned protocols preserve the key properties of interest (such as consistency and liveness) originally established in the standard permissioned model, and are thus suitable for use within an epoch-based compiler.

To overcome this challenge, we introduce the notion of an epoch-ending block (akin to epoch transition in [73]). When the validators of an epoch $e$ determine that the time has come to end the epoch (the conditions for this are discussed in the “Preserving liveness” paragraph below), they issue special epoch-ending transactions. They then wait for the first finalized block that, along with its ancestors, finalizes epoch-ending transactions from at least a quorum of the epoch’s validators. This uniquely determined block becomes the epoch-ending block and serves as the genesis block for the next epoch. (Any data required to prove finality, such as blocks produced after the epoch-ending one, is retained in the protocol’s history but does not contribute to the transactions finalized in that epoch.)

Our compiler addresses this challenge by ensuring that all correct validators overlap in each epoch (after the network stabilizes) for at least $\mathrm{\ell }$ time, which allows for all new transactions to be finalized. To enforce this, each validator of an epoch $e$ locally measures a period of $\mathrm{\ell }+\mathrm{\Delta }$ time, where $\mathrm{\Delta }$ denotes the known bound on message delays after the network stabilizes (i.e., after GST; cf. Sec.˜2). Given that messages propagate within $\mathrm{\Delta }$ time, this local timing ensures that correct validators overlap for at least $\mathrm{\ell }$ time during the epoch $e$ (assuming the epoch takes place after stabilization). After this $\mathrm{\ell }+\mathrm{\Delta }$ interval elapses, a validator knows the epoch has run long enough and issues an epoch-ending transaction (as previously explained in the “Preserving consistency” paragraph). Because each epoch concludes with the finalization of an epoch-ending block – one that includes epoch-ending transactions from a quorum of validators, and thus from at least one correct validator – it is guaranteed that every epoch following network stabilization runs long enough to ensure finalization of new transactions, in accordance with the $\mathrm{\ell }$-liveness property of the underlying permissioned protocol.

This raises the question: how broad is the class of safety properties we can hope to preserve? Given the epoch-based approach, we must limit ourselves not only to safety properties but to those that are “closed under concatenation”. To formalize this, we focus on log-specific properties – predicates that depend solely on the validators’ running logs of finalized transactions (and not on, say, the precise sequence of messages that led to the creation of those logs). For log-specific properties, “safety” then means that a violation of the property must be evident from a finite-length prefix of (possibly unbounded-length) logs, and “composable” means that the property is preserved under unions of sets of logs. A canonical example of a composable log-specific safety property is an external validity property, such as “every finalized transaction is accompanied by appropriate signatures”. We prove that our transformation preserves, simultaneously, every composable log-specific safety property.

Intuitively, consistency guarantees that logs of correct processes never diverge.

If a protocol satisfies the consistency property against a $\rho$-bounded static adversary, we say the protocol is $\rho$-consistent.

The liveness property ensures that every transaction is finalized within a known time frame after GST.

If a protocol satisfies the $\mathrm{\ell }$-liveness property against a $\rho$-bounded static adversary, we say the protocol is $(\rho ,\mathrm{\ell })$-live.

Informally, the optimistic responsiveness property guarantees that transactions are finalized at network speed whenever all processes are correct.

If a protocol satisfies the ${\mathrm{\ell }}_{\mathrm{or}}$-optimistic responsiveness property against a $\rho$-bounded static adversary, we say that the protocol is $(\rho ,{\mathrm{\ell }}_{\mathrm{or}})$-responsive. Let us briefly compare our definition of ${\mathrm{\ell }}_{\mathrm{or}}$-responsiveness (Sec.˜3.1) and our definition of $\mathrm{\ell }$-liveness (Sec.˜3.1). As shown, ${\mathrm{\ell }}_{\mathrm{or}}\in O(\delta )$, where $\delta$ denotes the actual (and unknown) upper bound on message delays after GST (cf. Sec.˜2), while $\mathrm{\ell }$ may depend on the known upper bound $\mathrm{\Delta }$ and does not need to reflect actual network delays. Thus, while a responsive protocol can finalize transactions at the speed of the network, a live protocol may do so slower, depending on conservative bounds. Importantly, we note that our transformation ensures responsiveness even in non-failure-free executions assuming that all processes do behave correctly after GST.

Accountability is a property ensuring that, if consistency is ever violated, a sufficient number of faulty processes are conclusively identified through undeniable proofs of guilt. We begin by introducing the concept of a proof of guilt in quasi-permissionless consensus algorithms; this definition is inspired by that from [63].

We are ready to define the accountability property in quasi-permissionless algorithms. Recall that our transformation guarantees accountability in the resulting quasi-permissionless protocol, regardless of whether the original permissioned protocol satisfies it.⁶⁶6That is why we define accountability solely with respect to quasi-permissionless protocols.

Let us analyze the definition of the ${\rho }_{\mathrm{a}}$-accountability property. The property is “triggered” when a consistency violation occurs, meaning that two correct processes $p$ and $q$ output inconsistent logs. In such a case, the definition ensures that $p$ and $q$ collectively hold enough information to correctly identify as faulty a set of participants (i.e., identifiers) whose stake represents at least a ${\rho }_{\mathrm{a}}$-fraction of the total stake.

A log-specific property $P$ is a function $P:\mathbb{P}(\mathrm{𝖫𝗈𝗀𝗌})\to \{\mathrm{𝑡𝑟𝑢𝑒},\mathrm{𝑓𝑎𝑙𝑠𝑒}\}$, where $\mathbb{P}$ denotes the power set and $\mathrm{𝖫𝗈𝗀𝗌}$ denotes the set of all logs (cf. Sec.˜2). Next, we define log-specific safety properties.

Intuitively, the constraint specifies that if a set of logs fails to satisfy $S$, there must exist a finite subset that also does not satisfy $S$, and none of its supersets satisfy $S$. We underline that Sec.˜3.2 follows the spirit of safety properties as defined by Alpern and Schneider in their seminal work [4]. We are now ready to define composable log-specific safety properties.

In essence, a composable log-specific safety property $S$ indicates that if two sets of logs satisfy $S$, then every subset of their union also satisfies $S$. Properties that require correct processes to output only valid logs (according to some predetermined validity condition) are composable log-specific safety properties. These include, for example, the following properties: (1) no log contains futile transactions, and (2) no log contains transactions not signed by their issuers.

Lastly, we define what it means for a protocol to satisfy a (composable or not) log-specific safety property. Fix any (permissioned or quasi-permissionless) protocol $𝒫$. Given any execution $ℰ$ of the protocol $𝒫$, let $\mathrm{𝗅𝗈𝗀𝗌}(ℰ)$ denote the set of all logs held by correct processes in $ℰ$:

Finally, we present the definition.

A protocol $𝒫$ satisfies a log-specific safety property $S$ if correct processes output only logs that are allowed by $S$. Notably, we exclude executions in which the genesis log is not allowed by $S$; otherwise, no protocol could satisfy $S$ as it is initially violated. We underline that time is irrelevant in the context of satisfying $S$: for any two (arbitrarily different) executions ${ℰ}_1$ and ${ℰ}_2$ that have the same set of output logs (i.e., $\mathrm{𝗅𝗈𝗀𝗌}({ℰ}_1)=\mathrm{𝗅𝗈𝗀𝗌}({ℰ}_2)$), the property $S$ is either satisfied in both executions or in neither.

The correctness of our quasi-permis-sionless PoS protocol $𝒯(𝒫)$ crucially relies on the guarantees provided by the permissioned protocol $𝒫$. However, we observe that, within the epoch-based structure of $𝒯(𝒫)$, protocol $𝒫$ might display unexpected behavior as described below. In the standard permissioned setting, correct processes run $𝒫$ forever, as this is a fundamental characteristic of the setting. However, the epoch-based structure of $𝒯(𝒫)$ introduces a different environment for $𝒫$: correct processes stop executing $𝒫$ associated with epoch $e$ once they transition to epoch $e+1$. This minor change necessitates a re-evaluation of the guarantees offered by $𝒫$: $𝒫$’s guarantees in the standard permissioned setting do not directly extend to this new context.

To analyze $𝒫$’s behavior within the epoch-based structure of $𝒯(𝒫)$, one needs to (1) enrich $𝒫$’s interface by allowing correct processes to stop executing it, and (2) examine the guarantees provided by this enriched protocol. We achieve this by introducing the concept of quit-enhanced permissioned protocols (cf. App. B.3 in [54]): given any standard permissioned protocol ${𝒫}^{\prime }$, where correct processes are expected to participate forever, we define $\mathrm{𝑞𝑢𝑖𝑡}({𝒫}^{\prime })$ as the quit-enhanced version of ${𝒫}^{\prime }$, where correct processes have the option to stop participating. (We emphasize that $\mathrm{𝑞𝑢𝑖𝑡}(𝒫)$ merely extends the interface of the original permissioned protocol $𝒫$. In particular, analyzing the behavior of $\mathrm{𝑞𝑢𝑖𝑡}(𝒫)$ relies exclusively on understanding the behavior of $𝒫$ itself – there is no need to examine the internal mechanisms of the protocol. This makes our quit-based extension inherently “closed-box” in nature.) Using our concept of quit-enhanced protocols, we prove that consistency, liveness, optimistic responsiveness, and all log-specific safety properties translate from $𝒫$ to $\mathrm{𝑞𝑢𝑖𝑡}(𝒫)$ (cf. App. B.4 in [54]), allowing us to build $𝒯(𝒫)$ on top of $𝒫$ that satisfies these properties in the permissioned model.⁷⁷7Liveness and optimistic responsiveness are preserved in only some (and not all) executions of $\mathrm{𝑞𝑢𝑖𝑡}(𝒫)$. However, as we show in App. C in [54], only these executions are needed to prove $𝒯(𝒫)$’s liveness and optimistic responsiveness.

As $𝕋$ denotes the total stake (cf. Sec.˜2), identifiers utilized in (executed-in-an-epoch) permissioned protocol $𝒫$ are integers in the range $[1,𝕋]$; we refer to these identifiers as “permissioned-ids”. Similarly, we refer to identifiers from the set $\mathrm{𝖨𝖣𝗌}$ (cf. Sec.˜2) as “PoS-ids”.

Consider a correct process $p$ executing $𝒫$ in epoch $e$. To start executing $𝒫$ in epoch $e$, process $p$ invokes the $\mathrm{𝗌𝗍𝖺𝗋𝗍}\mathrm{\_}\mathrm{𝗌𝗂𝗆𝗎𝗅𝖺𝗍𝗂𝗈𝗇}(\cdot )$ function (ln. 55).⁸⁸8Throughout the remainder of this section and in the pseudocode, we say that processes simulate $𝒫$ to emphasize that this is the underlying permissioned protocol being executed, and that each PoS-id may be running $𝒫$’s state machine on behalf of multiple permissioned-ids. There, process $p$ begins by setting the current log of the PoS protocol $𝒯(𝒫)$, finalized at the end of the previous epoch $e-1$, as the genesis log $ℒ$ for epoch $e$ (ln. 56-ln. 60). It then maps each permissioned-id (from the $[1,𝕋]$ range) into one PoS-id (from the $\mathrm{𝖨𝖣𝗌}$ set) using the $\mathrm{𝑖𝑑}\mathrm{\_}{\mathrm{𝑚𝑎𝑝}}_p=\mathrm{𝗆𝖺𝗉}\mathrm{\_}\mathrm{𝗌𝗍𝖺𝗄𝖾}(ℒ)$ map (ln. 62). For instance, if $ℒ$ assigns 3 tokens to a PoS-id $\mathrm{𝑖𝑑}$, then there exist $x_1,x_2,x_3\in [1,𝕋]$ such that $\mathrm{𝑖𝑑}\mathrm{\_}{\mathrm{𝑚𝑎𝑝}}_p[x_1]=\mathrm{𝑖𝑑}\mathrm{\_}{\mathrm{𝑚𝑎𝑝}}_p[x_2]=\mathrm{𝑖𝑑}\mathrm{\_}{\mathrm{𝑚𝑎𝑝}}_p[x_3]=\mathrm{𝑖𝑑}$; intuitively, in epoch $e$, permissioned-ids $x_1$, $x_2$ and $x_3$ correspond to the PoS-id $\mathrm{𝑖𝑑}$, meaning that PoS-id $\mathrm{𝑖𝑑}$ is responsible for simulating $𝒫$’s state machines associated with permissioned-ids $x_1$, $x_2$ and $x_3$. This is also crucial because each process must know which identifier to use when forwarding messages related to the permissioned protocol $𝒫$. Specifically, if a permissioned-id $i_1$ needs to communicate with another permissioned-id $i_2$ in $𝒫$ (associated with some epoch), the process $p$ “responsible” for the permissioned-id $i_1$ must know a PoS-id corresponding to $i_2$ in order to forward the message correctly (ln. 87). After establishing the aforementioned permissioned-ids to PoS-ids mapping, process $p$ verifies whether it is validating epoch $e$, i.e., whether any of its identifiers have been assigned a positive stake by $ℒ$. If there exists a permissioned-id $x\in [1,𝕋]$ that maps into a $p$’s PoS-id $\mathrm{𝑖𝑑}\in \mathrm{𝗂𝖽}(p)$, process $p$ instantiates $𝒫$’s state machine initialized with permissioned-id $x$ and genesis log $ℒ$ (ln. 64 and 65). Then, $p$ updates $\mathrm{𝑠𝑖𝑚𝑢𝑙𝑎𝑡𝑖𝑜𝑛}\mathrm{\_}{\mathrm{𝑚𝑎𝑝}}_p[x]$ to the initialized state machine (ln. 67). Note that $\mathrm{𝑖𝑑}\mathrm{\_}{\mathrm{𝑚𝑎𝑝}}_p$ associates each permissioned-id with its PoS-id counterpart, whereas $\mathrm{𝑠𝑖𝑚𝑢𝑙𝑎𝑡𝑖𝑜𝑛}\mathrm{\_}{\mathrm{𝑚𝑎𝑝}}_p$ maps only $p$’s permissioned-ids into their respective state machines. Finally, if $p$ is indeed validating epoch $e$, it instructs its timer $\mathrm{𝑒𝑝𝑜𝑐ℎ}\mathrm{\_}{\mathrm{𝑡𝑖𝑚𝑒𝑟}}_p$ to measure $\mathrm{𝖤𝖣}=\mathrm{\ell }+\mathrm{\Delta }$ time (ln. 69). Here, $\mathrm{𝖤𝖣}=\mathrm{\ell }+\mathrm{\Delta }$ is selected large enough so that each simulated instance $𝒫$ is run sufficiently long to allow new transactions to be finalized after GST. Specifically, the time period $\mathrm{𝖤𝖣}=\mathrm{\ell }+\mathrm{\Delta }$ ensures that, after GST, all correct validators of some post-GST epoch $e$ overlap in their execution of $𝒫$ (associated with epoch $e$) for at least $\mathrm{\ell }$ time. This overlap, together with the $\mathrm{\ell }$-liveness property of $𝒫$, guarantees that new transactions are finalized.

Within every epoch $e$, processes output a log produced by $𝒫$ as the $𝒯(𝒫)$ log if the log is signed by any quorum of the set ${\mathrm{𝗏𝖺𝗅𝗂𝖽𝖺𝗍𝗈𝗋𝗌}}_e$ (ln. 20 and Def. 25 in [54]).

When $\mathrm{𝑒𝑝𝑜𝑐ℎ}\mathrm{\_}{\mathrm{𝑡𝑖𝑚𝑒𝑟}}_i$ expires, process $p$ gossips a special epoch-ending transaction $(\text{finish},e)$ on behalf of each of its validating PoS-ids (ln. 81). The purpose of these finish transactions is ensuring that epoch $e$ eventually concludes by producing a complete log (cf. Def. 23 in [54]), i.e., an epoch-ending block.

Process $p$ stops simulating $𝒫$ upon observing epoch-ending transactions from a quorum of identifiers with sufficient stake, i.e., some quorum $I\subseteq \{\mathrm{𝑖𝑑}|\mathrm{𝑖𝑑}\in {\mathrm{𝗏𝖺𝗅𝗂𝖽𝖺𝗍𝗈𝗋𝗌}}_e\}$ such that ${\sum }_{\mathrm{𝑖𝑑}\in I}𝖲(ℒ,\mathrm{𝑖𝑑})\ge (1-\rho )𝕋$ (ln. 23 and Def. 23 in [54]). At that point, $p$ stops each of its currently simulated state machines (ln. 72), cancels $\mathrm{𝑒𝑝𝑜𝑐ℎ}\mathrm{\_}{\mathrm{𝑡𝑖𝑚𝑒𝑟}}_p$ (ln. 74), and resets the simulation-specific variables (ln. 75-ln. 78).

The set ${\mathrm{𝗏𝖺𝗅𝗂𝖽𝖺𝗍𝗈𝗋𝗌}}_{e+1}$ of validators is selected based on the stake distribution determined by the log produced in epoch $e$ (ln. 62 and Def. 21 in [54]). More specifically, any identifier that has positive stake according to the log $ℒ$ produced in epoch $e$ is eligible to participate in the permissioned protocol instance $𝒫$ associated with the next epoch $e+1$.

How do we ensure that all correct validators of epoch $e$ eventually complete that epoch? And how do we ensure that all correct validators of epoch $e+1$ learn the up-to-date state of the system – that is, all blocks finalized up to epoch $e$? Both questions are resolved through the underlying communication model (cf. Sec.˜2). Specifically, before any correct validator of epoch $e$ departs, it gossips its current log of finalized blocks, which includes all blocks from epoch $e$ (ln. 17). This log is fully certified, allowing any recipient to locally verify its validity and commitment status (see the following paragraph for details). This mechanism guarantees that every correct validator eventually receives the fully-certified log, finalizes the blocks of epoch $e$, and is thus permitted to exit. Similarly, joining validators are ensured to eventually receive the finalized log up to epoch $e$, enabling them to reconstruct the current system state and safely begin executing epoch $e+1$. Importantly, this mechanism allows us to avoid imposing any restrictions on validator departures: the sets of validators in epochs $e$ and $e+1$ may be entirely disjoint.

The pseudocode of our transformation $𝒯$ utilizes many methods defined on logs. Their formal definition can be found in App. C.1 in [54], while an informal description is given below:

• $\mathrm{■}$

  $ℒ.\mathrm{𝖼𝗎𝗋𝗋𝖾𝗇𝗍}\mathrm{\_}\mathrm{𝗂𝖽𝗌}$: the set of identifiers with positive stake according to $ℒ$.

• $\mathrm{■}$

  $ℒ.\mathrm{𝖾𝗉𝗈𝖼𝗁}$: the epoch with which $ℒ$ is associated.

• $\mathrm{■}$

  $ℒ.\mathrm{𝗏𝖺𝗅𝗂𝖽𝖺𝗍𝗈𝗋𝗌}$: the set of identifiers validating the epoch of $ℒ$, i.e., the set of identifiers that “produced” $ℒ$.

• $\mathrm{■}$

  $ℒ.\mathrm{𝖼𝗈𝗆𝗉𝗅𝖾𝗍𝖾𝖽}$: $\mathrm{𝑡𝑟𝑢𝑒}$ if and only if $ℒ$ contains sufficiently many (i.e. $(1-\rho )𝕋$ worth of stake) epoch-ending transactions.

• $\mathrm{■}$

  $ℒ.\mathrm{𝖾𝗉}\mathrm{\_}\mathrm{𝗉𝗋𝖾𝖿𝗂𝗑}(e\in [0,ℒ.\mathrm{𝖾𝗉𝗈𝖼𝗁}))$: the completed log ${ℒ}^{\prime }$ of epoch $e$ such that $ℒ$ extends ${ℒ}^{\prime }$.

Moreover, we say that a log $ℒ$ is certified at a process $p$ if and only if $p$ receives signatures on the log $ℒ$ from a quorum of members (i.e. $(1-\rho )𝕋$ worth of stake) of $ℒ.\mathrm{𝗏𝖺𝗅𝗂𝖽𝖺𝗍𝗈𝗋𝗌}$. Finally, a certified log $ℒ$ is fully-certified at a process $p$ if and only if, for every $e\in [0,ℒ.\mathrm{𝖾𝗉𝗈𝖼𝗁})$, $ℒ.\mathrm{𝖾𝗉}\mathrm{\_}\mathrm{𝗉𝗋𝖾𝖿𝗂𝗑}(e)$ is certified at process $p$. Note that two fully-certified logs cannot be conflicting. A log attains full certification only if it is approved by a quorum of validators for each epoch it covers. Since any two quorums intersect in at least one correct validator, it is impossible for two conflicting logs to both become fully certified. Consequently, upon receiving a fully-certified log, any correct validator can safely adopt it as its local log (ln. 21).

The following theorem proves that our transformation preserves the consistency property from the permissioned to the quasi-permissionless setting.

We show that the consistency property translates from $𝒫$ to $𝒯(𝒫)$ by induction. Initially, all correct processes have ${ℒ}_{\mathrm{g}}$ as the genesis log. Given that the logs output by the first epoch are consistent (due to $𝒫$’s consistency), consistency is satisfied in the first epoch. Moreover, all correct processes agree on the genesis log and the set of validators for the second epoch. By inductively applying the same argument, we can show that the logs output by the correct processes remain consistent throughout the entire execution. A formal proof of the theorem is given in App. C.3 in [54]. $◀$

The theorem below asserts that our transformation carries over any composable log-specific safety property from the permissioned setting to the quasi-permissionless setting.

To prove that any composable log-specific safety property $S$ translates from $𝒫$ to $𝒯(𝒫)$, we again rely on induction. As $𝒫$ satisfies $S$, the set of logs output by the first epoch adheres to $S$. Similarly, the set of logs output by the second epoch adheres to $S$. Hence, their union adheres to $S$ as $S$ is composable (cf. Sec.˜3.2):

Again, the set of logs output by the third epoch adheres to $S$, which then implies:

By inductively applying this argument, we can show that $𝒯(𝒫)$ satisfies $S$. A formal proof of the theorem is given in App. C.4 in [54]. $◀$

The following theorem demonstrates the preservation of liveness and optimistic responsiveness by our transformation.

If the first correct process $p$ for which there exists an identifier $\mathrm{𝑖𝑑}\in \mathrm{𝗂𝖽}(p)\cap {\mathrm{𝗏𝖺𝗅𝗂𝖽𝖺𝗍𝗈𝗋𝗌}}_e$ enters an epoch $e$ at some timeslot $\tau \ge \text{GST}$, then all other correct validators enter epoch $e$ within $\mathrm{\Delta }$ timeslots after observing the log seen by $p$. Moreover, no correct process sends an epoch-ending transaction until $\mathrm{𝖤𝖣}=\mathrm{\ell }+\mathrm{\Delta }$ timeslots into epoch $e$, which implies that epoch $e$ cannot be completed before timeslot $\tau +\mathrm{𝖤𝖣}=\tau +\mathrm{\ell }+\mathrm{\Delta }$. Hence, all correct validators stay in epoch $e$ together for at least $\mathrm{\ell }$ timeslots. As $𝒫$ satisfies $\mathrm{\ell }$-liveness, this overlap is sufficient to finalize new transactions in epoch $e$. To prove optimistic responsiveness, we follow the previous argument while factoring in that the actual message delay bound is $\delta$. As a result, all correct validators join epoch $e$ within $\delta$ timeslots – rather than $\mathrm{\Delta }>\delta$ – after seeing the log observed by $p$. A formal proof is relegated to App. C.5 in [54]. $◀$

Finally, the following theorem demonstrates that our transformation ensures that the resulting quasi-permissionless protocol satisfies accountability. Note that this holds even if the original permissioned protocol lacks accountability.

Suppose two correct processes $p$ and $q$ output inconsistent logs ${ℒ}_p$ and ${ℒ}_q$, respectively. Therefore, ${ℒ}_p$ (resp., ${ℒ}_q$) is fully-certified at $p$ (resp., $q$). Hence, disseminating these two logs, along with their respective signatures, enables accountability: every correct process eventually receives these inconsistent logs, combines the received signatures, and obtains a set of identifiers $C$ such that, for each $\mathrm{𝑖𝑑}\in C$, $\mathrm{𝑖𝑑}$ signs two inconsistent logs associated with the same epoch, thus proving $\mathrm{𝑖𝑑}$’s culpability. Finally, since each of the two logs is signed by a quorum of validators – i.e., those holding at least $(1-\rho )𝕋$ stake – the identifiers in $C$ collectively represent at least $(1-\rho )𝕋+(1-\rho )𝕋-𝕋=(1-2\rho )𝕋$ stake. A formal proof of the theorem can be found in App. C.6 in [54]. $◀$

In terms of message complexity, the transformation $𝒯(𝒫)$ introduces an additional quadratic term to that of $𝒫$ in order to satisfy the accountability property in the quasi-permissionless setting, stemming from the signatures that processes must exchange before outputting a log. However, since any consensus protocol inherently requires a quadratic number of messages in the worst case [37], our transformation does not introduce any asymptotic worst-case overhead. A proof is deferred to App. C.7 in [54].