Pith. sign in

REVIEW 4 major objections 5 minor 28 references

Combating Reentrancy Bugs on Sharded Blockchains

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

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

Pith's one-line read Sharded blockchains' asynchronous messaging makes reentrancy bugs more likely, and a caller-scoped lock with trap-safe cleanup plus TLA+ model checking can stop them.

desk verdict Useful locking pattern and PlusCal strategy for sharded-blockchain reentrancy, but the prevalence stat lacks methodology and the trap-cleanup guarantee is asserted, not tested. read the letter →

arxiv 2506.05932 v1 pith:L373HOYI submitted 2025-06-06 cs.CR

Roman Kashitsyn , Robin Künzler , Ognjen Marić , Lara Schmid This is my paper
classification cs.CR
keywords reentrancyshardedblockchainasynchronousmessagingInternetComputerlockingpatternCallerGuardTLA+PlusCal
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

The paper argues that the asynchronous messaging model used by sharded blockchains makes reentrancy bugs more likely than Ethereum's synchronous transactional model, and that the usual Ethereum countermeasures fail to translate cleanly. It backs this with security reviews showing that 10 of 15 critical pre-production Internet Computer contracts had medium-or-high-severity reentrancy bugs. It then offers a concrete fix: a caller-scoped Rust locking pattern, CallerGuard, whose lock is released automatically even when a message handler traps, plus an analogous Motoko try/finally pattern. Finally, it shows that TLA+ model checking of a PlusCal model can find such bugs in real contracts and verify the absence of the known ones. A sympathetic reader should care because the result is a validated, low-cost pattern and verification strategy for preventing double-spend bugs in sharded-blockchain DeFi.

What carries the argument

The load-bearing mechanism has two parts. First, CallerGuard, a Rust struct that inserts the caller's principal, an ICP user identifier, into a pending-requests set on construction and removes it in Drop; ICP's runtime and Rust libraries are relied on to run that cleanup even when a message handler traps, so the lock cannot be left stuck. Second, a modeling strategy that translates async/await into PlusCal processes and labels, with queues for ordered requests and sets for unordered responses, so that the TLC model checker can explore all interleavings within small bounds; the ckBTC minter contract is the real-world case study.

What would settle it

Deploy a test canister on ICP whose message handler acquires a CallerGuard and then forces a trap, send a second request from the same principal, and check whether it is accepted; if the second request is permanently rejected, the runtime cleanup premise fails and the pattern does not hold.

Watch

Extended reading notes

Core claim

The central discovery is that reentrancy in sharded blockchains is not just Ethereum's problem restated: because cross-contract calls split into multiple message handlers with no reliable ordering, a check-then-act method like notify_minter can be interleaved with itself so that two executions both pass the 'unprocessed UTXOs' check and double-mint. The paper claims that 66% (10/15) of reviewed critical ICP contracts contained such bugs, and that a per-caller guard released by Rust's Drop on trap, combined with TLA+ and TLC verification, eliminates the class in practice. It further claims that eight of nine previously vulnerable Rust contract suites adopted the locking pattern in production with no known bugs.

Load-bearing premise

The locking pattern presupposes that the ICP runtime reliably runs cleanup code that drops local variables on every trap, a guarantee the paper asserts but does not demonstrate with a specification, test, or citation.

Editorial extensions

If this is right

  • Eight of the nine previously vulnerable Rust contract suites have adopted the locking pattern in production, and the reviewed contracts using it have no known reentrancy bugs.
  • The CallerGuard pattern can be adapted to contract-wide locks, locks on subsets of state, or limits on concurrent callers per principal, preserving more of the asynchronous model's parallelism.
  • Existing Ethereum patterns, checks-effects-interactions and simple mutexes, do not translate directly because trap rollbacks can leave a mutex stuck and contract-wide locking negates the performance benefits of interleaving.
  • TLA+ with TLC, run over small finite bounds, found reentrancy bugs in early versions of the ckBTC contracts and detects property violations whenever the protective locking is removed from the model.
  • The TLA+ modeling strategy applies to NEAR and MultiversX as well, where explicit callbacks map to the same two-handler pattern, though PlusCal sugar would be less relevant there.

Reading between the lines

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

  • Beyond the paper, the same modeling idiom could be applied to NEAR and MultiversX contracts directly, since their explicit callbacks already expose the same request-response decomposition that PlusCal labels model explicitly.
  • The trap-safe cleanup guarantee could be hardened by a runtime-level test suite that traps in every code path after acquiring a CallerGuard, since the paper asserts but does not formally specify this runtime behavior.
  • The per-principal locking granularity suggests a throughput trade-off the paper does not quantify: a single user issuing many serialized operations loses interleaving benefits, so DeFi applications with power users may need finer-grained locks or batching.
  • The property that total ckBTC supply never exceeds deposited Bitcoin is a natural invariant family that could be checked on other wrapped-asset chains as a cross-chain reentrancy benchmark.
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 / 5 minor

Summary. The paper studies reentrancy vulnerabilities in sharded blockchains that use asynchronous messaging, taking the Internet Computer (ICP), NEAR, and MultiversX as case studies. It argues that the asynchronous, interleaved message-handler model creates new opportunities for reentrancy bugs that do not arise in Ethereum's synchronous model, and it supports this with a simplified ckBTC minter example. The paper evaluates existing Ethereum countermeasures (checks-effects-interactions and mutex locking), identifies why they fail in the asynchronous setting, and proposes a Rust RAII-style CallerGuard pattern with Drop-on-trap cleanup for ICP, plus an analogous Motoko try/finally approach. It then presents a PlusCal/TLA+ model of the ckBTC minter and reports TLC model-checking results for safety and liveness properties under small bounds. The paper also reports that 66% (10/15) of reviewed critical ICP contracts contained medium or high severity reentrancy bugs, and that eight contract suites have adopted the proposed locking solution.

Significance. If the paper's claims hold, it provides two practically valuable contributions: a concrete locking pattern that is applicable to real ICP smart contracts, and a demonstration that TLA+/PlusCal can model and verify the absence of reentrancy bugs in the asynchronous messaging model. The paper is written clearly, and the interleaving examples are easy to follow. Its strengths include a public formal-models repository, a measured instruction overhead of 2.92% for the locking pattern, and a concrete case study (ckBTC minter) with a stated invariant and a reported previously unknown bug found by the model checker. However, the central prevalence statistic and the Drop-on-trap cleanup guarantee are not backed by the level of evidence the paper's recommendations require; these are the main load-bearing points that need strengthening before the results can be fully credited.

major comments (4)
  1. [Section I (Abstract and Introduction)] The headline statistic that 66% (10/15) of reviewed critical ICP contracts contained medium or high severity reentrancy bugs is not accompanied by any methodology. This figure is load-bearing for the thesis that the asynchronous model makes reentrancy bugs more likely, but the paper does not state how the 15 contracts were selected, what review procedure was used (manual audit, tool-assisted, or both), what severity rubric was applied, or whether the reviews were independent and reproducible. Please provide a detailed methodology, a complete list of reviewed contracts, and ideally a comparator (e.g., a similar review of Ethereum contracts) so the reader can assess representativeness and severity calibration.
  2. [Section IV, Figure 4 (Drop-on-trap cleanup)] The paper's central remedy for the lock-stuck-on-trap problem is asserted rather than demonstrated. The text states that 'ICP's system API and Rust libraries features that can call cleanup code on traps in order to make sure that any local variables are still dropped,' but no specification, test, or citation is provided. Since the paper itself notes in Section IV issue 1 that the analogous lock on NEAR and MultiversX would stick on a trap, the entire ICP-specific advantage of the CallerGuard pattern depends on this cleanup guarantee holding for every trap class (panic!, unwrap, stack overflow, out-of-memory, failed system API call, and traps raised while processing a response to a downstream call). If any trap path skips cleanup, a contract employing the pattern can become permanently locked. Please provide evidence from the ICP runtime/library implementation or a test suite covering the relevant trap classes, or explicitly state the assumption and its verification status.
  3. [Section V-A-c and Figure 5 (TLA+ model scope)] The PlusCal model releases locks manually on every path and does not model a trap or panic after a lock has been acquired. Lines 20-21 and 30-31 of Figure 5 show explicit lock removal, and the text says 'We manually release locks in all cases.' Consequently, the TLA+ verification does not cover the Drop-on-trap cleanup mechanism that is the key novel guarantee of the proposed pattern; it verifies the locking discipline only under the assumption that cleanup always runs. Please either add a nondeterministic trap transition (with and without cleanup) to the model, or state explicitly that the verified properties are conditional on the runtime cleanup guarantee and are therefore not a substitute for evidence of that guarantee.
  4. [Section VI (TLC bounds and generality)] The model-checking results are obtained under very small bounds: 2 parallel invocations of the minter notification call, 2 BTC withdrawal calls, 2 users, and a BTC supply of 3 Satoshi. The paper cites relevant precedents that most bugs reproduce with small bounds, which is a reasonable argument, but the statement that 'we are yet to manually find a reentrancy bug that was missed in the TLC analysis due to the bounds being too small' is anecdotal and does not quantify the coverage gap. Please either provide a more rigorous argument that the verified properties are independent of the bounds (e.g., via parameterized invariants or symmetry reduction), or temper the conclusion that small bounds are sufficient for this class of bugs.
minor comments (5)
  1. [Section II-A] Typo: 'leding' should be 'leading' in the last paragraph.
  2. [Section III (ckBTC example)] Typo: 'Bitcion' should be 'Bitcoin' in the first paragraph.
  3. [Figure 4] The signature 'Result<()), String>' contains mismatched parentheses; it should be 'Result<(), String>'.
  4. [Section V-B] The liveness property discussion would benefit from stating the exact fairness assumptions used in the TLC model, since the paper notes that the property requires users to call notify_minter sufficiently often.
  5. [References] The phrase 'a slurry of research papers' is informal for a journal venue; consider replacing with 'a substantial body of research.'

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the paper's claims rest on execution-model arguments, an empirical review statistic, and a machine-checked TLA+ model, none of which reduce to their own inputs.

full rationale

The paper's central claims are (i) that asynchronous sharded-blockchain messaging creates new reentrancy interleavings, (ii) that a per-caller RAII-style lock (CallerGuard) can prevent them on ICP, and (iii) that TLA+/PlusCal model checking can verify such protections. None of these is derived by definition from its inputs. The 66% (10/15) prevalence figure is reported as an empirical result of internal security reviews of ICP contracts; it is an input observation, not a fitted parameter or a prediction forced by construction. The CallerGuard pattern is proposed as a design, and its effectiveness is argued from the execution-model properties in Section II and from the PlusCal model in Section V. The TLA+ model checks an independently stated invariant (ckBTC supply cannot exceed controlled UTXOs) and can detect violations when protective mechanisms are removed; this is genuine model-based verification rather than a reformulation of the desired conclusion. The only noteworthy gaps are evidential, not circular: the claim that ICP's runtime runs Rust cleanup code on all traps is asserted without a specification or test (Section IV), and the PlusCal model manually releases locks on every path instead of modeling trap-driven cleanup. These are soundness and completeness concerns about the recommended pattern and the model's fidelity, but they are not cases where a prediction reduces to a fitted input or where a conclusion is imported from a self-citation. Self-references to DFINITY documentation and the authors' formal-models repository are non-load-bearing or are reproducible artifacts (the TLA+ model is checked with TLC and publicly available), so they do not raise the circularity score.

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

The paper's central claims rest on platform-specific execution semantics (message interleaving, trap rollback, guaranteed responses), a load-bearing but unverified cleanup-on-trap behavior for the Rust Drop pattern, manual model fidelity, and small model-checking bounds. No free parameters are fitted to data; the TLC bounds are chosen by hand and limit completeness. No invented entities are introduced.

free parameters (1)
  • TLC model-checking bounds = 2 parallel notify_minter invocations, 2 BTC withdrawal calls, 2 users, BTC supply 3 Satoshi
    TLC requires explicit finite bounds; the absence-verification result only holds within these bounds, and the paper relies on empirical heuristics (Lu et al., Yuan et al.) to argue small bounds suffice. These bounds are chosen by hand and limit the completeness of the verification.
assumptions (6)
  • domain assumption ICP executes at most one message handler per smart contract at a time, and message order is not reliable.
    Section II-A lists these as properties (1) and (2) of the ICP messaging model; the reentrancy examples depend on arbitrary interleaving of handlers.
  • domain assumption If a message handler traps or panics, its state changes are reverted.
    Section II-A property (3); used in Section IV to explain why naive locks can remain set after a trap.
  • domain assumption Every request eventually receives a response, possibly a system-generated error.
    Section II-A property (4); the TLA+ model assumes callbacks always arrive, which is needed for liveness properties.
  • domain assumption ICP Rust libraries guarantee that local variables are dropped, running cleanup code, even when a message handler traps.
    Section IV, Figure 4 discussion; this is load-bearing for CallerGuard but is asserted without specification or test.
  • ad hoc to paper The hand-written PlusCal model faithfully represents the ckBTC minter contract.
    Section V presents a manual translation of async/await into PlusCal labels; no automated extraction or conformance checking is provided.
  • domain assumption Small TLC bounds suffice to detect real reentrancy bugs in practice.
    Section VI justifies bounds of 2 concurrent calls, 2 users, and 3 Satoshi using empirical studies of concurrency bugs; this extrapolates from finite-state checking to the unbounded system.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Combating Reentrancy Bugs on Sharded Blockchains." pith.science (2026). https://pith.science/paper/L373HOYI

@misc{pith2026250605932,
  author       = {Pith},
  title        = {Pith review of: Combating Reentrancy Bugs on Sharded Blockchains},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/L373HOYI}},
  note         = {Machine review of arXiv:2506.05932}
}
read the original abstract

Reentrancy is a well-known source of smart contract bugs on Ethereum, leading e.g. to double-spending vulnerabilities in DeFi applications. But less is known about this problem in other blockchains, which can have significantly different execution models. Sharded blockchains in particular generally use an asynchronous messaging model that differs substantially from the synchronous and transactional model of Ethereum. We study the features of this model and its effect on reentrancy bugs on three examples: the Internet Computer (ICP) blockchain, NEAR Protocol, and MultiversX. We argue that this model, while useful for improving performance, also makes it easier to introduce reentrancy bugs. For example, reviews of the pre-production versions of some of the most critical ICP smart contracts found that 66% (10/15) of the reviewed contracts -- written by expert authors -- contained reentrancy bugs of medium or high severity, with potential damages in tens of millions of dollars. We evaluate existing Ethereum programming techniques (in particular the effects-checks-interactions pattern, and locking) to prevent reentrancy bugs in the context of this new messaging model and identify some issues with them. We then present novel Rust and Motoko patterns that can be leveraged on ICP to solve these issues. Finally, we demonstrate that the formal verification tool TLA+ can be used to find and eliminate such bugs in real world smart contracts on sharded blockchains.

Figures

Figures reproduced from arXiv: 2506.05932 by the authors.

Figure 1
Figure 1. Async/await for callback handling reentrancy bugs in those models and develop robust pro￾gramming techniques to counteract such bugs. Furthermore, we need practical ways of ensuring that these programming techniques are applied correctly and actually prevent the bugs. This paper makes the following contributions to the study of reentrancy: 1) We describe how reentrancy bugs manifest themselves in the novel, asynchro… view at source ↗
Figure 2
Figure 2. A simplified version of the real-world minter notification method [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 3
Figure 3. Basic mutex-based locking pattern back into notify_minter [2]. We will next see what the existing approaches to counteracting such bugs on Ethereum are, and why these approaches cannot be directly translated to the asynchronous models from section II. IV. PROGRAMMING TECHNIQUES FOR COMBATING REENTRANCY ATTACKS Reentrancy bugs can be avoided by using safe coding patterns. Demeyer et al. [3] identify two main such pat… view at source ↗
Figures from the paper (2 more)
Figure 4
Figure 4. Figure 4: Improved locking pattern code is not visible in the above example, because it is part of ICP’s smart contract Rust library that automatically registers the cleanup. While one can use finer-grained locks and release them in callbacks in both NEAR and MultiversX as well,…
Figure 5
Figure 5. Figure 5: PlusCal/TLA model of notify_minter method. message handlers in the same order as the actual smart contract method does. We desugar the async/await syntax by explicitly removing a response from the incoming buffer at the start of each message handler (except the first),…

Discussion (0). Sign in to comment.

Reference graph

Works this paper leans on

28 extracted references · 26 canonical work pages

  1. [1]

    A survey of attacks on ethereum smart contracts sok,

    N. Atzei, M. Bartoletti, and T. Cimoli, “A survey of attacks on ethereum smart contracts sok,” in Proceedings of the 6th International Conference on Principles of Security and Trust - Volume 10204. Berlin, Heidelberg: Springer-Verlag, 2017, p. 164–186. [Online]. Available: https://doi.org/10.1007/978-3-662-54455-6 8

    work page doi:10.1007/978-3-662-54455-6 2017

  2. [2]

    Smart contract security field guide - reentrancy,

    D. Muhs, “Smart contract security field guide - reentrancy,” (accessed April 15 2024) https://scsfg.io/hackers/reentrancy/, 2023

    work page 2024

  3. [3]

    Refactoring solidity smart contracts to protect against reentrancy exploits,

    S. Demeyer, H. Rocha, and D. Verheijke, “Refactoring solidity smart contracts to protect against reentrancy exploits,” in Leveraging Ap- plications of Formal Methods, Verification and Validation. Software Engineering, T. Margaria and B. Steffen, Eds. Cham: Springer Nature Switzerland, 2022, pp. 324–344

    work page 2022

  4. [4]

    Reguard: Finding reentrancy bugs in smart contracts,

    C. Liu, H. Liu, Z. Cao, Z. Chen, B. Chen, and B. Roscoe, “Reguard: Finding reentrancy bugs in smart contracts,” in Proceedings of the 40th International Conference on Software Engineering: Companion Proceeedings, ser. ICSE ’18. New York, NY , USA: Association for Computing Machinery, 2018, p. 65–68. [Online]. Available: https://doi.org/10.1145/3183440.3183495

    work page arXiv 2018

  5. [5]

    Online detection of effectively callback free objects with applications to smart contracts,

    S. Grossman, I. Abraham, G. Golan-Gueta, Y . Michalevsky, N. Rinetzky, M. Sagiv, and Y . Zohar, “Online detection of effectively callback free objects with applications to smart contracts,” Proc. ACM Program. Lang. , vol. 2, no. POPL, dec 2017. [Online]. Available: https://doi.org/10.1145/3158136

    doi:10.1145/3158136 2017

  6. [6]

    A survey on security verification of blockchain smart contracts,

    J. Liu and Z. Liu, “A survey on security verification of blockchain smart contracts,” IEEE Access, vol. 7, pp. 77 894–77 904, 2019

    work page 2019

  7. [7]

    Formal verification of smart contracts: Short paper,

    K. Bhargavan, A. Delignat-Lavaud, C. Fournet, A. Gollamudi, G. Gonthier, N. Kobeissi, N. Kulatova, A. Rastogi, T. Sibut-Pinote, N. Swamy, and S. Zanella-B ´eguelin, “Formal verification of smart contracts: Short paper,” in Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security , ser. PLAS ’16. New York, NY , USA: Associati...

    arXiv 2016

  8. [8]

    The internet computer for geeks,

    DFINITY , “The internet computer for geeks,” (accessed April 15 2024) https://eprint.iacr.org/2022/087, 2022

    work page 2024

Show all 28 references
  1. [9]

    The near white paper,

    NEAR, “The near white paper,” (accessed April 15 2024) https://pages. near.org/papers/the-official-near-white-paper/, 2021

    2024

  2. [10]

    MultiversX - A Highly Scalable Public Blockchain via Adaptive State Sharding and Secure Proof of Stake,

    T. M. Team, “MultiversX - A Highly Scalable Public Blockchain via Adaptive State Sharding and Secure Proof of Stake,” Tech. Rep., 2019. [Online]. Available: https://files.multiversx.com/multiversx-whitepaper. pdf

    2019

  3. [11]

    POLKADOT: VISION FOR A HETEROGENEOUS MULTI-CHAIN FRAMEWORK,

    G. Wood, “POLKADOT: VISION FOR A HETEROGENEOUS MULTI-CHAIN FRAMEWORK,” Tech. Rep

  4. [12]

    Cerberus: Minimalistic Multi-shard Byzantine-resilient Transaction Processing,

    J. Hellings, D. P. Hughes, J. Primero, and M. Sadoghi, “Cerberus: Minimalistic Multi-shard Byzantine-resilient Transaction Processing,” Aug. 2020, arXiv:2008.04450 [cs]. [Online]. Available: http://arxiv.org/ abs/2008.04450

    2020 arXiv

  5. [13]

    Motoko programming language,

    DFINITY , “Motoko programming language,” (accessed April 15 2024) https://internetcomputer.org/docs/current/motoko/main/motoko

    2024

  6. [14]

    Chain-key bitcoin (ckbtc),

    ——, “Chain-key bitcoin (ckbtc),” (accessed April 15 2024) https://inte rnetcomputer.org/docs/current/developer-docs/integrations/bitcoin/ckb tc

    2024

  7. [15]

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

    S. Nakamoto, “Bitcoin: A peer-to-peer electronic cash system,” Decen- tralized business review, 2008

    2008

  8. [16]

    Design and analysis of a distributed ecdsa signing service,

    J. Groth and V . Shoup, “Design and analysis of a distributed ecdsa signing service,” Cryptology ePrint Archive, Paper 2022/506, 2022, https://eprint.iacr.org/2022/506. [Online]. Available: https: //eprint.iacr.org/2022/506

    2022

  9. [17]

    Analysis of the bitcoin utxo set,

    S. Delgado-Segura, C. P ´erez-Sola, G. Navarro-Arribas, and J. Herrera- Joancomart´ı, “Analysis of the bitcoin utxo set,” in Financial Cryptog- raphy and Data Security: FC 2018 International Workshops, BITCOIN, VOTING, and WTSC, Nieuwpoort, Curac ¸ao, March 2, 2018, Revised Se...

    2018

  10. [18]

    Declarative control flow,

    A. Alexandrescu, “Declarative control flow,” (accessed April 15 2024) https://github.com/CppCon/CppCon2015/blob/18943d6288b1cba54922 627b71b7d21d7f1175f1/Presentations/Declarative%20Control%20Flow/ Declarative%20Control%20Flow%20-%20Andrei%20Alexandrescu% 20-%20CppCon%202015.pdf, 2015

    2024

  11. [19]

    Motoko try / finally construct,

    DFINITY , “Motoko try / finally construct,” (accessed Jan 9 2025) https: //internetcomputer.org/docs/current/motoko/main/reference/language-m anual/#try

    2025

  12. [20]

    Lamport, Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers

    L. Lamport, Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers . Addison-Wesley, June 2002. [Online]. Available: https://www.microsoft.com/en-us/research/publica tion/specifying-systems-the-tla-language-and-tools-for-hardware-and-s oftware-engineers/

    2002

  13. [21]

    Model checking tla+ specifica- tions,

    Y . Yu, P. Manolios, and L. Lamport, “Model checking tla+ specifica- tions,” in Correct Hardware Design and Verification Methods, L. Pierre and T. Kropf, Eds. Berlin, Heidelberg: Springer Berlin Heidelberg, 1999, pp. 54–66

    1999

  14. [22]

    Tla+ model checking made symbolic,

    I. Konnov, J. Kukovec, and T.-H. Tran, “Tla+ model checking made symbolic,” Proceedings of the ACM on Programming Languages, vol. 3, no. OOPSLA, pp. 1–30, 2019

    2019

  15. [23]

    Tla+ proofs,

    D. Cousineau, D. Doligez, L. Lamport, S. Merz, D. Ricketts, and H. Vanzetto, “Tla+ proofs,” in FM 2012: Formal Methods: 18th Inter- national Symposium, Paris, France, August 27-31, 2012. Proceedings

    2012

  16. [24]

    Springer, 2012, pp. 147–154

    2012

  17. [25]

    The pluscal algorithm language,

    L. Lamport, “The pluscal algorithm language,” in International Collo- quium on Theoretical Aspects of Computing. Springer, 2009, pp. 36–60

    2009

  18. [26]

    ckbtc tla+ model,

    O. Mari ´c, “ckbtc tla+ model,” (accessed April 17 2025) https://github.c om/dfinity/formal-models/tree/55f806d396a999a7a244545028f8d2187 4457f56/tla/ckbtc

    2025

  19. [27]

    Learning from mistakes: a comprehensive study on real world concurrency bug characteristics,

    S. Lu, S. Park, E. Seo, and Y . Zhou, “Learning from mistakes: a comprehensive study on real world concurrency bug characteristics,” in Proceedings of the 13th international conference on Architectural support for programming languages and operating systems , ser. ASPLOS XIII....

    2008

  20. [28]

    Simple Testing Can Prevent Most Critical Failures: An Analysis of Production Failures in Distributed Dataintensive Systems,

    D. Yuan, Y . Luo, X. Zhuang, G. R. Rodrigues, X. Zhao, Y . Zhang, P. U. Jain, and M. Stumm, “Simple Testing Can Prevent Most Critical Failures: An Analysis of Production Failures in Distributed Dataintensive Systems,” in Proceedings of the 11th Symposium on Operating Systems D...

    2014

Pith tools

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