​
Introduction

The Credible Layer is a security prevention framework that helps protect smart contracts by continuously verifying critical protocol invariants. This guide assumes that you have already installed the Credible Layer. If you haven’t, please see the Credible Layer Quickstart for instructions. For a visual learners a video introduction to assertions is available: We will use a simple ownership protocol as an example that demonstrates how to protect against unauthorized ownership transfers - a critical security concern in smart contracts. 
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.13;

// Do not use this in production, it is just an example!!!
contract Ownable {
    address private _owner;

    event OwnershipTransferred(address indexed previousOwner, address indexed newOwner);

    constructor() {
        _owner = address(0xdead);
        emit OwnershipTransferred(address(0), _owner);
    }

    modifier onlyOwner() {
        require(_owner == msg.sender, "Ownable: caller is not the owner");
        _;
    }

    // Get the current owner
    function owner() public view returns (address) {
        return _owner;
    }

    // Transfer ownership to a new address
    // Can only be called by the current owner
    function transferOwnership(address newOwner) public onlyOwner {
        require(newOwner != address(0), "Ownable: new owner is the zero address");
        emit OwnershipTransferred(_owner, newOwner);
        _owner = newOwner;
    }
}
In the above code, we have a simple contract that manages ownership transfers. While ownership transfer functionality is common in protocols, it should be carefully controlled since unauthorized changes can be catastrophic. For example, in 2024, Radiant Capital lost $50M when an attacker gained access to their multisig and changed the protocol owner. To prevent such incidents, we can write an assertion that guards ownership changes. The assertion will block transactions if ownership changes unexpectedly, though it can be temporarily paused when legitimate ownership transfers are planned. Our assertion will verify that the contract owner remains unchanged after each transaction.

​
1. Setting Up Your Project

For detailed instructions on setting up your Credible Layer project structure, please refer to the Credible Layer Quickstart Guide. Alternatively, you can quickly get started by cloning the Credible Layer starter repository: 
git clone --recurse-submodules https://github.com/phylaxsystems/credible-layer-starter 
cd credible-layer-starter
This repository includes the necessary file structure, dependencies, and configuration for writing and testing assertions.

​
2. Writing the Assertion

Let’s create our assertion in OwnableAssertion.a.sol. Here’s the complete code first, followed by a detailed breakdown: 
// SPDX-License-Identifier: MIT
pragma solidity ^0.8.13;

import {Assertion} from "credible-std/Assertion.sol";
import {Ownable} from "../../src/Ownable.sol"; // Ownable contract

contract OwnableAssertion is Assertion {
    // The triggers function tells the Credible Layer which assertion functions to run
    // This is required by the Assertion interface
    function triggers() external view override {
        // Register our assertion function to be called when transferOwnership is called
        registerCallTrigger(this.assertionOwnershipChange.selector, Ownable.transferOwnership.selector);
    }

    // This assertion checks if ownership has changed between pre and post transaction states
    function assertionOwnershipChange() external {
        // Get the adopter contract address using the cheatcode
        // This can be done instead of using the constructor and
        // is less error prone while storing and submitting the assertion
        Ownable ownable = Ownable(ph.getAssertionAdopter());

        // Create a snapshot of the blockchain state before the transaction
        ph.forkPreTx();

        // Get the owner before the transaction
        address preOwner = ownable.owner();

        // Create a snapshot of the blockchain state after the transaction
        ph.forkPostTx();

        // Get the owner after the transaction
        address postOwner = ownable.owner();

        // Assert that the owner hasn't changed
        // If this requirement fails, the assertion will revert
        require(postOwner == preOwner, "Ownership has changed");
    }
}

​
How Assertions Work

The key principle of assertions is simple: if an assertion reverts, it means the assertion failed and an undesired state was detected. In our case, the assertion will revert if the contract’s owner changes, allowing us to prevent unauthorized ownership transfers. If an assertion reverts, the transaction resulting in the undesired state is reverted and not included in the block. This results in actual hack prevention, not just mitigation.

​
Gas Consumption

Assertion functions are limited to a maximum execution of 100,000 gas. If an assertion function exceeds this gas limit, the transaction will be invalidated and dropped. Please be aware that the gas consumption of certain cheatcodes, such as getCallInputs, can be variable, due to unknown lengths of the call inputs. We are actively working to improve this as soon as possible. Staying mindful of gas consumption is in general a good practice. See the Assertion Patterns for more details on ways to optimize gas consumption.

​
Anatomy of the Assertion

Let’s break down the key components of our assertion:

​
1. Imports and Contract Definition

import {Assertion} from "credible-std/Assertion.sol";
import {Ownable} from "../../src/Ownable.sol";

contract OwnableAssertion is Assertion {
  • The contract inherits from Assertion, which provides the base functionality and cheatcodes for assertions
  • We import the contract we want to protect (Ownable)

​
2. State Variables and Constructor

// Optional constructor
constructor() {}
  • If you are defining state variables for additional contracts your assertion should know about this can be done in the constructor.
  • The constructor is optional and can be initialized during the storing and submitting of the assertion through the pcl.
  • In this example we entirely leave out the constructor, since we use the ph.getAssertionAdopter() cheatcode to get the address of the contract we want to protect.
  • The constructor runs against an empty state. This means you can pass values in the constructor but you can not read values from other contracts.
  • Storage that is set in the constructor persists in the assertion contract.
  • Cheatcodes/precompiles are not accessible in the constructor.

​
3. Triggering Assertions

// The triggers function tells the Credible Layer which assertion functions to run and when to run them
// This is required by the Assertion interface
function triggers() external view override {
    // Register our assertion function to be called when transferOwnership is called
    registerCallTrigger(this.assertionOwnershipChange.selector, Ownable.transferOwnership.selector);
}
  • The triggers function is required by the Assertion interface.
  • Each assertion function must be registered here via its function selector.
  • Multiple assertions can be defined in a single contract.
  • registerCallTrigger specifies the function selector of the assertion function to run and the function selector of the protected contract function that should trigger the assertion.
  • A trigger can only trigger one assertion function.
  • Use triggers to make sure that assertions are only called when they are needed in order to save gas and resources.
  • The Credible Layer supports different trigger types. See the “Triggers” section in the cheatcodes documentation for more information.

​
4. Assertion Logic

// This assertion checks if ownership has changed between pre and post transaction states
function assertionOwnershipChange() external {
    // Get the adopter contract address using the cheatcode
    // This can be done instead of using the constructor and
    // is less error prone while storing and submitting the assertion
    Ownable ownable = Ownable(ph.getAssertionAdopter());

    // Create a snapshot of the blockchain state before the transaction
    ph.forkPreTx();

    // Get the owner before the transaction
    address preOwner = ownable.owner();

    // Create a snapshot of the blockchain state after the transaction
    ph.forkPostTx();

    // Get the owner after the transaction
    address postOwner = ownable.owner();

    // Assert that the owner hasn't changed
    // If this requirement fails, the assertion will revert
    require(postOwner == preOwner, "Ownership has changed");
}
  • The main assertion logic uses cheatcodes:
    • ph.forkPreTx(): Creates a snapshot of the blockchain state before the transaction.
    • ph.forkPostTx(): Creates a snapshot of the blockchain state after the transaction.
  • The assertion reverts if the condition is not met. You can have several require checks in the same function to make sure no rules are violated.
  • The ph namespace gives access to the Credible Layer cheatcodes, which provide utility functions for assertions. For more information see the cheatcodes documentation.
  • All assertion functions must be public or external to be callable by the Credible Layer.

​
Best Practices for Writing Assertions

  1. Single Responsibility: Each assertion should verify one specific property or invariant.
    • Sometimes it makes sense to check multiple properties in the same assertion function.
    • Aim to have as many specific assertion functions as possible, since the Credible Layer executes assertions in parallel.
  2. State Management: Use forkPreTx() and forkPostTx() to compare values before and after transactions.
  3. State Management: Use forkPreCall() and forkPostCall() to compare values before and after specific calls.
  4. Gas Optimization: Use triggers to make sure that assertions are only called when they are needed in order to save gas and resources.
  5. Return Early: When writing more complex assertions checking multiple function calls in the callstack, it is recommended to check basic invariants first before starting to iterate over the callstack.
  6. Debugging: Use console.log() in assertion functions to print debug information to the console during testing with pcl test.

​
3. Testing the Assertion

Testing assertions is a critical step in developing effective security prevention. Since assertions act as automated guardians for your protocol, it’s essential to verify they correctly identify both safe and unsafe conditions. A false positive could unnecessarily block legitimate protocol operations, while a false negative could miss critical security violations. To run the tests, use the following command: 
pcl test
Good assertion tests should:
  • Verify that assertions fail when they should (e.g., when detecting unauthorized changes)
  • Confirm that assertions pass during normal operation
  • Simulate realistic protocol interactions as well as edge cases
Let’s break down how to test our assertion:

​
Test Imports

import {OwnableAssertion} from "../src/OwnableAssertion.a.sol";
import {Ownable} from "../../src/Ownable.sol";
import {CredibleTest} from "credible-std/CredibleTest.sol";
import {Test} from "forge-std/Test.sol";
Let’s examine each import:
  • OwnableAssertion: Imports the assertion we created that we want to test
  • Ownable: Imports the protocol contract that our assertion is protecting
  • CredibleTest: Provides special testing utilities for assertion testing, including the cl cheatcode interface
  • Test: Standard testing base contract from Forge, providing utilities like vm.prank and vm.expectRevert
These imports provide all the necessary components to test our assertion effectively, including access to both the assertion logic and the protocol being protected.

​
Test Contract Structure

contract TestOwnableAssertion is CredibleTest, Test {
    // Contract state variables
    Ownable public assertionAdopter;
    address public initialOwner = address(0xf00);
    address public newOwner = address(0xdeadbeef);
  • Inherits from CredibleTest and Test which provides testing utilities
  • CredibleTest provides the cl cheatcode interface for testing assertions
  • Test is the standard Forge test base contract
  • assertionAdopter is the contract we’re protecting
  • newOwner is used to test ownership transfers
  • initialOwner is the owner of the contract before the tests are run

​
Setup

// Set up the test environment
function setUp() public {
    assertionAdopter = new Ownable(initialOwner);
    vm.deal(initialOwner, 1 ether);
}
  • Creates a new instance of the Ownable contract for testing
  • Gives the owner some ETH using Forge’s vm.deal
  • This setup runs before each test function

​
Testing Assertion Reverted

This test checks that the assertion reverts when ownership changes. 
// Test case: Ownership changes should trigger the assertion
function test_assertionOwnershipChanged() public {
    assertEq(assertionAdopter.owner(), initialOwner);

    cl.assertion({
        adopter: address(assertionAdopter),
        createData: type(OwnableAssertion).creationCode,
        fnSelector: OwnableAssertion.assertionOwnershipChange.selector
    });

    // Simulate a transaction that changes ownership
    vm.prank(initialOwner);
    vm.expectRevert("Ownership has changed");
    assertionAdopter.transferOwnership(newOwner);

    // Check that owner didn't change
    assertEq(assertionAdopter.owner(), initialOwner);
}
Key components:
  1. cl.assertion(): Sets up the assertion to be run on the next transaction
    • adopter: Address of contract to protect
    • createData: Bytecode of the assertion contract
    • fnSelector: Selector of the assertion function to run
  2. vm.prank(): Simulates a call from the owner’s address
  3. vm.expectRevert(): Explicitly expects the assertion to revert with “Ownership has changed”
  4. assertionAdopter.transferOwnership(newOwner): Simulates a transaction that changes ownership
  5. assertEq(assertionAdopter.owner(), initialOwner): Checks that the owner didn’t change
cl is the cheatcode exposed by the CredibleTest contract used specifically for testing assertions. It provides tools to validate your assertions under different conditions without having to deploy them to a real blockchain.

​
Testing Assertion Success

// Test case: No ownership change should pass the assertion
function test_assertionOwnershipNotChanged() public {
    cl.assertion({
        adopter: address(assertionAdopter),
        createData: type(OwnableAssertion).creationCode,
        fnSelector: OwnableAssertion.assertionOwnershipChange.selector
    });

    // Simulate a transaction that doesn't change ownership (transferring to same owner)
    vm.prank(initialOwner);
    assertionAdopter.transferOwnership(initialOwner);
}
  • Similar to the failing test, but tests the case where no ownership change occurs.
  • Uses transferOwnership to the same owner to simulate a transaction that doesn’t change the state in ways that violate our assertion
  • transferOwnership will not revert if the assertion passes so we don’t need to use vm.expectRevert()

​
Full Test Contract

// SPDX-License-Identifier: MIT
pragma solidity ^0.8.13;

import {OwnableAssertion} from "../src/OwnableAssertion.a.sol";
import {Ownable} from "../../src/Ownable.sol";
import {CredibleTest} from "credible-std/CredibleTest.sol";
import {Test} from "forge-std/Test.sol";

contract TestOwnableAssertion is CredibleTest, Test {
    // Contract state variables
    Ownable public assertionAdopter;
    address public initialOwner = address(0xf00);
    address public newOwner = address(0xdeadbeef);

    // Set up the test environment
    function setUp() public {
        assertionAdopter = new Ownable(initialOwner);
        vm.deal(initialOwner, 1 ether);
    }

    // Test case: Ownership changes should trigger the assertion
    function test_assertionOwnershipChanged() public {
        assertEq(assertionAdopter.owner(), initialOwner);

        cl.assertion({
            adopter: address(assertionAdopter),
            createData: type(OwnableAssertion).creationCode,
            fnSelector: OwnableAssertion.assertionOwnershipChange.selector
        });

        // Simulate a transaction that changes ownership
        vm.prank(initialOwner);
        vm.expectRevert("Ownership has changed");
        assertionAdopter.transferOwnership(newOwner);

        // Check that owner didn't change
        assertEq(assertionAdopter.owner(), initialOwner);
    }

    // Test case: No ownership change should pass the assertion
    function test_assertionOwnershipNotChanged() public {
        cl.assertion({
            adopter: address(assertionAdopter),
            createData: type(OwnableAssertion).creationCode,
            fnSelector: OwnableAssertion.assertionOwnershipChange.selector
        });

        // Simulate a transaction that doesn't change ownership (transferring to same owner)
        vm.prank(initialOwner);
        assertionAdopter.transferOwnership(initialOwner);
    }
}

​
Key Testing Concepts

  1. Assertion Registration: Use cl.assertion() to register assertions that will be run on the next transaction
  2. State Manipulation: Use Forge’s cheatcodes (vm.prank, vm.deal) to set up test scenarios
  3. Verification: Use vm.expectRevert() to verify that the assertion reverts when expected

​
Running the Tests

pcl test

​
Conclusion

Assertions provide a powerful mechanism for protecting your protocol’s state and preventing security violations in real-time. By implementing well-designed assertions, you can:
  1. Enhance Security: Block unauthorized changes to critical protocol parameters
  2. Eliminate Risk: Prevent potential exploits before any damage occurs
  3. Build Trust: Demonstrate to users that your protocol is actively protected
  4. Sleep Better: Know that your protocol has an active defense layer
The simple ownership assertion we built in this guide demonstrates just one application. In practice, you might want to secure more complex invariants, such as:
  • Total supply of tokens should never increase unexpectedly
  • Funds should never be withdrawn without proper authorization
  • Key protocol parameters should only change through governance
  • Protocol reserves should always be sufficient to cover liabilities
  • Transaction values should never exceed the protocol’s limits
  • Voting power recorded during snapshot should match the actual voting power
  • Deviation of the price of a token from the oracle should never exceed a certain threshold
  • And many more…
By following the best practices outlined in this guide, you can create assertions that are both effective and easy to maintain. Remember to test thoroughly, optimize for gas efficiency, and focus on the most critical aspects of your protocol.

​
What’s Next?