Pith. sign in

REVIEW 3 major objections 4 minor 27 references

Technical Report: Exploring Automatic Model-Checking of the Ethereum specification

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

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

Pith's one-line read 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.

desk verdict A useful, honest bounded model-checking case study of 3SF; the headline Alloy result depends on a completeness constraint the paper doesn't show. read the letter →

arxiv 2501.07958 v2 pith:MZWEJ3CX submitted 2025-01-14 cs.LO cs.DC

Igor Konnov , Jure Kukovec , Thomas Pani , Roberto Saltini , Thanh Hai Tran This is my paper · ORCID
classification cs.LOcs.DC MSC 68Q60
keywords Ethereum3-slotfinalityAccountableSafetymodelcheckingTLA+ApalacheAlloySMT
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 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.

What carries the argument

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.

What would settle it

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.

Watch

Extended reading notes

Core claim

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.

Load-bearing premise

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.

Editorial extensions

If this is right

  • 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.

Reading between the lines

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

  • 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.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

3 major / 4 minor

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.

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 (3)
  1. [8.1 / Table 5] 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.
  2. [6.2 / Figure 12] 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.
  3. [5.2, 8.1, 10.3] 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.
minor comments (4)
  1. [1 / Abstract] 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."
  2. [Abstract / Section 8.3] 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.
  3. [7.1] 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.
  4. [Appendix A] 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.

Circularity Check

0 steps flagged · score 1.0 of 10

No significant circularity: AccountableSafety is an externally defined property, no parameter is fitted to the verification outcome, and the load-bearing self-citations are tooling or protocol context rather than the argument for the property.

full rationale

The claimed derivation chain starts from the executable Python ffg.py and produces Spec1 through Spec4b, Spec3b, and Spec3c; the property checked is Accountable Safety, defined externally in Section 3 (Definition 1) as the implication from two conflicting finalized chains to a slashable set of at least n/3 validators, and encoded as an invariant in Figure 10. Nothing in the specifications is fitted to make that implication true: the SMT version (Section 7.2) negates the property and asks CVC5 for a model, the Alloy version runs `noAccountableSafety` as a satisfiability query (Section 8.2), and the mutation experiments (Section 1) show that deliberately broken specifications do yield counterexamples. The only self-citations are tooling ([13,14] Apalache), an optimization pattern ([15] Tendermint quorum sets), and the protocol/executable artifact under test ([9]/ffg.py); none is used as a uniqueness theorem or as the sole justification for the protocol property. The manuscript does flag genuine completeness risks: Section 5.2 admits the fold-flattening equivalence proof was not carried out, and Section 9.1 warns that omitting the completeness half of the justified-checkpoint characterization 'leads us to be unable to detect real violations of AccountableSafety.' The Alloy snippet in Section 8.1 shows only the consistency fact (`justifiedCheckpointsAreJustified`), so if the full Alloy model lacks the converse constraint, Table 5's no-violation results could be vacuous; the report's prose claims a fixpoint but does not display the Alloy converse. This is a soundness and model-completeness risk, not a demonstrated reduction of the conclusion to the input, so it does not raise the circularity score beyond 1.

Assumptions & free parameters 2 free parameters · 3 assumptions · 0 invented entities

The central claim rests on the fidelity of the Python specification, on the soundness of the manual abstractions, and on the chosen search scopes. None of these are established by formal proof in the report, so they are the main unpaid inputs.

free parameters (2)
  • Search scope bounds (blocks, checkpoints, signatures, FFG votes, votes) = e.g., 5 blocks, 7 checkpoints, 4 signatures, 6 FFG votes, 24 votes (largest exhaustive case)
    These bounds are hand-chosen; the verification results only apply within them. Table 5 shows the chosen scopes for Alloy experiments.
  • MAX_SLOT (fold depth bound) = not stated in the paper
    Used in Spec2 to bound recursion via folds. If too small, the fold returns incorrect results; the paper describes a post-hoc check but does not report the actual value used.
assumptions (3)
  • domain assumption The Python executable specification (ffg.py) faithfully formalizes the 3SF protocol.
    The report treats the Python spec as ground truth; no formal link to the 3SF paper is provided. Two report authors also authored the Python spec and the 3SF paper.
  • ad hoc to paper The abstractions (folds, integer graph encoding, two-chain restriction, configuration decomposition, Alloy/SMT encodings) preserve reachable states and the Accountable Safety property.
    Section 5.2 admits no TLAPS proof of functional equivalence; Section 8.1 provides no formal correspondence between Spec3 and Alloy; Section 10.3 assumes specific chain instances cover the relevant space.
  • domain assumption The chosen search scopes are large enough to contain all essentially different configurations for the claimed instance sizes.
    No argument is given that configurations within the scopes generalize to larger ones; indeed Table 5 reports timeouts for larger scopes.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Technical Report: Exploring Automatic Model-Checking of the Ethereum specification." pith.science (2026). https://pith.science/paper/MZWEJ3CX

@misc{pith2026250107958,
  author       = {Pith},
  title        = {Pith review of: Technical Report: Exploring Automatic Model-Checking of the Ethereum specification},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/MZWEJ3CX}},
  note         = {Machine review of arXiv:2501.07958}
}
read the original abstract

We investigate automated model-checking of the Ethereum specification, focusing on the Accountable Safety property of the 3SF consensus protocol. We select 3SF due to its relevance and the unique challenges it poses for formal verification. Our primary tools are TLA+ for specification and the Apalache model checker for verification. Our formalization builds on the executable Python specification of 3SF. To begin, we manually translate this specification into TLA+, revealing significant combinatorial complexity in the definition of Accountable Safety. To address these challenges, we introduce several layers of manual abstraction: (1) replacing recursion with folds, (2) substituting abstract graphs with integers, and (3) decomposing chain configurations. To cross-validate our results, we develop alternative encodings in SMT (CVC5) and Alloy. Despite the inherent complexity, our results demonstrate that exhaustive verification of Accountable Safety is feasible for small instances - supporting up to 7 checkpoints and 24 validator votes. Moreover, no violations of Accountable Safety are observed, even in slightly larger configurations. Beyond these findings, our study highlights the importance of manual abstraction and domain expertise in enhancing model-checking efficiency and showcases the flexibility of TLA+ for managing intricate specifications.

Figures

Figures reproduced from arXiv: 2501.07958 by the authors.

Figure 1
Figure 1. The relation between the specification artifacts [PITH_FULL_IMAGE:figures/full_fig_p007_1.png] view at source ↗
Figure 2
Figure 2. The callgraph of the 3SF specification Python code [PITH_FULL_IMAGE:figures/full_fig_p012_2.png] view at source ↗
Figure 3
Figure 3. pset filter definition Data structures and types. Type definitions come in the form of Python classes annotated with the @dataclass decorator, which automatically gener￾ates constructors, comparator methods, and other boilerplate code. Compos￾ite types are defined using the pyrsistent library, which provides immutable data structures such as sets and maps. Functions. The function definitions are pure functions that … view at source ↗
Figures from the paper (14 more)
Figure 4
Figure 4. Figure 4: Python definition of is ancestor descendant relationship Python and TLA+ operators. 5 Spec2 : Fold-Based Specification in TLA+ Spec2 addresses some of the limitations inherent in the straightforward trans￾lation of Spec1 from the Python executable specification. 5.1 Tr…
Figure 5
Figure 5. Figure 5: Definition of is ancestor descendant relationship in TLA+ TLA+ model checker TLC supports recursive operators, it does not scale to model-checking of this problem. To resolve this, we reformulate Spec1 into Spec2 , by substituting (mutu￾ally) recursive constructs with …
Figure 7
Figure 7. Figure 7: What does this give us? For instance, instead of re-evaluating the fold op￾18 [PITH_FULL_IMAGE:figures/full_fig_p018_7.png]
Figure 7
Figure 7. Figure 7: Memoizing the ancestor-descendant relationship [PITH_FULL_IMAGE:figures/full_fig_p019_7.png]
Figure 8
Figure 8. Figure 8: The definition of conflicting blocks, using memoization [PITH_FULL_IMAGE:figures/full_fig_p019_8.png]
Figure 9
Figure 9. Figure 9: A false invariant for producing an example [PITH_FULL_IMAGE:figures/full_fig_p020_9.png]
Figure 10
Figure 10. Figure 10: A state invariant for accountable safety [PITH_FULL_IMAGE:figures/full_fig_p020_10.png]
Figure 11
Figure 11. Figure 11: Small instances of chains and non-chains [PITH_FULL_IMAGE:figures/full_fig_p022_11.png]
Figure 13
Figure 13. Figure 13: The transition predicate of Spec3 24 [PITH_FULL_IMAGE:figures/full_fig_p024_13.png]
Figure 14
Figure 14. Figure 14: Chain and forking lemmas in IndInv 34 [PITH_FULL_IMAGE:figures/full_fig_p034_14.png]
Figure 15
Figure 15. Figure 15: Justified checkpoint lemmas in IndInv Init Step Invariant Depth Memory Time Init Next IndInv 0 0.6 GB 2sec IndInit Next IndInv 1 0.6 GB 2sec IndInit Next AccountableSafety 0 1.5 GB TO (> 6d) [PITH_FULL_IMAGE:figures/full_fig_p035_15.png]
Figure 16
Figure 16. Figure 16: Quorum sets By using quorum sets, we further replace cardinality comparisons like in Equation (2) with membership tests like in Equation (3): validatorsWhoCastJustifyingVote ∈ LargeQuorums (3) 36 [PITH_FULL_IMAGE:figures/full_fig_p036_16.png]
Figure 17
Figure 17. Figure 17: Initialization predicate for the configuration M5b [PITH_FULL_IMAGE:figures/full_fig_p037_17.png]
Figure 18
Figure 18. Figure 18: Rm and auxiliary operators B Detailed Proofs In the following, we show soundness of our translation rules for the recursive operators. B.1 Additional Definitions Let f be any TLA+ function. We use the shorthand Df := domain f . We use N0 to refer to the set of all nat…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

27 extracted references · 24 canonical work pages

  1. [1]

    https://apalache-mc.org, 2024

    The Apalache model checker. https://apalache-mc.org, 2024. Ac- cessed: 2024-10-25

    work page 2024

  2. [2]

    https: //github.com/tlaplus/Examples, 2024

    A collection of TLA + specifications of varying complexities. https: //github.com/tlaplus/Examples, 2024. Accessed: 2024-10-25

    work page 2024

  3. [3]

    Barrett, Andrew Reynolds, and Cesare Tinelli

    Kshitij Bansal, Clark W. Barrett, Andrew Reynolds, and Cesare Tinelli. Reasoning with finite sets and cardinality constraints in SMT. Log. Methods Comput. Sci. , 14(4), 2018

    work page 2018

  4. [4]

    Haniel Barbosa, Clark W. Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mo- hamed, Aina Niemetz, Andres N¨ otzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, and Yoni Zohar. CVC5: A versatile and industrial-strength SMT solver. In Dana Fisman and Grigore Rosu, editors, TACAS, ...

    work page 2022

  5. [5]

    CaDiCaL, Gimsatul, IsaSAT and Kissat en- tering the SAT Competition 2024

    Armin Biere, Tobias Faller, Katalin Fazekas, Mathias Fleury, Nils Fro- leyks, and Florian Pollitt. CaDiCaL, Gimsatul, IsaSAT and Kissat en- tering the SAT Competition 2024. In Marijn Heule, Markus Iser, Matti J¨ arvisalo, and Martin Suda, editors,SAT Competition, volume B-2024- 1, pages 8–10, 2024

    work page 2024

  6. [6]

    The latest gossip on BFT consensus

    Ethan Buchman, Jae Kwon, and Zarko Milosevic. The latest gossip on BFT consensus. CoRR, abs/1807.04938, 2018

    arXiv 2018

  7. [7]

    Combining ghost and casper

    Vitalik Buterin, Diego Hernandez, Thor Kamphefner, Khiem Pham, Zhi Qiao, Danny Ryan, Juhyeok Sin, Ying Wang, and Yan X Zhang. Combining ghost and casper. arXiv preprint arXiv:2003.03052 , 2020

    arXiv 2003

  8. [8]

    A theorem on trees

    Arthur Cayley. A theorem on trees. Quart. J. Math. , 23:376–378, 1878

    work page

Show all 27 references
  1. [9]

    3-slot-finality protocol for ethereum

    Francesco D’Amato, Roberto Saltini, Thanh-Hai Tran, and Luca Zanolini. 3-slot-finality protocol for ethereum. arXiv preprint arXiv:2411.00558, 2024

    2024 arXiv

  2. [10]

    Leonardo Mendon¸ ca de Moura and Nikolaj S. Bjørner. Z3: an efficient SMT solver. In C. R. Ramakrishnan and Jakob Rehof, editors, TACAS, volume 4963 of LNCS, pages 337–340. Springer, 2008. 41

    2008

  3. [11]

    Software Abstractions: logic, language, and analysis

    Daniel Jackson. Software Abstractions: logic, language, and analysis . MIT press, 2012

    2012

  4. [12]

    alloytools.org

    Daniel Jackson. alloytools.org. https://https://alloytools.org/,

  5. [13]

    TLA+ model check- ing made symbolic

    Igor Konnov, Jure Kukovec, and Thanh-Hai Tran. TLA+ model check- ing made symbolic. Proc. ACM Program. Lang. , 3(OOPSLA):123:1– 123:30, 2019

    2019

  6. [14]

    Specification and verification with the TLA + trifecta: Tlc, apalache, and TLAPS

    Igor Konnov, Markus Kuppe, and Stephan Merz. Specification and verification with the TLA + trifecta: Tlc, apalache, and TLAPS. In Tiziana Margaria and Bernhard Steffen, editors, ISoLA, volume 13701 of LNCS, pages 88–105. Springer, 2022

    2022

  7. [15]

    TLA + specification of Tendermint consensus and its accountability

    Igor Konnov and Zarko Milosevic. TLA + specification of Tendermint consensus and its accountability. https://github.com/cometbft/ cometbft/blob/main/spec/light-client/accountability/ TendermintAcc_004_draft.tla, 2024. Accessed: 2024-10-23

    2024

  8. [16]

    Paxos made simple

    Leslie Lamport. Paxos made simple. ACM SIGACT News (Distributed Computing Column) 32, 4 (Whole Number 121, December 2001) , pages 51–58, 2001

    2001

  9. [17]

    TLA + specification of Paxos

    Leslie Lamport. TLA + specification of Paxos. https: //github.com/tlaplus/Examples/blob/master/specifications/ Paxos/Paxos.tla, 2024. Accessed: 2024-12-17

    2024

  10. [18]

    Ebb-and-flow proto- cols: A resolution of the availability-finality dilemma

    Joachim Neu, Ertem Nusret Tas, and David Tse. Ebb-and-flow proto- cols: A resolution of the availability-finality dilemma. In 2021 IEEE Symposium on Security and Privacy (SP) , pages 446–465. IEEE, 2021

    2021

  11. [19]

    Consensus: bridging theory and practice

    Diego Ongaro. Consensus: bridging theory and practice . PhD thesis, Stanford University, USA, 2014

    2014

  12. [20]

    The sleepy model of consensus

    Rafael Pass and Elaine Shi. The sleepy model of consensus. In Advances in Cryptology–ASIACRYPT 2017: 23rd International Conference on the Theory and Applications of Cryptology and Information Security, Hong Kong, China, December 3-7, 2017, Proceedings, Part II 23 , pages 380–

    2017

  13. [23]

    Formulate translations from Python to TLA+ in the intuitive way, potentially introducing constructs like recursion, and then

  14. [24]

    iterative

    Pair them with a TLA+-to-TLA+ rule, ending in a supported frag- ment. We have to do that, as the ssf code extensively uses recursive definitions. A.2.1 Bounded recursion rule Assume we are given a recursive operator R. Without loss of generality, we can take the arity to be 1,...

  15. [25]

    If x ∈ DRm (f ′), by the induction hypothesis, we know that R m(f ′)[x ] = R(x )

  16. [26]

    Here, G m(f , Rm(f ′)) trivially evaluates to e as well

    If x /∈ DRm (f ′), but P (x ) holds, we know R(x ) = e. Here, G m(f , Rm(f ′)) trivially evaluates to e as well

  17. [27]

    As x ∈ Df , f [x ] ⊆ Df ′ by definition and Df ′ ⊆ DRm (f ′) by Lemma B.1, so for every element v ∈ V (x ) it is the case that R(v ) = Rm(f ′)[v ]

    Otherwise, it remains to be shown that the following holds true: G(x , F (f [x ], Rm(f ′))) = R(x ) Since we know P (x ) does not hold for this x , it follows that: R(x ) = G(x , F (V (x ), Op)) Hence, it suffices to see that: 59 F (f [x ], Rm(f ′)) = F (V (x ), Op) By the pro...

  18. [409]

    42 The work done in this section is the main contribution of Milestone 3

    Springer, 2017. 42 The work done in this section is the main contribution of Milestone 3. Since this section is quite long and technical, we have decided to add it in the appendix. A Translating Python Specifications to TLA + In this section, we present our results on translat...

    2017

  19. [2024]

    Accessed: 2024-10-11

    2024

Pith tools

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