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. Mutants are identical copies of the tested program with a single random change. The objective is to assess how well a test suite can identify and detect faulty logic in 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. Using Gambit with the Prover describes how to use Gambit with the Certora Prover to evaluate specifications, while Gambit: Mutant Generation for Solidity describes how Gambit can be used to generate mutants for use with any tool.

• Using Gambit with the Prover
  • Installation
  • Running the Mutation Verifier
  • Mutation Configuration
  • Mutation Sources
  • Original Verification Run
  • The Mutations Dashboard
  • Mutation Test Report
  • CLI Options
  • Troubleshooting
• Gambit: Mutant Generation for Solidity
  • Requirements
  • Installation
  • Usage
  • Examples
  • Configuration Files
  • Results Directory
  • CLI Options
  • Mutation Operators