The call for invariant-driven development
<p><em>By Josselin Feist</em></p>
<p>Writing smart contracts requires a higher level of security assurance than most other fields of software engineering. The industry has evolved from simple ERC20 tokens to complex, multi-component DeFi systems that leverage domain-specific algorithms and handle significant monetary value. This evolution has unlocked immense potential but has also introduced an escalating number of hacks.</p>
<p>We need a paradigm shift toward invariant-driven development to drive the industry toward a more secure future. By embedding invariants—key properties that must always hold—into every stage of the software development lifecycle, you can significantly enhance the robustness of your smart contracts.</p><div class="code-block code-block-12 ai-track" data-ai="WzEyLCIiLCJCbG9jayAxMiIsIiIsMV0=" style="margin: 8px 0; clear: both;">
<style>
.ai-rotate {position: relative;}
.ai-rotate-hidden {visibility: hidden;}
.ai-rotate-hidden-2 {position: absolute; top: 0; left: 0; width: 100%; height: 100%;}
.ai-list-data, .ai-ip-data, .ai-filter-check, .ai-fallback, .ai-list-block, .ai-list-block-ip, .ai-list-block-filter {visibility: hidden; position: absolute; width: 50%; height: 1px; top: -1000px; z-index: -9999; margin: 0px!important;}
.ai-list-data, .ai-ip-data, .ai-filter-check, .ai-fallback {min-width: 1px;}
</style>
<div class="ai-rotate ai-unprocessed ai-timed-rotation ai-12-1" data-info="WyIxMi0xIiwyXQ==" style="position: relative;">
<div class="ai-rotate-option" data-index="1" data-name="VGVjaHN0cm9uZyBHYW5nIFlvdXR1YmU=" data-time="MTA=" style="visibility: hidden;">
<div class="custom-ad">
<div style="margin: auto; text-align: center;"><a href="https://youtu.be/Fojn5NFwaw8" target="_blank"><img alt="Techstrong Gang Youtube" src="https://securityboulevard.com/wp-content/uploads/2024/12/Techstrong-Gang-Youtube-PodcastV2-770.png"/></a></div>
<div class="clear-custom-ad"></div>
</div></div>
<div class="ai-rotate-option" data-index="1" data-name="QVdTIEh1Yg==" data-time="MTA=" style="visibility: hidden; position: absolute; top: 0; left: 0; width: 100%; height: 100%;">
<div class="custom-ad">
<div style="margin: auto; text-align: center;"><a href="https://devops.com/builder-community-hub/?ref=in-article-ad-1&utm_source=do&utm_medium=referral&utm_campaign=in-article-ad-1" target="_blank"><img alt="AWS Hub" src="https://devops.com/wp-content/uploads/2024/10/Gradient-1.png"/></a></div>
<div class="clear-custom-ad"></div>
</div></div>
</div>
</div>
<p>In this blog post, we’ll explore what invariant-driven development means, why it’s essential, and how you can adopt this approach to elevate your security practices and build more robust smart contracts.</p>
<h2>What are invariants?</h2>
<p>At its core, invariant-driven development involves defining and maintaining invariants: statements about a program that must always hold, regardless of its state or execution path. These invariants act as the backbone of a system, ensuring its logical and functional integrity.</p><div class="code-block code-block-15" style="margin: 8px 0; clear: both;">
<script async="" crossorigin="anonymous" src="https://pagead2.googlesyndication.com/pagead/js/adsbygoogle.js?client=ca-pub-2091799172090865" type="1239ba93ff6a2803b1cf2704-text/javascript"></script>
<!-- SB In Article Ad 1 -->
<ins class="adsbygoogle" data-ad-client="ca-pub-2091799172090865" data-ad-format="auto" data-ad-slot="8723094367" data-full-width-responsive="true" style="display:block"></ins>
<script type="1239ba93ff6a2803b1cf2704-text/javascript">
(adsbygoogle = window.adsbygoogle || []).push({});
</script></div>
<p>In smart contracts, invariants can take many forms depending on the application. For example:</p>
<ul>
<li><strong>ERC20 supply:</strong> An ERC20 invariant is that a user’s balance must never exceed the token’s total supply.</li>
<li><strong>Automated market makers (AMMs):</strong> In a system using the <em>x * y = k</em> formula—like Uniswap—the formula acts as an invariant for the swaps, ensuring that this equation remains true after every trade (assuming no fee).</li>
<li><strong>Lending protocol:</strong> An invariant of the function computing interest earned over time is that it is an increasing monotonic function (e.g., the return value increases as time increases).</li>
</ul>
<p>Invariants can generally be categorized into two types:</p>
<ul>
<li><strong>Function-level invariants</strong> often focus on specific computations and typically don’t need to change the state (e.g., the <code>pure</code> or <code>view</code> function in Solidity). For example, the lending invariant described above (the function that computes interest is an increasing monotonic function) can be expressed through a function-level invariant.</li>
<li><strong>System-level invariants</strong> span the entire system’s state and transitions, such as ensuring that its assets are always greater than or equal to its liabilities. An example of a system-level invariant is ensuring no user has a token balance greater than the total supply.</li>
</ul>
<p>If you are familiar with fuzzing or formal verification, you are already familiar with invariants. Yet, as the next section shows, invariants are not limited to these techniques; you can also use them in the context of:</p>
<ul>
<li><strong>Monitoring</strong>, through external tools, watching for transactions that break invariants</li>
<li><strong>On-chain invariants</strong>, which are executed directly within the smart contract and act as post-conditions when users interact with the contract</li>
<li><strong>Manual reviews</strong>, where the code review focuses on verifying key invariants</li>
</ul>
<p>If you want to learn more about developing invariants in the context of fuzzing, see see <a href="https://secure-contracts.com/program-analysis/echidna/index.html" rel="noopener">the fuzzing page</a> on our Building Secure Contracts website and our <a href="https://www.youtube.com/watch?v=QofNQxW_K08&list=PLciHOL_J7Iwqdja9UH4ZzE8dP1IxtsBXI" rel="noopener">fuzzing workshop</a>.</p>
<p>Security researchers have used invariants to assess contracts for many years; our <a href="https://github.com/trailofbits/publications/blob/master/reviews/basis.pdf" rel="noopener">public reports</a> include invariants that are over six years old, and their usage has been crucial in most of our security reviews. Nowadays, many of our competitors follow our approach, highlighting its efficiency. However, software engineers still barely use invariants despite their success in the security community. This is what we hope will change in the upcoming years.</p>
<p>Invariants are not a one-time consideration—they should guide every step of your smart contracts’ development. Here’s how you can apply them at every step of the process.</p>
<h3>Design the invariants</h3>
<p>The earlier you start thinking about and documenting invariants, the more significant their impact on your project. Start by identifying invariants during the initial design of the protocol before any code is written. Ask the following questions:</p>
<ul>
<li><strong>What are the main invariants?</strong> Ask your team to identify the 10 most essential invariants so they can keep them in mind at every stage of the project’s development. If they can’t answer, then dedicate more time to identifying them.</li>
<li><strong>How will these invariants be checked?</strong> How invariants are checked will influence the code’s design. For example, invariants that will be monitored require the emission of relevant events, and invariants that will be run on-chain can benefit from specific code isolation.</li>
<li><strong>How will these invariants be specified and kept in sync with the code?</strong> Chances are that your specification will evolve as your code and project’s requirements change. Having a process to ensure that they remain in sync will be crucial for the long-term success of the protocol.</li>
</ul>
<p>This phase requires no special tools—just basic note-taking and documentation. Use this schema as a baseline:</p>
<table>
<tr>
<th>ID</th>
<th>Invariant</th>
<th>Components</th>
<th>Testing strategy</th>
</tr>
<tr>
<td> </td>
<td><English description></td>
<td><contracts/functions involved></td>
<td><fuzzing, formal verification, unit test, manual review></td>
</tr>
</table>
<p>The English description can be as simple as how you describe it verbally. However, a good practice for complex invariants is to describe them through a Hoare Triple-like format (pre-condition, command, post-condition). Despite the formal-sounding name, a Hoare Triple simply captures three key elements:</p>
<ul>
<li>Pre-condition: Assumptions about the state/parameters before the actions</li>
<li>Command: The actions to be tested</li>
<li>Post-condition: What must be true after the actions</li>
</ul>
<p>Conceptually, this is the same as following an <a href="https://xp123.com/3a-arrange-act-assert/">Arrange, Act, Assert</a> or <a href="https://en.wikipedia.org/wiki/Given-When-Then">Given, When, Then</a> design pattern if you’re familiar with them.</p>
<p>For example, the <em>x * y = k</em> invariant may be expressed following this schema; see ToB1:</p>
<table>
<tr>
<th>ID</th>
<th>Invariants</th>
<th>Components</th>
<th>Testing Strategy</th>
</tr>
<tr>
<td>ToB0</td>
<td>The balance of any user must never exceed the total supply of the token</td>
<td><code>MyToken</code></td>
<td>Fuzzing</td>
</tr>
<tr>
<td>ToB1</td>
<td>
<ul>
<li>If the pool has no fee (<em>pre-condition</em>)</li>
<li>Call the swap function (<em>command</em>)</li>
<li><em>x * y = k</em> has not changed (<em>post-condition</em>)</li>
</ul>
</td>
<td><code>MyAMM</code></td>
<td>Fuzzing</td>
</tr>
<tr>
<td>ToB2</td>
<td>The function computing the interest earned over time is an increasing monotonic function</td>
<td><code>Lending.compute_interest</code></td>
<td>Formal verification</td>
</tr>
</table>
<p class="wp-caption-text">Figure 1: Examples of invariants</p>
<p>If you’re looking for inspiration on creating invariants, you can find a set of predefined invariants in our <a href="https://github.com/crytic/properties">properties</a> repo.</p>
<h3>Implement and test the invariants</h3>
<p>The longest part of the smart contract development lifecycle is development and testing. Here, an iterative process between developing the code, creating and updating the invariant, and general testing will be crucial.</p>
<p>For example, identifying functions-level invariants will help you design the right level of modularity for your codebase, separating the components in a way that makes them easier to test.</p>
<p>During this phase, the tools at your disposal are:</p>
<ul>
<li>Fuzzers (e.g., <a href="https://github.com/crytic/medusa">Medusa</a>, <a href="https://github.com/crytic/echidna">Echidna</a>, and <a href="https://github.com/foundry-rs/foundry">Foundry</a>)</li>
<li>Formal verification tools (e.g., <a href="https://github.com/a16z/halmos">Halmos</a>, <a href="https://www.certora.com/">Certora</a>, and <a href="https://github.com/runtimeverification/evm-semantics">KEVM</a>)</li>
<li>Manual review</li>
</ul>
<p>The invariants can typically be written in Solidity (as shown below) or in a domain-specific language like <a href="https://docs.certora.com/en/latest/docs/cvl/index.html">CVL</a> for the Certora Prover.</p>
<pre style="margin-bottom: 5px;">
<span style="color:#6C737C">// User balance must not exceed the total supply</span>
<span style="color:#C6474E">function</span> test_ERC20_userBalanceNotHigherThanSupply() <span style="color:#C6474E">public</span> {
assertLte(
balanceOf(<span style="color:#C6474E">msg.sender</span>),
totalSupply(),
<span style="color:#112E5F">"User balance higher than total supply"</span>
);
}
</pre>
<p class="wp-caption-text">Figure 2: ToB0: The balance of any user must never exceed the total supply of the token (<a href="https://github.com/crytic/properties/blob/9b91ad9569cb3064b7e4b252a266c2ee1d8e9c7f/contracts/ERC20/internal/properties/ERC20BasicProperties.sol#L18-L25">properties/ERC20BasicProperties.sol#L18-L25</a>)</p>
<p>As your codebase evolves after deployment, continue testing the invariants on every code change/PRs. <a href="https://github.com/crytic/cloudexec">CloudExec</a> will help you run your fuzzer continuously in the cloud, while <a href="https://github.com/crytic/fuzz-utils">fuzz-utils</a> will convert the fuzzing findings into Foundry unit tests.</p>
<p>The choice of tool will depend on the invariant and the codebase; see <a href="https://blog.trailofbits.com/2024/03/22/why-fuzzing-over-formal-verification/">our blog post describing when to fuzz versus using formal verification</a>. If some invariants are straightforward enough—or the opposite, too complex to test with tooling—thorough documentation and unit testing will be crucial.</p>
<h4>On-chain invariants</h4>
<p>Some invariants can be part of the on-chain code. These invariants can act as post-conditions of the contract’s execution. Uniswap’s <em>x * y = k</em> is an example of such an invariant. On-chain invariants are a powerful tool: they provide strong guarantees and are very effective at preventing hacks.</p>
<p>However, making every invariant part of the on-chain code may not be possible. Some invariants require complex computation (e.g., unbounded loop iteration), which increases the gas cost or the risks of bugs in the invariants themselves. One example of a broken invariant is an issue (TOB-UNI-005) in our <a href="https://github.com/trailofbits/publications/blob/master/reviews/UniswapV3Core.pdf">Uniswap V3 report</a> that could have allowed a malicious user to drain any Uniswap pool. This issue highlights that on-chain invariants are a double-edged sword, carrying unique benefits and risks. That’s why it’s crucial to identify potential on-chain invariants during the design phase to determine which ones will fit the contracts’ code and apply special care to them.</p>
<h3>Validate the invariants</h3>
<p>Having the list of invariants ready for third-party or internal code evaluation (security review, bug contest, or bug bounties) will help security engineers understand the system’s critical parts and focus on the most significant risks. This is an example of where invariant-driven development shines: you can onboard security engineers on your codebase more quickly and better understand code review coverage.<br/>
During this phase, you will have the same tools as during the implementation: fuzzers, formal verification tools, and manual review. An example of this approach is our <a href="https://github.com/trailofbits/publications/blob/master/reviews/2024-07-uniswap-v4-core-securityreview.pdf">Uniswap V4</a> report, where we tested 100 invariants through automated techniques (fuzzing, formal methods, and custom static analysis). Each technique was tailored for the right invariant:</p>
<div class="wp-caption aligncenter" id="attachment_108967" style="width: 700px"><img alt="" aria-describedby="caption-attachment-108967" class="size-full wp-image-108967" data-attachment-id="108967" data-comments-opened="1" data-image-caption="<p>Figure 3: Automated Testing section of our Uniswap V4 report</p>
" data-image-description="" data-image-meta='{"aperture":"0","credit":"","camera":"","caption":"","created_timestamp":"0","copyright":"","focal_length":"0","iso":"0","shutter_speed":"0","title":"","orientation":"0"}' data-image-title="invariant-post-1" data-large-file="https://blog.trailofbits.com/wp-content/uploads/2025/02/invariant-post-1.png" data-medium-file="https://blog.trailofbits.com/wp-content/uploads/2025/02/invariant-post-1-300x238.png" data-orig-file="https://blog.trailofbits.com/wp-content/uploads/2025/02/invariant-post-1.png" data-orig-size="936,744" data-permalink="https://blog.trailofbits.com/2025/02/12/the-call-for-invariant-driven-development/invariant-post-1/" decoding="async" fetchpriority="high" height="744" sizes="(max-width: 936px) 100vw, 936px" src="https://blog.trailofbits.com/wp-content/uploads/2025/02/invariant-post-1.png" srcset="https://blog.trailofbits.com/wp-content/uploads/2025/02/invariant-post-1.png 936w, https://blog.trailofbits.com/wp-content/uploads/2025/02/invariant-post-1-300x238.png 300w, https://blog.trailofbits.com/wp-content/uploads/2025/02/invariant-post-1-768x610.png 768w" width="936"/>
<p class="wp-caption-text" id="caption-attachment-108967">Figure 3: Automated Testing section of our <a href="https://github.com/trailofbits/publications/blob/master/reviews/2024-07-uniswap-v4-core-securityreview.pdf">Uniswap V4 report</a></p>
</div>
<p>For insights into how we created the fuzzing harness for this project, watch our presentation on how we designed invariants for Uniswap V4 next week. The date and time will be announced on X.</p>
<h3>Monitor the invariants</h3>
<p>It can be challenging to know which aspects of a system are crucial to monitor. This is another area where the invariant-driven development approach shines: the invariants indicate these aspects.</p>
<p>Solutions like <a href="https://www.hexagate.com/">Hexagate</a> and <a href="https://tenderly.co/">Tenderly</a> let you monitor invariants through events and transaction analysis (note that the invariants must be adapted to follow the tools’ custom APIs). You can also leverage on-chain fuzzers (including <a href="https://blog.trailofbits.com/2023/07/21/fuzzing-on-chain-contracts-with-echidna/">Echidna</a> and <a href="https://github.com/crytic/medusa/pull/513">Medusa</a>) to continuously stress-test the invariants written in Solidity with actual values.</p>
<p>Here, invariants must be part of your incident response strategy. For each invariant to be monitored, you must define the following:</p>
<ul>
<li>How to interpret and debug why the invariant is broken</li>
<li>Who in your organization has the proper knowledge</li>
<li>What actions are at your disposal (e.g., pausing the system, changing a parameter, upgrading the contracts)</li>
</ul>
<p>Follow our <a href="https://secure-contracts.com/development-guidelines/incident_response.html#incident-response-recommendations">Incident Response Recommendations</a> to plan accordingly, and consider validating your process by hosting a <a href="https://github.com/security-alliance/drill-template">SEAL wargame</a> to simulate a security incident triggered by a broken invariant.</p>
<h2>Why invariant-driven development is powerful</h2>
<p>Most smart contract hacks involve a business logic or domain-specific issue. Developers should safeguard against these issues, and invariant-driven development aims to solve them.</p>
<p>By integrating invariants through the entire development process, you will:</p>
<ul>
<li>Immediately detect bugs</li>
<li>Clarify your protocol’s core assumptions</li>
<li>Reduce the attack surface</li>
<li>Streamline code review and monitoring</li>
</ul>
<p>Ultimately, you will shift your mindset to focus on security as a priority.<br/>
Invariant-driven development is not just a technique—it’s a development mindset. It’s about integrating a security approach through development and driving the design’s decision to reduce risks. We hope to see several teams adopt this approach moving forward. If you need help identifying and testing your invariants, <a href="https://www.trailofbits.com/contact/">contact us</a>.</p>
<div class="spu-placeholder" style="display:none"></div>
<p class="syndicated-attribution">*** This is a Security Bloggers Network syndicated blog from <a href="https://blog.trailofbits.com">Trail of Bits Blog</a> authored by <a href="https://securityboulevard.com/author/0/" title="Read other posts by Trail of Bits">Trail of Bits</a>. Read the original post at: <a href="https://blog.trailofbits.com/2025/02/12/the-call-for-invariant-driven-development/">https://blog.trailofbits.com/2025/02/12/the-call-for-invariant-driven-development/</a> </p><!-- CONTENT END 1 -->
