Formal Methods

Finding Real-World Bugs in Smart Contract Interactions with Property-Based Testing (Mon, Dec 14, 2020) By Mikkel Milo et al.

Recently, Nomadic Labs made a blog post detailing their work on formally verifying the Dexter smart contract, a contract that provides decentralized exchange of digital assets. They verified functional properties of the contract using Mi-Cho-Coq, a Coq framework for proving properties about Michelson contracts in Tezos. A key limitation of Mi-Cho-Coq is that it does not allow for proving properties about contract-to-contract communications (also referred to as inter-contract communications, or just contract interactions).

Read more