A declarative approach to specifying distributed algorithms using three-valued modal logic

Luca Zanolini; Murdoch J. Gabbay

REVIEW 2 major objections 4 minor 12 references

A declarative approach to specifying distributed algorithms using three-valued modal logic

T0 review · 2 major / 4 minor · reviewed 2026-08-09 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read Paxos can be presented as a logical theory in Coalition Logic, with validity, agreement, and termination derived as theorems.

desk verdict The fixed-point semantics are internally inconsistent: 'forever' and 'finally' denote bottom, making the Paxos axioms unsatisfiable and the correctness proofs vacuous. read the letter →

arxiv 2502.00892 v1 pith:552YNEI5 submitted 2025-02-02 cs.LO math.LO

Murdoch J. Gabbay , Luca Zanolini This is my paper · ORCID

classification cs.LOmath.LO MSC 03B4568M1403B7068Q60

keywords three-valuedlogicmodalfixed-pointdistributedalgorithmsPaxosconsensussemitopologyquorumintersectiondeclarativespecification

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

Coalition Logic is a three-valued modal fixed-point logic for describing distributed algorithms as logical theories: an algorithm is a signature plus axioms, and its correctness properties are derived from those axioms rather than from a step-by-step description of state changes. The paper's central demonstration is an axiomatisation of Paxos, called Declarative Paxos, from which validity, agreement, and termination are proved as theorems. The reason this matters is that it turns correctness arguments into ordinary proofs about an abstract model, with message passing and control flow deliberately elided. The framework is intended as a general tool for specifying and checking distributed algorithms, with the Paxos case study showing the approach can handle a non-trivial protocol.

What carries the argument

The load-bearing object is the semitopology: a set of participants with a family of open sets closed under arbitrary unions, where open sets model quorums or actionable coalitions. On top of it, the logic uses three truth-values $t$, $b$, $f$ (true, crashed/no value, false), modalities that quantify over participants and open sets, a fixed-point operator for temporal iteration, and the $R\rightarrow$ construct that looks back to the most recent value making a predicate true. The $n$-twined property, meaning any $n$ nonempty open sets intersect, supplies the logical form of quorum intersection on which the agreement proof rests.

What would settle it

A concrete test: instantiate the theory on the semitopology $\mathrm{AllBut}_1(2)$, where the two participants form two disjoint singleton quorums, and give a valuation in which one quorum accepts value $v_0$ and the other accepts $v_1$ while the leader writes $v_0$ to the first and $v_1$ to the second. All axioms except (Pax2Twined) can hold, yet one participant decides $v_0$ and the other decides $v_1$; checking that the proof of Lemma 7.3.2 really fails at the step invoking (Pax2Twined) settles whether the quorum-intersection axiom is necessary.

Watch

Extended reading notes

Core claim

On its own terms, the paper establishes that Paxos has a declarative logical essence: a small set of axioms in Coalition Logic that mention no messages and no machine states still suffice to derive the standard correctness properties. The derivations are Theorem 7.2.3 (if a participant decides v then some leader proposed v), Theorem 7.3.6 (any two decided values are equal), and Theorem 7.4.7 (every correct participant eventually decides). The key modelling choice is to let quorums be open sets of a semitopology, so that the classic quorum-intersection condition becomes the single axiom (Pax2Twined): any two nonempty open sets intersect. Under the standard all-but-f model this axiom is exactly the condition $N > 2f$.

Load-bearing premise

The load-bearing premise is axiom (Pax2Twined), which asserts that any two nonempty quorums share at least one participant; in the standard all-but-f model this is exactly the condition $N > 2f$, and if quorums are allowed to be disjoint the agreement proof no longer goes through.

Editorial extensions

If this is right

Paxos correctness becomes a consequence of the axioms: validity, agreement, and termination are theorems of Declarative Paxos, not separate checked properties.
Because the theory is parametric in the underlying semitopology, the same axioms cover every quorum system satisfying the 2-twined intersection property, not just strict-majority quorums.
A failure to derive a property from the axioms indicates either a missing assumption or a logical error in the algorithm design, giving the framework a diagnosis role.
The minimal theory Simpler Declarative Paxos distills exactly the axioms needed for the correctness proofs, identifying the logical essence that makes Paxos work.
Message passing and control flow are absent from the specification, so correctness can be studied at the level of logical assertions about what participants believe and decide.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

If the method scales, other consensus protocols whose safety rests on quorum intersection could be axiomatised by choosing the appropriate $n$-twined property, with agreement proofs following the same template.
The deliberate absence of message passing means Coalition Logic complements, rather than replaces, operational specifications: it can state what must hold, while an operational model would still be needed to ask how messages are delivered in time.
A testable extension would be to instantiate the axioms on finite all-but-f semitopologies and run a proof search or SAT-based checker, turning the derived theorems into machine-checkable certificates for small $N$ and $f$.
The paper's treatment of integrity — a decided participant stops — as 'decide(v) remains true forever' suggests a general pattern: in this logic, termination of a process is expressed as eventual stability of a predicate's truth-value, not as halting.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

Colleague,

The stress-test note is right, and it lands hard. Figure 4 defines [[µX.φ]] as the least fixed point (the meet of all pre-fixed points). For foreverφ = µX. tomorrow(φ ∧ X), the constant-bottom function ⊥ is a fixed point of the operator κ ↦ λctx. φ(next(ctx)) ∧ κ(next(ctx)), since ⊥ ∧ anything = ⊥. So [[foreverφ]] = ⊥ for every φ. Then finallyψ = sometime⊥ = ⊥. That makes every forward axiom in Figure 10 — (PaxSend!), (PaxAccept!), (PaxWrite!), (PaxDecideL!), (PaxDecide¬L!) — and also (LdrCorrect) and everything built from infinitely/finally, denote f at every context. The theory Θ_Pax has no model, and the Section 7 "derivations" are vacuously true rather than substantive. The right-hand denotation column for forever (the infinite conjunction over future stages) is the greatest fixed point of that operator, not the least; Remark 3.4.1(2)'s accumulator starting at t also computes the greatest fixed point. So the formal definition of µ and the intended semantics of the derived connectives flatly contradict each other.

That's a load-bearing flaw, not a nitpick. But the paper has real content around it: the three-valued modal setup with semitopological quorums is a genuine new combination, the axiomatisation of Paxos is detailed and recognisably Paxos, and the discussion of the forward/backward rule recipe and GSLT is thoughtful. The 2-twined assumption is explicit and correctly encodes N > 2f; that part is fine. The proofs are manual and long, and the termination proof leans heavily on GSLT, but the bigger problem is that the axioms they use are formally unsatisfiable.

The reader's conditional verdict was too kind: the correctness risk is not medium but high, because the central semantics are broken. The circularity concern is real but secondary. I also think the paper overclaims generality in the abstract.

This deserves scrutiny — the ideas could be salvageable with a corrected fixed-point semantics (possibly using greatest fixed points for forever/infinitely, or a different operator). But as written, the formal core is inconsistent. I would not cite it yet, but I would send it to a knowledgeable referee to see whether the repair is straightforward or reveals deeper issues.

Referee Report

2 major / 4 minor

Summary. The paper introduces Coalition Logic, a three-valued modal fixed-point logic interpreted over semitopological models, and proposes using it to specify distributed algorithms declaratively. It develops the syntax, denotational semantics, and a number of proof-theoretic lemmas, then axiomatizes a 'Declarative Paxos' theory Θ_Pax (Figure 10) and claims to derive the standard correctness properties of validity, agreement, and termination (Theorems 7.2.3, 7.3.6, and 7.4.7). The central claim is that these properties follow from the axioms, with message passing abstracted away and quorum structure represented by open sets.

Significance. If the technical problems were repaired, the methodological idea is genuinely interesting: a declarative, semitopological account of quorums, with a clean separation between backward rules, forward progress rules, and explicit liveness/correctness axioms. The identification of n-twined semitopologies with quorum intersection conditions (Proposition 5.2.3) and the substantial Paxos case study are valuable. The paper is also unusually explicit about the design choices in the axioms. However, the current manuscript has a fundamental internal inconsistency in its fixed-point semantics that makes the stated Paxos derivations vacuous. I do not see circularity in the use of (Pax2Twined) or (LdrCorrect): these are explicitly stated axioms, and the agreement proof uses them transparently; the problem is elsewhere. Because the central claim is unsupported as written, the paper cannot be accepted in its present form, although the error is localized enough that a major revision could plausibly repair it.

major comments (2)

[Figures 4-5; Proposition 3.4.8] The fixed-point semantics is internally inconsistent and makes `forever` and all of its derivatives denote the bottom truth-value f. Figure 4 defines [µX.φ] as the meet of all prefixed points {κ | [φ[X:=κ]] ≤ κ}, which is the least fixed point, exactly as Proposition 3.4.8 states. For `foreverφ = µX. tomorrow(φ ∧ X)`, the defining functional is F(κ)(n,p,O,ς) = [φ](n+1,p,O,ς) ∧ κ(n+1,p,O,ς). The constant function ⊥ = λctx.f satisfies F(⊥) = ⊥, so ⊥ is a prefixed point; hence the least fixed point is ⊥. Therefore [foreverφ] = ⊥ for every φ. In particular, for φ = t the displayed denotation ⋀_{n'>n} t = t in Figure 5 is false. That denotation is the greatest fixed point of F, not the least one, and Remark 3.4.1(2)'s accumulator initialized to t confirms that a greatest fixed point was intended. Consequently `finally φ = sometime foreverφ` also denotes ⊥, since [sometime ⊥] = µX. tomorrow X = ⊥. This is not a cosmetic issue: every `finally`-wrapped axiom in Figure 10—(PaxSend!), (PaxWrite!), (PaxAccept!), (PaxDecideL!), (PaxDecide¬L!)—and also (LdrCorrect), which uses `inﬁnitely`, has denotation f, and f is not a valid truth-value.
[Figure 10; Definition 3.5.2; Section 7] Because of the fixed-point problem described above, the theory Θ_Pax has no model in the sense of Definition 3.5.2: no valuation satisfies all axioms, since the `finally`-wrapped forward rules and (LdrCorrect) are invalid everywhere. As a result, the statements Θ_Pax ⊨ φ in Theorem 7.2.3, Theorem 7.3.6, and Theorem 7.4.7 are vacuously true for every φ, rather than being genuine derivations of Paxos correctness. Lemma 4.5.3 is also false under the stated semantics: for φ = t it would require [inﬁnitely t] = t, but the definition gives f. The paper should either introduce a greatest fixed-point operator (e.g., ν) and use it for `forever`, `inﬁnitely`, and `ﬁnally`, or define these connectives directly by their intended infinite meet/join semantics; in either case, the consequences for the proofs in Sections 4 and 7 must be rechecked.

minor comments (4)

[Definition 3.1.2(2)(a)] The closure condition for open sets says `⋃ O ∈ Point`; it should say `⋃ O ∈ Open`.
[Lemma 2.2.7(3)] The 'In words' line says 'T tv is valid' but the statement is about `F tv`; the wording should be corrected.
[Definition 7.4.2(2)] The definition refers to 'the rules in Figure 4 that start with `finally`' but the forward rules are in Figure 10, not Figure 4.
[Figure 5] The right-hand denotation column for derived expressions is presented without a proof that it matches the syntactic sugar under the fixed-point semantics; after correcting the fixed-point clauses, these equivalences should be verified systematically.

Circularity Check

1 steps flagged · score 8.0 of 10

The µ-fixed-point clause makes `forever` and `finally` denote bottom, so the forward axioms are unsatisfiable and the Section 7 derivations are vacuous.

self definitional [Figure 5 (derived syntax for forever, sometime, finally); Figure 4 (clause for µ); Proposition 3.4.8; Remark 3.4.1(2)]
"foreverφ =µ X. tomorrow (φ ∧ X) ... [[foreverφ]]_{n,p,O,ς} = ⋀_{n'>n} [[φ]]_{n',p,O,ς} ... [[µ X.φ]]_{n,p,O,ς} = (⋀ {κ ∈ 3Ctx | [[φ[X:=κ]]]≤ κ})(n,p,O,ς) ... Proposition 3.4.8: [[µ X.φ]] is a least fixedpoint ... foreverφ ... Set an accumulator to t."

For F(κ) = λctx. [[φ]]_{next(ctx)} ∧ κ(next(ctx)), the constant-bottom function ⊥ is a fixed point: F(⊥) = ⊥. Since Proposition 3.4.8 defines µ as the least fixed point, [[foreverφ]] = ⊥ for every φ. Then finallyφ = sometime foreverφ is also ⊥, so every finally-wrapped axiom — (PaxSend!), (PaxAccept!), (PaxWrite!), (PaxDecideL!), (PaxDecide¬L!) — denotes f at every context and is never valid. Hence Θ_Pax has no satisfying valuation, and the Section 7 claims Θ_Pax ⊨ validity/agreement/termination hold only vacuously. The advertised derivation reduces, by the paper's own fixed-point definition, to inference from an inconsistent theory rather than from the protocol axioms.

full rationale

The paper's proof strategy is, on its face, not circular: the correctness properties are not listed as axioms; they are proved from explicit protocol and environment assumptions such as (PaxPropose?), (PaxDecideL?), (Pax2Twined), (LdrCorrect), and (PaxPCorrect). Those axioms encode standard Paxos quorum-intersection and liveness assumptions, and such encodings are ordinary logical modeling rather than circularity. However, the manuscript's own semantics contains a self-definitional collapse that undermines the entire derivation. Figure 5 defines forever as µX. tomorrow(φ ∧ X), while Proposition 3.4.8 states µ is the least fixed point; the constant-bottom function is a fixed point of that operator, so forever is bottom, and consequently finally is bottom. The forward progress axioms are wrapped in finally and therefore denote f everywhere, making the theory unsatisfiable. As a result, the claimed correctness theorems are entailed only vacuously, so the central claim that Paxos correctness properties are 'derived' from the axioms is not supported by the paper's own equations. This is a definitional vacuity rather than a fitted parameter or self-citation chain; it is the dominant issue for assessing the derivation chain.

Assumptions & free parameters 0 free parameters · 7 assumptions · 0 invented entities

The central results rest on the explicit axioms of Declarative Paxos and on background mathematical facts. No numeric free parameters are fitted to data, but the choice of model (semitopology, value set, validity convention) is a structural parameter. The ledger lists the axioms invoked in the proofs of validity, agreement, and termination.

assumptions (7)

standard math Semitopology axioms: Open is closed under arbitrary unions and Point is open.
Definition 3.1.2. Underlies the meaning of modalities and quorum quantification; taken from prior semitopology work [Gab24, Gab25].
standard math Knaster-Tarski fixed-point theorem for the complete lattice 3^Ctx.
Invoked in Proposition 3.4.8 to justify the least-fixed-point semantics of the mu operator.
domain assumption Validity convention: 3valid = {t, b}, so crashed participants returning b are valid.
Definition 2.2.1 and Remark 2.2.2. Makes liveness statements concise, but it is a modeling choice used throughout the paper.
ad hoc to paper Backward rules: (PaxPropose?), (PaxSend?), (PaxWrite?), (PaxAccept?), (PaxDecideL?), (PaxDecide not L?).
Figure 10. These axioms specify the protocol's constraints and are used directly in the validity and agreement proofs.
ad hoc to paper Forward rules: (PaxPropose!), (PaxSend!), (PaxWrite!), (PaxAccept!), (PaxDecideL!), (PaxDecide not L!), wrapped in finally except (PaxPropose!).
Figure 10. Encode eventual network synchrony and GSLT; used in the termination proof.
ad hoc to paper Leader axioms: (LdrExist), (LdrExt), (LdrCorrect).
Used in Lemma 7.3.2(1) for agreement and in Theorem 7.4.7 for termination; (LdrExt) is an axiom scheme over closed predicates.
ad hoc to paper Correctness and quorum axioms: (PaxPCorrect), (PaxPropose01), (PaxWrite01), (Pax2Twined).
PaxPCorrect assumes quorums of uncrashed participants; PaxPropose01 and PaxWrite01 assume at most one proposed or written value; Pax2Twined is a logical form of quorum intersection, equivalent to N > 2f in AllBut_f(N).

how reviews work

0 comments

Cite this review

Pith. "Pith review of A declarative approach to specifying distributed algorithms using three-valued modal logic." pith.science (2026). https://pith.science/paper/552YNEI5

@misc{pith2026250200892,
  author       = {Pith},
  title        = {Pith review of: A declarative approach to specifying distributed algorithms using three-valued modal logic},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/552YNEI5}},
  note         = {Machine review of arXiv:2502.00892}
}

read the original abstract

We present Coalition Logic, a three-valued modal fixed-point logic designed for declaratively specifying and reasoning about distributed algorithms, such as the Paxos consensus algorithm. Our methodology represents a distributed algorithm as a logical theory, enabling correctness properties to be derived directly within the framework -- or revealing logical errors in the algorithm's design when they exist. Coalition Logic adopts a declarative approach, specifying the overall logic of computation without prescribing control flow. Notably, message-passing is not explicitly modeled, distinguishing our framework from approaches like TLA+. This abstraction emphasises the logical essence of distributed algorithms, offering a novel perspective on their specification and reasoning. We define the syntax and semantics of Coalition Logic, explore its theoretical properties, and demonstrate its applicability through a detailed treatment of the Paxos consensus algorithm. By presenting Paxos as a logical theory and deriving its standard correctness properties, we showcase the framework's capacity to handle non-trivial distributed systems. We envision Coalition Logic as a versatile tool for specifying and reasoning about distributed algorithms. The Paxos example highlights the framework's ability to capture intricate details, offering a new lens through which distributed algorithms can be specified, studied, and checked.

Figures

Figures reproduced from arXiv: 2502.00892 by the authors.

**Figure 2.** Truth-tables for notions of equivalence (Definition [PITH_FULL_IMAGE:figures/full_fig_p008_2.png] view at source ↗

**Figure 3.** Term and predicate syntax of Coalition Logic (Definit [PITH_FULL_IMAGE:figures/full_fig_p015_3.png] view at source ↗

Figures from the paper (8 more)

**Figure 4.** Figure 4: Denotational semantics of Coalition Logic (Definiti [PITH_FULL_IMAGE:figures/full_fig_p017_4.png]

**Figure 5.** Figure 5: Derived syntactic sugar expressions (Definition [PITH_FULL_IMAGE:figures/full_fig_p018_5.png]

**Figure 6.** Figure 6: Bounded complete lattice structure on the function s [PITH_FULL_IMAGE:figures/full_fig_p021_6.png]

**Figure 7.** Figure 7: Validity of φ in a theory Θ (Definition 3.5.2) We read this as φ is valid in the context ctx. (2) n, p ς φ means ∀O ∈ Open6=∅.(n, p, O ς φ). (3) n ς φ means ∀p ∈ Point.∀O ∈ Open6=∅.(n, p, O ς φ). (4) ς φ means ∀n ∈ N≥0.∀p ∈ Point.∀O ∈ Open6=∅.(n, p, O ς φ). (5) …

**Figure 8.** Figure 8: Abbreviations inspired by higher-order logic (Nota [PITH_FULL_IMAGE:figures/full_fig_p024_8.png]

**Figure 9.** Figure 9: Some easy equivalences 4.2. Two commutation lemmas We note some simple commutation lemmas. These results are all easy facts of our model, but it only takes a few lines to spell them out: Lemma 4.2.1 (Commuting connectives). Suppose φ and φ ′ are closed predicates and s…

**Figure 10.** Figure 10: ΘTyPax: Axioms of Declarative Paxos (Definition 6.3.1) where: (1) the signature ΣTyPax is ΣTyPax = [leader : 0; propose,send,write, accept, decide : 1], as per the notation in Definition 3.2.1(3), and (2) the axioms ΘTyPax are as written in [PITH_FULL_IMAGE:figures/f…

**Figure 11.** Figure 11: Simpler Declarative Paxos (Definition 8.2.1) (1) the signature ΣTySPax is ΣTySPax = [leader : 0; propose,write, accept, decide : 1], as per the notation in Definition 3.2.1(3), and (2) the axioms ΘTySPax are as written in [PITH_FULL_IMAGE:figures/full_fig_p064_11.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

12 extracted references · 10 canonical work pages

[1]

1-3, 31–60

[AAZ11] Ofer Arieli, Arnon Avron, and Anna Zamansky, Ideal paraconsistent logics, Studia Logica 99 (2011), no. 1-3, 31–60. [ACM20] Ignacio Amores-Sesar, Christian Cachin, and Jovan a Micic, Security analysis of ripple consen- sus, 24th International Conference on Principles of Distribut ed Systems, OPODIS 2020, December 14-16, 2020, Strasbourg, France (Vi...

work page 2011
[3]

Gabbay, Semitopology: decentralised collaborative action via top ology, algebra, and logic, College Publications, August 2024, ISBN 9781848904651

[Gab24] Murdoch J. Gabbay, Semitopology: decentralised collaborative action via top ology, algebra, and logic, College Publications, August 2024, ISBN 9781848904651. [Gab25] , Semitopology: a topological approach to decentralised collaborative action, The Jour- nal of Logic and Computation (2025), https://doi.org/10.1093/logcom/exae050. [Got22] Siegfried ...

doi:10.1093/logcom/exae050 2025
[9]

Reiter, Byzantine quorum systems , Distributed Comput

Declarative distributed algorithms via modal logic 69 [MR98] Dahlia Malkhi and Michael K. Reiter, Byzantine quorum systems , Distributed Comput. 11 (1998), no. 4, 203–213. [NTT21] Joachim Neu, Ertem Nusret Tas, and David Tse, Ebb-and-ﬂow protocols: A resolution of the availability-ﬁnality dilemma , 42nd IEEE Symposium on Security and Privacy, SP 2021, San...

work page 1998
[65]

27, IEEE, 1994, pp

[NW94] Moni Naor and Avishai Wool, The load, capacity and availability of quorum systems , Proceed- ings 35th Annual Symposium on Foundations of Computer Scien ce, vol. 27, IEEE, 1994, pp. 214–225. [OKK+23] Rodrigo Otoni, Igor Konnov, Jure Kukovec, Patrick Eugst er, and Natasha Sharygina, Symbolic model checking for TLA+ made faster, Tools and Algorithms ...

work page 1994
[1962]

2705–2718

[SGSK22] Alexander Spiegelman, Neil Giridharan, Alberto S onnino, and Lefteris Kokoris-Kogias, Bull- shark: DAG BFT protocols made practical , Proceedings of the 2022 ACM SIGSAC Con- ference on Computer and Communications Security, CCS 2022, Los Angeles, CA, USA, November 7-11, 2022 (Heng Yin, Angelos Stavrou, Cas Cremers , and Elaine Shi, eds.), ACM, 202...

work page 2022
[1990]

Seltz er and Paul J

[CL99] Miguel Castro and Barbara Liskov, Practical byzantine fault tolerance, Proceedings of the Third USENIX Symposium on Operating Systems Design and Implement ation (OSDI), New Or- leans, Louisiana, USA, February 22-25, 1999 (Margo I. Seltz er and Paul J. Leach, eds.), USENIX Association, 1999, pp. 173–186. [CV17] Christian Cachin and Marko Vukolic, Bl...

work page 1999
[1999]

Korhonen, eds.), ACM, 2021, pp

[KKNS21] Idit Keidar, Eleftherios Kokoris-Kogias, Oded Na or, and Alexander Spiegelman, All you need is DAG, PODC ’21: ACM Symposium on Principles of Distributed Compu ting, Virtual Event, Italy, July 26-30, 2021 (Avery Miller, Keren Censor-Hillel, and Janne H. Korhonen, eds.), ACM, 2021, pp. 165–175. [KLR19] Markus Alexander Kuppe, Leslie Lamport, and Da...

work page 1994
[2002]

3-Slot-Finality Protocol for Ethereum

[DSTZ24] Francesco D’ Amato, Roberto Saltini, Thanh-Hai Tr an, and Luca Zanolini, 3-slot-ﬁnality pro- tocol for ethereum, CoRR abs/2411.00558 (2024). [DZ23] Francesco D’ Amato and Luca Zanolini, A simple single slot ﬁnality protocol for ethereum , Computer Security. ESORICS 2023 International Workshops - CyberICS, DPM, CBT, and SECPRE, The Hague, The Neth...

work page Pith review arXiv 2024

Show all 12 references

[2008]

Zhang, Combining GHOST and Casper , CoRR abs/2003.03052 (2020)

[BHK+20] Vitalik Buterin, Diego Hernandez, Thor Kamphefner, Khi em Pham, Zhi Qiao, Danny Ryan, Juhyeok Sin, Ying Wang, and Y an X. Zhang, Combining GHOST and Casper , CoRR abs/2003.03052 (2020). [BKM18] Ethan Buchman, Jae Kwon, and Zarko Milosevic, The latest gossip on BFT con...

2020 arXiv
[2011]

[CDL+12] Denis Cousineau, Damien Doligez, Leslie Lamport, Steph an Merz, Daniel Ricketts, and Hern´ an Vanzetto,TLA + proofs , FM 2012: Formal Methods - 18th International Sym- posium, Paris, France, August 27-31,

2012
[2012]

7436, Springer, 2012, pp

Proceedings (Di mitra Giannakopoulou and Dominique M´ ery, eds.), Lecture Notes in Computer Science, vol. 7436, Springer, 2012, pp. 147–154. [CGR11] Christian Cachin, Rachid Guerraoui, and Lu´ ıs E. T. Rodrigues, Introduction to reliable and secure distributed programming (2. ...

2012
[2024]

Y akovenko, Solana: A new architecture for a high performance blockchain v0.8.13, Whitepa- per, 2018, https://solana.com/solana-whitepaper.pdf

[Y ak18] A. Y akovenko, Solana: A new architecture for a high performance blockchain v0.8.13, Whitepa- per, 2018, https://solana.com/solana-whitepaper.pdf. [YML99] Yuan Yu, Panagiotis Manolios, and Leslie Lamport, Model checking TLA+ speciﬁcations , Cor- rect Hardware Design a...

2018

Pith tools

Reviewed August 9, 2026 · model on record in the stance chip above.

[1] [1]

1-3, 31–60

[AAZ11] Ofer Arieli, Arnon Avron, and Anna Zamansky, Ideal paraconsistent logics, Studia Logica 99 (2011), no. 1-3, 31–60. [ACM20] Ignacio Amores-Sesar, Christian Cachin, and Jovan a Micic, Security analysis of ripple consen- sus, 24th International Conference on Principles of Distribut ed Systems, OPODIS 2020, December 14-16, 2020, Strasbourg, France (Vi...

work page 2011

[2] [3]

Gabbay, Semitopology: decentralised collaborative action via top ology, algebra, and logic, College Publications, August 2024, ISBN 9781848904651

[Gab24] Murdoch J. Gabbay, Semitopology: decentralised collaborative action via top ology, algebra, and logic, College Publications, August 2024, ISBN 9781848904651. [Gab25] , Semitopology: a topological approach to decentralised collaborative action, The Jour- nal of Logic and Computation (2025), https://doi.org/10.1093/logcom/exae050. [Got22] Siegfried ...

doi:10.1093/logcom/exae050 2025

[3] [9]

Reiter, Byzantine quorum systems , Distributed Comput

Declarative distributed algorithms via modal logic 69 [MR98] Dahlia Malkhi and Michael K. Reiter, Byzantine quorum systems , Distributed Comput. 11 (1998), no. 4, 203–213. [NTT21] Joachim Neu, Ertem Nusret Tas, and David Tse, Ebb-and-ﬂow protocols: A resolution of the availability-ﬁnality dilemma , 42nd IEEE Symposium on Security and Privacy, SP 2021, San...

work page 1998

[4] [65]

27, IEEE, 1994, pp

[NW94] Moni Naor and Avishai Wool, The load, capacity and availability of quorum systems , Proceed- ings 35th Annual Symposium on Foundations of Computer Scien ce, vol. 27, IEEE, 1994, pp. 214–225. [OKK+23] Rodrigo Otoni, Igor Konnov, Jure Kukovec, Patrick Eugst er, and Natasha Sharygina, Symbolic model checking for TLA+ made faster, Tools and Algorithms ...

work page 1994

[5] [1962]

2705–2718

[SGSK22] Alexander Spiegelman, Neil Giridharan, Alberto S onnino, and Lefteris Kokoris-Kogias, Bull- shark: DAG BFT protocols made practical , Proceedings of the 2022 ACM SIGSAC Con- ference on Computer and Communications Security, CCS 2022, Los Angeles, CA, USA, November 7-11, 2022 (Heng Yin, Angelos Stavrou, Cas Cremers , and Elaine Shi, eds.), ACM, 202...

work page 2022

[6] [1990]

Seltz er and Paul J

[CL99] Miguel Castro and Barbara Liskov, Practical byzantine fault tolerance, Proceedings of the Third USENIX Symposium on Operating Systems Design and Implement ation (OSDI), New Or- leans, Louisiana, USA, February 22-25, 1999 (Margo I. Seltz er and Paul J. Leach, eds.), USENIX Association, 1999, pp. 173–186. [CV17] Christian Cachin and Marko Vukolic, Bl...

work page 1999

[7] [1999]

Korhonen, eds.), ACM, 2021, pp

[KKNS21] Idit Keidar, Eleftherios Kokoris-Kogias, Oded Na or, and Alexander Spiegelman, All you need is DAG, PODC ’21: ACM Symposium on Principles of Distributed Compu ting, Virtual Event, Italy, July 26-30, 2021 (Avery Miller, Keren Censor-Hillel, and Janne H. Korhonen, eds.), ACM, 2021, pp. 165–175. [KLR19] Markus Alexander Kuppe, Leslie Lamport, and Da...

work page 1994

[8] [2002]

3-Slot-Finality Protocol for Ethereum

[DSTZ24] Francesco D’ Amato, Roberto Saltini, Thanh-Hai Tr an, and Luca Zanolini, 3-slot-ﬁnality pro- tocol for ethereum, CoRR abs/2411.00558 (2024). [DZ23] Francesco D’ Amato and Luca Zanolini, A simple single slot ﬁnality protocol for ethereum , Computer Security. ESORICS 2023 International Workshops - CyberICS, DPM, CBT, and SECPRE, The Hague, The Neth...

work page Pith review arXiv 2024