Posted on by Achim D. Brucker, licensed under CC BY-ND 4.0.

Announcement: Isabelle/Solidity

Ever wondered how to verify smart contracts written in Solidy? Thanks to our deep embedding of Solidty into Isabelle/HOL, you can now start verifying smart contracts in Isabelle.

Our formalization is available in the Archive of Formal Proofs [1], which can be easily added to Isabelle/HOL. If you want to read a more high-level description of the underlying work, read our conference papers on the topic [3].


D. Marmsoler and A. D. Brucker, Isabelle/solidity: A deep embedding of solidity in isabelle/HOL,” Archive of Formal Proofs, Jul. 2022,
D. Marmsoler and A. D. Brucker, A denotational semantics of Solidity in Isabelle/HOL,” in Software engineering and formal methods (SEFM), R. Calinescu and C. Pasareanu, Eds. Heidelberg: Springer-Verlag, 2021.
D. Marmsoler and A. D. Brucker, Conformance testing of formal semantics using grammar-based fuzzing,” in TAP 2022: Tests and proofs, L. Kovacs and K. Meinke, Eds. Heidelberg: Springer-Verlag, 2022.

Welcome to the blog of the Software Assurance & Security Research Team at the University of Exeter. We blog regularly news, tips & tricks, as well as fun facts about software assurance, reliability, security, testing, verification, hacking, and logic.

You can also follow us on Twitter: @logicalhacking.




academia ai android apidesign appsec bitcoin blockchain bpmn browser browserextensions browsersecurity bug certification chrome composition cordova dast devops devsecops dom dsbd efsm epsrc event extensions fixeffort floss formaldocument formalmethods funding hol-ocl hol-testgen humanfactor hybridapps iast industry internetofthings iot isabelle/hol isabelledof isadof latex logic maintance malicous mbst mobile mobile apps modelinference modeling monads monitoring msc ocl ontology opensource owasp patches pet phd phdlife phishing policy protocols publishing reliability research safelinks safety sap sast sdlc secdevops secureprogramming security securityengineering securitytesting semantics servicecomposition skills smartcontract smartthings softwareeinginering softwaresecurity softwaresupplychain solidity staff&positions statemachine studentproject tcb test&proof testing tips&tricks tools transport tuos uk uoe upgrade usability verification vulnerabilities vulnerableapplication webinar websecurity


blog whole site