{"id":"86151d5a-5449-43a5-b7dc-8859dd04ca04","arxiv_id":"2506.23395","paper_version":3,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":5.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"A protocol that settles arbitrary weakly independent claims in parallel, proving that every validator converges to the same state without any validator-to-validator communication.","lead":"FastSet is a new decentralized settlement protocol where independent claims, such as payments, data updates, and verified computations, are processed in parallel by validators that never need to talk to each other. It aims to break the total-order bottleneck of blockchains while keeping a formal correctness proof.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Correctness proofs are conditional on Assumption 1, which setl explicitly does not enforce; without a formal bridge from setl to the abstract model, the practical protocol is unproven.","rationale":"The reader's conditional verdict is appropriate. I did not find an error in the Section 3 proofs themselves: Theorem 2's induction and Proposition 3 appear sound, Theorem 3's double induction respects well-foundedness, and Theorem 4's choice of the first missing claim is justified by the comparability condition. The security/liveness sketch in Section 2 also has the standard quorum-intersection argument. The load-bearing gap is external to that formal core: the paper presents setl as the concrete claim language, and repeatedly and deliberately allows contracts that violate Assumption 1. Since all correctness theorems are stated for claim sequences satisfying that assumption, they have no force for those contracts. The Monotonicity Enforcement Resolution makes this explicit by adding an unmodeled transition that settles undefined claim blocks; this is a modification of the protocol's step 7, not a conservative extension of the partial semantics. So the central claim, as a statement about FastSet/setl, is not established. I still would not reject the paper: the abstract theorems are valuable and the assumption is clearly stated; the missing piece is a formal bridge from setl (or a restriction of it) to Assumption 1, plus implementation evidence. That is exactly a CONDITIONAL situation, so the reader's verdict should remain unchanged.","tokens_in":42713,"tokens_out":12106,"duration_ms":147912,"concrete_test":"Implement a small executable semantics for the setl features used in the Section 4.17 AUCTION variant (contract fields, instance bid with conditional transfer to instance.owner, Step-7 processing, and the Monotonicity Enforcement Resolution). Feed the same two certified bid messages to two validators in opposite orders, let both quiesce, and compare Bob's balance and the instance balances. The paper's own discussion predicts divergence; if the run confirms divergent final states, setl does not implement the assumptions of Theorem 2 and the practical protocol is unproven.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central formal claim is conditional: Theorems 2–4 (Section 3.4) are proved under Assumption 1 (Section 3.3) that claims are partitioned by address and claims of different addresses are weakly independent (Definition 3.3). The paper's own practical language deliberately drops this condition. Section 4.17 states 'setl does not enforce weak independence', and Appendix A.4 says the same. Moreover, the proposed Monotonicity Enforcement Resolution adds a Step-7 behavior: 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 and settles the message without applying effects. No operation of this kind exists in Definition 3.1–3.2 or in the abstract Step 7 of Figure 1, so the theorems do not cover the language as specified. The gap is not merely stylistic: in the modified AUCTION of Section 4.17 (paying the previous highest bidder's owner instead of the instance), the same certified bids settle with different balance effects depending on order and the validators never converge. Thus the headline statement that FastSet is 'proved to be correct' is only true for an abstract protocol whose main hypothesis is not realized by the proposed implementation.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":42950,"tokens_out":7074,"duration_ms":74800,"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":[{"comment":"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.","section":"§2.4, §3.4"},{"comment":"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.","section":"§3.3, §4.17, Appendix A.4"},{"comment":"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.","section":"§4.17"},{"comment":"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.","section":"§4.14, Appendix A.4"}],"minor_comments":[{"comment":"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'.","section":"§4.9"},{"comment":"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.","section":"§2.4, Theorem 1 proof"},{"comment":"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.","section":"§4.15"},{"comment":"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.","section":"Abstract, §1"}],"recommendation":"major_revision","confidential_remarks":"For the editor: the paper sits between a theoretical protocol paper and a design document for a real system. The formal core is sound, but the claims in the abstract and Section 1 exceed what is proved. If the journal is willing to accept a conditional contribution with a clearly narrowed scope, major revision may suffice; if the journal expects the correctness claim to cover the proposed language, the manuscript is not ready. The setl part is informal and would need a specification document or a companion formalization."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"FastSet is a real extension of FastPay, not just a relabeling. The core idea is sound: if claims from different clients are weakly independent, then validators that process the same claims in different orders converge to the same state, and progress is monotone. The formalization in Section 3 is precise, the theorems are stated cleanly, and the proofs are mostly convincing. The generalization from payments to arbitrary state-effectful claims under a commutation condition is genuinely new, even though the underlying commutativity idea appears in FastPay, CRDTs, and trace theory. That is not a criticism; the paper builds on those ideas and takes them further.\n\nThe paper also does something unusual and good: it clearly admits the limits of its own formal result. Section 4.17 and Appendix A.4 say explicitly that setl does not enforce weak independence, and the proposed Monotonicity Enforcement Resolution changes Step 7 to settle messages with undefined effects. That behavior is not part of the abstract protocol, so Theorems 2-4 simply do not cover setl as described. The modified auction example in 4.17 shows a concrete divergence scenario. This is not a minor gap. The abstract claim that the protocol is 'proved to be correct' is only true for the abstract model under Assumption 1, not for the language the paper presents as the practical implementation. The authors are upfront about this, but the consequence remains: the headline result is conditional on a hypothesis the paper's own language deliberately violates.\n\nTwo smaller soft spots. The Byzantine liveness part of Theorem 1 is a sketch rather than a full proof; the later theorems are about interleaving equivalence, not about the Byzantine quorum dynamics in detail. And there is no implementation or benchmark, so the million-TPS-style performance claims are unvalidated. These are limitations, not fatal flaws.\n\nWho should read this? Distributed-systems researchers working on parallel settlement, DeFi protocols, and languages for commutative updates. It deserves serious peer review, and the reviewers should push on the setl-to-protocol bridge. The core protocol is worth publishing; the setl claims need either a formal bridge or a much more modest framing.","headline":"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.","tokens_in":661,"tokens_out":1524,"would_cite":true,"duration_ms":33343,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68M14","68Q85","68Q60"],"pacs":[],"model":"deepseek-v4-flash","headline":"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.","keywords":["FastSet","weak independence","parallel claim settlement","strong eventual consistency","distributed consensus","actor model","verifiable computing","blockchain"],"falsifier":"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.","tokens_in":42502,"feed_emoji":"⚡","tokens_out":5780,"duration_ms":61325,"temperature":0.7,"pith_summary":"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.","feed_headline":"No total order needed: parallel settlement proven correct","feed_subtitle":"Validators converge on the same state even when claims arrive in different orders.","key_machinery":"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}]$.","core_discovery":"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.","pith_inferences":["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."],"forward_implications":["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."],"supporting_citations":[{"why":"Supplies the payment-commutativity observation and the settlement protocol that FastSet generalizes.","marker":"[3]"},{"why":"Argues that total order is not required to prevent double spending, motivating the decision to drop consensus.","marker":"[9]"},{"why":"Defines commutativity-based strong eventual consistency and CRDTs, which weak independence generalizes.","marker":"[21]"},{"why":"Provides the trace-theoretic notion of event independence that weak independence adapts.","marker":"[15]"},{"why":"Supplies the actor model of massive concurrency that FastSet's account-and-claim structure follows.","marker":"[11]"}],"fun_headline_variants":["Settle claims in parallel, no ordering or consensus needed","Parallel claim settlement without global ordering or consensus","No total order, no consensus: parallel settlement proven correct","Validators converge without talking: parallel claim settlement proven","Actor-style parallelism for settlement, no consensus, proven correct"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Settle claims in parallel, no ordering or consensus needed","Parallel claim settlement without global ordering or consensus","No total order, no consensus: parallel settlement proven correct","Validators converge without talking: parallel claim settlement proven","Actor-style parallelism for settlement, no consensus, proven correct"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000538,"raw_usage":{"total_tokens":2499,"prompt_tokens":779,"completion_tokens":1720,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":395,"completion_tokens_details":{"reasoning_tokens":1643}},"tokens_in":395,"tokens_out":1720,"duration_ms":12532,"temperature":1.0,"reasoning_tokens":1643,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-06T21:44:01.889026+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[{"cited_title":"FastPay: High- performance byzantine fault tolerant settlement","cited_arxiv_id":null,"evidence_quote":"Supplies the payment-commutativity observation and the settlement protocol that FastSet generalizes."},{"cited_title":"The consensus number of a cryptocurrency","cited_arxiv_id":null,"evidence_quote":"Argues that total order is not required to prevent double spending, motivating the decision to drop consensus."},{"cited_title":"Preguiça, Carlos Baquero, and Marek Zawirski","cited_arxiv_id":null,"evidence_quote":"Defines commutativity-based strong eventual consistency and CRDTs, which weak independence generalizes."},{"cited_title":"Trace theory","cited_arxiv_id":null,"evidence_quote":"Provides the trace-theoretic notion of event independence that weak independence adapts."},{"cited_title":"A universal mod- ular ACTOR formalism for artificial intelligence","cited_arxiv_id":null,"evidence_quote":"Supplies the actor model of massive concurrency that FastSet's account-and-claim structure follows."}],"review_version":1}