Pith. sign in

REVIEW 4 major objections 4 minor 26 references

FastSet: Parallel Claim Settlement

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

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

Pith's one-line read FastSet claims validators need no consensus or communication if claims from different accounts are weakly independent: processing them in either order yields the same state.

desk verdict A genuine generalization of FastPay to arbitrary weakly-independent claims with solid core proofs, but the practical language setl explicitly drops the central hypothesis and the theorems don't cover it. read the letter →

arxiv 2506.23395 v3 pith:FUZWV6UK submitted 2025-06-29 cs.DC

Xiaohong Chen , Grigore Rosu This is my paper · ORCID
classification cs.DC MSC 68M1468Q8568Q60
keywords FastSetweakindependenceparallelclaimsettlementstrongeventualconsistencydistributedconsensusactormodelverifiablecomputingblockchain
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

This paper proposes FastSet, a settlement protocol in which clients broadcast signed claims and validators process them independently, in the order they happen to arrive, without communicating with each other. The central claim is that this works correctly whenever claims issued by different accounts are weakly independent: if two such claims are each valid in a state, either processing order is valid and produces the same state. Under that assumption, the paper proves four properties: certificates cannot be double-spent, validator results do not depend on message arrival order, a valid claim stays valid, and validators never get stuck. If correct, this would let payments, votes, data updates, and verifiable computations settle in parallel, avoiding the global transaction ordering that limits blockchain throughput.

What carries the argument

The load-bearing object is weak independence, written $c \parallel c'$: two claims are weakly independent iff whenever both are valid in a state, both orders of processing are valid and produce the same resulting state. The paper extends this from single claims to claim sequences and assumes (Assumption 1) that the whole claim set is partitioned by account, with claims from different accounts weakly independent. This commutation property is what lets the proofs shuffle claims across accounts (Proposition 4) and derive determinism, monotonicity, and liveness; the effect of claims is captured by a denotational semantics $\llbracket\_\rrbracket : \mathrm{Claim} \to [\mathrm{State} \rightharpoonup \mathrm{State}]$.

What would settle it

Construct two accounts A and B, a state s, and claims c from A and c' from B that are each valid in s but either make one processing order invalid or give $\llbracket c\,c'\rrbracket_s \neq \llbracket c'\,c\rrbracket_s$. A live FastSet deployment that accepts and settles both claims would then let validators diverge. A direct check is to feed the same certified claims to two validators in opposite orders and compare their final states: any difference falsifies the determinism claim.

Watch

Extended reading notes

Core claim

The paper's discovery is a generalization of payment-settlement commutativity to arbitrary state-effectful claims. Theorem 2 states that claim sequences that are interleaving equivalent—each account's own subsequence is the same in both—are weakly equivalent, so whenever two validators have processed the same claims they have the same state even if they saw different interleavings. Theorem 3 states that once a claim is valid for a validator, claims by other accounts cannot invalidate it; Theorem 4 states that progress is uniform, so no validator is stranded by an unfortunate order. Together these theorems establish strong eventual consistency without consensus or validator-to-validator communication.

Load-bearing premise

The proofs rest on Assumption 1: claims issued by different accounts must be weakly independent—if two such claims are each valid, either order of processing must be valid and produce the same state—and the paper explicitly notes that its proposed language setl does not enforce this property.

Editorial extensions

If this is right

  • Validators can settle claims from different accounts concurrently, with no inter-validator consensus or coordination, and still converge to the same global state.
  • A client that has a valid claim can settle it later without fear that other clients' claims will invalidate it, so re-submission and re-validation are unnecessary.
  • Nonce-based certification prevents double spending: at most one message per client per nonce can ever obtain validator quorum, even with Byzantine validators present.
  • Liveness is uniform across validators: if any validator can make progress, then every validator that has seen the same claims can too, provided messages are eventually delivered.
  • Commutative operations on shared state—such as token transfers, votes, and set additions—are the natural sweet spot; the paper proves a TOKEN contract obeys weak independence so transfers settle deterministically in any order.

Reading between the lines

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

  • Because setl deliberately does not enforce weak independence, the formal theorems apply to a deployment only if every contract is audited or verified to satisfy the commutation property; otherwise the Monotonicity Enforcement Resolution of Section 4.17 changes the protocol's stated semantics.
  • A practical test suggested by the paper's design: run two validators on the same certified claims in opposite arrival orders; if their final states ever differ, the deployment has violated Assumption 1 rather than disproved the theorem.
  • The auction example suggests a design rule for contract authors—express conditional behavior as commutative effects rather than guards that invalidate claims—which could be automated into a static checker for weak independence.
  • If validators process claims in parallel, throughput should scale with the number of independent accounts; benchmarking FastSet-style settlement against a total-order baseline on disjoint-account workloads would make that concrete.
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.

Referee Report

4 major / 4 minor

Summary. FastSet is a replica-based settlement protocol that removes the need for validators to agree on a total order of claims. Clients sign blocks of claims; validators validate them, approve them via quorum, and settle them asynchronously. The paper defines a notion of weak independence for claims and proves three abstract results under Assumption 1: determinism (Theorem 2), monotonicity (Theorem 3), and liveness (Theorem 4). It then proposes setl, an actor-inspired scripting language illustrated with many Web3 examples. The abstract theorems are mostly sound, but the paper claims that 'the protocol is proved to be correct' while the concrete language deliberately drops the key assumption: Section 4.17 states that setl does not enforce weak independence, and it adds a settlement rule not present in the formal model. The practical correctness claims therefore outrun the formal results.

Significance. The paper identifies a clean and potentially important generalization: under weak independence, arbitrary effectful claims can be settled in parallel without validator communication, extending FastPay's payment commutativity. The formalization is careful, and the abstract theorems are plausible; I found no circularity or parameter fitting. If the protocol-level liveness were fully proved and setl either enforced or provably encoded Assumption 1, this would be a significant contribution to parallel settlement. In its current form, however, the value is a design proposal with a sound but narrow theoretical core; the gap between the core and the proposed language is large enough that the headline claim cannot be accepted as stated. The paper's own modified-auction example is a concrete falsifiable failure of determinism under setl.

major comments (4)
  1. [§2.4, §3.4] Theorems 2-4 are statements about claim sequences, not about the operational protocol in Figure 1. The formal model has no validators, quorums, certificates, Byzantine faults, message-delivery guarantees, nonces, or pending/presettled sets. Theorem 4, for instance, asserts that from any compatible pair of valid sequences there exists a next claim c such that γc△γ′ and γc↓s; this does not imply the protocol-level liveness stated in Theorem 1(4) ('if one makes progress, then all do'). The proof sketch in Section 2.4 only addresses the security property and defers monotonicity and liveness; its Byzantine-liveness discussion is not a proof. Consequently, the statement in the abstract that 'the protocol is proved to be correct' is not supported by the formal material as written.
  2. [§3.3, §4.17, Appendix A.4] The paper's key hypothesis, Assumption 1, is not satisfied by setl. Section 4.17 states explicitly that 'setl does not enforce weak independence', and Appendix A.4 repeats that the weak-independence assumption is deliberately not enforced at the syntactic/language level. Because Theorems 2-4 are proved only under Assumption 1, the formal correctness results do not cover the proposed concrete language. A formal bridge—either a proof that setl programs respect Assumption 1, or a revised language that enforces it—is necessary before the correctness claims can be attributed to setl.
  3. [§4.17] The 'Monotonicity Enforcement Resolution' in Section 4.17 changes Step 7 of Figure 1: if a certified message has the right nonce and pending set but its claim block is undefined in the validator state, the validator increments the nonce, resets pending, and moves the message to settled without applying effects. No such operation exists in Definitions 3.1-3.2 or in Figure 1's Step 7. This is not a cosmetic extension: the modified AUCTION contract in the same section shows two validators processing the same certified bids in opposite orders and ending with different balances for the same account, with no convergence. The paper's informal induction there covers only the auction-specific property and does not restore the general determinism and monotonicity guarantees.
  4. [§4.14, Appendix A.4] The setl examples rely on atomic, deterministic claim blocks, but this assumption is only stated informally in Appendix A.4 and is explicitly acknowledged in Section 4.14 as 'a very strong assumption' left to future work. The formal model in Section 3 works with individual claims and sequences and does not define atomic block processing or the synchronization mechanism that Section 4.12 invokes when it says 'we assume that location updates are atomic'. Consequently, even for contracts that do satisfy weak independence, the semantics of setl is not fully specified at the level required to apply Theorems 2-4.
minor comments (4)
  1. [§4.9] The paragraph on concurrent instance creation contains a duplicated sentence: 'A voter attempting to create two concurrent (same nonce) instances would therefore risk to get their account stuck.' appears twice, with 'their' and 'its'.
  2. [§2.4, Theorem 1 proof] After stating Theorem 1, the proof says 'We only prove the security property here and the Byzantine aspect of monotonicity and liveness'; however, the paragraph that follows proves only the security property (unique certificate per nonce). The Byzantine aspects of monotonicity and liveness are not actually proved there; either provide the proof or remove the claim.
  3. [§4.15] The proof that AUCTION satisfies weak independence is left partly as 'an exercise to the curious reader', and the prose sketch does not handle all cases (e.g., ties, identical bidders, or the deadline guard). Since this is a central example for the practical claim, either provide a complete proof or clearly label the discussion as informal.
  4. [Abstract, §1] The abstract and introduction state that 'the protocol is proved to be correct' without the crucial qualification 'under Assumption 1'. Given Section 4.17, this overstates the results; a qualified statement would be more accurate.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: correctness theorems are conditional on an explicit weak-independence assumption; the setl gap is a scope limitation, not a self-referential derivation.

full rationale

The paper's derivation chain is: define claims and claim semantics (Definition 3.1), define weak independence as a pairwise commutativity condition (Definition 3.3), assume claims are partitioned into weakly independent address classes (Assumption 1), and then prove sequence-level determinism, monotonicity, and liveness (Theorems 2, 3, and 4). Weak independence is an input assumption, not a conclusion of the paper; the theorems are conditional on it. Theorem 2 is a genuine closure result: it derives that all interleaving-equivalent valid sequences have the same final state from the pairwise claim-level assumption via Propositions 3-5 and an induction, so it is not merely a restatement of Assumption 1. Theorems 3 and 4 are proved from Theorem 2 plus Assumption 1 and carry their own nontrivial induction arguments. No parameter is fitted and no externally predicted quantity is renamed as a result; the 2f+1 quorum is a standard Byzantine quorum choice, not a fitted parameter. The paper's own admissions that setl does not enforce weak independence (Section 4.17 and Appendix A.4) and that the proposed Monotonicity Enforcement Resolution adds a Step-7 behavior not present in the abstract Figure 1 are important scope limitations: the formal correctness result does not cover the practical language as specified, and violations of weak independence can lead validators to diverge on account balances, as the modified auction example shows. This is a correctness and completeness gap between the abstract protocol and its proposed implementation, not circular reasoning. The paper does not rely on any load-bearing self-citation: references to FastPay and CRDT literature are external results used as inspiration or context, not as the justification for the paper's own correctness claims. Therefore the analysis finds no significant circularity.

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

The protocol's correctness rests on explicit domain assumptions: weak independence, Byzantine bounds, unforgeable signatures, eventual delivery, and honest per-nonce client behavior. No numerical parameters are fitted and no new physical or ontological entities are introduced. The setl language adds an atomicity assumption not present in the core formalization.

assumptions (6)
  • domain assumption Assumption 1: claims are partitioned by address and claims by different addresses are weakly independent.
    Invoked in Section 3.3 (Assumption 1) and used throughout the proofs of Theorems 2, 3, and 4 in Section 3.4. This is the central condition that makes the protocol deterministic.
  • domain assumption At most f Byzantine validators among 3f+1, with quorum 2f+1.
    Section 2.3. Needed for the quorum intersection argument in Theorem 1 to prevent double spending and to guarantee that quorums always contain an honest validator.
  • domain assumption Signatures and aggregated signatures cannot be forged.
    Section 2.3 and Step 5 in Figure 1. Required for certificate authenticity and for the claim that only valid messages receive validator quorum.
  • domain assumption All messages are eventually delivered.
    Section 2.3 and Step 7. Used to justify liveness, specifically that validators eventually receive all certificates and can settle all claims.
  • domain assumption Honest clients issue a single determined sequence of claims per nonce.
    Section 3, paragraph after Theorem 4 lists this as one of two major assumptions. It is needed so that different validators see compatible per-account sequences.
  • ad hoc to paper Claim blocks in setl are processed atomically and deterministically.
    Appendix A.4: 'We assume that all blocks are deterministic' and 'a block is processed as an atomic action'. This assumption is not part of the core abstract protocol and is needed for the setl examples.

how reviews work

0 comments
Cite this review

Pith. "Pith review of FastSet: Parallel Claim Settlement." pith.science (2026). https://pith.science/paper/FUZWV6UK

@misc{pith2026250623395,
  author       = {Pith},
  title        = {Pith review of: FastSet: Parallel Claim Settlement},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/FUZWV6UK}},
  note         = {Machine review of arXiv:2506.23395}
}
read the original abstract

FastSet is a distributed protocol for decentralized finance and settlement, which is inspired from both actors and blockchains. Account holders cooperate by making claims, which can include payments, holding and transferring assets, accessing and updating shared data, medical records, digital identity, and mathematical theorems, among others. The claims are signed by their owners and are broadcast to a decentralized network of validators, which validate and settle them. Validators replicate the global state of the accounts and need not communicate with each other. In sharp contrast to blockchains, strong consistency is purposely given up as a requirement. Yet, many if not most of the blockchain benefits are preserved, while capitalizing on actor's massive parallelism. The protocol is proved to be correct, despite its massively parallel nature.

Figures

Figures reproduced from arXiv: 2506.23395 by the authors.

Figure 1
Figure 1. FastSet protocol. 11 [PITH_FULL_IMAGE:figures/full_fig_p011_1.png] view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

26 extracted references · 24 canonical work pages

  1. [1]

    Agha.Actors: A Model of Concurrent Computation in Distributed Systems

    Gul A. Agha.Actors: A Model of Concurrent Computation in Distributed Systems. MIT Press, Cambridge, MA, USA, 1986. 55

    work page 1986

  2. [2]

    Pod: An optimal- latency, censorship-free, and accountable generalized consensus layer

    Orestis Alpos, Bernardo David, and Dionysis Zindros. Pod: An optimal- latency, censorship-free, and accountable generalized consensus layer. CoRR, abs/2501.14931, 2025

    work page arXiv 2025

  3. [3]

    FastPay: High- performance byzantine fault tolerant settlement

    Mathieu Baudet, George Danezis, and Alberto Sonnino. FastPay: High- performance byzantine fault tolerant settlement. InAFT ’20: 2nd ACM Conference on Advances in Financial Technologies, New York, NY, USA, October 21-23, 2020, pages 163–177. ACM, 2020

    work page 2020

  4. [4]

    Partial algebras—survey of a unifying approach to- wards a two-valued model theory for partial algebras.Algebra Universalis, 15(1):306–358, 1982

    Peter Burmeister. Partial algebras—survey of a unifying approach to- wards a two-valued model theory for partial algebras.Algebra Universalis, 15(1):306–358, 1982

    work page 1982

  5. [5]

    Algebraic gossip: a network coding approach to optimal multiple rumor mongering.IEEE Transactions on Information Theory, 52(6):2486–2507, 2006

    Supratim Deb, Muriel Médard, and Clifford Choute. Algebraic gossip: a network coding approach to optimal multiple rumor mongering.IEEE Transactions on Information Theory, 52(6):2486–2507, 2006

    work page 2006

  6. [6]

    Fide laws of chess, 2023

    FIDE. Fide laws of chess, 2023. Accessed: 2025-06-02. Section E: Algebraic Notation outlines the standard for recording chess moves in international competitions

    work page 2023

  7. [7]

    Algorand: Scaling byzantine agreements for cryptocurrencies

    Yossi Gilad, Rotem Hemo, Silvio Micali, Georgios Vlachos, and Nickolai Zeldovich. Algorand: Scaling byzantine agreements for cryptocurrencies. In Proceedings of the 26th Symposium on Operating Systems Principles, Shanghai, China, October 28-31, 2017, pages 51–68. ACM, 2017

    work page 2017

  8. [8]

    The consensus number of a cryptocurrency (extended version), 2019

    Rachid Guerraoui, Petr Kuznetsov, Matteo Monti, Matej Pavlovic, and Dragos-Adrian Seredinschi. The consensus number of a cryptocurrency (extended version), 2019

    work page 2019

Show all 26 references
  1. [9]

    The consensus number of a cryptocurrency

    Rachid Guerraoui, Petr Kuznetsov, Matteo Monti, Matej Pavlovic, and Dragos-Adrian Seredinschi. The consensus number of a cryptocurrency. Distributed Computing, 35(1):1–15, 2022

    2022

  2. [10]

    Maurice Herlihy and Jeannette M. Wing. Linearizability: A correctness condition for concurrent objects.ACM Transactions on Programming Lan- guages and Systems, 12(3):463–492, 1990

    1990

  3. [11]

    A universal mod- ular ACTOR formalism for artificial intelligence

    Carl Hewitt, Peter Boehler Bishop, and Richard Steiger. A universal mod- ular ACTOR formalism for artificial intelligence. InProceedings of the 3rd International Joint Conference on Artificial Intelligence. Standford, CA, USA, August 20-23, 1973, pages 235–245. William Kaufmann, 1973

    1973

  4. [12]

    Time, clocks, and the ordering of events in a distributed system

    Leslie Lamport. Time, clocks, and the ordering of events in a distributed system. Communications of the ACM, 21(7):558–565, July 1978

    1978

  5. [13]

    The part-time parliament

    Leslie Lamport. The part-time parliament. Technical Report SRC Report 49, Digital Equipment Corporation Systems Research Center, Palo Alto, CA, September 1989. 56

    1989

  6. [14]

    The part-time parliament

    Leslie Lamport. The part-time parliament. ACM Transactions on Com- puter Systems, 16(2):133–169, May 1998

    1998

  7. [15]

    Trace theory

    Antoni Mazurkiewicz. Trace theory. In Wilfried Brauer, Wolfgang Reisig, and Grzegorz Rozenberg, editors, Advances in Petri Nets 1986, Part II: Proceedings of an Advanced Course, Bad Honnef, 8.–19. September 1986, volume 255 ofLecture Notes in Computer Science, pages 279–324. S...

    1986

  8. [16]

    Bitcoin: A peer-to-peer electronic cash system, Nov

    Satoshi Nakamoto. Bitcoin: A peer-to-peer electronic cash system, Nov

  9. [17]

    Ousterhout

    Diego Ongaro and John K. Ousterhout. In search of an understandable consensus algorithm. InProceedings of the 2014 USENIX Annual Techni- cal Conference, USENIX ATC 2014, Philadelphia, PA, USA, June 19-20, 2014, pages 305–320, Philadelphia, PA, June 2014. USENIX Association

    2014

  10. [18]

    Designing a commutative replicated data type for cooperative editing systems

    Nuno Preguiça, Marc Shapiro, and Jose Legatheaux Martins. Designing a commutative replicated data type for cooperative editing systems. Re- search Report TR-02-2008 DI-FCT-UNL, Universidade Nova de Lisboa, Dep. Informática, FCT, 2008

    2008

  11. [19]

    Groundhog: Linearly-scalable smart contracting via commutative transaction semantics

    Geoffrey Ramseyer and David Mazières. Groundhog: Linearly-scalable smart contracting via commutative transaction semantics. CoRR, abs/2404.03201, 2024

    2024 arXiv

  12. [20]

    Designing a commutative replicated data type

    Marc Shapiro and Nuno Preguiça. Designing a commutative replicated data type. Research Report RR-6320, Institut National de Recherche en Informatique et en Automatique (INRIA), October 2007

    2007

  13. [21]

    Preguiça, Carlos Baquero, and Marek Zawirski

    Marc Shapiro, Nuno M. Preguiça, Carlos Baquero, and Marek Zawirski. Conflict-free replicated data types. In Xavier Défago, Franck Petit, and Vincent Villain, editors,Stabilization, Safety, and Security of Distributed Systems - 13th International Symposium, SSS 2011, Grenoble, ...

    2011

  14. [22]

    Eventually consistent.Commun

    Werner Vogels. Eventually consistent.Commun. ACM, 52(1):40–44, 2009

    2009

  15. [23]

    Practical rateless set reconciliation

    Lei Yang, Yossi Gilad, and Mohammad Alizadeh. Practical rateless set reconciliation. In Proceedings of the ACM SIGCOMM 2024 Conference, ACM SIGCOMM 2024, Sydney, NSW, Australia, August 4-8, 2024, pages 595–612. ACM, 2024. 57 A Understanding SETL A setl state includes a finite ...

    2024

  16. [25]

    A user-driven accountis fully controlled by the account owner, defined as thepossessorofitsprivatekey, andisnotprescribedtoany setlscripts. A user-driven account can generate any claims, including but not limited to making native payments, creating accounts, creating contracts...

  17. [26]

    Alice Wonderland

    A contract-based accountis fully controlled by some fixed, prescribedsetl script that is persistently associated to the account at creation time. Once created, the script cannot be modified. A contract-based account can only submit claims that are generated by the prescribed s...

  18. [2008]

    Accessed: 2025-06-15

    2025

Pith tools

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