Britten, DanielReeves, SteveArtho, CyrilleÖlveczky, Peter Csaba2023-01-302023-01-3020229781450399074https://hdl.handle.net/10289/15470To create trustworthy programs, the 'gold standard' is specifications at a high-enough level to clearly correspond to the informal specifications, and also a refinement proof linking these high-level specifications down to, in our case, executable bytecode. The DeepSEA system demonstrates how this can be done, in the context of smart contracts on the Ethereum blockchain. A key component of this is the model of the blockchain on which the smart contracts reside. When doing proofs in DeepSEA, it is critical to have such a model, which allows for the writing of specifications at a high-level clearly corresponding to informal specifications. A candidate model for doing so and its usefulness for carrying out proofs is discussed in this paper.application/pdfenThis is an author’s accepted version of a conference paper published in FTSCS 2022: Proceedings of the 8th ACM SIGPLAN International Workshop on Formal Techniques for Safety-Critical Systems. © 2022 Copyright held by the authors. Publication rights licensed to ACM.blockchainformal methodssmart contractssoftware engineeringConference Contribution10.1145/3563822.3568011