# Density wave halo around anyons in fractional quantum anomalous hall states

Xue-Yang Song  T. Senthil  Department of Physics, Massachusetts Institute of
Technology, Cambridge, Massachusetts 02139, USA

###### Abstract

The recent observation of fractional quantum anomalous Hall (FQAH) states in
tunable moiré materials encourages study of several new phenomena that may be
uniquely accessible in these platforms. Here, we show that an isolated
localized anyon of the FQAH state will nucleate a ‘halo’ of Charge Density
Wave (CDW) order around it. We demonstrate this effect using a a recently
proposed quantum Ginzburg-Landau theory that describes the interplay between
the topological order of the FQAH and the broken symmetry order of a CDW. The
spatial extent of the CDW order will, in general, be larger than the length
scale at which the fractional charge of the anyon is localized. The strength
and decay length of the CDW order around anyons induced by doping or magnetic
field differs qualitatively from that nucleated by a random potential. Our
results leverage a precise mathematical analogy to earlier studies of the
superfluid-CDW competition of a system of lattice bosons which has been used
to interpret the observed CDW halos around vortices in high-$T_{c}$
superconductors. We show that measurement of these patches of CDW order can
give an indirect route to measuring the fractional charge of the anyon. Such a
measurement may be possible by scanning tunneling microscopy (STM) in moiré
systems.

##  I Introduction

The (fractional) quantum Hall effect usually occurs in the setting of two
dimensional electron gases subject to a strong magnetic field. It has been
clear for some time now that quantum Hall physics can be realized without a
magnetic field if electrons either completely or partially fillSun  _et al._
(2011); Sheng  _et al._ (2011); Neupert  _et al._ (2011); Wang  _et al._
(2011); Tang  _et al._ (2011); Regnault and Bernevig (2011); Bergholtz and Liu
(2013); Parameswaran  _et al._ (2013) a Chern band in a lattice system. When
the required time reversal symmetry breaking occurs spontaneously, the
resulting phases have been dubbed (Fractional) Quantum Anomalous Hall states.
In the last few months, Fractional Quantum Anomalous Hall (FQAH) states have
been discovered in two different two dimensional moire heterostructuresCai
_et al._ (2023); Zeng  _et al._ (2023); Park  _et al._ (2023); Lu  _et al._
(2023), following directions suggested by a number of theoretical studiesZhang
_et al._ (2019); Ledwith  _et al._ (2020); Repellin and Senthil (2020);
Abouelkomsan  _et al._ (2020); Wilhelm  _et al._ (2021); Wu  _et al._ (2019);
Yu  _et al._ (2020); Devakul  _et al._ (2021); Li  _et al._ (2021a); Crépel
and Fu (2023).

These FQAH states compete with a number of other states of matter. At the
lattice fillings $p/(2p+1)$ (for $p$ an integer), where current experiments
see an FQAH state, a natural competing insulating state is a commensurate
Charge Density Wave (CDW) insulator. Indeed it has been possible to tune out
of the FQAH phase into insulating phases with large longitudinal (and small
Hall) resistivity using a perpendicular displacement field. The
competition/intertwinement between the FQAH and CDW potentially manifests
itself in ways that are unique to the lattice setting, and are absent in the
continuum realization of quantum hall physics studied experimentally over the
previous decades.

Figure 1: (a): The charge density pattern around an anyon ‘core’. The gray
scale is correlated with the intensity of the CDW order which decays
exponentially in space. Lower panel shows the FQAH phase with a finite density
of anyons (big disks), where the anyon fractional charge (red small disks) is
more localized than the surrounding CDW halo. (b):(Top to bottom) Schematic
plot of the anyon charge density, the charge density wave, and the composite
boson density. The spatial region where the fractional charge of the anyon is
localized is related to the quantum zero point motion of the vortex (of the
composite boson superfluid) while the induced CDW order decays at a
‘coherence’ scale $xi$ related to the distance to the critical point. The
composite boson density is depleted at the same coherence length scale.

Recent theoretical workSong  _et al._ (2023), which we briefly review below,
has derived a quantum Ginzburg-Landau (q-GL) theory to describe the
competition/intertwinement between the FQAH and CDW state, and used it to
address possible phase transitions (and phases proximate to the FQAH state).
Much like in other instances of the use of such theories, we can use the q-GL
theory to address many other questions pertinent to the interplay between FQAH
and CDW physics.

In this paper we show that in the FQAH phase, a localized anyon nucleates
around it a halo where there is CDW ordering. The size of the halo region is
determined by the “distance” to the fully ordered CDW phase in the phase
diagram (assuming the FQAH-CDW transition is at least approximately second
order). In a device where a finite (but low) density of anyons are present,
perhaps due to a small doping away from the filling $p/(2p+1)$, there will be
a corresponding finite density of CDW patches. If the inter-anyon separation
is larger than the halo size (which is guaranteed at sufficiently small
doping), then the CDW patches will be well separated from each other. A
schematic depiction is in Fig. 1.

Such CDW patches may in principle be imaged through future STM experiments. We
point out that such an imaging can be an indirect measure of the anyon charge.
For instance at filling $\nu=\frac{p}{q}+\delta$, suppose the anyons that are
induced by the doping have a charge $q*$ (for odd denominator states, $q^{*}$
will be a multiple of $\frac{1}{q}$). Then there will be $\delta/q^{*}$ CDW
patches per unit cell. Thus the ratio of CDW patch density to the doping
density within the FQAH plateau directly gives the fractional charge $q^{*}$
of the anyon.

The phenomenon of CDW order nucleating in a halo around the anyon is analogous
to the observation of CDW order in a halo around a vortex core in cuprate
superconductorsHoffman  _et al._ (2002). In the latter system too, this arises
due to a competition between superconducting and CDW orderings. This
competition was discussed theoretically in simplified models of bosonic Cooper
pairs at fractional lattice density in a series of papersLannert  _et al._
(2001); Balents  _et al._ (2005a, b). The resulting q-LG theories for the
superfluid-CDW Mott transition of bosons at fractional lattice filling enable
addressing the physics of the vortex structure in the superfluid state and the
nucleation of CDW order once the superfluid order parameter is suppressed near
the vortex coreBalents  _et al._ (2005a, b).

The q-LG theory for the FQAH-CDW competition in our previous work is a
modification of the q-LG theory for the superfluid-CDW competition of bosons
on a lattice. To explain this connection, we recall that, in the usual Landau
level setting, there is a Ginzburg-Landau descriptionZhang  _et al._ (1989);
Read (1989) of the fractional quantum Hall system in terms of “composite
bosons” (electrons with an odd number of attached vortices) coupled to
emergent gauge fields with a Chern-Simons action. In this description, the
quantum Hall phase is a condensate (a ‘superfluid’) of composite bosons. The
theory of Ref. Song  _et al._ (2023) described the FQAH state at any lattice
filling in a generalization of this standard composite boson picture. The
composite bosons are at the same lattice filling as the electron. Condensing
the composite boson gives the FQAH phase while a CDW Mott insulator of these
composite bosons is a possible proximate electronic CDW insulator. Thus there
is a close relationship between the theory of the FQAH-CDW competition and
that of the superfluid-CDW competition, though the physical interpretation is
different.

Interestingly for our purposes, the vortices of the composite boson condensate
are precisely the fractionally charged anyons of the FQAH state. Thus the
earlier discussionBalents  _et al._ (2005b) of the nucleation of CDW around
vortices in the superfluid phase of bosons on a lattice can be essentially
taken over directly to reach the conclusions outlined above on CDW halos
around anyons in the FQAH state. We also study defects in the CDW ordered
phase, and show that, apart from having fractional charge, there are
circulating electrical currents in their vicinity that reflects the proximate
FQAH phase.

In the rest of this paper we will flesh out the details of these introductory
remarks.

##  II Quantum Ginzburg-Landau theory for FQAH-CDW competition

To be concrete, we specialize to lattice filling $\nu=-\frac{2}{3}$ where the
most prominent FQAH state is seen in t-MoTe2. It is convenient to go to a hole
picture and describe this FQAH state as having the same topological order as
the Laughlin state of holes at $1/3$ filling. The phase transition out of the
quantum Hall phase can be thought of as a superfluid-insulator transition of
(generalized) composite bosons $\Phi$ at a lattice filling of $1/3$. The
theory is conveniently describedSong  _et al._ (2023) in terms of vortices
$\Phi_{vI}$ (with $I=1,2,3$) of the composite boson field, with a
LagrangianSong  _et al._ (2023)

${\cal
L}=\sum_{I=1}^{3}|\left(\partial_{\mu}-i\alpha_{\mu}\right)\Phi_{vI}|^{2}+{\mathcal{L}}_{4}+\cdots-\frac{3}{4\pi}\alpha
d\alpha+\frac{1}{2\pi}Ad\alpha,$ (1)

The ellipses represent terms consistent with the translation and $C_{3}$
symmetries of the lattice. The $\alpha$ is a dynamical $U(1)$ gauge field and
$A$ is a probe $U(1)$ gauge field that can be used to calculate the
electromagnetic response. We omitted an additional term $1/(4\pi)AdA$
describing an integer quantum anomalous Hall effect of the filled Chern band,
which does not affect the main discussion.

The symmetry action of translations and $C_{3}$ (the subscript $I+1$ are
defined modulo $3$, i.e. $I\mod 3+1$)Burkov and Balents (2005) reads,

$\displaystyle T_{1}$ $\displaystyle:$
$\displaystyle\Phi_{v,I}\rightarrow\Phi_{v,I+1}$ $\displaystyle T_{2}$
$\displaystyle:$ $\displaystyle\Phi_{v,I}\rightarrow
e^{i\frac{2(I+1)\pi}{3}}\Phi_{v,I+1}$ $\displaystyle C_{3}$ $\displaystyle:$
$\displaystyle\Phi_{v,1}\rightarrow
e^{i\frac{\pi}{6}}\Phi_{v,3},\Phi_{v,2}\rightarrow-i\Phi_{v,1},$ (2)
$\displaystyle\Phi_{v,3}\rightarrow e^{i\frac{\pi}{6}}\Phi_{v,2}.$

The allowed quartic terms for the dual vortex fields have the structure

$\displaystyle\mathcal{L}_{4}[\Phi_{vI}]$ $\displaystyle=$ $\displaystyle{\cal
L}_{u}+{\cal L}_{v}$ $\displaystyle{\cal L}_{u}$ $\displaystyle=$
$\displaystyle u(\sum_{I=1}^{3}|\Phi_{vI}|^{2})^{2}$ $\displaystyle{\cal
L}_{v}$ $\displaystyle=$ $\displaystyle
v(|\Phi_{v1}|^{2}|\Phi_{v2}|^{2}+|\Phi_{v1}|^{2}|\Phi_{v3}|^{2}+|\Phi_{v2}|^{2}|\Phi_{v3}|^{2}),$

where the sign of $v$ determines the nature of the symmetry breaking state
when $\Phi_{vI}$’s condense.

Clearly if the $\Phi_{vI}$ are all gapped, we get the Laughlin $1/3$ state. If
however the $\Phi_{v}$ condense, then the $\alpha$-field is Higgsed and the
quantum hall effect is destroyed. The low energy long wavelength response to
the probe $A$ field is then given by a Maxwell action (with no Chern-Simons
term). Thus we get a CDW insulating state, where the non-trivial translation
action on $\Phi_{vI}$ ensures that translation symmetry is spontaneously
broken. The pattern of charge ordering in the CDW is determined by the
structure of the non-linear terms in Eq. (1)Burkov and Balents (2005).

Let $\mathbf{R}_{1,2}$ be the primitive vectors of the real space moiré
superlattice, and $\mathbf{b}_{1,2}$ be the corresponding reciprocal lattice
vectors. The charge density operator at a wavevector
$\frac{2m}{3}\mathbf{b}_{1}+\frac{2n}{3}\mathbf{b}_{2}$ can be written in
terms of the low energy vortex fields as (where again the index $j$ on vortex
field is to be interpreted as $(j-1)\textrm{mod }3+1$)

$\displaystyle\rho_{mn}(\mathbf{R})$ $\displaystyle=$ $\displaystyle
S(m,n)\sum_{j=1,2,3}\Phi_{v,j}^{\dagger}(\mathbf{r})\Phi_{v,j+n}(\mathbf{r})e^{i(n-m)j\frac{2\pi}{3}},$
$\displaystyle\rho(\mathbf{R})$ $\displaystyle=$
$\displaystyle\sum_{m,n}\rho_{mn}(\mathbf{R})e^{i\frac{2\pi
m}{3}\mathbf{R}_{1}+i\frac{2\pi n}{3}\mathbf{R}_{2}},$ (3)

where $S(m,n)$ is a form factor unknown from the low energy properties of the
vortex fields. It is straightforward to verify that the vortex transformation
in Eq (II) determines that the $\rho_{mn}$ sits at the correct wavevector.

Thus the theory in Eq. (1) enables discussion of the competition between the
FQAH and CDW phases within a continuum field theory. It can thus be thought of
as a quantum Ginzburg-Landau theory that is suitable for discussing universal
aspects of the physics. We can use it to study many different aspects of the
interplay between the two kinds of orders, such as, eg, their phase
transition, and inhomogenous situations involving interfaces between the FQAH
and the CDW. Here however we will study the structure of the charged anyon
defects of the FQAH phase.

For simplicity, we assume that the charge-density-wave order is obtained by
condensing only one of the $\Phi_{v}$ fields, which happens when $v>0$. The
resulting CDW order pattern is the simplest one for $1/3$ filling on
triangular lattices – with a tripled unit cell shown in Fig. 1. Other
condensation patterns in Ref. Burkov and Balents, 2005 are allowed for
different signs of $v,u$ in $\mathcal{L}_{4}$, though this does not affect the
discussion below, with the only difference being the detailed CDW pattern
nucleated by an anyon.

##  III Intertwinement of FQAH and CDW phases

The FQAH state is formed by ‘condensing’ the composite bosons $\Phi$ which is
equivalent to considering a phase where the vortex fields $\Phi_{vI}$ are
gapped. A vortex defect, localized at some spatial point, in the composite
boson condensate is thus a unit charged source for the $\alpha$ gauge field in
Eq. (1). The Chern-Simons term binds a magnetic flux of $2\pi/3$ of $\alpha$
to the localized $\Phi_{vI}$ defect. The coupling to the probe gauge field $A$
then tells us that this defect has charge-$1/3$ and is identified with the
$1/3$ Laughlin quasiparticles.

The intertwinement of the two phases is manifested by the defect of ‘order
parameters’ in one phase carrying quantum numbers of the order parameters of
the other phase. In the FQAH phase, the defect of composite boson superfluid,
i.e. the vortices $\Phi_{v}$, transforms in a projective representation of the
space group, which directly leads to the charge density wave pattern, obtained
when the vortices condense. In particular, $\Phi_{v}$ obeys
$T_{1}T_{2}T_{1}^{-1}T_{2}^{-1}=e^{i2\pi/3}$ (the magnetic translation due to
$1/3$ filling of the bosons). The CDW pattern will have a minimal $3$-site
unit cell to trivialize the magnetic translation of the vortices. Fig. 1 shows
a schematic CDW nucleated around a vortex. The amplitude of the CDW, denoted
by the gray scale of the disks, decays exponentially away from the vortex
core. Hence we arrive at a remarkable conclusion: a localized $e/3$ anyon in
the FQAH phase will nucleate CDW orders at its ‘core’, indicative of the
symmetry breaking competing phase proximate to the FQAH.

On the other hand, in the CDW phase when $\Phi_{v}$ condenses, we can see
traces of the FQAH in the defect of the CDW order. In Fig 2 we schematically
show a defect of the CDW order, which carries $-1/3$ or $2/3$ excess charge
upon careful counting. From the field theory for the closely related
superfluid-insulator transition at this lattice filling, it has been argued
that the bosons will be fractionalized near the critical point into $3$
fundamental fields each carrying $1/3$ of the boson chargeBalents  _et al._
(2005b). This is because a $2\pi$ dual ‘vortex’ of any $\Phi_{v}$ field
induces $2\pi/3$ of $d\alpha$ flux, and hence carries $1/3$ of boson charge.
The same argument continues to hold in our theory with the extra Chern-Simons
term for $\alpha$. As we show below, the Chern-Simons term leads to the
presence of circulating electrical currents which will lead to a change of the
local magnetization.

We identify the defect as a vortex in the $\Phi_{v}$ superfluid. An effective
Lagrangian for the superfluid as

$\displaystyle\mathcal{L}_{CDW}=\frac{\rho_{s}}{2}|(\nabla\theta-\alpha)|^{2}+\frac{3}{4\pi}\alpha
d\alpha$ $\displaystyle+\frac{g^{2}}{8\pi}(-b^{2}+e^{2}),$ (4)

where $\Phi_{v}\sim e^{i\theta}$, and $\rho_{s}$ is the corresponding
“superfluid density”. The last term is the Maxwell term for the internal gauge
field $\alpha$ with $e=-\nabla\alpha_{0}$ (we fix the gauge to be _time
independent_). $g^{2}$ is a coupling constant with the dimension of length.
The equations of motion

$\displaystyle-g^{2}\nabla\times b$ $\displaystyle=$
$\displaystyle-4\pi\rho_{s}(\nabla\theta-\alpha)+6\vec{e}\times\hat{z},$
$\displaystyle\frac{3b}{2\pi}$ $\displaystyle=$
$\displaystyle\frac{g^{2}\nabla\cdot e}{4\pi},$ (5)

correspond to modified Maxwell equations due to the Chern Simons term, where
$\left(\vec{e}\times\hat{z}\right)_{i}=\epsilon_{ij}e_{j}$. We consider a
$2\pi$ vortex of $\Phi_{v}$ located at the origin. Then
$\nabla\times\nabla\theta=2\pi\delta^{2}(r)$. We take a curl for the first
equation, and substitute $\vec{e}=-\nabla\alpha_{0}$ to arrive at the modified
vortex equation

$\displaystyle\nabla^{2}(b-\frac{6\alpha_{0}}{g^{2}})-\frac{b}{\lambda^{2}}$
$\displaystyle=$ $\displaystyle\frac{1}{2\lambda^{2}}\delta^{2}(r),$
$\displaystyle 6b$ $\displaystyle=$ $\displaystyle g^{2}\nabla^{2}\alpha_{0},$
(6)

where the penetration length $\lambda=|g|/\sqrt{4\pi\rho_{s}}$. Using the
second equation and eliminating $\alpha_{0}$ in the first equation, we recover
the usual London equation for a vortex in a BCS superconductor, with a
modified penetration length

$\displaystyle\frac{1}{\lambda^{\prime
2}}=\frac{1}{\lambda^{2}}+\frac{36}{g^{4}}.$ (7)

As expected, the vortex in the $\Phi_{v}$ condensate traps a flux of $b$
localized to a length scale $\lambda^{\prime}$ around it. From the modified
Gauss law $\frac{3b}{2\pi}=\frac{g^{2}\nabla\cdot e}{4\pi}$, it follows that a
defect induces a radial electric field $e$. Since $d\alpha$ is coupled to the
physical probe field $A$, the physical current is given by
$\vec{J}=\vec{e}\times\hat{z}$. So a circulating current appears around the
defect of the CDW phase.

We see that the role of the Chern-Simons term is to lead to a circulating
electrical current near the defect core which will lead to a change of the
orbital magnetization compared to the bulk regions far away from the defect. A
heuristic picture is that in the vicinity of the defect the CDW order is
suppressed and we instead nucleate a small bubble of the FQAH phase. Thus
there is an interface created, at a scale of the coherence length, between
FQAH and CDW which then leads to a circulating electric current. We thus see
that the $e/3$ Laughlin quasiparticles imprint on the defect of the CDW order
parameters $|\Phi_{v}|$ in the CDW phase.

Figure 2: Left: The defect in the CDW ordered phase where a $-1/3$ charge
deficit as drawn of an empty site. The dashed lines are the domain walls of
the CDW order parameter: the orders on two sides of the wall are related by
translation by one lattice constant along the domain wall direction. The
charge patterns in different domains are distinguished by colors. Around the
defect, the coarse-grained charge density $\bar{\rho}_{e}$ will deviate from
the average $1/3$ in the CDW phase. A circulating current around the defect,
i.e. an FQAH patch, will change the local magnetization. Right: The defect is
identified as a flux of the gauge field $\alpha$, with a spatial extent given
by the penetration depth of the vortex condensate.

##  IV Density wave halo around anyons

We now study in more detail the spatial structure of an anyon defect in the
FQAH phase and the halo of charge density modulation. This charge modulation
pattern is indicative of the CDW phase on the other side of the transition,
obtained e.g. by tuning the displacement field in the dual-gate moire TMD
system. This phenomenon is reminiscent of the modulation of the local density
of states foundHoffman  _et al._ (2002) near the vortex cores in
superconducting high $T_{c}$ cuprates, which has been attributed to the
intertwinement with charge ordering in the underdoped regime originating from
proximity to the Mott insulator.

For our purposes it is sufficient to work with an approximate version of Eq.
(1) where we retain only quadratic terms in $\Phi_{vI}$. This will be
legitimate so long as we are close enough to the phase transition to warrant
using a long wavelength theory but not so close as to require a full-blown
solution of the interacting field theory. In this regime, the effective action
for the vortex can be taken to have the form

$\displaystyle S=\int
d^{2}rd\tau\sum_{I=1}^{3}|\left(\partial_{\mu}-i\alpha_{\mu}\right)\Phi_{vI}|^{2}+m^{2}|\Phi_{vI}|^{2}+\mathcal{L}_{4}$
$\displaystyle-\frac{3}{4\pi}\alpha d\alpha+\frac{1}{2\pi}Ad\alpha,$ (8)

with the transition tuned by the mass $m$ (here $m$ is real in the FQAH). We
have renormalized the spatial and temporal scales to set the velocity $v=1$.
To leading order, we ignore the fluctuation of $\alpha_{i}$ . $\alpha_{0}$,
however is needed to account for the vortex chemical potential, i.e. magnetic
field effects and mediate vortex interactions.

We discuss three ways to induce the anyon defect in the system: first through
an impurity potential, second through doping within the quantum Hall plateau,
and third by turning on a small magnetic field.

Impurity pinning: A static impurity potential couples linearly to the charge
density through the form

$\displaystyle H_{i}=\int d^{2}r\sum_{mn}V_{mn}(r)\rho_{mn}(r).$ (9)

Linear response theory gives an induced charge density wave in terms of the
impurity potential asBalents  _et al._ (2005b)

$\displaystyle\langle\rho_{mn}(r)\rangle=S(m,n)^{2}\int
d^{2}r^{\prime}\Pi_{0}(r-r^{\prime})V_{mn}(r^{\prime}),$
$\displaystyle\Pi_{0}(r)\approx-\frac{3m}{4\pi^{2}}\frac{e^{-2mr}}{(2mr)^{3/2}},\textrm{
as }r\rightarrow\infty,$ (10)

Hence an impurity localized at some spatial position $\mathbf{r}_{0}$ induces
a charge density wave that decays exponentially from $\mathbf{r}_{0}$ over a
characteristic length $\xi\sim 1/(2m)$ related to the distance to the critical
point. This length scale can either be viewed as the correlation length for
CDW fluctuations, or, equivalently, as the coherence length of the superfluid
of the composite bosons. Fig 1(a) schematically shows the CDW modulation with
a tripled unit cell induced by an impurity (blue disk). The detailed
modulation pattern depends on microscopic details of the impurity and
energetics etc.

As an impurity weakens the composite boson superfluidity, it is likely for the
impurity site to overlap with a vortex core. An important difference from the
analogous discussion of Ref. Balents  _et al._ , 2005b is that the vortex
carries $e/3$ physical electrical charge. Hence the impurity potential will
couple directly to the vortex density as a chemical potential $-|\mu|$. When
the impurity strength is strong enough to overcome the vortex energy gap
($|\mu|>m$), an anyon is nucleated at the impurity location. In the case
considered in Ref Balents  _et al._ , 2005b, as the vortex does not carry
charge, the impurity potential mainly only couples to the CDW order
$\rho_{mn}$ with nonzero momenta. In contrast here, the impurity can also act
directly as a chemical potential for the vortex, which is similar to the case
of a nonzero magnetic field in Ref. Balents  _et al._ , 2005b.

To investigate the spatial profile of the pinned anyon, we approximate the
impurity potential close to its minimum in space by a harmonic expansion:

$\displaystyle
i\alpha_{0}(\vec{r})=-\mu+\frac{1}{2}m\omega^{2}r^{2}\quad(\mu>0).$ (11)

We work in the limit $|i\alpha_{0}-m|\ll m$ and ignore the vacuum fluctuations
of vortex-antivortex pairs . We can then perform an expansion to the lowest
order of $\tau$\- derivative and $|i\alpha_{0}-m|$. Following the procedure of
Ref Balents  _et al._ , 2005b, define
$\Phi_{v,l}=\frac{1}{\sqrt{2i\alpha_{0}}}\Psi_{l}$ and the low energy action
reads

$\displaystyle S=\int
d^{2}rd\tau\sum_{I=1}^{3}[\Psi^{*}_{l}\frac{\partial\Psi_{l}}{\partial\tau}+\frac{|\partial\Psi_{l}|^{2}}{2m}$
$\displaystyle+(m-\mu+\frac{1}{2}m\omega^{2}r^{2})|\Psi_{l}|^{2}],$ (12)

This describes a system of harmonic oscillators. The main effect of the Chern
Simons term for $\alpha$ is that the vortex carries charge and hence its
density couples directly to the impurity potential, which was accounted for in
deriving Eq (IV). Hence the anyon wavefunction should assume the form

$\Psi_{anyon}\propto exp\left(-\frac{m\omega r^{2}}{2}\right),$

with a decay length $\sim\frac{1}{\sqrt{m\omega}}$ (a characteristic length
describing the quantum zero-point motion of the vortex).

Note that for the strong impurity potential, near the impurity potential
minima, the CDW order $\rho_{mn}$ obtained from linear response and one-loop
expansion in Eq (10) does not hold anymore. It is only valid away from the
deep potential minima, as shown in the middle panel of Fig 1(b).

In summary, as one tunes close to the transition and $m\rightarrow 0$, the
decay length of the CDW order $1/m$ is much larger than the spatial extent of
the anyon wavefunction $\sim 1/\sqrt{m\omega}$. Fig 1(b) shows the profile of
composite boson condensate, charge modulation and localized anyon, with two
characteristic length scales $1/m,\sim 1/\sqrt{m\omega}$.

Doping or weak magnetic field: The vortex, identified with the Laughlin
quasiparticle, can also be induced by slightly doping the system or turning on
an out-of-plane magnetic field. The incompressible state in density-magnetic
field $n-B$ plane traces a line with slope proportional to Hall conductivity
(as per the Strada formula). Doping or turning on $B$ away from this
incompressible line will create anyon excitations above the ground state,
given the robustness of the fractional quantum hall plateau.

If a vortex $\Phi_{v}$ that carries $e/3$ is the lowest energy excitation,
doping of $\delta$ electrons per unit cell will induce an anyon density of
$3\delta$ per unit cell, and associated CDW patches. It is also possible,
depending on microscopic details, that an anyon with $2e/3$, is the lowest
energy excitation carrying electric charge111It is in principle possible that
even an electron with charge-$e$, is the lowest energy charged excitation.
However this would be unlikely if the Chern band has close to ideal quantum
geometry which naturally have Laughlin quasiparticles at low energy.. Then
doping $\delta$ charge per unit cell induces $3\delta/2$ patches of
quasiparticle excitations, and associated CDW halos. When doping $\delta$
electrons induces $3\delta$ or $3\delta/2$ patches of CDW halos, this
indicates fractionalized particles in the system.

On the dual vortex side, the doping of electrons, equivalently $\Phi$’s, leads
to a magnetic field $\nabla\times\alpha(r)=\delta f(r)$ felt by vortex
$\Phi_{v}$’s. The vortex action is supplemented with a term $\alpha_{0}\delta
f(r)$ in Eq (IV) from the self Chern-Simons term of $\alpha$, which induces a
nonzero chemical potential $\alpha_{0}$. The $\delta f(r)$ profile hence
should be determined self-consistently. A vortex lattice with CDW pattern
$\rho_{mn}$ is hence formed, coexisting with FQAH phase. At low anyon or
vortex density, we consider a single vortex near the origin in a potential
$\alpha_{0}(r)=\alpha_{0}^{external}(r)+\alpha_{0}^{lattice}(r)$ with
contributions both from external fields and impurities, as well as other
vortex excitations in the vortex lattice. The potential from other vortices
mediates a ’Coulomb’ interaction among vortices.

As in the discussion for impurities, we expand the potential around its minima
as in Eq (11), although now, a magnetic field $\delta f(r)$ is also present.
The ground state in this potential is given by $3$ harmonic oscillator modes
with a Gaussian form. $\Psi\propto e^{-m\omega_{v}r^{2}/2}$, where
$\omega_{v}$ depends the coefficient in a harmonic approximation of the
$\alpha_{0}(r)$ potential, as well as the magnetic field $\delta f(r)$. Ref
Balents  _et al._ , 2005b showed the charge density modulation to be
independent of the pinning potential of the vortex lattice, unlike the case of
impurity pinning where $\rho_{mn}\propto V_{mn}$. Essentially this is because
vortex excitations already form a vortex lattice and the $V_{mn}$ associated
with spatially oscillating potential acts as off-diagonal perturbation within
the degenerate $3$ vortex species $\Phi_{v}$’s space. The resulting
$\rho_{mn}$ is given by degenerate perturbation theory with the effective
Hamiltonian within the degenerate space depending on $V_{mn}$ and form factors
in Eq (II). The eigenvectors depend on $V_{mn}$ though its amplitude depends
on the harmonic oscillator wavefunction solved from Eq (IV), not the overall
scale of $V_{mn}$. The profile of the modulation around each vortex core, from
Eq (II), is thus given by a product of the harmonic oscillator wavefunctions
for $\Phi_{v}$’s, i.e. is of the Gaussian form $e^{-m\omega_{v}r^{2}}$. The
anyon localized around each vortex is again of the size
$1/\sqrt{m\omega_{v}}$.

In the FQAH phase, magnetic field flux will nucleate anyons from the quantum
hall response. The case for small magnetic field is similar to doping where
CDW order forms with the vortex lattice.

For impurity pinning the charge density wave nucleated near the vortex core
$\rho_{mn}\propto V_{mn}$ is much weaker than those induced by doping or
magnetic field. Thus the dominant CDW patches will be those around localized
anyons with a much weaker background of CDW order induced by a weak random
potential. Note that Ref Song  _et al._ , 2023 considered an alternative
scenario where commensurate CDW coexists with the FQAH and proposed a direct
transition to a trivial CDW insulator. There we do not expect anyons to
further indpattern uce charge modulations.

Proximate CDW with neutral topological order:

At lattice filling $2/3$, Ref Song  _et al._ , 2023 also proposed another
proximate CDW insulator with coexisting neutral topological order. The
resulting q-GL theory reads,

$\displaystyle{\cal
L}=\sum_{I=1}^{3}|\left(\partial_{\mu}-i\alpha_{\mu\i}\beta_{\mu}\right)\Phi_{vI}|^{2}+{\mathcal{L}}_{4}+\cdots$
$\displaystyle-\frac{3}{4\pi}\alpha d\alpha+\frac{1}{4\pi}\beta
d\beta+\frac{1}{2\pi}Ad(\alpha+\beta),$ (13)

where $\alpha,\beta$ are both dynamical $U(1)$ gauge fields. Condensing the
$\Phi_{v}$’s locks $\alpha=-\beta$ leading to a CDW insulator coexisting with
a neutral topological sector described $U(1)_{2}$ Chern-Simons terms.

If this scenario is realized, in the FQAH phase, a vortex $\Phi_{v}$ will
carry $2/3$ units of electric charge instead of $1/3$ charge. All the
discussion in the manuscript can otherwise be applied to this q-LG theory -
essentially the CDW halo around anyons from intertwinement of $2$ phases is
predicted by both theories. Unfortunately this also means that this probe can
not distinguish the two scenarios. The clear way to achieve this would be a
combined measurement of electric and thermal Hall conductivitySong  _et al._
(2023).

##  V Summary and experimental probes

A natural competitor to FQAH ordering at rational fractional filling of a
Chern band is a CDW insulator. Indeed numerical calculations often find that
these two states are close in energy. In the context of moiré systems like
twisted MoTe2 or pentalayer rhombohedral graphene, phase transitions between
FQAH and a CDW insulator can be driven by small changes in the displacement
field. Thus it is only natural that when FQAH order is suppressed in some
local region of space, CDW order rears its head. A simple way to suppress the
FQAH locally is to introduce an anyon defect. The quantum Ginzburg-Landau
theory of Ref. Song  _et al._ , 2023 enables a theoretical treatment of this
effect, as we demonstrated in this paper.

The best experimental probe of the nucleation of density wave order around
anyon defects is through Scanning Tunneling Microscopy (STM). However the
delicate charge modulation pattern in the FQAH layer and the requirement of
high spatial resolution might makes it challenging to observe the effects we
predict. In ref Li  _et al._ (2021b), the charge ordering pattern associated
with commensurate Wigner crystals in some moiré TMDs was imaged using a novel
technique where a graphene sensor layer, separated by a thin hBN, is placed on
top of the TMD bilayers. The charge modulation of the of the TMD layer induces
associated charge modulation in the graphene layer. Coupling the tip of an STM
to the graphene sensing layer then enables observation of this induced charge
modulation. This procedure results in a small perturbation to the TMD system
while achieving high spatial resolution. Such a measurement technique is a
promising setup to probe the density wave halo around the anyons in FQAH
phases.

Our results potentially also apply to twisted bilayer graphene/hBN system
where a CDW state occurs at zero magnetic field, and is replaced by a
fractional Chern insulator in a small magnetic fieldXie  _et al._ (2021) at a
fractional filling of the moiré lattice. Thus clearly there is a close
competition between FCI and CDW in this system as well. A small doping of the
fractional Chern insulator will induce anyons with CDW halos as an indication
of the intertwinement we have discussed.

The twisted TMD or twisted bilayer graphene/hBN system will presumably be
better suited for this probe than pentalayer graphene, as the FQAH phase
occurs at much smaller displacement fields which can presumably also be
obtained using the sensor layer as a top gate. Recent theoretical workDong
_et al._ (2023a); Zhou  _et al._ (2023); Dong  _et al._ (2023b) proposes other
rhombohedral graphene multilayers as possible platforms for FQAH physics, and,
some of these may also offer opportunities to explore the physics discussed in
this paper.

We also note that the extended CDW halo around anyons will complicate coherent
physical braiding processes that one might want to do to probe their
statistics (as the moving the anyons around will require also moving the large
region of CDW order).

Finally should a CDW order be observed at some fraction (for, eg.at $1/3$
filling in twisted MoTe2, or by tuning the displacement field at other
fillings), it may be interesting to study the fractionally charged defects of
the CDW order. As we discussed, these defects will have an orbital
magnetization that reflects the proximity to the FQAH phase. This local change
of orbital magnetization compared to the region away from defects may
potentially be detected using a scanning nano-SQUIDVasyukov  _et al._ (2013)
probe.

_Acknowledgements:_ We thank Seth Musser and Kevin Nuckolls for discussions.TS
was supported by NSF grant DMR-2206305, and partially through a Simons
Investigator Award from the Simons Foundation. XYS was supported by the Gordon
and Betty Moore Foundation EPiQS Initiative through Grant No. GBMF8684 at the
Massachusetts Institute of Technology. This work was also partly supported by
the Simons Collaboration on Ultra-Quantum Matter, which is a grant from the
Simons Foundation (Grant No. 651446, T.S.).

## References

  * Sun  _et al._ (2011) K. Sun, Z. Gu, H. Katsura, and S. D. Sarma, Physical review letters 106, 236803 (2011).
  * Sheng  _et al._ (2011) D. Sheng, Z.-C. Gu, K. Sun, and L. Sheng, Nature communications 2, 389 (2011).
  * Neupert  _et al._ (2011) T. Neupert, L. Santos, C. Chamon, and C. Mudry, Physical review letters 106, 236804 (2011).
  * Wang  _et al._ (2011) Y.-F. Wang, Z.-C. Gu, C.-D. Gong, and D. Sheng, Physical review letters 107, 146803 (2011).
  * Tang  _et al._ (2011) E. Tang, J.-W. Mei, and X.-G. Wen, Physical review letters 106, 236802 (2011).
  * Regnault and Bernevig (2011) N. Regnault and B. A. Bernevig, Physical Review X 1, 021014 (2011).
  * Bergholtz and Liu (2013) E. J. Bergholtz and Z. Liu, International Journal of Modern Physics B 27, 1330017 (2013).
  * Parameswaran  _et al._ (2013) S. A. Parameswaran, R. Roy, and S. L. Sondhi, Comptes Rendus Physique 14, 816 (2013).
  * Cai  _et al._ (2023) J. Cai, E. Anderson, C. Wang, X. Zhang, X. Liu, W. Holtzmann, Y. Zhang, F. Fan, T. Taniguchi, K. Watanabe, Y. Ran, T. Cao, L. Fu, D. Xiao, W. Yao, and X. Xu, Nature (2023), 10.1038/s41586-023-06289-w.
  * Zeng  _et al._ (2023) Y. Zeng, Z. Xia, K. Kang, J. Zhu, P. Knüppel, C. Vaswani, K. Watanabe, T. Taniguchi, K. F. Mak, and J. Shan, Nature (2023), 10.1038/s41586-023-06452-3.
  * Park  _et al._ (2023) H. Park, J. Cai, E. Anderson, Y. Zhang, J. Zhu, X. Liu, C. Wang, W. Holtzmann, C. Hu, Z. Liu, T. Taniguchi, K. Watanabe, J.-h. Chu, T. Cao, L. Fu, W. Yao, C.-Z. Chang, D. Cobden, D. Xiao, and X. Xu, Nature (2023), 10.1038/s41586-023-06536-0.
  * Lu  _et al._ (2023) Z. Lu, T. Han, Y. Yao, A. P. Reddy, J. Yang, J. Seo, K. Watanabe, T. Taniguchi, L. Fu, and L. Ju, “Fractional quantum anomalous hall effect in a graphene moire superlattice,” (2023), arXiv:2309.17436 [cond-mat.mes-hall] .
  * Zhang  _et al._ (2019) Y.-H. Zhang, D. Mao, Y. Cao, P. Jarillo-Herrero, and T. Senthil, Physical Review B 99, 075127 (2019).
  * Ledwith  _et al._ (2020) P. J. Ledwith, G. Tarnopolsky, E. Khalaf, and A. Vishwanath, Physical Review Research 2, 023237 (2020).
  * Repellin and Senthil (2020) C. Repellin and T. Senthil, Physical Review Research 2, 023238 (2020).
  * Abouelkomsan  _et al._ (2020) A. Abouelkomsan, Z. Liu, and E. J. Bergholtz, Physical review letters 124, 106803 (2020).
  * Wilhelm  _et al._ (2021) P. Wilhelm, T. C. Lang, and A. M. Läuchli, Physical Review B 103, 125406 (2021).
  * Wu  _et al._ (2019) F. Wu, T. Lovorn, E. Tutuc, I. Martin, and A. MacDonald, Physical review letters 122, 086402 (2019).
  * Yu  _et al._ (2020) H. Yu, M. Chen, and W. Yao, National Science Review 7, 12 (2020).
  * Devakul  _et al._ (2021) T. Devakul, V. Crépel, Y. Zhang, and L. Fu, Nature communications 12, 6730 (2021).
  * Li  _et al._ (2021a) H. Li, U. Kumar, K. Sun, and S.-Z. Lin, Physical Review Research 3, L032070 (2021a).
  * Crépel and Fu (2023) V. Crépel and L. Fu, Phys. Rev. B 107, L201109 (2023).
  * Song  _et al._ (2023) X.-Y. Song, Y.-H. Zhang, and T. Senthil, arXiv preprint arXiv:2308.10903 (2023).
  * Hoffman  _et al._ (2002) J. E. Hoffman, E. W. Hudson, K. M. Lang, V. Madhavan, H. Eisaki, S. Uchida, and J. C. Davis, Science 295, 466 (2002), https://www.science.org/doi/pdf/10.1126/science.1066974 .
  * Lannert  _et al._ (2001) C. Lannert, M. P. Fisher, and T. Senthil, Physical Review B 63, 134510 (2001).
  * Balents  _et al._ (2005a) L. Balents, L. Bartosch, A. Burkov, S. Sachdev, and K. Sengupta, Physical Review B 71, 144508 (2005a).
  * Balents  _et al._ (2005b) L. Balents, L. Bartosch, A. Burkov, S. Sachdev, and K. Sengupta, Phys. Rev. B 71, 144508 (2005b).
  * Zhang  _et al._ (1989) S. C. Zhang, T. H. Hansson, and S. Kivelson, Physical review letters 62, 82 (1989).
  * Read (1989) N. Read, Physical Review Letters 62, 86 (1989).
  * Burkov and Balents (2005) A. Burkov and L. Balents, Physical Review B 72, 134502 (2005).
  * Note (1) It is in principle possible that even an electron with charge-$e$, is the lowest energy charged excitation. However this would be unlikely if the Chern band has close to ideal quantum geometry which naturally have Laughlin quasiparticles at low energy.
  * Song  _et al._ (2023) X.-Y. Song, C.-M. Jian, L. Fu, and C. Xu, arXiv e-prints , arXiv:2310.11632 (2023), arXiv:2310.11632 [cond-mat.str-el] .
  * Li  _et al._ (2021b) H. Li, S. Li, E. C. Regan, D. Wang, W. Zhao, S. Kahn, K. Yumigeta, M. Blei, T. Taniguchi, K. Watanabe, S. Tongay, A. Zettl, M. F. Crommie, and F. Wang, Nature 597, 650 (2021b).
  * Xie  _et al._ (2021) Y. Xie, A. T. Pierce, J. M. Park, D. E. Parker, E. Khalaf, P. Ledwith, Y. Cao, S. H. Lee, S. Chen, P. R. Forrester, _et al._ , Nature 600, 439 (2021).
  * Dong  _et al._ (2023a) Z. Dong, A. S. Patri, and T. Senthil, arXiv preprint arXiv:2311.03445 (2023a).
  * Zhou  _et al._ (2023) B. Zhou, H. Yang, and Y.-H. Zhang, arXiv preprint arXiv:2311.04217 (2023).
  * Dong  _et al._ (2023b) J. Dong, T. Wang, T. Wang, T. Soejima, M. P. Zaletel, A. Vishwanath, and D. E. Parker, arXiv preprint arXiv:2311.05568 (2023b).
  * Vasyukov  _et al._ (2013) D. Vasyukov, Y. Anahory, L. Embon, D. Halbertal, J. Cuppens, L. Neeman, A. Finkler, Y. Segev, Y. Myasoedov, M. L. Rappaport, _et al._ , Nature nanotechnology 8, 639 (2013).


11institutetext: Univ Rennes, Inria, CNRS, IRISA 22institutetext: The
University of Sydney 33institutetext: Fantom Research

# Reusable Formal Verification
of DAG-based Consensus Protocols

Nathalie Bertrand 11 0000-0002-9957-5394 Pranav Ghorpade 22
0009-0001-0421-4490 Sasha Rubin 22 0000-0002-3948-129X Bernhard Scholz 33
0000-0002-7672-7359 Pavle Subotić 33 0000-0002-6536-3932

###### Abstract

DAG-based consensus protocols are being adoption by blockchain companies to
decrease energy footprints and improve security. A DAG-based consensus
protocol collaboratively constructs a partial order of blocks of transactions
and produces linearly ordered blocks. The ubiquity and strategic importance of
blockchains call for formal proof of the correctness of key components,
namely, consensus protocols.

This paper presents a safety-proven formal specification of two DAG-based
protocols. Our specification highlights several dissemination, DAG
construction, and ordering variations that can be combined to express the two
protocols. The formalization requires a refinement approach for modeling the
consensus. In an abstract model, we first show the safety of DAG-based
consensus on leader blocks and then further refine the specification to
encompass all blocks for all processes. The TLA+ specification for a given
protocol consists of 492-732 lines, and the proof system TLAPS verifies
2025-2294 obligations in 6-8 minutes.

###### Keywords:

Formal verification Theorem Proving TLA+ Consensus Blockchain

##  1 Introduction

Cryptocurrencies, and by extension decentralized finance (DeFi), provide a
decentralized alternative to conventional banking and financial institutions,
changing how financial services are accessed, managed, and implemented.
Blockchains are the core technology behind cryptocurrency, and a core
component of modern blockchains is the consensus protocol. These protocols
coordinate processes so that they agree on the state of the blockchain. Early
blockchain consensus protocols assume degrees of synchrony in the environment
to ensure safety and liveness [34, 8, 28, 21]. Recently, a family of
asynchronous probabilistic consensus protocols have been introduced that are
based on Directed Acyclic Graphs (DAGs) [24, 25, 4, 18, 16, 22]. These
protocols report high performance while guaranteeing Byzantine Fault Tolerance
(BFT), utilize processes fairly, and exhibit low communication complexity.
Several leading blockchains have adopted DAG-based protocols as their main
consensus mechanism [3, 16, 23]. Given the trillions of dollars locked in
various blockchains [19], manipulating the blockchain’s consensus protocol is
a natural attack vector. Notably, double-spending attacks [27] attempt to
exploit unsafe protocols by discovering inputs and environment settings that
cause the blockchain to have inconsistent states, resulting in a unit of
currency being used twice. While consensus protocols are almost exclusively
designed with the intent to be safe and thus mitigate such attacks, ad-hoc
software design makes it difficult to ensure that a consensus protocol is safe
for all inputs. For instance, well-established, state-of-the-art blockchains
are unsafe [35].

A rigorous method to ensure safety is to employ _formal verification_ , and
thus construct mathematical objects describing the system behavior and
mathematical proof that the consensus protocol model is correct for all
possible inputs and configurations. While such proof efforts exist for a small
number of consensus protocols [37, 9, 38, 7, 5, 2], the vast majority of
consensus protocols operate with an informal assumption of safety. This is
because formal models of protocols are seen as tedious, time-consuming, and
complex to prove since there is a lack of compositional _building blocks_ that
can be used for proving the correctness of a new protocol. While reuse is
often supported at the specification level, proofs for the given properties
are not compositional and require a rewrite of the proof from scratch. On the
other hand, forgoing modeling and safety proofs is not a safe option because
the number of possible interleavings in an asynchronous environment is
prohibitive. A testing regime for a software implementation might not reveal
deficiencies in the protocol design itself, and malicious behaviors of
Byzantine processes may not be fully understood and covered by test cases.
Generally, testing and traditional model checking do not uphold correctness
for participating processes and their configurations and behavior.

In this paper, we present an industrial case study where proven models of
consensus protocols are used to drive development. In our case study, we
formally verify the safety of two DAG-based protocols: DAG-Rider [24] and
Cordial Miners [25]. Our experience shows that while these (and many other)
DAG-based protocols collectively operate on the same basic principles, the
nuances introduced to improve performance can impact the protocol’s
correctness. Thus, the challenge is to produce specifications and proofs that
_become compositional and extensible_ for existing and new DAG-based
protocols. We create compositional specifications that encapsulate
commonalities between protocols and allow for the reuse of proofs. This relies
on _equality by abstraction_ [39]: Choosing the right abstractions for DAG-
based protocols allows us to decompose protocol properties and proofs into
components. Thus, our work is an important step towards creating
specifications and a collection of proofs that can be largely reused and
require only small changes to handle DAG-based protocols.

We have implemented an open-source formal specification and proof of DAG-rider
and Cordial Miners, publicly available at [20]. Our specification is in the
Temporal Logic of Actions (TLA+) [29]. We perform proofs using the TLA+ proof
system (TLAPS) [12], a proof system for mechanically checking proofs written
in TLA+. Our approach applies to other popular DAG-based protocols, including
BullShark [22], Aleph [18], Hashgraph [4], Lachesis [16] with limited effort.
Additionally, apart from formally proving the safety of DAG-Rider and Cordial
Miners, our proof effort has led us to discover many similarities between DAG-
based consensus protocols, that are not immediately obvious.

The rest of the paper is structured as follows. In Section 2, we give an
introduction to DAG-based consensus protocols. In Section 3, we describe the
abstractions that render verification modular and reusable. In Section 4, we
present the TLA+ specifications of our framework and explain how we
instantiate TLA+ specifications for two popular DAG-based protocols in our
framework. Section 5 discusses how we prove safety compositionally. In Section
6, we evaluate our specification and proof. In Section 7 we discuss how other
DAG protocols can be specified and verified in our framework. We present
related work in Section 8 and conclude in Section 9 with our experience and
future work.

##  2 DAG-based Consensus Protocols in Blockchains

DAG-based consensus protocols [24, 25, 4, 18, 16, 22] solve the Byzantine
Atomic Broadcast (BAB) problem [33, 10, 15], which is to totally order blocks
(a block is a sequence of messages representing transactions, e.g., exchange
of assets) in the presence of a certain proportion of Byzantine processes.
They assume a network of $n$ processes where up to $f$ are byzantine [30] with
$n\geq 3f+1$. Processes can create, sign, and send messages to each other. It
is assumed that every message sent from one correct process to another is
eventually received. In addition, each process can sequentially output (aka
“deliver”) messages. Thus, each process outputs a sequence of messages. In
particular, a DAG-based consensus protocol solves the Ordering Consensus
Problem [25] by ensuring the outputs satisfy two properties: safety and
liveness. Informally, safety states that the output sequence of any two
correct processes is consistent, i.e., one is the prefix of the other;
liveness states that every message sent by a correct process is eventually
output by all the correct processes with probability one. Note that safety and
liveness essentially imply BAB.111BAB also requires message uniqueness (called
non-equivocation in Blockchain). DAG-based protocols are constructed in two
phases: (1) a _communication phase_ also referred to as the DAG construction
phase, and (2) an _ordering phase_. The rest of our description focuses on two
specific protocols called DAG-Rider [24] and Cordial Miners [25]. However, our
description largely extends to other DAG-based protocols as well; we elaborate
on this in Section 7.

##### Communication phase.

In the communication phase, processes create and broadcast vertices in rounds.
Effectively, a vertex consists of the following: the creator’s ID, a round
number, a set of references to vertices from previous rounds (empty for round
0 vertices), and the block that the creator is proposing. Each process builds
a Directed Acyclic Graph (DAG), called its _local DAG_. Vertices in process
$p_{j}$’s local DAG are the vertices that process $p_{j}$ created, as well as
those received from other processes. Outgoing edges in the local DAG from
vertex $v$ go to vertices $v^{\prime}$ referenced by $v$. These are necessary
to ensure that processes understand what other processes see in their local
DAG. A vertex is only added to $p_{j}$’s local DAG once its references have
already been added; in the meantime, the vertex is stored in a buffer. A
process $p_{j}$ is said to have _completed round $r$_ once its local DAG
contains at least $n-f$ vertices with round number $r$. Process $p_{j}$ can
only create and broadcast a vertex in round $r$ once it has completed round
$r-1$. Each local DAG has a natural layered structure: the vertices in round
zero form the bottom layer, and those in round $r$ have edges to (some of)
those in lower layers — this is illustrated in Fig. 1(a), representing the
local DAG of each of the $N=4$ processes $P1$ to $P4$. Thus, each local DAG
imposes a partial order on its vertices. Notice that the local DAGs of
different processes do not have to be equal or even subgraphs of each other.
However, by the above construction, if a vertex $v$ appears in two local DAGs,
then the sub-DAG rooted at $v$ (aka “causal history of $v$”) is the same in
both local DAGs.

##### Ordering phase.

From their local DAG, which represents a partial order of vertices, the task
of each process is to, _independently_ and with no additional communication,
totally order the vertices, and output a sequence of blocks. Totally ordering
the partially-ordered DAG can be achieved by some topological sort of the DAG.
The challenge is to ensure that all correct processes order the vertices
identically. For this if processes could agree on some “anchor” vertices, then
they can linearize the so-far unsorted vertices in the causal history of
anchor vertices by a deterministic procedure like topological sort — agreed
upon prior — for producing the linear order. In Fig. 1(b), the first anchor is
labeled $1$, and the second is $2$. We observe that the difference in causal
history between anchors, indicated by the vertices in the shaded regions, can
now be totally ordered independently by a pre-defined topological sort for
each process. We note that, as a consequence of the FLP impossibility result
[17] and the fact that the rest of the protocol is completely asynchronous and
deterministic, the anchors must be chosen at random. To do this, each process
divides its local DAG into a fixed number of consecutive rounds called _waves_
($4$ in DAG-Rider, $5$ in Cordial Miners). The processes use a Global Perfect
Coin (GPC) to agree on a random leader vertex in each wave. The waves are used
to allow the processes to commit certain leader vertices as anchors. _Thus
reaching a consensus on the sequence of committed wave leaders (aka anchors)
is sufficient to obtain a consistent ordering of vertices in the DAGs._ Blocks
in these ordered vertices can then be sequentially output, ensuring consistent
output sequences (safety).

(a) Communication phase: building local DAGs for each processes and our grid
abstraction depicted for P1.

(b) Ordering phase: selecting wave-leaders across local DAGs.

Figure 1: High-level depiction of the two phases of DAG-based consensus. The
dotted blue lines represent a round that ends a wave, and the dotted black
line represents a round in a wave. Thus, a wave has two rounds in this
example.

At a high level, various DAG-based protocols share the same core aspects.
However, at the component level, they exhibit subtle yet important
differences. For instance, DAG-Rider [24], Aleph [18], and BullShark [22] rely
on a reliable broadcast to disseminate blocks in the communication phase. As a
consequence, from a given round one may receive at most one vertex from any
other process so that non-equivocation — also known as forking — is immediate.
However, use of reliable broadcast can be costly in terms of message
complexity and latency, so for efficiency reasons, protocols such as Cordial
Miners [25], Hashgraph [4], and Lachesis [16] use unreliable communication to
disseminate blocks. As a consequence, a process may receive several blocks
created in the same round by a faulty process, leading to equivocations. This
also complicates the commit wave leader procedure as a wave can have several
leader vertices, and committing a unique one adds extra difficulty.

##  3 Abstractions towards Generic and Simple Specifications

In this section, we describe the overall architecture of our specifications
and proofs. The challenge in creating a reusable formalization is to devise
the appropriate abstractions to make the specifications and the proofs
compositional. The key to the abstraction lies in the representation of the
network state itself. The processes in the network may have received different
sets of messages, and hence might have different local DAGs (as described in
Section 2). Our network state abstraction stores a local DAG for each process.
Each local DAG is stored as a two-dimensional array: an index $(q,r)$ in the
array stores vertices $v$ created by process $q$ at round $r$, and we call
$(q,r)$ the _position_ of the vertex $v$ in the local DAG. Some positions can
be empty; for instance, in the local DAG of $p_{2}$ in in Figure 1(a), the
position $(p_{1},4)$ is empty, representing that $p_{2}$ has not heard (yet)
from process $p_{1}$ at round $4$.

Note that the use of reliable broadcast ensures the presence of at most one
vertex at each position of any local DAG, whereas, with unreliable broadcast
communication, local DAGs may have more than one vertex in each position. To
handle both these cases in a uniform way, and to exploit compositionality, we
break the problem of agreeing on committed wave leader vertices into two
subproblems: (1) agree on a vertex for every position (since a position may
contain multiple vertices), (2) agree on committed wave leader positions. With
this decomposition, we can separate the specification of the consensus
protocols into two specifications. The communication specification encompasses
the communication phase in which the DAGs are constructed, as well as the
protocol that agrees on a vertex for every position.222Thus, we make the
subproblem “agree on a vertex for every position” part of the communication
phase specification (even if it is described in the ordering phases in certain
protocols, such as Cordial Miners). The ordering specification encompasses the
protocol that agrees on committed wave leader positions.

Toward a uniform presentation of the ordering specification, we perform an
abstraction of the local DAGs. Instead of recording all the positions in a
local DAG, we can focus on wave leader positions only. Since each wave has a
unique leader position, we construct and store a _wave-DAG_. Vertices of the
_wave-DAG_ are only the wave leader vertices constructed in the communication
phase. Edges of the _wave-DAG_ represent: (1) the transitive closure of strong
edges for DAG-Rider, and (2) the ratification relation for Cordial Miners
between the representative vertex of wave leader positions. On the other hand,
we provide separate communication specifications for reliable broadcast and
unreliable broadcast. Unreliable broadcast is a basic form of communication
and can be implemented in various ways. Thus, towards a uniform presentation
of unreliable broadcast communication, we abstract out actual communication.
We represent the reception of a vertex by process $p$ from process $q$ as
process $p$ non-deterministically copying a vertex from the local DAG of
process $q$. Non-determinism here allows us to represent all possible
interleavings that a specific communication implementation would yield. For
reliable broadcast, we assume that the network will ignore all but the first
message from a process with a given round. Finally, in the refinement step,
for each communication specification, we instantiate the ordering
specification from it and perform a synchronous product of the two
specifications. Although the specifications do not have the same set of
actions, we use a function that maps actions in the communication
specification to the actions in the ordering specification. This gives us
complete specifications and proof of safety for protocols; DAG-Rider and
Cordial Miners as shown in Fig. 2.

Figure 2: Structure of the specification of two DAG-based protocols.

##### Miscellaneous Simplifying Abstractions.

In our specification, a vertex in a position not only represents a block but
the entire causal history of this vertex in the DAG (inspired by [24]). This
abstraction significantly helps us to provide formal proofs of safety, as it
implies that agreeing on anchor vertex in our abstraction equates to agreeing
on the causal history of the anchor vertex. Since we focus on safety
properties in this paper, we simplify the protocol specification by removing
features that can be ignored for safety and are only required for liveness. In
particular, random coin tosses (used by the GPC) can be replaced with
deterministic ones. The choice of leader position for each wave is thus
represented by a deterministic function (a parameter to the specification, not
a fixed function) that maps wave IDs to positions. Not only does this simplify
the specification by overcoming the impossibility of encoding random choices
in TLA+, but this also allows us to obtain a unique specification for DAG
protocols, even if they differ in the way they propose random wave leaders, as
is the case for instance for BullShark [22], Aleph [18], and Lachesis [16].

We employ a _procedural abstraction_ that ignores all states that are internal
to a procedure of the pseudo-code of the protocol and only represents the
input/output behaviour of each procedure. For instance, in the
$\mathtt{wave\\_ready}$ procedure described in algorithm 3 in DAG-Rider [24],
the relevant variables are $\mathtt{decidedWave}$,
$\mathtt{deliveredVertices}$, and $\mathtt{leadersStack}$, but neither the
loop variable $\mathtt{w^{\prime}}$ nor the auxiliary variable
$\mathtt{v^{\prime}}$ are important in our specification. We also use
_memoization_ to efficiently compute the values taken by recursive functions,
by introducing a fresh state variable that stores the needed information to
evaluate recursive functions in a single step.

##  4 Specifications of DAG-based Consensus Protocols

In this section, we discuss in detail our TLA+ specifications and how to
compose them to get specifications of DAG-Rider and Cordial Miners [20]:

  * •

ReliableBcastCommunicationSpecification.tla

  * •

UnreliableBcastCommunicationSpecification.tla

  * •

LeaderConsensusSpecification.tla

###  4.1 Specifying Communication in TLA+

####  4.1.1 Specifying Reliable Broadcast Communication

Reliable broadcast ensures three crucial properties, namely validity,
agreement and integrity [24]. Validity and agreement are only necessary to
prove the liveness of the consensus. Since we focus on the safety properties
of consensus, we simplify the specification of reliable broadcast into a
weaker version that does not guarantee validity nor agreement, yet ensures
integrity. Integrity in our setting states that every correct process is
delivered at most one vertex with a round, from a process. In our weakened
specification, we assume that only the first broadcast vertex of a process
with a round $r$ can be delivered, thus ensuring integrity.

Our state variables are shown in Listing 1. The variable broadcastNetwork
stores the sets of vertices to be delivered for each process, whereas
broadcastRecord tracks processes that have broadcasted a vertex in each round.
Whenever any process broadcasts vertex $v$ with round $r$, then $v$ is only
added to the broadcastNetwork provided the broadcastRecord indicates no
previous broadcast by that process with round $r$. For each process $p$,
blocksToPropose stores the sequence of blocks proposed by $p$ but whose vertex
is not yet created and broadcasted by $p$; dag and round, respectively store
the local DAG and recently completed round for $p$; finally buffer stores
vertices received via reliable broadcast that are not yet added to the DAG of
$p$. Variable faulty stores a set of faulty processes.

Listing 1: State variables of Reliable broadcast communication.

⬇

broadcastNetwork \in [ProcessSet \cup {"History"}->SUBSET(TaggedVertexSet)]

broadcastRecord \in [ProcessSet->[RoundSet -> BOOLEAN]]

blocksToPropose \in [ProcessSet->Seq(BlockSet)]

dag \in [ProcessSet->[RoundSet->[ProcessSet->VertexSet \cup NilVertexSet]]]

round \in [ProcessSet->RoundSet]

buffer \in [ProcessSet->SUBSET(VertexSet)]

faulty \in SUBSET(ProcessSet)

The DAG construction is encoded by a state machine with four types of
transitions. Propose adds a new block to blocksToPropose; ReceiveVertex picks
a vertex to be delivered, verifies its creator’s identity and checks if it has
enough parent vertices ($2f+1$) to add it to the buffer. Under specific
conditions AddVertex transfers a vertex from the buffer to the dag; NextRound
increments round whenever a new round is completed. Additionally, it creates a
new vertex for the new next round in the dag and broadcasts it to other
processes (i.e. tries to add to the broadcastNetwork).

The safety of the reliable broadcast communication phase is formalized as a
state invariant DagConsistency as shown in Listing 2. This invariant states
that, at every position, the added vertex is the same for all correct
processes.

Listing 2: DagConsistency Invariant. Here VertexSet is set of all possible
vertices in the local DAG.

⬇

DagConsistency ==

\A p, q \in ProcessSet, r \in RoundSet, o \in ProcessSet :

(r /= 0 /\ dag[p][r][o] \in VertexSet /\ dag[q][r][o] \in VertexSet ) =>
dag[p][r][o] = dag[q][r][o]

####  4.1.2 Specifying Unreliable Broadcast Communication

Recall from section 3, with an unreliable broadcast, processes can have more
than one vertex in the same position in their local DAG. Thus specifying
unreliable broadcast communication has the additional challenge of specifying
a protocol for picking a unique representative vertex for every position. This
is done using the concept of Ratification [25].

In unreliable broadcast communication as mentioned in Section 3, we abstract
out the actual communication. This abstraction eliminates the need for
variables broadcastNetwork and buffer. Similarly, we also abstract away block
proposals by non-deterministically choosing to add a vertex, containing a
block in its DAG. This eliminates variable blocksToPropose. Finally, we also
remove variable round that stores the recently completed round as this can be
computed by simply looking at the local DAG. As shown in Listing 3, our
unreliable broadcast communication specification only has two state variables,
namely, dag and faulty. Variable dag in this case is defined slightly
differently. First, at each position, the sets of vertices along with a
ratified vertex are stored.

Listing 3: State variables of unreliable broadcast communication.

⬇

dag \in [ProcessSet->[RoundSet->[ProcessSet->[ vertices: SUBSET(VertexSet),
ratifiedVertex: VertexSet \cup {"Nil"} ]]]]

faulty \in SUBSET(ProcessSet)

The communication phase here performs two tasks: constructing local DAGs and
computing a ratified vertex for each position. These are encoded in the TLA+
state machine using AddVertex and RatifyVertex. For every correct process $p$;
AddVertex adds a vertex $v$ to the DAG of $p$ If; 1) source of $v$ is $p$ and
a round of $v$ is a new round of the DAG construction. Vertex $v$ has $2f+1$
parents in the previous round of the DAG of $p$; or 2) source of $v$ is some
other process $q$ such that $v$ is in DAG of $q$. Additionally, all the
parents of $v$ are in the DAG of $p$ with at least $2f+1$ of them in the round
previous to that of $v$. Lastly, RatifyVertex ratifies a vertex for a position
and stores it in the dag, as prescribed in the Cordial Miners [25].

The safety of the unreliable broadcast communication phase is formalized as a
state invariant RatificationConsistency as shown in Listing 4. This invariant
states that for every correct process, at every position the ratified vertex
is the same as for all other correct processes.

Listing 4: RatificationConsistency invariant.

⬇

RatificationConsistency ==

\A p \in ProcessorSet, q \in ProcessorSet, r \in RoundSet, o \in ProcessorSet:
( p \notin faulty /\ dag[p][r][o].ratifiedVertex =/ "Nil" /\ q \notin faulty
/\ dag[q][r][o].ratifiedVertex =/ "Nil" ) =>

dag[p][r][o].ratifiedVertex = dag[q][r][o].ratifiedVertex

###  4.2 Specifying the Ordering in TLA+

Towards a uniform presentation of the ordering phase in which protocols use a
global perfect coin to obtain an order on transactions from local DAG
structures, we consider an abstraction of the DAG structures local to each
process. As explained in Section 3, reaching a consensus on the sequence of
committed wave-leaders is sufficient to obtain an ordering of vertices in the
DAGs. Thus each process has a _wave-DAG_. Vertices of the _wave-DAG_ are only
the wave leader vertices in the DAG constructed in the communication phase.
Edges of the _wave-DAG_ represent: (1) the transitive closure of edges for
DAG-Rider, and (2) the ratification relation for Cordial Miners.

As shown in Listing 5, the state variables include the LeaderRelation to
represent a snapshot of the wave-DAG: For every process $p$ and wave ID $w$
LeaderRelation stores information about the presence of the leader vertex of
wave $w$ in the wave-DAG of $p$, along with the set of all other waves, wave
$w$ has an edge pointing to. Four extra variables are added: decidedWave
stores the last decided wave by $p$, leaderSeq stores the Sequence of waves
committed in increasing order by the current and the last decided wave and for
every wave $w$, commitWithRef stores the sequence of waves that $w$ will
commit if decided by process $p$, and faulty stores IDs of faulty processes.

Listing 5: State variables of ordering phase.

⬇

leaderRelation \in [ ProcessSet->[WaveSet->[exists: BOOLEAN, edges:
SUBSET(WaveSet)]]]

decidedWave \in [ProcessSet->WaveSet \cup {0}]

leaderSeq \in [ProcessSet->[current: Seq(WaveSet),last: Seq(WaveSet)]]

commitWithRef \in [ProcessSet->[WaveSet->Seq(WaveSet)]]

faulty \in SUBSET(ProcessSet)

The state machine performs two tasks, each represented by a transition. First,
CreateNewWave constructs the wave-DAG. It adds a new wave with its edges to
LeaderRelation, and it computes and stores in commitWithRef the sequence of
waves that this wave would commit if decided. Second, DecideWave decides a
wave and further commits waves. It updates decidedWave with a new wave ID,
additionally, it updates leaderSeq for the newly decided wave (by querying to
commitWithRef). The two transitions are only enabled from states that satisfy
some specific conditions, illustrated in the code snippet in Listings 6 and 7.

Listing 6: CreateNewWave transition.

⬇

CreateNewWaveTn(p, w, E) ==

/\ p \notin faulty =>

(/\ leaderRelation[p][w].exists = FALSE \\* 1

/\ \A x \in E : leaderRelation[p][x].exists = TRUE \\* 2

/\ \A x \in E : x < w \\* 3

/\ \A q \in ProcessSet: \\* 4

q \notin faulty /\ leaderRelation[q][w].exists = TRUE

=> leaderRelation[q][w].edges = E /\ \A q \in ProcessSet: \\* 5

q \notin faulty /\ decidedWave[q] # 0

/\ decidedWave[q] < w => decidedWave[q] \in E)

/\ commitWithRef’=[commitWithRef EXCEPT ![p][w] =

IF E = {} THEN <<w>> ELSE Append(commitWithRef[p][max(E)], w)]

/\ leaderRelation’ = [leaderRelation

EXCEPT ![p][w] = [exists |-> TRUE, edges |-> E]]

/\ UNCHANGED <<decidedWave, leaderSeq, faulty>>

Listing 7: DecideWave transition.

⬇

DecideWaveTn(p, w) ==

/\ p \notin faulty =>

(/\ leaderRelation[p][w].exists=TRUE \\* 1

/\ w >= decidedWave[p] \\* 2

/\ \A x \in WaveSet: \\* 3

x > w => leaderRelation[p][x].exists=FALSE

/\ \A q \in ProcessSet, x \in WaveSet: \\* 4

q \notin faulty /\ x > w /\ leaderRelation[q][x].exists = TRUE

=> w \in leaderRelation[q][x].edges)

/\ decidedWave’ = [decidedWave EXCEPT ![p] = w]

/\ leaderSeq’ = [leaderSeq EXCEPT ![p]= [current |-> commitWithRef[p][w],

last |-> leaderSeq[p].current]]

/\ UNCHANGED <<commitWithRef, leaderRelation, faulty>>

The safety properties the ordering specification should meet are formalized as
two-state invariants LeaderConsistency and LeaderMonotonicity as shown in
Listing 8. On the one hand, LeaderConsistency informally states that the
sequences of committed leaders of any two correct processes are a prefix one
of the other. On the other hand, LeaderMonotonicity intuitively states that
wave commits happen monotonically concerning the order in which waves are
decided. This implies that the order in which waves were committed by the last
decided wave will not be altered by the new decided wave.

Listing 8: LeaderConsistency and LeaderMonotonicity invariants.

⬇

LeaderConsistency ==

\A p, q \in ProcessorSet:

p \notin faulty /\ q \notin faulty /\ decidedWave[p] <= decidedWave[q] =>

IsPrefix(leaderSeq[p].current, leaderSeq[q].current)

LeaderMonotonicity ==

\A p \in ProcessorSet: p \notin faulty =>

IsPrefix(leaderSeq[p].last, leaderSeq[p].current)

###  4.3 Complete Protocol Specification

Our complete specification is a refinement of the ordering phase, including
the communication phase. More precisely, we use the _interface refinement_
construct of TLA+ that allows one to obtain a lower-level specification by
instantiating the variables of a higher-level specification. The use of this
construct is shown in Listing 9. The refinement and the interactions between
the two phases are instantiated with GPC, that gives a candidate leader
position for each wave. Whenever a vertex is added (ratified in the case of
Cordial Miners) at the candidate leader position for a wave in the
communication phase, CreateNewWave is instantiated in the ordering phase.
Similarly, whenever a wave is ready and can be decided in the local DAG
constructed by the communication phase (DAG-Rider and Cordial Miners use
different criteria for this), DecideWave is instantiated on the ordering
specification. For the rest of the actions in the communication phase, the
state of the ordering phase remains unchanged. Thus, the complete
specification additionally requires specifying GPC and modifying actions in
communication specification to instantiate ordering specification.

Listing 9: Instantiation of ordering phase in concrete protocol specification.

⬇

LeaderConsensus ==

INSTANCE LeaderConsensusVerification

WITH NumWaves <- w,

NumProcesses <- n,

f <- f,

commitWithRef <- commitWithRef,

decidedWave <- decidedWave,

leaderRelation <- leaderRelation,

leaderSeq <- leaderSeq,

faulty <- faulty

##### Details of specifying GPC.

GPC ensures unpredictability, agreement, termination, and fairness when
choosing candidate wave-leaders. Intuitively GPC samples uniformly at random a
process ID for each wave, together with a holding mechanism to force
unpredictability if only Byzantine processes query the global coin. Similarly
to how we specified reliable broadcast, we relax the guarantees of the global
perfect coin to obtain a compact specification. Our specification does not
guarantee unpredictability and need not imply fairness, however it ensures
agreement and termination. Dropping unpredictability and fairness enables us
to model the global perfect coin as an arbitrary function, common to all
correct processes, from the set of waves WaveSet to the set of processes
ProcessSet. In a sense, this relaxation of the global perfect coin simulates
an increased power for Byzantine processes. However, we observe it is
sufficient to prove safety, thus establishing that the consensus is safe,
independent of the function ChooseLeader.

##  5 Safety Proofs in TLAPS

In this section, we discuss the invariants, theorems, and proof technique for
formally proving the safety of the specifications described in section 4. The
invariants and proofs for each specification can be found in their
corresponding Verification.tla files [20].

####  5.0.1 Theorems and Invariants

To prove the DAGConsistency invariant (Listing 2) we identify and formalize 6
new invariants (Inv1, …, Inv6). Intuitively, Inv2 and Inv3 formalize the
correctness of our weaker Reliable Broadcast abstraction. Inv1 states that
every vertex in the dag of a correct process is in its buffer. Inv4 states
that every message in the buffer of a correct process is in the history of
broadcastNetwork. Inv5 states that the history of broadcastNetwork has at most
one message for each round and source process. Finally, Inv6 states that
vertices in the dag of a correct process are placed at the right positions,
i.e., they have consistent round and source with respect to the position. Fig.
3 illustrates the dependencies between these six invariants. Inv1, Inv2, Inv3,
and Inv6 are proven independently whereas Inv4 and Inv5 are proven assuming
invariants Inv2 and Inv3 hold, respectively. Finally, DagConsistency is proved
assuming Inv1, Inv4, Inv5 and Inv6.

Figure 3: Invariant dependency for safety (naming is local to each tree)

To prove the RatificationConsistency invariant (Listing 4) we identify,
formalize and prove 6 more invariants. Similarly, to prove the safety of the
ordering specification, namely LeaderConsistency and LeaderMonotonicity
(Listing 8) invariants, we identify, formalize and prove ten further
invariants. Dependencies of all these invariants are depicted in Figure
3.Finally, to prove the complete safety of DAG-Rider and Cordial Miners we
prove the Safety Theorem described in Listing 10.

Listing 10: Complete safety theorem for DAG-Rider and Cordial Miners
specification.

⬇

THEOREM DAGRiderSpec => [](DagConsistency /\ LeaderConsistency /\
LeaderMonotonicity)

THEOREM CordialMinersSpec => [](RatificationConsistency /\ LeaderConsistency
/\ LeaderMonotonicity)

####  5.0.2 Proof Strategy

The proofs in TLAPS follows a standard hierarchical structure and use proofs
by induction and proofs by contradiction. Here, we simply give a high-level
outline of the proof strategy for proving invariants. We outline the proof for
an inductive invariant (Inv1) of the ordering specification in Fig. 11. To
prove that this invariant holds on all reachable states of the ordering phase
specification, we state the following: $\texttt{LEMMA
Inv1correctness}=\texttt{Spec}\rightarrow\Box\texttt{Inv1}.$ Here Spec is a
TLA+ macro name for the ordering specification, it has the form
$\texttt{Spec}=\texttt{Init}\land\Box\texttt{[Next]}_{\texttt{vars}}$, where
vars, Init, Next are TLA+ macro names for set of variables, the initial state,
and the possible actions leading to the next state. The lemma is proved by
induction. The induction basis $\texttt{Init}\rightarrow\texttt{Inv1}$ is
trivial and TLAPS proves it automatically. The induction step is captured by
$\texttt{Inv1}\land\Box\texttt{[Next]}_{\texttt{vars}}\rightarrow\texttt{Inv1'}\enspace,$
where $\texttt{[Next]}_{\texttt{vars}}$ represents that either the state
machine performs a Next step, or remains idle, and Inv1’ states that the
invariant holds on the state after performing
$\texttt{[Next]}_{\texttt{vars}}$. These two cases are reflected in the code
snippet as $\mathtt{{<}2{>}1}$ and $\mathtt{{<}2{>}2}$. Then, Next is a
disjunction of three cases, each of which is proved separately in
$\mathtt{{<}3{>}1}$, $\mathtt{{<}3{>}2}$, and $\mathtt{{<}3{>}3}$, and these
lower-level goals are proven using the same strategy of identifying even
lower-level goals. This process is somewhat mechanical, and TLAPS allows one
to write proofs in such a fashion, i.e. breaking it into lower-level proof
obligations. Ultimately, the lowest-level proof obligations are proved by
breaking down the definition of the terms in the statements.

Listing 11: Proof structure of a specific invariant for the ordering
specification.

⬇

LEMMA Inv1Lem == Spec => []Inv1

<1>1 Init => Inv1

...

<1>2 ASSUME StateType, StateType’, Inv1, [Next]_vars

PROVE Inv1’

<2>1 ASSUME StateType, StateType’, Next, Inv1

PROVE Inv1’

<3>1 ASSUME NEW p \in ProcessSet, NEW w \in WaveSet, NEW E \in
SUBSET(WaveSet),

UpdateWaveTn(p, w, E)

PROVE Inv1’

...

<3>2 ASSUME NEW p \in ProcessSet, NEW w \in WaveSet, UpdateDecidedWaveTn(p, w)

PROVE Inv1’

...

<3>3 ASSUME NEW p \in ProcessSet, ProcessFailureTn(p)

PROVE Inv1’

...

<3> QED BY <3>1, <3>2, <3>3, <2>1 DEF Next

<2>2 ASSUME UNCHANGED vars, Inv1

PROVE Inv1’

...

<2> QED BY <2>1, <2>2

<1> QED BY <1>1, <1>2, TypeLem, PTL DEF Spec

##  6 Evaluation

Overall, the effort to understand, specify, and prove DAG-Rider and Cordial
Miners required approximately 9 and 3 person-months respectively, distributed
across 5 people. We evaluate the performance of our formal proof using TLA+
and TLAPS. Table 1 lists metrics including the sizes of the specifications for
the respective communication phases (reliable communication for DAG-Rider and
unreliable communication for Cordial Miners) and the common ordering phase. It
also reports on metrics related to proof complexity, such as the size of proof
files, the maximum depth of the proof, the maximum branching in the tree-like
proof structure and the number of base proof obligations. Finally, the table
displays the verification time for proving the safety of each phase.

Table 1: Specification and proof metrics. Performed on a 2.10 GHz CPU with 8 GB of memory, running Windows 11 and TLAPS v1.4.5. In the table DR is DAG-Rider and CM is Cordial Miners. Metric $\backslash$ Phase | Ordering | RB Comm. | unRB Comm. | DR | CM
---|---|---|---|---|---
Size of spec. (# loc) | 272 | 403 | 160 | 272+460 | 432+60
Size of proof (# loc) | 822 | 460 | 594 | 521 | 657
Max level of proof tree nodes | 9 | 10 | 9 | 10 | 9
Max degree of proof tree nodes | 7 | 7 | 8 | 7 | 8
# obligations in TLAPS | 1302 | 633 | 895 | 1303+722 | 1303+991
Time to check by TLAPS (s) | 125 | 49 | 68 | 125+224 | 125+360

Remarkably, the safety of both DAG-based protocols can be proved within
minutes. The modularity of our specifications is a clear advantage since DAG-
Rider’s and Cordial Miner’s specifications share the same ordering phase
specification in the common file LeaderConsensusSpecification.tla, and the
corresponding same safety proof in LeaderConsensusVerification.tla. As far as
the communication phase is concerned, as we found with these two case studies,
even if the communication mechanisms differ, the effort to adapt the
specification and the proofs was minimal (approximately 3 times less) when
moving from DAG-Rider to Cordial Miners. Lastly, the glue specification needed
was around 60 lines for both DAG-rider and Cordial Miners.

##  7 Discussion

We now explain how to specify and prove safety properties for other DAG-based
protocols using our framework, namely BullShark [22], Aleph [18], Hashgraph
[4], and Lachesis [16]. For BullShark, there are two variants: partially
synchronous and eventually synchronous. Using our framework with no additional
effort we have formally verified the eventually synchronous BullShark, the
specification and proofs can be found in [20]. Eventually synchronous
BullShark and DAG-Rider have three key differences: (i) It has additional
timeouts in the DAG construction — this only refines our RB communication
specification and thus requires no additional work for safety; (ii) wave-
leaders are predetermined instead of randomized — we already handle arbitrary
deterministic wave-leader functions, and thus this also requires no additional
work; (iii) the wave size is two instead of four. We created an eventually
synchronous BullShark specification file that is similar to the DAG-Rider
specification file except that the wave size is two instead of four.
Additionally, we had to update some of the proofs from handling arithmetic
modulo of two to four. The changes required for BullShark took us $1$ person
months. Handling partially synchronous BullShark and the other protocols
listed requires more work, mainly on the Ordering Specification, which reduces
the entire effort by at least $50\%$. To see that handling the Communication
Specification is light, note that partially synchronous BullShark has same
communication as eventually synchronous BullShark and thus RB communication
file can be used here as well without any change. For Hashgraph/Lachesis, one
would only refine the unRB communication specification to handle the
unstructured DAG and use the fact that the unRB communication specification
already specifies the structure of the so-called witness-DAG/root-DAG (thus
our existing proofs prove non-equivocation), while for Aleph we can use our RB
communication file without change [18].

##  8 Related work

Parameterized verification is the problem of verifying a protocol for
arbitrarily many processes [6]. For consensus protocols that tolerate
Byzantine failures, this means verifying the protocol is correct for all
values of the parameters $n,f$ with $n\geq 3f+1$. In comparison, traditional
model-checking only handles finite-state systems, and thus finitely many
values of the parameters $n,f$. For instance, the Tendermint consensus
protocol [28] has been modeled in TLA+, and certain properties, such as
termination, were model-checked for small values of the parameters [7]. Our
work can be seen as a contribution to the parameterized verification of
distributed protocols by machine-checkable proofs. An alternative approach is
to use parameterized model-checkers, e.g., ByMC [26]. For instance, Safety and
Liveness of the consensus algorithm used in the Red Belly Blockchain [13] has
been verified for all values of the parameters $n,f$ with $n\geq 3f+1$[5].
Although the algorithm only broadcasts binary values, that work verified both
safety and liveness (under a weak fairness assumption).

Other BFT consensus protocols have been verified using interactive theorem
provers. The work in [37] uses the IVy interactive theorem prover [1] to
formally verify a variant of the Moonshine consensus protocol [37]. The work
in [32] uses IVy and Isabelle/HOL [36] to verify the Stellar Consensus
Protocol [31]. The Algorand [21] consensus protocol has been verified using
Coq [11]. The safety of several non-Byzantine protocols such as variants of
Paxos [9, 38] have been verified using interactive theorem proving. However,
these protocols are not robust to Byzantine faults and they have limited
application in blockchains.

To the best of our knowledge, the only other work specific to DAG-based
consensus protocols is an unpublished technical report by Crary [14]
describing a formal verification of a DAG-based consensus algorithm, Hashgraph
[4], with the theorem prover Coq. In contrast to that approach, our TLA+
specifications of DAG-based consensus protocols are lower-level; they are
closer to actual implementations of the protocols and therefore require fewer
manual abstractions. Clear advantages of our approach are its separation of
concerns between the communication phase and the ordering phase, and the
reusability for several DAG-based consensus protocols.

##  9 Conclusion and Experience

Overall the effort to specify and prove three DAG-based consensus protocols
required approximately 13 person months. However, with modularization, we
found that the turn-around time for specifying and proving Cordial Miner’s
protocol was significantly reduced, taking 3 person months. Specifying and
proving Eventually synchronous BullShark took even less time, taking just 1
person month. We believe several other protocols can be modeled and proven
with equally reduced efforts. We argue that while the effort required of our
approach is arguably more than that of typical pen-and-paper proofs, machine-
checkable specifications and proofs forced us to be much more rigorous and
define our specification as a precise abstraction of the source code. In the
future, we can leverage our proven specification as a model for model-driven
test-case generation [40] which would not be possible with paper&pen proofs.
Thus we not only were able to prove the safety of our conceptual model of the
protocol but also ensure that the implementation corresponded to the model. We
are currently expanding the specifications and proofs to support additional
improved DAG-based protocols designed from insights obtained during the
specification and proving process.

## References

  * [1] Ahn, K.Y., Denney, E.: Testing first-order logic axioms in program verification. In: Fraser, G., Gargantini, A. (eds.) Tests and Proofs - 4th International Conference, TAP@TOOLS 2010, Málaga, Spain, July 1-2, 2010\. Proceedings. Lecture Notes in Computer Science, vol. 6143, pp. 22–37. Springer (2010). https://doi.org/10.1007/978-3-642-13977-2_4, https://doi.org/10.1007/978-3-642-13977-2_4
  * [2] Aminof, B., Rubin, S., Stoilkovska, I., Widder, J., Zuleger, F.: Parameterized model checking of synchronous distributed algorithms by abstraction. In: Dillig, I., Palsberg, J. (eds.) Verification, Model Checking, and Abstract Interpretation - 19th International Conference, VMCAI 2018, Los Angeles, CA, USA, January 7-9, 2018, Proceedings. Lecture Notes in Computer Science, vol. 10747, pp. 1–24. Springer (2018). https://doi.org/10.1007/978-3-319-73721-8_1, https://doi.org/10.1007/978-3-319-73721-8_1
  * [3] Aptos Foundation: Understanding Aptos: A comprehensive overview (2024), https://messari.io/report/understanding-aptos-a-comprehensive-overview
  * [4] Baird, L., Luykx, A.: The hashgraph protocol: Efficient asynchronous BFT for high-throughput distributed ledgers. In: Proceedings of COINS 2020. pp. 1–7. IEEE (2020). https://doi.org/10.1109/COINS49042.2020.9191430
  * [5] Bertrand, N., Gramoli, V., Konnov, I., Lazic, M., Tholoniat, P., Widder, J.: Holistic verification of blockchain consensus. In: Scheideler, C. (ed.) 36th International Symposium on Distributed Computing, DISC 2022, October 25-27, 2022, Augusta, Georgia, USA. LIPIcs, vol. 246, pp. 10:1–10:24. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022). https://doi.org/10.4230/LIPICS.DISC.2022.10, https://doi.org/10.4230/LIPIcs.DISC.2022.10
  * [6] Bloem, R., Jacobs, S., Khalimov, A., Konnov, I., Rubin, S., Veith, H., Widder, J.: Decidability of Parameterized Verification. Synthesis Lectures on Distributed Computing Theory, Morgan & Claypool Publishers (2015). https://doi.org/10.2200/S00658ED1V01Y201508DCT013, https://doi.org/10.2200/S00658ED1V01Y201508DCT013
  * [7] Braithwaite, S., Buchman, E., Konnov, I., Milosevic, Z., Stoilkovska, I., Widder, J., Zamfir, A.: Formal specification and model checking of the tendermint blockchain synchronization protocol (short paper). In: Bernardo, B., Marmsoler, D. (eds.) 2nd Workshop on Formal Methods for Blockchains, FMBC@CAV 2020, July 20-21, 2020, Los Angeles, California, USA (Virtual Conference). OASIcs, vol. 84, pp. 10:1–10:8. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020). https://doi.org/10.4230/OASICS.FMBC.2020.10, https://doi.org/10.4230/OASIcs.FMBC.2020.10
  * [8] Buterin, V.: Ethereum white paper: A next generation smart contract & decentralized application platform (2013), https://github.com/ethereum/wiki/wiki/White-Paper
  * [9] Chand, S., Liu, Y.A., Stoller, S.D.: Formal verification of multi-paxos for distributed consensus. In: Fitzgerald, J.S., Heitmeyer, C.L., Gnesi, S., Philippou, A. (eds.) FM 2016: Formal Methods - 21st International Symposium, Limassol, Cyprus, November 9-11, 2016, Proceedings. Lecture Notes in Computer Science, vol. 9995, pp. 119–136 (2016). https://doi.org/10.1007/978-3-319-48989-6_8, https://doi.org/10.1007/978-3-319-48989-6_8
  * [10] Coelho, P., Junior, T.C., Bessani, A., Dotti, F., Pedone, F.: Byzantine fault-tolerant atomic multicast. In: 2018 48th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN). pp. 39–50 (2018). https://doi.org/10.1109/DSN.2018.00017
  * [11] Coquand, T., Huet, G.P.: The calculus of constructions. Inf. Comput. 76(2/3), 95–120 (1988). https://doi.org/10.1016/0890-5401(88)90005-3, https://doi.org/10.1016/0890-5401(88)90005-3
  * [12] Cousineau, D., Doligez, D., Lamport, L., Merz, S., Ricketts, D., Vanzetto, H.: TLA + proofs. In: Proceedings of FM 2012. Lecture Notes in Computer Science, vol. 7436, pp. 147–154. Springer (2012). https://doi.org/10.1007/978-3-642-32759-9_14, https://doi.org/10.1007/978-3-642-32759-9_14
  * [13] Crain, T., Natoli, C., Gramoli, V.: Red belly: A secure, fair and scalable open blockchain. In: 42nd IEEE Symposium on Security and Privacy, SP 2021, San Francisco, CA, USA, 24-27 May 2021. pp. 466–483. IEEE (2021). https://doi.org/10.1109/SP40001.2021.00087, https://doi.org/10.1109/SP40001.2021.00087
  * [14] Crary, K.: Verifying the hashgraph consensus algorithm. Tech. rep., CMU (2021), https://arxiv.org/abs/2102.01167
  * [15] Cristian, F., Aghili, H., Strong, R., Dolev, D.: Atomic broadcast: From simple message diffusion to byzantine agreement. Information and Computation 118(1), 158–179 (1995). https://doi.org/https://doi.org/10.1006/inco.1995.1060, https://www.sciencedirect.com/science/article/pii/S0890540185710607
  * [16] Fantom Foundation: Lachesis aBFT (2024), https://docs.fantom.foundation/technology/lachesis-abft
  * [17] Fischer, M.J., Lynch, N.A., Paterson, M.S.: Impossibility of distributed consensus with one faulty process. Journal of the ACM 32(2), 374–382 (1985)
  * [18] Gagol, A., Lesniak, D., Straszak, D., Swietek, M.: Aleph: Efficient atomic broadcast in asynchronous networks with Byzantine nodes. In: Proceedings of the 1st ACM Conference on Advances in Financial Technologies, AFT 2019, Zurich, Switzerland, October 21-23, 2019. pp. 214–228. ACM (2019). https://doi.org/10.1145/3318041.3355467, https://doi.org/10.1145/3318041.3355467
  * [19] Geko, C.: Ethereum white paper: A next generation smart contract & decentralized application platform (2024), https://www.coingecko.com/en/chains
  * [20] Ghorpade, P.: Reusable TLA+ specification and Proofs for DAG based Consensus Protocols. https://github.com/pranavg5526/Reusable-Formal-Verification-of-DAG-based-Consensus (2024), [Online; accessed 26-April-2024]
  * [21] Gilad, Y., Hemo, R., Micali, S., Vlachos, G., Zeldovich, N.: Algorand: Scaling Byzantine agreements for cryptocurrencies. In: Proceedings of SOSP 2017. pp. 51–68. ACM (2017). https://doi.org/10.1145/3132747.3132757
  * [22] Giridharan, N., Kokoris-Kogias, L., Sonnino, A., Spiegelman, A.: Bullshark: Dag bft protocols made practical. Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security (2022), https://api.semanticscholar.org/CorpusID:246015617
  * [23] Hedra: Streamlining consensus (2024), https://hedera.com/blog/streamlining-consensus-throughput-and-lower-latency-with-about-half-the-events
  * [24] Keidar, I., Kokoris-Kogias, E., Naor, O., Spiegelman, A.: All you need is DAG. In: Proceedings of PODC 2021. pp. 165–175. ACM (2021). https://doi.org/10.1145/3465084.3467905, https://doi.org/10.1145/3465084.3467905
  * [25] Keidar, I., Naor, O., Poupko, O., Shapiro, E.: Cordial miners: Fast and efficient consensus for every eventuality. In: Oshman, R. (ed.) 37th International Symposium on Distributed Computing, DISC 2023, October 10-12, 2023, L’Aquila, Italy. LIPIcs, vol. 281, pp. 26:1–26:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023). https://doi.org/10.4230/LIPICS.DISC.2023.26, https://doi.org/10.4230/LIPIcs.DISC.2023.26
  * [26] Konnov, I.V., Lazic, M., Veith, H., Widder, J.: A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms. In: Castagna, G., Gordon, A.D. (eds.) Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017. pp. 719–734. ACM (2017). https://doi.org/10.1145/3009837.3009860, https://doi.org/10.1145/3009837.3009860
  * [27] Kumar, A., Kumar Sah, B., Mehrotra, T., Rajput, G.K.: A review on double spending problem in blockchain. In: 2023 International Conference on Computational Intelligence and Sustainable Engineering Solutions (CISES). pp. 881–889 (2023). https://doi.org/10.1109/CISES58720.2023.10183579
  * [28] Kwon, J.: Tendermint: Consensus without mining. https://tendermint.com/docs/tendermint.pdf (2014)
  * [29] Lamport, L.: Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley (2002), http://research.microsoft.com/users/lamport/tla/book.html
  * [30] Lamport, L., Shostak, R., Pease, M.: The byzantine generals problem. ACM Transactions on Programming Languages and Systems (TOPLAS) 4(3), 382–401 (1982)
  * [31] Lokhava, M., Losa, G., Mazières, D., Hoare, G., Barry, N., Gafni, E., Jove, J., Malinowsky, R., McCaleb, J.: Fast and secure global payments with stellar. In: Brecht, T., Williamson, C. (eds.) Proceedings of the 27th ACM Symposium on Operating Systems Principles, SOSP 2019, Huntsville, ON, Canada, October 27-30, 2019. pp. 80–96. ACM (2019). https://doi.org/10.1145/3341301.3359636, https://doi.org/10.1145/3341301.3359636
  * [32] Losa, G., Dodds, M.: On the formal verification of the stellar consensus protocol. In: Bernardo, B., Marmsoler, D. (eds.) 2nd Workshop on Formal Methods for Blockchains, FMBC@CAV 2020, July 20-21, 2020, Los Angeles, California, USA (Virtual Conference). OASIcs, vol. 84, pp. 9:1–9:9. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2020). https://doi.org/10.4230/OASICS.FMBC.2020.9, https://doi.org/10.4230/OASIcs.FMBC.2020.9
  * [33] Milosevic, Z., Hutle, M., Schiper, A.: On the reduction of atomic broadcast to consensus with byzantine faults. In: 2011 IEEE 30th International Symposium on Reliable Distributed Systems. pp. 235–244 (2011). https://doi.org/10.1109/SRDS.2011.36
  * [34] Nakamoto, S.: Bitcoin: A peer-to-peer electronic cash system (2008)
  * [35] Neu, J., Tas, E.N., Tse, D.: Two more attacks on proof-of-stake ghost/ethereum. In: Proceedings of the 2022 ACM Workshop on Developments in Consensus. p. 43–52. ConsensusDay ’22, Association for Computing Machinery, New York, NY, USA (2022). https://doi.org/10.1145/3560829.3563560, https://doi.org/10.1145/3560829.3563560
  * [36] Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL - A Proof Assistant for Higher-Order Logic, Lecture Notes in Computer Science, vol. 2283. Springer (2002). https://doi.org/10.1007/3-540-45949-9, https://doi.org/10.1007/3-540-45949-9
  * [37] Praveen, M., Ramesh, R., Doidge, I.: Formally verifying the safety of pipelined moonshot consensus protocol. CoRR abs/2403.16637 (2024). https://doi.org/10.48550/ARXIV.2403.16637, https://doi.org/10.48550/arXiv.2403.16637
  * [38] Schultz, W., Dardik, I., Tripakis, S.: Formal verification of a distributed dynamic reconfiguration protocol. In: Popescu, A., Zdancewic, S. (eds.) CPP ’22: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Philadelphia, PA, USA, January 17 - 18, 2022. pp. 143–152. ACM (2022). https://doi.org/10.1145/3497775.3503688, https://doi.org/10.1145/3497775.3503688
  * [39] Soffer, P.: Refinement equivalence in model-based reuse: Overcoming differences in abstraction level. J. Database Manag. 16, 21–39 (07 2005)
  * [40] Wang, D., Dou, W., Gao, Y., Wu, C., Wei, J., Huang, T.: Model checking guided testing for distributed systems. In: Proceedings of the Eighteenth European Conference on Computer Systems. p. 127–143. EuroSys ’23, Association for Computing Machinery, New York, NY, USA (2023). https://doi.org/10.1145/3552326.3587442, https://doi.org/10.1145/3552326.3587442