Release of Imandra EVM: A formal model of the Ethereum Virtual Machine

We’re pleased to announce the first public release of our Imandra-based formal model of the Ethereum Virtual Machine (EVM). We’ve made the model open source under the Apache 2.0 license. This model gives Imandra a formal semantics of Ethereum bytecode, so that Imandra can be used to reason about the possible behaviours of compiled Ethereum smart contracts. It’s the first public entry in our community models repository.

We hope this model will be useful to the community, and that it will be improved (see the ongoing TODO in the github repository), ported and built upon by many.

Happy verifying!

By using this website, you agree to our cookie policy

Please note that the Imandra website no longer supports Internet Explorer

We recommend upgrading to the latest Microsoft Edge, Google Chrome, or Firefox