DevCon 2: Imandra Contracts: Formal Verification for Ethereum

Imandra formalizes the EVM inside an Ocaml-based formal verification language. This allows companies to prove which risks are present in their contracts so that they can take the steps necessary to hedge that risk. These proofs help to translate systems between platforms, like Ethereum and Corda. Imandra can generate visual representations of the space of possible behaviors in a contract and drill down to which constraints apply in each category.

Dr. Grant Passmore and Evgeny Gokhberg presenting in DevCon2 in Shanghai, China

This series was a collaborative research project written by Bill Gleim, Simon de la Rouviere, Paul Kohlhaas, and Niran Babalola. It was crowdfunded by the Ethereum Movement, a decentralized nonprofit built on Benefactory.