Gambit: Mutation Generator for Solidity

This chapter describes how Certora uses ideas from mutation testing to evaluate and improve CVL specifications.

Mutation testing is a technique for evaluating and improving test suites. The key idea is to introduce faults, called mutants, to the program under test and measure a test suite’s ability to detect these mutants. The more mutants a test suite detects, or kills, the better the test suite is. Live mutants—those that pass all tests in the test suite—are indications of potential shortcomings in the test suite and can be used as test goals to improve the test suite.

At Certora, we use mutation testing to evaluate and improve formal specifications used in automated verification. We built Gambit, an open-source mutation generator for Solidity. We use the mutants generated by Gambit to assess the CVL specifications written for a verification task. Gambit is a general-purpose mutation generation tool that can be used with many kinds of verifiers or testing tools. Gambit: Mutant Generation for Solidity describes how Gambit can be used to generate mutants for use with any tool; while Using Gambit with the Prover describes how to use Gambit with the Certora Prover to evaluate specifications.