Smart contracts Verification
High-assurance smart contracts
The goal of this project is to use formal verification to improve assurance of smart contracts. By providing mathematical rigorous proofs that smart contracts do what we think they should do, we better leverage of such technology and enable its use for safety- and security-critical purposes.
We have developed a framework to reason formally about Ethereum Virtual Machine bytecode execution in Isabelle/HOL. We have used that framework to verify Ethereum smart contracts. Now we are extending that framework to be able to verify realistic food supply-chain smart contracts.
This project is one of many Trustworthy Systems projects and is done in collaboration with the Blockchain research group in Data61's Software and Computational Systems.
Publications
Contact
Mark Staples, mark.staples<at>data61.csiro.au