prover

/prover — prove it, don't just fuzz it

Fuzzing samples inputs; formal verification proves a property over all inputs (or returns a concrete counter-example). This command defaults to Halmos — symbolic execution that runs offline against your existing Foundry tests — and falls back to Certora (CVL spec) when configured.

Procedure

Step 1 — Pick the property

$ARGUMENTS is [contract] [property]. If no property is named, propose from the templates by protocol type below. Each maps to a check_ test function.

ERC-20 — supply conservation / no inflation

function check_transfer_preservesSupply(address to, uint256 amt) public {
    uint256 pre = token.totalSupply();
    token.transfer(to, amt);
    assert(token.totalSupply() == pre);   // no mint/burn on transfer
}

AMM — constant-product K monotonicity

• reserve0 * reserve1 after a fee-paying swap is >= before. [[flash-loan-attacks]].

Access control — only-owner can call X

function check_setFee_onlyOwner(address caller, uint16 bps) public {
    vm.assume(caller != owner);
    vm.prank(caller);
    try vault.setFee(bps) { assert(false); } catch { }   // must revert
}

No-reentrancy invariant — a guarded function cannot be re-entered (assert the guard slot is set during the external call).

Solvency — sum(balances) <= totalAssets holds after any single state transition.

Step 2 — Run Halmos

halmos --function check_transfer_preservesSupply --solver-timeout-assertion 0

Or via the runner MCP so it shares the Foundry build:

mcp__forge-runner__symbolic(tool="halmos", function="check_setFee_onlyOwner")

Step 3 — Interpret the result

• PASS = a proof. The property holds for every input within the explored bounds. State the bounds explicitly (e.g. "all uint256 amt, loop unrolled to 3").
• COUNTEREXAMPLE = a concrete input that violates the property → this is a finding. Minimize it and write a /exploit PoC.
• TIMEOUT / path explosion = inconclusive, not a pass. Narrow scope (bound array lengths, --loop unroll limit, constrain inputs with vm.assume) and re-run.