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.

Read more at
http://www.github.com/imandra-ai/contracts/

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!

Previous:
AI Submits Reg AT Comment Letter

Next:
Checkout all media!