Quick tips to start your next invariant test campaign

This post is a written version of the Invariant Testing Workshop presentation given at OpenSense. It aims to share tips and best practices for invariant testing.

1. Define Invariants from Documentation

A crucial step in fuzz testing is defining your invariants, the properties that should consistently hold in your system. An effective method to identify these invariants is to start from your project's white paper or documentation.

For instance, Pods Finance's "stETH Volatility Vault" strategy implies that a user's initial deposit amount should always be retrievable, regardless of other activities within the vault. Similarly, their strategy of using staked earnings to purchase options translates to another invariant: the yield should be the only aspect utilized for external strategies, ensuring the principal remains protected.

2. Write Your Properties in Plain English

Summarizing these properties in plain English before translating them to code is always beneficial. This practice helps maintain clarity and facilitates communication across different teams, especially between those with varying levels of technical knowledge. You can do it in a simple PROPERTIES.md file or a Notion database.

3. Categore Your Properties

Certora's tutorials on GitHub offers an excellent framework for categorizing properties and expanding the scope of your invariants. They propose categories like "valid states," "state transitions," and "variable transitions," among others. This categorization aids in identifying potential gaps in your properties and ensures comprehensive coverage.

4. Prioritize Your Invariants

When it comes to prioritization, it's best to start with high-level properties. These overarching principles apply to the entire system from a user's perspective. For example, a banking system should ensure that total balances remain constant, preventing issues like double spending or asset creation from thin air.

A good strategy can be to start with the "easier to implement" and "most impactful" first. This way you can already have some good confidence in important invariants right from the beginning and expand on more specific or more complex properties later.

5. Writing Solidity Code for Invariants

Following Trail of Bits' fuzzing series on YouTube, a recommended approach is to structure your code with preconditions, actions, and postconditions. This format enhances clarity, and maintainability, and reveals the necessary comparisons between states before and after certain actions.

Conclusion

This article offered a quick guide on fuzz testing, emphasizing the importance of defining, categorizing, and prioritizing invariants, along with practical tips for writing effective Solidity code. For any further questions of invariant testing guidelines, please feel free to reach out.