C

ConCert

A framework for smart contract verification in Coq