Detailed Instructions

Begin by examining all state variables and their intended relationships. For a token contract, a core invariant is that the total supply must equal the sum of all individual balances. For a lending protocol, the total borrowed assets cannot exceed the total supplied assets. Write these properties in plain language first. For each variable, ask: "What condition must always be true about this data?" This includes conditions that must hold before and after every transaction. Avoid specifying implementation details; focus on the abstract, logical rules of the system.

• Sub-step 1: List all public and private state variables (e.g., totalSupply, balances, totalBorrows).
• Sub-step 2: For each variable or group, articulate the fundamental rule it represents (e.g., "sum(balances) == totalSupply").
• Sub-step 3: Document any pre-conditions and post-conditions for public functions that affect these variables.

solidityCopy
// Example: Identifying a basic ERC-20 invariant
// Invariant: totalSupply == sum(balances[address]) for all addresses
uint256 public totalSupply;
mapping(address => uint256) public balances;

Tip: Use comments in your contract to informally document these properties as you identify them.

Detailed Instructions

Convert your plain-language invariants into formal specifications. Use Scribble annotations for inline specifications in Solidity or Certora Verification Language (CVL) for external rules. The key is to express the property as a logical assertion. For state invariants, use the if_updated or invariant keyword to specify a condition that must hold after any state change. For functional correctness, use if_succeeds to define post-conditions. Be precise with quantifiers; for a total supply invariant, you must assert it holds for all possible addresses in the balances mapping.

• Sub-step 1: Choose a specification framework compatible with your development stack (e.g., Scribble for Foundry).
• Sub-step 2: Write the invariant using the correct annotation syntax. For example: /// #if_succeeds old(totalSupply) == totalSupply.
• Sub-step 3: Use universal quantifiers (forall) where necessary to specify properties over all elements of a mapping or array.

solidityCopy
// Scribble annotation example for an ERC-20 invariant
/// #invariant {:msg "Total supply matches balances"} unchecked_sum(balances) == totalSupply;

Tip: Start with simple invariants before attempting complex ones involving quantifiers or ghost variables.

Detailed Instructions

Real-world invariants often depend on abstract state not directly stored. Ghost variables are specification-only variables that track this state, like the sum of all historical deposits. Function summaries specify the behavior of untrusted external calls or complex internal functions, limiting what they can change. For example, when a function calls an external token transfer, you might summarize it with /// #if_succeeds $result == true => balances[msg.sender] == old(balances[msg.sender]) - amount. This prevents the prover from assuming the external call can arbitrarily break your invariants.

• Sub-step 1: Identify hidden state (e.g., total ever minted) and declare a ghost variable to track it.
• Sub-step 2: Update the ghost variable in specifications at the points where the real state changes.
• Sub-step 3: For functions making external calls, write summaries that define the maximum possible effect on your contract's state.

solidityCopy
// Using a ghost variable to track total minted
/// #define ghost mapping(address => uint256) _totalMinted;
/// #invariant {:msg "Total supply equals total minted"} totalSupply == unchecked_sum(_totalMinted);
// In the mint function annotation:
/// #if_succeeds _totalMinted[to] == old(_totalMinted[to]) + amount;

Tip: Ghost variables are crucial for specifying invariants that involve historical data or complex aggregations.

Detailed Instructions

Run your specifications through tools like Certora Prover, SolCMC, or Foundry's invariant testing to validate them. This process will either prove the invariant holds under all conditions or provide a counterexample—a specific transaction sequence that breaks it. Analyze counterexamples carefully; they may reveal a bug in your contract, an error in your specification, or a need for additional constraints. For testing in Foundry, write an invariant test that uses the invariant keyword and a handler contract to randomly call functions, asserting your property after each run.

• Sub-step 1: Integrate the verification tool (e.g., Certora) into your build process or run Foundry tests with forge test --match-contract InvariantTest.
• Sub-step 2: Examine the first counterexample provided by the prover. Trace through the transaction steps.
• Sub-step 3: Determine if the counterexample represents a real bug, a spec over-approximation, or a missing precondition, and iterate.

solidityCopy
// Foundry invariant test example
contract InvariantToken is Test {
    MyToken token;
    function setUp() public { token = new MyToken(); }
    function invariant_totalSupplyBalances() public view {
        // ... logic to sum all tester balances and compare to totalSupply
        assertEq(total, token.totalSupply());
    }
}

Tip: A failing invariant test is a success for the discovery process—it has found a scenario you hadn't considered.

Detailed Instructions

Formal specification is an iterative process. Initial invariants are often too weak (allowing bad states) or too strong (broken by legitimate operations). Strengthen a weak invariant by adding more constraints—for example, not just totalSupply == sum(balances), but also totalSupply <= MAX_SUPPLY. If an invariant is too strong, add preconditions using require statements in the spec or refine the property's scope. This cycle may also lead to refactoring the contract itself to make correct behavior easier to specify and prove, such as adding checks or simplifying state transitions.

• Sub-step 1: Review verification reports for "rule not proved" or test failures. Categorize the cause.
• Sub-step 2: For weak invariants, add conjunctive clauses (using &&) to rule out the counterexample state.
• Sub-step 3: For overly strong invariants, introduce preconditions in the spec (e.g., /// #require old(balance) > 0) or modify the property to be conditional.

solidityCopy
// Refining an invariant by adding a constraint
/// #invariant {:msg "Stronger supply invariant"}
///     unchecked_sum(balances) == totalSupply && totalSupply <= cap;
// Adding a precondition to a function specification
/// #require amount <= balances[msg.sender];
/// #if_succeeds balances[msg.sender] == old(balances[msg.sender]) - amount;

Tip: The goal is a set of invariants that are strong enough to guarantee safety but are provably maintained by the actual code.

Detailed Instructions

Start by analyzing your protocol's logic to isolate its stateful invariants. These are properties that must remain true across all possible user interactions and state transitions. For a lending protocol, a key invariant is that the sum of all user deposits plus accrued interest must equal the total protocol assets, less any bad debt. For an AMM, a constant product invariant like x * y = k must be maintained after every swap. Write these down as clear, testable assertions. Avoid overly broad statements; focus on properties that, if violated, would indicate a critical bug or exploit vector. This step requires deep protocol understanding and is the foundation for all subsequent testing.

• Sub-step 1: Review all state variables and write down the logical relationships between them.
• Sub-step 2: Identify external dependencies (e.g., oracle prices) and define invariants that account for their potential failure.
• Sub-step 3: Formalize each invariant into a Solidity function that returns a boolean, such as function invariant_totalAssetsMatch() public view returns (bool).

Tip: Collaborate with protocol designers and auditors during this phase. A well-defined invariant is more valuable than dozens of poorly specified ones.

Detailed Instructions

Install Foundry and initialize a new project or integrate it into your existing one. The key tool is Forge's invariant testing command. Create a dedicated test contract that inherits from Test and StdInvariant. This contract will hold your invariant functions and define the actors (fuzzers) for the test. You must deploy your protocol's core contracts within the setUp() function and seed them with an initial state, such as minting test tokens and providing initial liquidity. Crucially, you need to exclude certain addresses (like the zero address or the test contract itself) from fuzzing using targetContract() and excludeSender(). This prevents the fuzzer from sending calls from addresses that would trivially break invariants in unrealistic ways.

• Sub-step 1: Run forge init or add Foundry via foundryup. Install via forge install foundry-rs/forge-std.
• Sub-step 2: Create Invariant.t.sol and structure it with setUp(), invariant_{name}() functions, and handler contracts.
• Sub-step 3: Configure foundry.toml with parameters like invariant.runs = 1000 and invariant.depth = 30 to define test intensity.

solidityCopy
// Example setUp() snippet
function setUp() public {
    deployProtocol();
    targetContract(address(myProtocol));
    excludeSender(address(0));
}

Tip: Start with a low number of runs (e.g., 100) for faster iteration, then increase for final validation.

Detailed Instructions

The fuzzer needs a way to interact with your protocol. Handler contracts act as a proxy, wrapping your protocol's external functions. Their purpose is to manage state and preconditions to make random calls meaningful. For example, a handler for a deposit function would first ensure the fuzzed caller has sufficient ERC-20 balance by minting tokens to them. It should also track internal state, like a mapping of user balances within the handler, to help with invariant validation later. You will need a handler for each major action (deposit, withdraw, swap, borrow, repay). In your test's setUp(), add the handler addresses as targets using targetSender(). This directs the fuzzer to call the protocol primarily through these handlers, generating complex, stateful sequences of operations.

• Sub-step 1: For each protocol action, create a public function in a handler contract that calls the real contract.
• Sub-step 2: Inside the handler, manage pre-conditions (e.g., mint tokens before a deposit) and log state changes.
• Sub-step 3: Add the handler contract addresses as target senders: targetSender(address(myDepositHandler)).

solidityCopy
// Example handler function
function deposit(uint256 amount) public {
    amount = bound(amount, 1, 1e30); // Bound fuzzed input
    token.mint(address(this), amount);
    token.approve(address(vault), amount);
    vault.deposit(amount, msg.sender);
    // Track deposited amount per user in a mapping
}

Tip: Use Foundry's bound() utility to constrain random inputs to realistic ranges and avoid overflow reverts.

Detailed Instructions

Run the tests with forge test --match-test invariant --ffi. When an invariant fails, Foundry provides a counterexample sequence—a list of calls that led to the broken state. Your job is to analyze this trace. First, determine if the failure reveals a genuine bug or a false positive. A false positive often occurs because an invariant was incorrectly specified or the handler allowed an unrealistic edge case. If it's a bug, you must fix the core contract logic. If it's a false positive, refine your invariant assertion or add constraints to your handler. The process is iterative: run tests, analyze failures, refine invariants/handlers, and repeat. Use forge inspect to get coverage reports and ensure your fuzz tests are exercising all code paths.

• Sub-step 1: Run the invariant test suite and note any failing properties.
• Sub-step 2: Examine the call sequence in the failure report. Reproduce it locally in a separate test.
• Sub-step 3: Classify the failure as a bug (fix contract) or specification error (refine test).

Tip: Save important counterexample sequences as standalone unit tests to ensure the bug remains fixed and to document the edge case.

Detailed Instructions

To prevent regressions, integrate invariant testing into your Continuous Integration (CI) pipeline. Configure your CI script (e.g., GitHub Actions, GitLab CI) to run forge test --match-test invariant on every pull request and main branch commit. Set failure thresholds; any broken invariant should block merging. For comprehensive coverage, consider running extended invariant tests with higher runs (e.g., 10,000+) on a nightly schedule. Furthermore, as the protocol evolves, you must maintain the invariant suite. When adding new features or modifying state variables, revisit your defined invariants. Add new ones for the new logic and verify existing ones still hold. Treat the invariant test suite as a living specification of the protocol's core correctness properties.

• Sub-step 1: Add a job in your .github/workflows/test.yml that runs Foundry invariant tests.
• Sub-step 2: Set up a scheduled workflow (cron job) for longer, more intensive fuzzing runs.
• Sub-step 3: Enforce a review process for updating handler contracts and invariant definitions when protocol code changes.

Tip: Use differential fuzzing by comparing your protocol's behavior against a simple, audited reference implementation to catch subtle discrepancies.