# Counterexample Generation

## Overview

Counterexample generation is a new experimental feature in Kontrol that helps developers understand why their proofs fail by providing concrete examples of inputs and execution paths that violate the properties being tested. It enables the users to easily reproduce the failing test case with Foundry and is essential for debugging and improving smart contract verification.

## What Are Counterexamples?

A counterexample in the context of formal verification is a concrete execution trace that demonstrates how a property can be violated. In Kontrol, counterexamples show input values that lead to property violations and the path conditions that should be satisfied for the failure to occur.

## How Counterexample Generation Works

Kontrol generates counterexamples by:

1. **Analyzing failed proofs**: When a proof fails, Kontrol identifies the specific execution path that led to the failure and generates the model that demonstrates the concrete values that symbolic variables should take for the failure to happen
2. **Extracting concrete values**: Symbolic variables are instantiated with concrete values that trigger the failure
3. **Constructing execution trace**: The complete execution path is reconstructed with concrete values in the form of a Foundry test case and is saved in a new file

## Basic Usage

{% hint style="warning" %}
**Experimental Feature**: Counterexample generation is currently experimental, and dynamically-sized types like `bytes` of variable length, mappings, and arrays are not supported. The `KontrolTest` contract generated by `kontrol init` includes some auxiliary functions that allow setting up symbolic storage for these types manually.
{% endhint %}

### Step 1: Enable Counterexample Generation

Counterexample generation is enabled by providing the `--generate-counterexample` option to `kontrol prove`. When a proof fails, Kontrol automatically generates concrete counterexample test functions:

```bash
kontrol prove --function testMyProperty --generate-counterexample
```

### Step 2: Generated Counterexample Functions

When a proof fails, Kontrol generates a new Solidity test file with concrete counterexample functions. For example, let's consider the following failing test:

**Original Failing Test:**

```solidity
function test_storage_setup(
    uint256 totalSupply, 
    uint256 _totalSupply, 
    address _owner, 
    uint256 _currentUser_id, 
    address _currentUser_wallet, 
    bool _currentUser_isActive, 
    uint256 _anotherTotalSupply
) public {
    assert(totalSupply != 0);

    simpleStorageStorageSetup(address(simpleStorage), _totalSupply, _owner, _currentUser_id, _currentUser_wallet, _currentUser_isActive);
    assert(simpleStorage.totalSupply() == _anotherTotalSupply);
}
```

This proof, when executed with `kontrol prove --no-fail-fast`, will result in two failing nodes: one for the violation of `assert(totalSupply != 0)`, and one for `assert(simpleStorage.totalSupply() == _anotherTotalSupply)`. When executed with `--generate-counterexample`, `kontrol prove` will generate a file named `SimpleStorageTestCounterexampleTest.t.sol` with these two functions:

**Generated Counterexample Functions:**

```solidity
function test_storage_setup_ce0() public {
    // Counterexample values from failed proof:
    uint256 totalSupply = 0;
    uint256 _totalSupply = 0;
    address _owner = address(0);
    uint256 _currentUser_id = 0;
    address _currentUser_wallet = address(0);
    bool _currentUser_isActive = false;
    uint256 _anotherTotalSupply = 0;

    assert(totalSupply != 0);

    simpleStorageStorageSetup(address(simpleStorage), _totalSupply, _owner, _currentUser_id, _currentUser_wallet, _currentUser_isActive);
    assert(simpleStorage.totalSupply() == _anotherTotalSupply);
}

function test_storage_setup_ce1() public {
    // Counterexample values from failed proof:
    uint256 totalSupply = 1;
    uint256 _totalSupply = 1;
    address _owner = address(0);
    uint256 _currentUser_id = 0;
    address _currentUser_wallet = address(0);
    bool _currentUser_isActive = false;
    uint256 _anotherTotalSupply = 0;

    assert(totalSupply != 0);

    simpleStorageStorageSetup(address(simpleStorage), _totalSupply, _owner, _currentUser_id, _currentUser_wallet, _currentUser_isActive);
    assert(simpleStorage.totalSupply() == _anotherTotalSupply);
}
```

These tests can now be concretely executed with Foundry to reproduce the failing test cases:

```bash
forge test --match-test test_storage_setup_ce0
forge test --match-test test_storage_setup_ce1
```

**Key Features:**

* **Multiple failing nodes**: Generates indexed counterexample functions (`_ce0`, `_ce1`) for different failure scenarios
* **Concrete values**: Automatically maps symbolic variables of supported types to concrete values that trigger the failure. Supported types including `uint` and `int` of any width, `address`, `bool`, `bytes` of fixed length, and `struct` variables
* **Automatic file generation**: Creates `{OriginalTestContractName}CounterexampleTest.t.sol` in the same directory as the original proof contract
* **Type conversion**: Properly handles Solidity type conversions between SMT model assignments (usually of `int` type) and Solidity types

## Generated Files

The counterexample generation creates a new test file with the naming pattern:

* **Original file**: `MyContractTest.t.sol`
* **Generated file**: `MyContractTestCounterexampleTest.t.sol`

The generated file is placed in the same directory as the original test file to maintain accurate import paths.

## Development Workflow

1. **Write property**: Define the property you want to verify
2. **Run initial proof**: `kontrol prove --function testProperty --generate-counterexample`
3. **Analyze counterexample**: If it fails, examine the generated counterexample
4. **Fix the issue**: Use the counterexample to validate, identify, and fix the problem using Foundry's concrete execution for faster iteration
5. **Re-run proof**: Verify the fix resolves the counterexample
6. **Iterate**: Repeat until the proof passes

## Related Features

* [Structured Symbolic Storage Generation](/kontrol/guides/structured-symbolic-storage-generation.md) - Automated storage setup
* [Symbolic Storage](/kontrol/guides/advancing-proofs/symbolic-storage.md) - Manual storage management
* [Debugging Failing Proofs](/kontrol/tips/debugging-failing-proofs.md) - General debugging guide

## References

* [Kontrol Cheatcodes Reference](/kontrol/cheatsheets/kontrol-cheatsheet.md)


---

# Agent Instructions: Querying This Documentation

If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question.

Perform an HTTP GET request on the current page URL with the `ask` query parameter:

```
GET https://docs.runtimeverification.com/kontrol/guides/counterexample-generation.md?ask=<question>
```

The question should be specific, self-contained, and written in natural language.
The response will contain a direct answer to the question and relevant excerpts and sources from the documentation.

Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.