Pith. sign in

REVIEW 4 major objections 4 minor 46 references

Set-Based Models for Cryptocurrency Software

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

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

Pith's one-line read The paper argues that set-based formal specifications can accurately and concisely describe cryptocurrency software, and that the same specification yields prototypes, simulations, test cases, and automated proofs.

desk verdict A well-written advocacy paper for gradual set-based formal methods in crypto, but the central claim is broader than the small fragments actually shown. read the letter →

arxiv 1908.00591 v1 pith:3KHEX7FV submitted 2019-08-01 cs.SE

Gustavo Betarte , Maximiliano Cristiá , Carlos Luna , Adrián Silveira , Dante Zanarini This is my paper · ORCID
classification cs.SE
keywords formalmethodsset-basedspecificationcryptocurrencysoftwaresmartcontractsEthereumVirtualMachineconsensusprotocolmodel-basedtestingautomatedtheoremproving
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 argues that cryptocurrency software can be brought under formal methods gradually, starting not with full code verification but with set-based specifications: models written in plain set theory and first-order logic. It claims such specifications are accurate and concise enough to describe key components such as a consensus protocol and the Ethereum Virtual Machine, and that once a specification exists, the same artifact yields an executable prototype for simulation, a source of model-based test cases, and automated proofs of specification properties. The payoff would be a realistic adoption path for an industry that currently treats smart-contract code as closer to loose web code than to safety-critical software. A sympathetic reader is asked to accept that proving functional correctness on abstract models, with cryptography and security set aside, is the right first step toward better cryptocurrency software.

What carries the argument

The load-bearing object is the set-based specification itself: states and data are built from finite sets, partial functions, sequences, and records, and every operation is written as a logical predicate relating an input state, an output state, and any parameters. Because this is just set theory plus first-order logic, the same text can be read as mathematics, executed as a prototype, or queried as a theorem. The execution side is provided by a Prolog-based constraint solver that treats sets as first-class values and can both simulate a transition by chaining state predicates and prove a property by showing its negation is unsatisfiable. The test-generation side is provided by the Test Template Framework, which partitions each set-theoretic operator into cases, for the relational override $\oplus$ yielding eight standard test conditions, and then combines them with the surrounding predicate. These pieces make the specification the single source of prototypes, tests, and proofs.

What would settle it

Extend the set-based EVM model to include the omitted transaction-validity predicate, the missing create case, and all remaining opcodes, then rerun the invariant proofs and compare the resulting model's length with the implementation. If the model grows to implementation scale, or if the automated proofs can no longer discharge invariants such as the account mapping remaining a partial function, the claim that set-based specifications accurately and concisely describe cryptocurrency software is refuted. A complementary check is to take a documented smart-contract exploit caused by an EVM detail the paper abstracts away and confirm that prototypes and generated tests from the model do not reveal it.

Watch

Extended reading notes

Core claim

The central discovery is a workflow: write the critical behavior of cryptocurrency components as set-theoretic predicates, with states as records of finite sets and partial functions and transitions as logical formulas, rather than as code. The paper demonstrates this workflow on a consensus protocol from the literature and on the Ethereum Virtual Machine transaction-processing model from the Yellow Paper, including a simplified create instruction. It then shows three downstream products falling out of the same model: a runnable prototype by encoding the predicates in a set constraint solver, test conditions by applying standard partitions to the postcondition $s'.acc = s.acc \oplus \{(t?.sender, a')\}$, and automated proofs by checking whether the negation of a desired invariant is satisfiable. The claim is that these artifacts are obtained easily, and that this makes formal methods affordable before any attempt at full code verification.

Load-bearing premise

The argument assumes the behavior that matters for cryptocurrency correctness can be captured while deliberately ignoring cryptography, security properties, and parts of the EVM, so that functional properties proved on this incomplete model still justify calling the software accurately described.

Editorial extensions

If this is right

  • A cryptocurrency team can begin formal assurance without hiring full verification specialists, because writing the set-based specification is the first and main investment.
  • A single specification can be checked in three independent ways, simulation, generated tests, and invariant proofs, so errors in the specification itself can be caught before code is written.
  • The same model animates the protocol, produces test suites for the implementation, and supplies machine-checkable evidence for properties such as the account mapping remaining a partial function.
  • If the approach spreads, the expected standard for critical cryptocurrency components shifts from unverified code to at least a formal functional model with automated checks, while full code-level verification remains a later stage.

Reading between the lines

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

  • A natural extension is to apply the same set-based pipeline to other critical distributed components such as wallets, payment channels, and consensus variants, where the mathematical core is small enough to specify but the failure cost is high.
  • The paper's ease claim is testable: one could measure model size and authoring time against the corresponding implementation for a complete EVM, rather than the selected excerpts, and compare the bug-finding power of generated tests against a real collection of smart contracts.
  • Because the paper's appendix notes that security properties do not enjoy the refinement property, an implication the authors leave implicit is that this pipeline should not be marketed as a security guarantee; its real value is likely as executable documentation and a functional-correctness backstop, with security handled in a separate layered verification effort.
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

4 major / 4 minor

Summary. The paper argues that cryptocurrency software should be treated as critical software and that formal methods should be adopted gradually, starting with set-based, first-order-logic specifications. It presents guidelines for such adoption, then exhibits excerpts of a set-based model of a consensus protocol (Section 3) and of the Ethereum Virtual Machine (Section 4). It uses these models to demonstrate three verification techniques: set-based prototyping and simulation with {log} (Section 5.1), model-based test generation via the Test Template Framework (Section 5.2), and automated proofs of two small properties (Section 5.3). The paper concludes that set-based specifications 'accurately and concisely describe cryptocurrency software' and that prototypes, simulations, test cases, and automated proofs can be obtained from such specifications.

Significance. If the demonstration were faithful and complete, the paper would provide a concrete, low-cost entry path to formal methods for cryptocurrency developers, with a concrete toolchain and a staged adoption strategy. Its strengths include the use of an existing, tool-supported set-based language ({log}), the connection to a prior machine-checked blockchain consensus formalization (Pirlea-Sergey), the concrete TTF test-condition derivation, and the honest discussion in Appendix A that security properties do not enjoy the refinement property. However, the paper's central claim is broader than its evidence: the EVM model is a fragment, TransactionValidity and Create1 are omitted, and the printed mathematics contains undefined variables. As a result, the paper currently reads as a position/experience statement whose load-bearing examples need repair before the central claim can be accepted.

major comments (4)
  1. [Section 3, RcvAddr definition] The second set comprehension in RcvAddr is written as `{a : s.as • (p?.2,a,AddrMsg p'.as)}`. Here `p'` is a packet, i.e., an element of `Addr × Addr × Msg`, not a record, so `p'.as` is undefined. The accompanying prose says these messages tell already-known peers that the node has learned new peers, and the {log} encoding uses `addrMsg(As_)`, where `As_` is the updated local address set. As printed, the mathematical specification cannot be checked against the executable prototype. This is not a purely cosmetic typo: the precision and clarity of the set-based notation is the central evidence for the paper's claim, so the formula must be corrected (most likely to `s'.as`) and aligned with the {log} clause.
  2. [Section 4, CheckpointState] The transaction record is defined with field `snd : Addr`, but the CheckpointState predicate refers to `t?.sender`. In addition, the post-state update `{(t?.sender,a')}` uses `a'`, which is neither a parameter of CheckpointState nor otherwise bound in the displayed predicate; `a'` is also passed to UpdateSender. These mismatches make the mathematical specification ill-formed and prevent a reader from judging whether the {log} implementation is faithful to the printed model. The signature and field names must be repaired, and `a'` must be declared or existentially quantified.
  3. [Section 5.3, automated proof of pfun preservation] The submitted {log} formula refers to `checkpointState(World,Trans,World_)`, but the full definition of `checkpointState` is not given: Section 4 says TransactionValidity is 'not shown' and Create1 is omitted 'due to space restrictions'. A reader therefore cannot check whether the proved property applies to the real predicate or only to a simplified placeholder, and the paper supplies no artifact or appendix with the omitted definitions. To support the claim that automated proofs are 'easily' obtained, the complete {log} encodings must be made available, or the paper must explicitly state and justify that the proved subset is sufficient for the claim.
  4. [Section 2.4 point 5 and Section 6] The paper deliberately abstracts away cryptography and security properties (Section 2.4, point 5) and Appendix A states that security properties do not enjoy the refinement property. Nevertheless, Section 6 concludes without qualification that set-based specifications 'accurately and concisely describe cryptocurrency software'. Given that the EVM and consensus excerpts omit precisely the security- and boundary-critical parts (TransactionValidity, Create1, cryptographic primitives), the final claim is stronger than the demonstrated scope. The conclusion should be explicitly restricted to functional specifications of representative components, and the paper should explain how the Appendix A layered approach would connect to the set-based models.
minor comments (4)
  1. [Section 4, 'Lesson learned' paragraph] The claim that the Yellow Paper contains 'many obscure (probably inconsistent) issues' is unsupported; either give at least one concrete example or soften the wording, since this assertion is not necessary for the paper's main argument.
  2. [Section 5.2, TTF derivation] The step from the eight standard partitions of `R ⊕ G` to the two test conditions `dom s.acc = {t?.sender}` and `{t?.sender} ⊂ dom s.acc` is stated as 'after some simplifications' without details. Show the simplification or cite a source where the same derivation is carried out, so the test-generation claim is reproducible.
  3. [Section 5.1, simulation output] The reported answer for `Ps1` is `ris(A in {a1,a2/_N2},[],true,[this,A,connectMsg],true)` with constraints `subset(_N2,{a1,a2})`; this is not a ground answer, and the text does not explain that the set remainder `_N2` is underspecified. Clarify the semantics of the answer or display a fully simplified ground answer.
  4. [Throughout] There are repeated typos and wording issues, including 'developtment' in Section 2.4 and 'irreparable loses' used several times; 'loses' should be 'losses'.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the paper illustrates a methodology with externally sourced models and independently checkable tool runs; self-citations are tooling references, not load-bearing premises.

full rationale

The paper does not derive predictions from fitted parameters or define its conclusions into its premises. Its two models are taken from external sources: the consensus model is 'based on the work by Pîrlea and Sergey [36]' and the EVM model 'departs from the Yellow Paper [43]'. The central claim that set-based specifications accurately and concisely describe cryptocurrency software is supported by excerpts and by demonstrations that the resulting {log} prototype can simulate the RcvAddr transition, that the Test Template Framework can generate test conditions from CheckpointState, and that {log} can discharge proof obligations such as disjointness of PsD and PsAs and preservation of the pfun invariant. These checks are against the models, not against the paper's own conclusions, and {log} is a pre-existing tool; there is no fitted parameter, no renaming of a known result, and no uniqueness theorem imported from the authors' prior work. Self-citations ([10], [15]–[19]) supply tooling, prior method descriptions, and prior applications; they are not invoked to forbid alternatives or to force the set-based choice. The paper itself flags a limitation in Section 2.4 and Appendix A: cryptography and security are abstracted away, and Appendix A states that security properties do not enjoy the refinement property. This is an applicability limitation, not circularity. No equation reduces to its own input, and no 'prediction' is statistically forced, so the honest finding is no significant circularity.

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

The central recommendation rests on four unproved assumptions: the adequacy of the abstract basic sets, the permissibility of abstracting away cryptography and security, the fidelity of the EVM model to the Yellow Paper, and the representativeness of the fragments. The paper explicitly states the first two and implicitly relies on the last two.

assumptions (4)
  • domain assumption Basic sets (Addr, Hash, Proof, Tx, A, B, W, etc.) are given, pairwise disjoint, and equipped with equality.
    Section 3 states the only condition required for these sets is that they come equipped with equality and be pairwise disjoint. This abstracts the structure of addresses, hashes, proofs, and transactions.
  • domain assumption Cryptography and security properties can be abstracted away in the first stage of formal-method adoption, focusing on functional specifications.
    Section 2.4 point 5 says 'Abstract away cryptography, assume it is correct, focus on functional specifications'; Appendix A explains that security properties do not enjoy the refinement property, which limits what can be concluded from the abstract models.
  • domain assumption The Ethereum Yellow Paper is the authoritative semantics of the EVM, and the set-based model is derived from it.
    Section 4 says 'we depart from the Yellow Paper' and models the EVM accordingly; the paper also claims to have found inconsistencies in the Yellow Paper but does not enumerate them, so fidelity to the actual EVM execution semantics is assumed.
  • ad hoc to paper The displayed specification fragments are representative of the full consensus protocol and EVM, so the demonstrated techniques generalize.
    Sections 3 and 4 present only excerpts and a simplified 'create' instruction; the paper does not justify that the omitted parts do not change the feasibility or results of the verification techniques.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Set-Based Models for Cryptocurrency Software." pith.science (2026). https://pith.science/paper/3KHEX7FV

@misc{pith2026190800591,
  author       = {Pith},
  title        = {Pith review of: Set-Based Models for Cryptocurrency Software},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/3KHEX7FV}},
  note         = {Machine review of arXiv:1908.00591}
}
read the original abstract

Emin G\"un Sirer once said: It's clear that writing a robust, secure smart contract requires extreme amounts of diligence. It's more similar to writing code for a nuclear power reactor, than to writing loose web code [...] Yet the current Solidity language and underlying EVM seems designed more for the latter. Formal methods (FM) are mathematics-based software development methods aimed at producing "code for a nuclear power reactor". That is, due application of FM can produce bug-free, zero-defect, correct-by-construction, guaranteed, certified software. However, the software industry seldom use FM. One of the main reasons for such a situation is that there exists the perception (which might well be a fact) that FM increase software costs. On the other hand, FM can be partially applied thus producing high-quality software, although not necessarily bug-free. In this paper we outline some FM related techniques whose application the cryptocurrency community should take into consideration because they could bridge the gap between "loose web code" and "code for a nuclear power reactor".

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

46 extracted references · 46 canonical work pages

  1. [1]

    J.-R. Abrial. The B-book: Assigning Programs to Meanings . Cambridge University Press, New York, NY, USA, 1996

    work page 1996

  2. [2]

    Schneider

    Bowen Alpern and Fred B. Schneider. Defining liveness. Inf. Process. Lett. , 21(4):181–185, 1985

    work page 1985

  3. [3]

    Anderson

    James P. Anderson. Computer Security technology plannin g study. Technical report, Deputy for Command and Management System, USA, 1972

    work page 1972

  4. [4]

    System- level non-interference of constant-time cryptography

    Gilles Barthe, Gustavo Betarte, Juan Diego Campo, and Car los Luna. System- level non-interference of constant-time cryptography. pa rt I: model. J. Autom. Reasoning, 63(1):1–51, 2019

    work page 2019

  5. [5]

    System-level non-interference for constant-t ime cryptography

    Gilles Barthe, Gustavo Betarte, Juan Diego Campo, Carlos Daniel Luna, and David Pichardie. System-level non-interference for constant-t ime cryptography. In Gail- Joon Ahn, Moti Yung, and Ninghui Li, editors, Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security , Scottsdale, AZ, USA, November 3-7, 2014 , pages 1267–1279. ACM, 2014

    work page 2014

  6. [6]

    A machine-checked formalization of sigma- protocols

    Gilles Barthe, Daniel Hedin, Santiago Zanella B´ eguelin , Benjamin Gr´ egoire, and Sylvain Heraud. A machine-checked formalization of sigma- protocols. In Pro- ceedings of the 23rd IEEE Computer Security Foundations Sym posium, CSF 2010, Edinburgh, United Kingdom, July 17-19, 2010 , pages 246–260. IEEE Computer Society, 2010

    work page 2010

  7. [7]

    D. E. Bell and L. J. LaPadula. Secure computer systems: Mat hematical founda- tions. Technical Report MTR-2547, Vol. 1, MITRE Corp., Bedf ord, MA, 1973

    work page 1973

  8. [8]

    Interactive theorem proving and program development: Coq’ Art : the calculus of inductive constructions

    Yves Bertot, Pierre Castran, Grard (informaticien) Huet , and Christine Paulin- Mohring. Interactive theorem proving and program development: Coq’ Art : the calculus of inductive constructions . Texts in theoretical computer science. Springer, Berlin, New York, 2004. Donnes complmentaires http://coq. inria.fr

    work page 2004

Show all 46 references
  1. [9]

    Formal analysis of android’s permission-based security model,

    Gustavo Betarte, Juan Diego Campo, Carlos Luna, and Agust ´ ın Romano. Formal analysis of android’s permission-based security model,. Sci. Ann. Comp. Sci. , 26(1):27–68, 2016

    2016

  2. [10]

    Towards a formally verified implementation of the mimblewimble cryp- tocurrency protocol

    Gustavo Betarte, Maximiliano Cristi´ a, Carlos Luna, Ad ri´ an Silveira, and Dante Zanarini. Towards a formally verified implementation of the mimblewimble cryp- tocurrency protocol. CoRR, abs/1907.01688, 2019

    1907 arXiv

  3. [11]

    Formal ver- ification of smart contracts: Short paper

    Karthikeyan Bhargavan, Antoine Delignat-Lavaud, C´ ed ric Fournet, Anitha Gol- lamudi, Georges Gonthier, Nadim Kobeissi, Natalia Kulatov a, Aseem Rastogi, Thomas Sibut-Pinote, Nikhil Swamy, and Santiago Zanella B´ eguelin. Formal ver- ification of smart contracts: Short paper. ...

    2016

  4. [12]

    Handbook of Satisfiability , volume 185 of Frontiers in Artificial Intelligence and Applications

    Armin Biere, Marijn Heule, Hans van Maaren, and Toby Wals h, editors. Handbook of Satisfiability , volume 185 of Frontiers in Artificial Intelligence and Applications . IOS Press, 2009

    2009

  5. [13]

    Critical update re: Dao vulnerability

    Vitali Buterin. Critical update re: Dao vulnerability. https://blog.ethereum.org/2016/06/17/critical-update-re-dao-vulnerability, 2016

    2016

  6. [14]

    Clarke, Orna Grumberg, and Doron A

    Edmund M. Clarke, Orna Grumberg, and Doron A. Peled. Model checking. MIT Press, 2001

    2001

  7. [15]

    Cristi´ a, Pablo Albertengo, Claudia S

    M. Cristi´ a, Pablo Albertengo, Claudia S. Frydman, Bria n Pl¨ uss, and Pablo Rodr ´ ıguez Monetti. Tool support for the test templat e framework. Softw. Test., Verif. Reliab. , 24(1):3–37, 2014

    2014

  8. [16]

    Cristi´ a and G

    M. Cristi´ a and G. Rossi. Rapid prototyping and animatio n of Z specifications using {log}. In 1st International Workshop about Sets and Tools (SETS 2014) , pages 4– 18, 2014. Informal proceedings: http://sets2014.cnam.fr /papers/sets2014.pdf

    2014

  9. [17]

    Cristi´ a and G

    M. Cristi´ a and G. Rossi. A decision procedure for restri cted intensional sets. In CADE, volume 10395 of LNCS, pages 185–201. Springer, 2017

    2017

  10. [18]

    Cristi´ a and G

    M. Cristi´ a and G. Rossi. Solving quantifier-free first-o rder constraints over finite sets and binary relations. Journal of Automated Reasoning , Apr 2019

    2019

  11. [19]

    Fry dman, Brian Pl¨ uss, and Pablo Rodr ´ ıguez Monetti

    Maximiliano Cristi´ a, Pablo Albertengo, Claudia S. Fry dman, Brian Pl¨ uss, and Pablo Rodr ´ ıguez Monetti. Applying the test template frame work to aerospace software. In James L. Rash and Christopher A. Rouff, editors, 34th Annual IEEE Software Engineering Workshop, SEW 2011...

    2011

  12. [20]

    Fitzgerald, Juan Bicarregui, Peter Gorm Larsen, and Jim Woodcock

    John S. Fitzgerald, Juan Bicarregui, Peter Gorm Larsen, and Jim Woodcock. In- dustrial deployment of formal methods: Trends and challeng es. In Alexander B. Romanovsky and Martyn Thomas, editors, Industrial Deployment of System En- gineering Methods, pages 123–143. Springer, 2013

    2013

  13. [21]

    Goguen and Jos´ e Meseguer

    Joseph A. Goguen and Jos´ e Meseguer. Security policies a nd security models. In IEEE Symposium on Security and Privacy , pages 11–20, 1982

    1982

  14. [22]

    A semantic frame- work for the security analysis of ethereum smart contracts

    Ilya Grishchenko, Matteo Maffei, and Clara Schneidewind . A semantic frame- work for the security analysis of ethereum smart contracts. In Lujo Bauer and Ralf K¨ usters, editors, Principles of Security and Trust - 7th International Con- ference, POST 2018, Held as Part of the E...

    2018

  15. [23]

    Validation of formal models by refinement animation

    Stefan Hallerstede, Michael Leuschel, and Daniel Plagg e. Validation of formal models by refinement animation. Sci. Comput. Program. , 78(3):272–292, 2013

    2013

  16. [24]

    Hierons, Kirill Bogdanov, Jonathan P

    Robert M. Hierons, Kirill Bogdanov, Jonathan P. Bowen, R ance Cleaveland, John Derrick, Jeremy Dick, Marian Gheorghe, Mark Harman, Kalpes h Kapoor, Paul Krause, Gerald L¨ uttgen, Anthony J. H. Simons, Sergiy Vilkomir, Martin R. Wood- ward, and Hussein Zedan. Using formal speci...

    2009

  17. [25]

    Defining the ethereum virtual machine for i nteractive theorem provers

    Yoichi Hirai. Defining the ethereum virtual machine for i nteractive theorem provers. In Michael Brenner, Kurt Rohloff, Joseph Bonneau, A ndrew Miller, Pe- ter Y. A. Ryan, Vanessa Teague, Andrea Bracciali, Massimili ano Sala, Federico Pintore, and Markus Jakobsson, editors, Fina...

    2017

  18. [26]

    Eval- uation of logic-based smart contracts for blockchain syste ms

    Florian Idelberger, Guido Governatori, R´ egis Riveret , and Giovanni Sartor. Eval- uation of logic-based smart contracts for blockchain syste ms. In Jos´ e J´ ulio Alferes, Leopoldo E. Bertossi, Guido Governatori, Paul Fodor, and Du mitru Roman, ed- itors, Rule Technologies. ...

    2016

  19. [27]

    Cliff B. Jones. Systematic Software Development Using VDM (2Nd Ed.) . Prentice- Hall, Inc., Upper Saddle River, NJ, USA, 1990

    1990

  20. [28]

    Murray, Thomas Sewell, Rafal Kolanski, and Gernot Heiser

    Gerwin Klein, June Andronick, Kevin Elphinstone, Toby C . Murray, Thomas Sewell, Rafal Kolanski, and Gernot Heiser. Comprehensive f ormal verification of an OS microkernel. ACM Trans. Comput. Syst. , 32(1):2:1–2:70, 2014

    2014

  21. [29]

    Applying a formal method in industry: A 25-year trajectory

    Thierry Lecomte, David D´ eharbe, ´Etienne Prun, and Erwan Mottin. Applying a formal method in industry: A 25-year trajectory. In Simone A ndr´ e da Costa Cav- alheiro and Jos´ e Luiz Fiadeiro, editors, Formal Methods: Foundations and Appli- cations - 20th Brazilian Symposium,...

    2017

  22. [30]

    Formal verification of a realistic compile r

    Xavier Leroy. Formal verification of a realistic compile r. Commun. ACM , 52(7):107–115, 2009

    2009

  23. [31]

    Michael Leuschel and Michael J. Butler. Prob: an automat ed analysis toolset for the B method. STTT, 10(2):185–203, 2008

    2008

  24. [32]

    Mak- ing smart contracts smarter

    Loi Luu, Duc-Hiep Chu, Hrishi Olickel, Prateek Saxena, a nd Aquinas Hobor. Mak- ing smart contracts smarter. In Edgar R. Weippl, Stefan Katz enbeisser, Christo- pher Kruegel, Andrew C. Myers, and Shai Halevi, editors, Proceedings of the 2016 ACM SIGSAC Conference on Computer a...

    2016

  25. [33]

    Madanlal Musuvathi and Dawson R. Engler. Model checking large network pro- tocol implementations. In Robert Tappan Morris and Stefan S avage, editors, 1st Symposium on Networked Systems Design and Implementati on (NSDI 2004), March 29-31, 2004, San Francisco, California, USA, ...

    2004

  26. [34]

    Nakamoto

    S. Nakamoto. Bitcoin: A peer-to-peer electronic cash sy stem. Cryptography Mailing list at https://metzdowd.com , 03 2009

    2009

  27. [35]

    Automated theorem proving - theory and practice

    Monty Newborn. Automated theorem proving - theory and practice . Springer, 2001

    2001

  28. [36]

    P ˆ ırlea and I

    G. P ˆ ırlea and I. Sergey. Mechanising blockchain consensus. In Proc. of CPP 2018 , pages 78–90, New York, USA, 2018. ACM

    2018

  29. [37]

    Ever- crypt: A fast, verified, cross-platform cryptographic prov ider

    Jonathan Protzenko, Bryan Parno, Aymeric Fromherz, Chr is Hawblitzel, Marina Polubelova, Karthikeyan Bhargavan, Benjamin Beurdouche, Joonwon Choi, An- toine Delignat-Lavaud, C´ edric Fournet, Tahina Ramananan dro, Aseem Rastogi, Nikhil Swamy, Christoph Wintersteiger, and Santi...

    2019

  30. [38]

    {log}, 2008

    Gianfranco Rossi. {log}, 2008

    2008

  31. [39]

    J. M. Spivey. The Z notation: a reference manual . Prentice Hall International (UK) Ltd., Hertfordshire, UK, UK, 1992

    1992

  32. [40]

    Carrington

    Phil Stocks and David A. Carrington. A framework for spec ification-based testing. IEEE Trans. Software Eng. , 22(11):777–793, 1996

    1996

  33. [41]

    The Coq Dev. Team. The Coq Proof Assistant Reference Manual – V. 8.9.0 , 2019

    2019

  34. [42]

    Practical Model-Based Testing: A Tools Ap- proach

    Mark Utting and Bruno Legeard. Practical Model-Based Testing: A Tools Ap- proach. Morgan Kaufmann Publishers Inc., San Francisco, CA, USA, 2 006

  35. [43]

    Ethereum: A secure decentralised generalis ed transaction ledger eip- 150 revision (759dccd - 2017-08-07), 2017

    Gavin Wood. Ethereum: A secure decentralised generalis ed transaction ledger eip- 150 revision (759dccd - 2017-08-07), 2017. Accessed: 2018- 01-03. A Subtleties and Traps with Security Properties Security properties have proved to be unexpectedly complex to gr asp and for- mal...

    2017

  36. [44]

    Verification is performed on idealized models that abstract away t he specifics of any particular implementation, and yet provide a realistic setting in which to explore the security issues that pertain to the realm of those (c ritical) mechanisms

  37. [45]

    Additionally, verification is performed on more concrete models wh ere low level mechanisms (such as pointer arithmetic) are specified

  38. [46]

    A particular class of the idealized models mentioned above are those c alled se- curity models

    Finally, the low level model is proved to be a correct implementation of the idealized model. A particular class of the idealized models mentioned above are those c alled se- curity models. These models have played an important role in the design and eval- uation of high assur...

    1973

Pith tools

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