Exploring Solidity’s Model Checker
Read my article here:
Model checking is a method of formally verifying whether a model of a system meets a specification. Modern model checkers can determine whether certain security properties hold true for a given program, and can automate the discovery of memory corruption bugs, unsafe arithmetic, assertion failures, and more. When a property is not found to hold, a model checker produces a counterexample that acts as a proof of its contradiction.
While working with our clients to test the security of high assurance software, such as smart contracts that transact valuable digital assets, we often find ourselves seeking a high level of confidence in a program’s correctness. A model checker is one type of tool with the potential of delivering this level of confidence when used effectively. Furthermore, the security properties we formulate can be later used by our clients to perform their own formal verification even after an engagement has ended. Many of these companies would not otherwise use formal methods due to their reputation of having steep learning curves and being highly academic.
This is why we are excited to see the development of a model checker within the Solidity compiler itself. Solidity is the predominant programming language for the Ethereum Virtual Machine (EVM), and is what many widely used smart contracts today are written in. While there are already several formal verification tools that support Solidity and/or the EVM, our hope is that having a model checker built directly into Solidity will make formal methods more accessible to developers. In addition, specifications are written inline using the Solidity language itself. This means that while there is some extra work involved in writing a specification, it does not come with the usual overhead of having to install a new tool and learn a new language.