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.
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.