How it works

The introduction covers what a proof is: your code and a property translated into one formula, handed to a solver that searches for an input which breaks it. This page covers the part you actually write — and the path your code takes to get there.

Symbolic inputs

A proof needs something to range over. You mark the unknowns with helpers like anyInt() — each is a hole the solver is free to fill with any value while it hunts for a counterexample.

@BmcProof
fun `addition commutes`() {
    val a = anyInt()        // each stands for every Int, at once
    val b = anyInt()
    check(a + b == b + a)   // holds for every pair — overflow and all
}

You shrink that space with assumptions. assume(x > 0) restricts the search to positive inputs; assumeValid { Score(anyInt()) } runs the constructor’s require checks and folds them into the domain, so the proof ranges over exactly the valid values — nothing more, nothing less.

The path a proof takes

From the @BmcProof you write to the verdict you get back:

1. Load the bytecode — the real compiled classes, not the source.
2. Substitute — external or heavy code is replaced by a model or havoc’d, so the solver only sees what matters.
3. Unwind loops and recursion to the bound (auto-discovered by default, or one you pin).
4. Translate the bytecode and your check into one logical formula.
5. Solve — the SAT solver searches for an input that breaks it.
6. Report the verdict: Verified, Refuted with the counterexample, or Unknown.

Steps 2, 3 and 6 lean on ideas from the Key Concepts — models, havoc, unwinding, and the three-way verdict. Here they’re just the stations your code passes through.

Proof vs. test

• A green test means the inputs you chose worked.
• A green proof means no input exists that breaks the property, up to the bound.

Fuzzing narrows the gap by generating many inputs, but it’s still sampling — at best “no bug found yet.” A proof is a statement about all inputs at once.