A tool for proving Michelson Smart Contracts in WHY3*. - Luís Pedro Arrojado da Horta; João Santos Reis; Simão Melo de Sousa; Mário Pereira (Blockchain, 2020)

Tezla, an Intermediate Representation for Static Analysis of Michelson Smart Contracts. - João Santos Reis; Paul Andrew Crocker; Simão Melo de Sousa (FMBC@CAV, 2020)

WhylSon: Proving your Michelson Smart Contracts in Why3. - Luís Pedro Arrojado da Horta; João Santos Reis; Mário Pereira; Simão Melo de Sousa (CoRR, 2020)