Introducing Invariant Development as a Service

Understanding and rigorously testing system invariants are essential aspects of developing robust smart contracts. Invariants are facts about the protocol that should remain true no matter what happens. Defining and testing these invariants allows developers to prevent the introduction of bugs and make their code more robust in the long term. However, it is difficult to build up internal knowledge and processes to create and maintain such invariants. As a result, only the most matured teams have already integrated invariants into their development life cycle.

Recognizing this need, we are thrilled to announce our new service: Invariant Development. Clients of this service will receive:

Invariants, as code and specification
Guidance on how to integrate the invariants in their development lifecycle
Training on how to write invariants
Preferential treatment for additional Trail of Bits services

Comprehensive invariant development

Our invariant development service identifies, develops, and tests invariants for your codebase. While our security reviews typically encompass some development of invariants in areas believed to contain bugs, this service aims to cover invariants more broadly across your codebase, helping you achieve a more holistic approach to long-term security throughout your development lifecycle—not just at the end.

This service is particularly well suited for codebases that are still in development, as they will equip your engineers to write more secure contracts in the long term.

Trail of Bits engineers will lead discussions with your team to identify and understand the different invariants of the system. Our service includes the following activities:

Invariant identification. Based on our experience and discussion with the developers, we will identify potential invariants. This can include function-level invariants that must hold with respect to the execution of the function (e.g., addition is commutative) or system-level invariants (e.g., the balancer of a user cannot be greater than the total supply). We will specify the invariants in English and identify their pre-conditions (e.g., a parameter is within a given bound).
Invariant implementation. We will implement part of the identified invariants in Solidity. We will identify the best testing approach (internal, external, or partial testing), create the relevant wrappers, and set the fuzzing initialization (contract deployments and pre-conditions). We will aim to minimize disruption to the codebase, and will select the most appropriate approach to ensure that the invariants can be used in the long term.
Invariant testing and integration. We will run the invariants locally and on dedicated cloud infrastructure. We will refine the specification based on the fuzz run results, identify arithmetic bounds, and narrow the precondition to reflect realistic scenarios. We will work with the development team to integrate the fuzzing in the CI (e.g., through GitHub actions) for short-term fuzzing campaigns, and we will provide recommendations to run long-term fuzzing campaigns locally or in the cloud.
Training and guidance. Through this service, our engineers will aim to upskill your team, whom we will empower to write their own invariants and to make fuzzing an integral part of your development process. We will provide guidance and advice on how to maintain the provided invariants, and write new ones. Additionally, our experts will provide design recommendations tailored to optimize the codebase for fuzzing. Finally, we will invite the developers to co-write invariants with our engineers for immediate feedback.

In addition, customers that go through our invariant offering will receive preferential treatment for additional Trail of Bits services. For example, our engineers will leverage the knowledge gained during the invariant development to reduce the effort and cost needed for a security review.

Trail of Bits is uniquely positioned to offer this service. Our engineers have been writing invariants for more than half of a decade (for examples, see the Balancer, Primitive, and Liquity reports). We are the authors of multiple fuzzers (Echidna, Medusa, test-fuzz), and we are the authors of numerous educational materials on fuzzing (+150 pre-defined invariants, How to fuzz like a pro (conference workshop), 10-hour fuzzing workshop, fuzzing tutorials).

Enhance your security

Invariant-based development is set to become a standard for smart contract developers. Our new offering will allow you to do the following:

Become proactive instead of reactive in securing your codebase. Invariants prevent the introduction of bugs and address their root causes.
Identify and develop the most impactful invariants. Understanding which invariants will have an impact on security requires dedicated expertise, which our team will provide.
Educate the team on invariant-driven development. This reorients the development lifecycle toward bug prevention, and enables developers to integrate invariant reasoning into their development process.