How Good Is Your Formal Specification? Mutation Testing To The Rescue!

Thu, Nov 16, 2023, 08:10 AM · 29:24

The result of a smart contract verification tool is only as good as the specification. But how does one know if their specification is good? To address this problem, we present Gambit, an automated Solidity mutation testing tool. Gambit injects small faults in the code to create "mutants”. These mutants are automatically verified by The Certora Prover against a formal specification. Mutants passing verification reveal potential specification gaps which can guide the user in improving the specification. Gambit thus increases confidence in the results of formal verification. Gambit can be used not just for formal verification but also for smart contract testing. Join us to learn how Gambit works and how it can benefit your use case!