Thursday 30 January 2020, 14:00, LSV library: Functional Verification of Tezos Smart Contracts in Coq, Raphaël Cauderlier (nomadic labs).

Smart contract blockchains such as Ethereum and Tezos let their users program their crypto-money accounts. Bugs in these smart contracts can lead to huge losses. Yet smart contracts are necessarily small programs because checking the blockchain requires to evaluate all the smart contract calls in the history of the chain. For these reasons, smart contract languages are a good spot for formal methods.

The Tezos blockchain and its smart contract language Michelson have been designed with verification in mind. In this talk, I will present Mi-Cho-Coq, a formal specification of Michelson in the Coq proof assistant, and its applications for functional verification and certified compilation.