{"id":"97a8aea4-114f-4d92-a499-79f7e5b8c1e3","arxiv_id":"2501.07958","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":2,"one_line_summary":"Bounded model checking of the 3SF consensus protocol's Accountable Safety property found no counterexamples in small configurations, using new TLA+, SMT, and Alloy encodings.","lead":"Engineers from the formal verification community translated the Python specification of Ethereum's 3SF consensus protocol into TLA+, SMT, and Alloy models, then model-checked the Accountable Safety property. For small configurations, up to 7 checkpoints and 24 validator votes, exhaustive checks found no violations, though larger instances timed out.","discovery_kind":"new_application","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Alloy justified-checkpoint fact may be incomplete, making Table 5's exhaustive no-violation result vacuous.","rationale":"The reader's weakest assumption is that the abstract models are sound and complete with respect to the Python specification, with no equivalence proof. My stress-test identifies a concrete, potentially fatal instance of that gap: the Alloy specification that produces the headline results appears to constrain the justified-checkpoint set only by consistency, not completeness. The paper's own Section 9.1 explains that omitting completeness lets the solver choose a minimal justified set, which would make AccountableSafety trivially hold. This is directly load-bearing because the largest exhaustive instances in Table 5 come from the Alloy toolchain, not from the SMT or TLA+ encodings. The concern is empirically testable by inspecting the .als file and rerunning the relevant check with and without a completeness fact. If the concern lands, the Key Outcomes claim must be retracted or drastically weakened; if the completeness fact is already present, the claim survives this particular challenge. The reader's verdict of CONDITIONAL already captures the need for such evidence, so the verdict does not need to change, but the condition should be made explicit: demonstrate that the Alloy model's justified/finalized sets are complete, or soften the claim to 'no violations were found in the under-constrained bounded model'.","tokens_in":29057,"tokens_out":6917,"duration_ms":65276,"concrete_test":"Inspect `spec3c/ffg.als` in the public repository: does it contain a completeness fact such as `all c: Checkpoint | isJustified[c] implies c in JustifiedCheckpoints.justified`? If absent, add it and rerun the Table 5 row 8 command (`run noAccountableSafety for 10 but 5 Block, 7 Checkpoint, 4 Signature, 6 FfgVote, 24 Vote`) with Kissat. If a counterexample appears, the reported no-violation result was vacuous. If the fact is already present, rerun the check without it to confirm it is load-bearing.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The paper's strongest experimental claim (Key Outcomes: 'up to 7 checkpoints and 24 validator votes') comes from the Alloy specification Spec3c (Table 5, row 8). In Section 8.1, the only displayed fact about JustifiedCheckpoints is `justifiedCheckpointsAreJustified`, which states `all c: JustifiedCheckpoints.justified | ...` — i.e., every checkpoint in the set satisfies the justification condition. Nothing in the snippet requires the converse: that every checkpoint satisfying the justification condition belongs to the set. Without such a completeness constraint, an Alloy instance can choose `JustifiedCheckpoints.justified` to be empty or to omit justified checkpoints, making `noAccountableSafety` (the negated property checked in Section 8.2) unsatisfiable for the trivial reason that no finalizing checkpoints exist. The report itself flags this exact pitfall for Spec4 in Section 9.1: omitting completeness 'leads us to be unable to detect real violations of AccountableSafety'. Since the Alloy results are the headline evidence, the central claim stands only if the Alloy model actually includes a completeness fact (which the report does not show) or if the spec otherwise rules out such under-constrained models.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper reports a model-checking study of the Accountable Safety property of the 3SF finality gadget as specified in the Ethereum Python specification. It develops a chain of artifacts: Spec1 (a direct TLA+ translation), Spec2 (a fold-based version), Spec3 (a state-machine abstraction), Spec4/Spec4b (a two-chain restriction with an inductive invariant and configuration decomposition), Spec3b (an SMT/CVC5 encoding), and Spec3c (an Alloy/Kissat encoding). The headline claim is exhaustive verification of Accountable Safety for configurations up to 7 checkpoints and 24 validator votes (Table 5, row 8), with no counterexamples found in larger timed-out runs, and quick counterexamples on deliberately mutated models.","tokens_in":29235,"tokens_out":5812,"duration_ms":61307,"significance":"If the verification claim is sound, the paper is a useful case study of how manual abstraction layers and cross-tool validation can make an intricate consensus property amenable to bounded exhaustive checking. Strengths include the public artifacts, the cross-validation across three solver families, the mutation experiments that act as sensitivity checks, and the detailed translation rules with supporting proofs in Appendix B. However, the scientific value depends on the soundness of the Alloy encoding and on the abstraction correspondence between the executable Python specification and the checked models, and both of these are not yet established.","major_comments":[{"comment":"The displayed Alloy fact `justifiedCheckpointsAreJustified` is only a consistency constraint: it says every member of `JustifiedCheckpoints.justified` satisfies the justification condition. It does not assert the converse, that every checkpoint satisfying that condition belongs to the set. Without such a completeness constraint, `noAccountableSafety` can be unsatisfiable for the trivial reason that `JustifiedCheckpoints.justified` is chosen too small, so no conflicting finalized checkpoints exist. The paper itself identifies this pitfall for Spec4 in Section 9.1. Because Table 5 and the Key Outcomes rely on the Alloy runs, the main claim is vacuous unless the actual Alloy file contains a completeness fact and the experiments are re-run with it. Please include the full fact and confirm that the reported runs used it.","section":"8.1 / Table 5"},{"comment":"In Figure 12, the second conjunct of `CastVotes` is written as `all c in (allCheckpoints intersection allJustifiedCheckpoints): not IsJustified(c, votes0, allJustifiedCheckpoints)`. Since `allJustifiedCheckpoints` is declared to be a subset of `allCheckpoints`, this intersection is exactly `allJustifiedCheckpoints`, so the action requires every justified checkpoint both to satisfy `IsJustified` (first conjunct) and not to satisfy it. The transition relation is therefore inconsistent as written, which undermines the Spec3 results in Table 3. If this is a typographical error for set difference, it should be corrected and the experiments re-checked against the corrected formula.","section":"6.2 / Figure 12"},{"comment":"The central claim concerns the executable Python specification, but no soundness or completeness argument is supplied for the abstraction chain. Section 5.2 says an equivalence proof for the fold optimization could be produced with TLAPS but is not. Section 8.1 says the Alloy specification was written \"relatively easily\" from Spec3 without a correspondence proof. Section 10.3 replaces a general family of chain configurations by five hand-picked instances (M3, M4a, M4b, M5a, M5b), while Section 3.1 itself notes that the number of labelled rooted forests on n vertices is (n+1)^(n-1). The paper should either prove that each abstraction preserves or over-approximates the reachable states with respect to Accountable Safety, or explicitly restate the verified theorem as applying only to the abstract models, not to the Python specification.","section":"5.2, 8.1, 10.3"}],"minor_comments":[{"comment":"The phrase \"absolute confidence\" overstates what bounded exhaustive checking and timed-out runs can establish; recommend rewording to \"no counterexample found within the checked scopes.\"","section":"1 / Abstract"},{"comment":"The statement that \"no violations of Accountable Safety are observed, even in slightly larger configurations\" should be qualified: Table 5 rows with timeouts did not terminate, so absence of counterexamples is not a verification result.","section":"Abstract / Section 8.3"},{"comment":"The SMT snippet defines `justified checkpoints` by a set comprehension that refers to itself through `(set.member (source vote) justified checkpoints)`. Since this is a fixed-point definition, its semantics should be stated explicitly and the CVC5 treatment of self-referential set comprehensions should be documented; otherwise the SMT results are not reproducible.","section":"7.1"},{"comment":"Many translation rules are annotated with \"see Source\" or \"Source\" without including the source text in the report; for a standalone technical report, the relevant Python definitions or stable links should be included so the claimed equivalences can be checked.","section":"Appendix A"}],"recommendation":"major_revision","confidential_remarks":"This is a technical-report-style verification study. The load-bearing issue is the Alloy completeness constraint: if the authors can confirm that the artifact contains a completeness fact for `JustifiedCheckpoints.justified` and that the reported runs used it, the main claim may survive. I would also ask the editor to decide whether the journal expects a full abstraction-soundness proof or is willing to accept a bounded model-checking case study with explicitly scoped claims; at minimum the paper must stop claiming verification of the Python specification without that proof."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"What you should know: this technical report is a bounded model-checking study of Accountable Safety for Ethereum's 3SF protocol, with a genuinely useful tower of abstractions (Python to TLA+, folds, state machine, SMT, Alloy) and public artifacts. The strongest claim is exhaustive verification up to 7 checkpoints and 24 validator votes. That claim rests on the Alloy model, and the paper's displayed justification fact only states consistency (every checkpoint in the set is justified), not completeness (every justified checkpoint is in the set). Without completeness, the Alloy no-violation result is vacuous. The authors know this pitfall—they flag it explicitly in Section 9.1 for Spec4—so they likely included the completeness constraint in the actual Alloy code, but the paper never shows it. That is a load-bearing omission because the headline numbers come from Alloy.\n\nWhat is genuinely new and good: the abstraction sequence is concrete, reproducible, and cross-validated across three toolchains, with mutation testing as a sensitivity check. The paper is refreshingly honest about timeouts, the combinatorial explosion, and the limits of automated translation. The translation rules in Appendix A and the formal equivalence proofs for the recursion-to-fold rules are a real contribution for anyone doing similar work.\n\nSoft spots, in proportion: the absence of abstraction-correctness proofs is real but clearly acknowledged—Section 5.2 notes a TLAPS equivalence proof is still to be done, and Section 10.3 uses hand-picked chain configurations rather than covering all labelled rooted forests. The paper is therefore a bounded case study, not a safety proof; the phrase \"absolute confidence\" in Key Outcomes overstates what bounded model checking gives. The biggest concrete issue is the Alloy completeness fact not being shown or precisely cited in the repo. That is fixable but essential.\n\nWho this is for: formal verification practitioners working on consensus protocols, and the Ethereum 3SF team. It deserves a serious referee, but one who will insist on either displaying the Alloy completeness constraint or softening the claims accordingly. I'd send it to a formal methods workshop or conference, not desk reject it.","headline":"A useful, honest bounded model-checking case study of 3SF; the headline Alloy result depends on a completeness constraint the paper doesn't show.","tokens_in":29827,"tokens_out":2349,"would_cite":false,"duration_ms":24468,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q60"],"pacs":[],"model":"deepseek-v4-flash","headline":"Exhaustive model checking of the Ethereum 3SF protocol confirms Accountable Safety on all tested configurations up to 7 checkpoints and 24 validator votes, with no violations in larger scopes.","keywords":["Ethereum","3-slot finality","Accountable Safety","model checking","TLA+","Apalache","Alloy","SMT"],"falsifier":"Run the Alloy encoding (Spec3c) with the same instance parameters (e.g., 6 blocks, 6 checkpoints, 4 signatures, 6 FFG votes, 15 votes) and ask Kissat to satisfy the predicate noAccountableSafety; a satisfying assignment would be a concrete state with two conflicting finalized checkpoints and fewer than n/3 slashable validators. A complementary test is to generate random or guided block graphs and votes directly from the Python specification ffg.py and look for such a state; finding one would falsify the report's conclusion even if the abstract models miss it.","tokens_in":28779,"feed_emoji":"⛓️","tokens_out":7124,"duration_ms":63165,"temperature":0.7,"pith_summary":"This paper asks whether Ethereum's 3-slot-finality (3SF) consensus gadget satisfies Accountable Safety: whenever two conflicting chains are finalized, at least a third of the validators must be slashable. The authors translate the executable Python specification of 3SF into TLA+ and then apply three layers of manual abstraction—replacing recursion with fold operations, encoding block graphs as integers, and decomposing chain configurations—until the property becomes checkable by Apalache, CVC5 (SMT), and Alloy with the Kissat SAT solver. They report exhaustive verification of Accountable Safety for all tested configurations up to 7 checkpoints and 24 validator votes, and no counterexamples in larger runs that timed out. The result matters because 3SF is a proposed speed-up for Ethereum finality, and Accountable Safety is its hardest-to-verify guarantee; the paper also shows how human-guided abstraction, not automated translation, is what makes the check feasible.","feed_headline":"Model checkers verify Ethereum 3SF safety up to 7 checkpoints","feed_subtitle":"Three independent encodings - TLA+, SMT, Alloy - find no violation of the double-finality slashing rule.","key_machinery":"The argument runs on a chain of abstractions that converts the Python spec's recursive, graph-heavy definitions into a bounded satisfiability problem. Recursive computations are rewritten as bounded fold operations (ApaFoldSeqLeft) so Apalache can handle them; the block graph is abstracted to integer-labelled chains, with a fork represented by a sign change; and the infinite space of chain configurations is decomposed into a handful of hand-chosen instances (M3, M4a, M4b, M5a, M5b). Cardinality constraints for supermajority and slashing thresholds are replaced either by the specialized theory of finite set cardinalities (CVC5) or by explicit quorum sets (TLA+). The decisive artifact is an Alloy specification that searches with a SAT solver for a model of 'noAccountableSafety'; within the bounded scopes that formula is unsatisfiable.","core_discovery":"On the paper's own terms, the central discovery is that the modeled 3SF protocol satisfies Accountable Safety in every configuration that could be exhaustively searched, and no configuration violating it was found in any larger search. The largest exhaustive instances cover up to 7 checkpoints and 24 validator votes (Alloy/Kissat), with TLA+/Apalache handling smaller configurations and CVC5 up to 5 blocks and 6 checkpoints. The claim is bounded by the search scopes and by the unproven correspondence between the abstract models and the executable Python specification: the paper states that an equivalence proof 'could' be produced with TLAPS but has not been written, and that the Alloy encoding was derived from Spec3 without a formal correspondence proof.","pith_inferences":["If the abstraction correspondence were proven (e.g., a simulation between the Python spec and Spec3c), the bounded check would upgrade to an unconditional statement about the executable spec for those sizes; the report leaves this connection open.","The decomposition into a few chain configurations suggests a cheap screening heuristic: for small block counts, fork-shaped two-chain graphs with justified non-genesis checkpoints are the configurations most likely to violate Accountable Safety, so future checks can target the search there.","Because the number of block graphs grows super-exponentially, exhaustive SAT-based checking will not scale past a handful of blocks; combining bounded checks with inductive invariants or theorem proving is the natural path to unbounded verification.","The three encodings form a ready-made benchmark set for evaluating new model checkers on cardinality-heavy, inductively defined consensus properties, since the same property can be checked in TLA+/SMT/SAT with known difficulty levels."],"forward_implications":["If the bounds hold, 3SF is accountably safe for every configuration with up to 7 checkpoints and 24 votes, giving strong evidence for the protocol's core safety guarantee before larger-scope verification is attempted.","The specifications double as example generators: both Apalache and Alloy quickly produce configurations with justified and finalized checkpoints, which the authors note are hard to reach by random inputs to the Python spec.","The Alloy/SAT encoding is the fastest of the three, suggesting that Boolean encodings with fine scope control may be the pragmatic route for verifying similar inductive properties of consensus protocols.","The paper's sequence of specifications (Spec1 to Spec4b) provides a worked template: one can start from an executable Python spec, translate directly, then iteratively abstract until a model checker finishes.","The same artifact suite could be used to verify other 3SF properties, such as reorg resilience and honest-node non-slashing, which the authors expect to be easier than Accountable Safety."],"supporting_citations":[{"why":"Defines the 3SF protocol and its Accountable Safety property; the subject of all verification work.","marker":"[9]"},{"why":"The TLA+ model checker Apalache is the primary verification tool for the TLA+ specifications.","marker":"[1]"},{"why":"Introduces Alloy, the specification language whose SAT-based encoding produced the largest verified scope.","marker":"[11, 12]"},{"why":"The Kissat SAT solver, used as the back-end for the Alloy specification's unsatisfiability checks.","marker":"[5]"},{"why":"The CVC5 SMT solver used for the Spec3b encoding that verified Accountable Safety up to 5 blocks and 6 checkpoints.","marker":"[4]"},{"why":"Provides the finite-set cardinalities theory that makes the SMT encoding of quorum and slashing constraints decidable.","marker":"[3]"},{"why":"Describes the symbolic encoding behind Apalache, the basis for all TLA+ model-checking experiments.","marker":"[13]"},{"why":"An earlier TLA+ accountability specification for Tendermint, used as a template for modeling accountability and quorum sets.","marker":"[15]"}],"fun_headline_variants":["3SF passes exhaustive model checks up to 7 checkpoints","Three tools verify 3SF safety up to 7 checkpoints","No safety violations in Ethereum 3SF in exhaustive checks","Exhaustive model check: 3SF safe at 7 checkpoints, 24 votes"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that the abstract TLA+, SMT, and Alloy models faithfully represent the executable Python specification, in the strong sense that every protocol state—and in particular every Accountable Safety violation—of the Python code has a corresponding instance in one of the checked models within the given search bounds.","fun_headline_variants_meta":{"raw":{"variants":["3SF passes exhaustive model checks up to 7 checkpoints","Three tools verify 3SF safety up to 7 checkpoints","No safety violations in Ethereum 3SF in exhaustive checks","Exhaustive model check: 3SF safe at 7 checkpoints, 24 votes"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001004,"raw_usage":{"total_tokens":4239,"prompt_tokens":928,"completion_tokens":3311,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":544,"completion_tokens_details":{"reasoning_tokens":3233}},"tokens_in":544,"tokens_out":3311,"duration_ms":20889,"temperature":1.0,"reasoning_tokens":3233,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-10T20:30:22.177671+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run the Alloy encoding (Spec3c) with the same instance parameters (e.g., 6 blocks, 6 checkpoints, 4 signatures, 6 FFG votes, 15 votes) and ask Kissat to satisfy the predicate noAccountableSafety; a satisfying assignment would be a concrete state with two conflicting finalized checkpoints and fewer than n/3 slashable validators. A complementary test is to generate random or guided block graphs and votes directly from the Python specification ffg.py and look for such a state; finding one would falsify the report's conclusion even if the abstract models miss it.","supporting_citations":[{"cited_title":"https://apalache-mc.org, 2024","cited_arxiv_id":null,"evidence_quote":"The TLA+ model checker Apalache is the primary verification tool for the TLA+ specifications."},{"cited_title":"CaDiCaL, Gimsatul, IsaSAT and Kissat en- tering the SAT Competition 2024","cited_arxiv_id":null,"evidence_quote":"The Kissat SAT solver, used as the back-end for the Alloy specification's unsatisfiability checks."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"The CVC5 SMT solver used for the Spec3b encoding that verified Accountable Safety up to 5 blocks and 6 checkpoints."},{"cited_title":"Barrett, Andrew Reynolds, and Cesare Tinelli","cited_arxiv_id":null,"evidence_quote":"Provides the finite-set cardinalities theory that makes the SMT encoding of quorum and slashing constraints decidable."},{"cited_title":"TLA+ model check- ing made symbolic","cited_arxiv_id":null,"evidence_quote":"Describes the symbolic encoding behind Apalache, the basis for all TLA+ model-checking experiments."},{"cited_title":"TLA + specification of Tendermint consensus and its accountability","cited_arxiv_id":null,"evidence_quote":"An earlier TLA+ accountability specification for Tendermint, used as a template for modeling accountability and quorum sets."}],"review_version":1}