Formal Design, Implementation and Verification of Blockchain Languages (Invited Talk)

Author Grigore Rosu

Thumbnail PDF


  • Filesize: 393 kB
  • 6 pages

Document Identifiers

Author Details

Grigore Rosu
  • University of Illinois at Urbana-Champaign and Runtime Verification, Inc., USA,

Cite AsGet BibTex

Grigore Rosu. Formal Design, Implementation and Verification of Blockchain Languages (Invited Talk). In 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 108, pp. 2:1-2:6, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)


This invited paper describes recent, ongoing and planned work on the use of the rewrite-based semantic framework K to formally design, implement and verify blockchain languages and virtual machines. Both academic and commercial endeavors are discussed, as well as thoughts and directions for future research and development.

Subject Classification

ACM Subject Classification
  • Security and privacy → Logic and verification
  • Software and its engineering → Software verification
  • Theory of computation → Logic and verification
  • Formal semantics
  • Program verification
  • Blockchain


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Nicola Atzei, Massimo Bartoletti, and Tiziana Cimoli. A survey of attacks on Ethereum smart contracts. IACR Cryptology ePrint Archive, 2016:1007, 2016. Google Scholar
  2. Mike Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs, and K. Rustan M. Leino. Boogie: A modular reusable verifier for object-oriented programs. In Formal Methods for Components and Objects (FMCO'05), volume 4111 of LNCS, pages 364-387, 2006. Google Scholar
  3. Lorenz Breidenbach, Phil Daian, Ari Juels, and Emin Gün Sirer. An in-depth look at the parity multisig bug, 2017. URL:
  4. Vitalik Buterin. Thinking about smart contract security, 2016. URL:
  5. Andrei Ştefănescu, Daejun Park, Shijiao Yuwen, Yilong Li, and Grigore Roşu. Semantics-based program verifiers for all languages. In Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'16). ACM, Nov 2016. Google Scholar
  6. Phil Daian. DAO attack, 2016. URL:
  7. Etherscan. Ethereum transactions, 2018. URL:
  8. Jean-Christophe Filliâtre and Claude Marché. The why/krakatoa/caduceus platform for deductive program verification. In CAV, volume 4590 of LNCS, pages 173-177, 2007. Google Scholar
  9. Everett Hildenbrandt, Manasvi Saxena, Xiaoran Zhu, Nishant Rodrigues, Philip Daian, Dwight Guth, Brandon Moore, Yi Zhang, Daejun Park, Andrei Ştefănescu, and Grigore Roşu. KEVM: A Complete Semantics of the Ethereum Virtual Machine. In Computer Security Foundations Symposium (CSF'18), 2018. URL:
  10. The Coq development team. The Coq proof assistant reference manual. LogiCal Project, 2004. Version 8.0. URL:
  11. Grigore Roşu and Traian Florin Şerbănuţă. An overview of the K semantic framework. Journal of Logic and Algebraic Programming, 79(6):397-434, 2010. Google Scholar
  12. Jutta Steiner. Security is a process: A postmortem on the parity multi-sig library self-destruct, 2017. URL:
  13. The Isabelle development team. Isabelle, 2018. URL:
  14. Gavin Wood. Ethereum: A secure decentralised generalised transaction ledger, 2014. (Updated for EIP-150 in 2017) URL:
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail