Formal Verification of Governance Timelocks & Multisigs

Governance mechanisms control protocol parameters and treasury assets. Logical flaws in timelocks or multisig validation rules can lead to protocol takeovers.

1. What is Formal Verification?

Formal verification mathematically proves that a smart contract behaves according to a formal specification. Unlike fuzzing, which tests millions of random inputs, formal verification evaluates all possible state transitions.

2. Formally Specifying a Timelock in CVL

Certora Verification Language (CVL) is used to specify invariants. Below is a CVL specification that verifies proposal state boundaries in a timelock.

Rule: Proposals cannot be executed before the timelock expiration

// CVL specification
rule proposalTimelockExecution {
    env e;
    method f;
    calldataarg args;
    uint256 proposalId;

    // Pre-condition: Proposal is queued and timelock has not expired
    require getProposalState(proposalId) == ProposalState.Queued;
    require e.block.timestamp < getProposalExecutionTime(proposalId);

    // Call any state-modifying function
    invoke f(e, args);

    // Post-condition: The state of the proposal cannot be Executed
    assert getProposalState(proposalId) != ProposalState.Executed, 
        "Proposal executed before timelock expired";
}

3. Common Vulnerability Categories

Our formal verification sweeps identify several common failure categories in multisigs and timelocks:

A. Reentrancy in Queue Operations

If the proposal execution logic triggers callbacks prior to changing proposal states, an attacker can reenter and execute the same proposal multiple times.

B. Chain ID Replay Vulnerabilities

Multi-signature verification logic that omits the block.chainid parameter can be replayed on fork networks or alternative chains:

// Vulnerable verification
function verifySignature(bytes32 txHash, bytes memory signature) public view returns (bool) {
    // VULNERABILITY: txHash does not include block.chainid or nonce
    address signer = recoverSigner(txHash, signature);
    return isOwner[signer];
}

C. Constructor Initialization Overrides

Constructor functions that fail to lock initializers can allow an attacker to hijack the contract post-deployment by calling initializations directly.

D. Threshold Drift

A multisig can become unsafe if owner removal changes the denominator without revalidating the threshold. For example, a 3-of-5 wallet that removes two owners but leaves the threshold at 3 becomes permanently unable to execute. The opposite failure is worse: lowering the threshold before owner changes are finalized can briefly create a 1-of-N authorization window.

function removeOwner(address owner) external onlyWallet {
    isOwner[owner] = false;
    ownerCount -= 1;
    require(threshold <= ownerCount, "threshold exceeds owners");
    require(threshold >= MIN_THRESHOLD, "threshold too low");
}

E. Operation Hash Ambiguity

Governance systems commonly identify queued operations by hashing target, value, calldata, predecessor, and salt. If any field is omitted, two different operations can collide into the same queue slot. Formal specs should prove operation identity is injective over the fields the protocol claims to bind.

rule operationHashBindsTargetAndData {
    address target1; address target2;
    bytes data1; bytes data2;
    uint256 value;
    bytes32 predecessor; bytes32 salt;

    require target1 != target2 || keccak256(data1) != keccak256(data2);

    bytes32 h1 = hashOperation(target1, value, data1, predecessor, salt);
    bytes32 h2 = hashOperation(target2, value, data2, predecessor, salt);

    assert h1 != h2, "operation hash does not bind target/data";
}

4. Specification Design for Governance

A useful formal verification campaign separates safety, liveness, and authority properties:

Safety properties are usually easiest to prove. Liveness properties require more care because solvers must reason about the existence of a valid path, not only the absence of an invalid one. In practice, we combine formal rules with bounded model tests for liveness-critical flows.

5. Modeling Signatures Correctly

Signature verification is the most common source of false confidence. A spec that treats isValidSignature() as a trusted oracle will miss replay and domain-separation failures. The model should include:

• The EIP-712 domain separator, including chainId and verifying contract.
• A nonce or operation ID that is consumed exactly once.
• Strict signer uniqueness, so one signer cannot submit duplicate signatures to meet threshold.
• Sorted signature assumptions, if the implementation depends on ordering.
• Contract-wallet signatures through EIP-1271, including failure and revert paths.

rule signerCannotCountTwice {
    env e;
    bytes32 op;
    address signer;

    require isOwner(signer);
    require signatureCount(op, signer) == 1;

    submitSignature(e, op, signer);

    assert signatureCount(op, signer) == 1,
        "duplicate signer increased approval weight";
}

6. Timelock State Machine

Every operation should move through a single monotonic path:

Unset -> Waiting -> Ready -> Done

Cancellation is the only valid side branch, and canceled operations must not become ready unless they are explicitly requeued with a fresh salt or nonce. The important invariant is monotonicity: no external call, upgrade, or role change should move Done or Canceled back into an executable state.

7. Verification Workflow

1. Freeze the governance threat model: assets controlled, roles, quorum, delay, emergency powers.
2. Write a state-machine diagram before writing specs.
3. Add invariants for early execution, replay, duplicate signers, threshold bounds, and operation hash binding.
4. Model malicious target contracts that reenter during execution.
5. Run the same specs against upgradeable proxy deployments and initialized implementation contracts.
6. Pair solver results with fuzzing for gas-limit and calldata-shape edge cases.

8. Auditor Checklist

• Operation hashes bind target, value, calldata, predecessor, salt, and chain context.
• Nonces or operation IDs are consumed once and cannot be replayed cross-chain.
• Duplicate signatures cannot increase approval weight.
• Threshold cannot exceed owner count or fall below the documented security floor.
• Queue, cancel, and execute state transitions are monotonic.
• External calls during execution cannot reenter queue or execution paths.
• Proxy upgrades and role changes are themselves governed by the timelock.

9. Conclusion

Governance verification is high leverage because a single timelock or multisig bug can dominate every other protocol control. The practical goal is not to prove that governance is benevolent; it is to prove that even valid administrators must pass through the exact delay, quorum, replay, and upgrade rules users were promised.