What is a conservation invariant in a smart contract?

A conservation invariant states that the total quantity of an asset within a contract is preserved across all operations, unless explicitly created (minted) or destroyed (burned) through authorized paths. For a token contract, this means the sum of all individual balances must equal the total supply at all times: sum(balance) == supply. If this invariant is violated, tokens can appear from nothing or disappear without authorization, which represents a critical security failure.

What are the most expensive smart contract invariant violations in history?

The Ronin bridge exploit ($600M, March 2022) resulted from an access control invariant violation where the attacker gained control of enough validator keys to authorize fraudulent withdrawals. The Wormhole bridge exploit ($326M, February 2022) was a conservation invariant violation where the attacker minted wrapped tokens without depositing corresponding assets. The Beanstalk exploit ($182M, April 2022) exploited a governance state machine invariant where flash-loaned voting power was used to pass a malicious proposal in a single transaction.

How does Formagine prove invariants at compile time?

Formagine proves invariants through algebraic verification. For each transition in a Form, the compiler computes the post-state of every variable referenced in the invariant and substitutes into the invariant expression. If the resulting expression can be reduced to the original invariant through arithmetic reasoning (cancellation, co-variance, bound propagation), the proof obligation is discharged. If not, compilation fails with a precise error identifying the invariant and transition that are incompatible. This process runs at compile time and covers all possible input values and state combinations.

Can invariants prevent reentrancy attacks?

Conservation invariants can detect and prevent the effects of reentrancy. If a contract's conservation invariant states that the sum of balances equals the total supply, and a reentrant call attempts to withdraw funds twice, the second withdrawal would violate conservation because the balance has already been decremented. In the Formagine model, transitions are atomic and the compiler verifies that each transition preserves invariants in isolation. Cross-contract reentrancy remains a systems-level concern that requires additional analysis beyond single-Form verification.

What Are Smart Contract Invariants and Why Do They Matter?

A smart contract invariant is a property that must hold in every reachable state of the contract. Invariants constrain how state variables relate to each other and define what it means for the contract to be correct. When an invariant is violated, the contract is in a state its designers considered impossible, which is precisely the condition that attackers exploit. The three critical invariant classes for smart contracts are conservation of funds, access control, and state machine correctness. Violations of these invariants have caused billions of dollars in losses across decentralized finance.

Conservation of Funds

A conservation invariant states that the total quantity of an asset within a contract is preserved across all operations unless explicitly created or destroyed through authorized paths. For a token contract, the canonical conservation invariant is sum(balance) == supply: the sum of all individual balances must equal the total supply at all times.

If conservation is violated, tokens can appear from nothing (inflation attack) or disappear without authorization (value destruction). Either case represents a critical security failure. Conservation invariants are the foundation of financial correctness in smart contracts.

invariant conservation :
  sum(balance) == supply

-- If this invariant holds for all transitions,
-- no operation can create or destroy value
-- outside of authorized mint/burn paths.

Access Control

Access control invariants restrict which addresses can invoke specific operations. A mint function should only be callable by the contract owner. A withdrawal should only be executable by the depositor. An upgrade should require multi-sig approval. When access control invariants fail, unauthorized parties can execute privileged operations, leading to unauthorized minting, fund theft, or contract takeover.

transition mint(to, amount) {
  require msg.sender == owner
  -- Access control: only the owner address
  -- can execute this transition
  balance[to] += amount
  supply      += amount
}

State Machine Correctness

Many contracts implement state machines where operations are only valid in certain states. An escrow contract might have states like Funded, Approved, and Released, where funds can only be released from the Approved state. A governance contract might require that proposals pass through Proposed, Voting, and Queued before reaching Executed. State machine invariants ensure that transitions only occur between valid states in the correct order.

Reentrancy Prevention

Reentrancy occurs when a contract makes an external call before updating its own state, allowing the called contract to re-enter and exploit the stale state. The classic invariant violation is that the balance mapping says an account has funds that have already been sent. Conservation invariants can detect and prevent the effects of reentrancy: if the invariant sum(balance) == supply holds and the contract enforces it atomically per transition, a reentrant withdrawal that would drain more than the balance would violate conservation and be rejected.

Real-World Invariant Violations

The following exploits demonstrate what happens when critical invariants are not enforced. Each one could have been prevented by proving the relevant invariant at compile time.

Ronin Bridge

$600M loss, March 2022. Access control violation.

The Ronin bridge required 5 of 9 validator signatures to authorize withdrawals. The attacker compromised 5 validator private keys, gaining the ability to sign fraudulent withdrawal transactions. The access control invariant (withdrawals require authorization from a quorum of independent validators) was violated because the validators were not truly independent. A compile-time proof that the access control set satisfies a minimum independence criterion would have flagged this structural weakness.

Wormhole Bridge

$326M loss, February 2022. Conservation violation.

The attacker exploited a signature verification bug to mint 120,000 wrapped Ether on Solana without depositing corresponding Ether on Ethereum. This is a direct conservation invariant violation: wrapped tokens were created without a corresponding lock of underlying tokens. A conservation invariant stating that total minted wrapped tokens must equal total locked underlying tokens, proven across all minting transitions, would have made this bug impossible.

Beanstalk

$182M loss, April 2022. State machine violation.

The attacker used a flash loan to acquire a supermajority of governance tokens, proposed a malicious governance action, voted on it, and executed it all within a single transaction. The governance state machine assumed that proposal, voting, and execution would occur across separate blocks with time for community review. The invariant (a proposal must survive a minimum waiting period before execution) was not enforced on-chain. A state machine invariant requiring that the proposal state transitions through a time-locked sequence would have prevented single-transaction governance attacks.

Proving Invariants at Compile Time

In the Form model, invariants are declared alongside state and transitions. The compiler performs algebraic verification: for each transition, it computes the effect on every variable in the invariant expression and checks whether the invariant is preserved. If every transition preserves every invariant, the contract is proven correct at compile time.

This is fundamentally different from runtime checking. A runtime check detects an invariant violation after it occurs and reverts the transaction. A compile-time proof demonstrates that the violation is impossible for any input, any state, any sequence of operations. The proven invariant is then erased from the output, producing a binary that is both provably correct and free of redundant runtime checks.

The practical consequence is that the class of bugs represented by the exploits above is eliminated at the language level. Not mitigated. Not made harder to exploit. Eliminated. If the invariant is declared and the code compiles, the invariant holds for all possible executions.

Frequently Asked Questions

What is a conservation invariant in a smart contract?: A conservation invariant states that the total quantity of an asset is preserved across all operations unless explicitly created or destroyed through authorized paths. For tokens: sum(balance) == supply. If violated, tokens can appear from nothing or disappear without authorization.
What are the most expensive invariant violations in history?: The Ronin bridge ($600M, access control violation), Wormhole bridge ($326M, conservation violation), and Beanstalk ($182M, governance state machine violation). Each exploited an invariant that was assumed but not proven.
How does Formagine prove invariants at compile time?: For each transition, the compiler computes the post-state of every invariant-referenced variable and checks whether the invariant expression is preserved through algebraic reasoning. If all transitions preserve all invariants, the proof is complete and the invariant annotations are erased from the WASM output.
Can invariants prevent reentrancy attacks?: Conservation invariants detect and prevent the effects of reentrancy. If conservation holds atomically per transition, a reentrant withdrawal violating it would be rejected. Cross-contract reentrancy remains a systems-level concern requiring additional analysis.

Form Templates

Token form (conservation proof) Vault form Escrow form (state machine proof) Governor form (access control proof)

Resources

All form templates API documentation Supported chains