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 randomly mutate the program to potentially introduce faults and then running the test suite on the “mutants” — if the test suite “kills” a large percentage of mutants, that is an indication of a “good” test suite. Mutants that pass the tests are often used as a guide to improve the test suite by adding more tests.

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 then 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. Generating Mutations 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.

• Generating Mutations
  • Installing Gambit
  • Usage
  • Mutation Types
• Using Gambit with the Prover
  • Installations and Setup
  • Running the Mutation Verifier
  • Configuration
  • Visualization