Imandra Contracts is a platform for analysing and reasoning about smart contracts, built on top of the Imandra formal verification system.
This repository contains our community models. These models customise Imandra for reasoning about various classes of smart contracts.
Our first community model is an Imandra model of the Ethereum Virtual Machine (EVM). This model provides an executable operational semantics for the EVM, empowering Imandra to reason about Ethereum bytecode.
For a quick example, see EVM/README. For more, see docs.imandra.ai.
Have an idea to improve these models? Please join us!
- Grant Passmore (grant@aestheticintegration.com)
- Kostya Kanishev (kostya@aestheticintegration.com)
Apache 2.0