(gambit-intro)=
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](https://github.com/Certora/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. 
{doc}`mutation-verifier` describes how to use Gambit with the Certora Prover to 
  evaluate specifications, 
  while {doc}`gambit` describes how Gambit can be used to generate mutants for use with any tool.

```{toctree}
:maxdepth: 2

mutation-verifier.md
gambit.md
```