Tutorial: Write Your First Assertion

This guide walks you through writing your first assertion from scratch. By the end, you’ll have a working assertion that prevents unauthorized ownership transfers.

Use this tutorial to learn the basic shape of an assertion. If you already understand the workflow and need specific syntax, jump to Triggers and the Cheatcodes API Reference.

Prerequisites: Familiarity with Solidity, the Assertions Overview, and pcl installed. What you’ll build: An assertion that blocks any transaction attempting to change a contract’s owner.

The Example Contract

We’ll protect a simple ownership contract:

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

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");
        _;
    }

    function owner() public view returns (address) {
        return _owner;
    }

    function transferOwnership(address newOwner) public onlyOwner {
        require(newOwner != address(0), "Ownable: new owner is the zero address");
        emit OwnershipTransferred(_owner, newOwner);
        _owner = newOwner;
    }
}

Our assertion will verify that the owner remains unchanged after each transaction. This protects against attacks like the 2024 Radiant Capital hack where attackers gained multisig access and changed the protocol owner, resulting in $50M losses.

Step 1: Set Up Your Project

Clone the starter repository:

git clone --recurse-submodules https://github.com/phylaxsystems/credible-layer-starter
cd credible-layer-starter

The starter repository includes the complete ownership assertion example from this guide. You can follow along or explore the finished code directly.

This includes the necessary structure:

my-protocol/
  assertions/
    src/      # Assertion source files (.a.sol)
    test/     # Test files (.t.sol)
  src/        # Protocol contracts

For manual setup, see the Quickstart Guide.

Step 2: Write the Assertion

Create assertions/src/OwnableAssertion.a.sol:

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

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

contract OwnableAssertion is Assertion {
    constructor() {
        registerAssertionSpec(AssertionSpec.Reshiram);
    }

    function triggers() external view override {
        registerFnCallTrigger(this.assertionOwnershipChange.selector, Ownable.transferOwnership.selector);
    }

    function assertionOwnershipChange() external view {
        Ownable ownable = Ownable(ph.getAssertionAdopter());

        PhEvm.ForkId memory preTx = _preTx();
        PhEvm.ForkId memory postTx = _postTx();

        address preOwner = address(uint160(uint256(ph.loadStateAt(address(ownable), bytes32(uint256(0)), preTx))));
        address postOwner = address(uint160(uint256(ph.loadStateAt(address(ownable), bytes32(uint256(0)), postTx))));

        require(postOwner == preOwner, "Ownership has changed");
    }
}

How It Works

This assertion compares the owner before and after the transaction. If the owner changed, the require fails, the assertion reverts, and the transaction is dropped from the block. In general: if an assertion reverts, the transaction is blocked. This prevents attacks entirely rather than just detecting them.

Key Components

Imports and inheritance:

import {Assertion} from "credible-std/Assertion.sol";
import {AssertionSpec} from "credible-std/SpecRecorder.sol";
contract OwnableAssertion is Assertion {
    constructor() {
        registerAssertionSpec(AssertionSpec.Reshiram);
    }

The Assertion base class provides cheatcodes via the ph namespace. Triggers:

function triggers() external view override {
    registerFnCallTrigger(this.assertionOwnershipChange.selector, Ownable.transferOwnership.selector);
}

Triggers define when assertions run. Here, assertionOwnershipChange runs whenever transferOwnership is called. Key points about triggers:

Each assertion function must be registered via its selector
You can define multiple assertion functions in one contract
Each trigger maps to exactly one assertion function
Use triggers to run assertions only when needed (saves gas)

See Triggers for more trigger types and optimization. Assertion logic:

function assertionOwnershipChange() external view {
    Ownable ownable = Ownable(ph.getAssertionAdopter());

    PhEvm.ForkId memory preTx = _preTx();
    PhEvm.ForkId memory postTx = _postTx();

    address preOwner = address(uint160(uint256(ph.loadStateAt(address(ownable), bytes32(uint256(0)), preTx))));
    address postOwner = address(uint160(uint256(ph.loadStateAt(address(ownable), bytes32(uint256(0)), postTx))));

    require(postOwner == preOwner, "Ownership has changed");
}

ph.getAssertionAdopter(): Returns the protected contract’s address
PhEvm.ForkId: Identifies the pre-transaction and post-transaction snapshots
ph.loadStateAt(): Reads the protected contract’s owner slot at the requested snapshot
The require blocks the transaction if ownership changed

Best Practices

Single responsibility: Each assertion should verify one property
Use triggers efficiently: Only run assertions when relevant functions are called
Return early: Check simple conditions before complex logic
Use explicit ForkIds: For checks around a matched call, use ph.context() and construct PhEvm.ForkId({forkType: 2, callIndex: ctx.callStart}) or PhEvm.ForkId({forkType: 3, callIndex: ctx.callEnd}).

Step 3: Test the Assertion

Create assertions/test/OwnableAssertion.t.sol:

// 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 {
    Ownable public assertionAdopter;
    address public initialOwner = address(0xf00);
    address public newOwner = address(0xdeadbeef);

    function setUp() public {
        assertionAdopter = new Ownable(initialOwner);
        vm.deal(initialOwner, 1 ether);
    }

    function test_assertionOwnershipChanged() public {
        assertEq(assertionAdopter.owner(), initialOwner);

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

        vm.prank(initialOwner);
        vm.expectRevert("Ownership has changed");
        assertionAdopter.transferOwnership(newOwner);

        assertEq(assertionAdopter.owner(), initialOwner);
    }

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

        vm.prank(initialOwner);
        assertionAdopter.transferOwnership(initialOwner);
    }
}

Key Testing Concepts

cl.assertion(): Registers the assertion to run on the next transaction
vm.expectRevert(): Verifies the assertion blocks the transaction
Test both cases: invalid (ownership changes) and valid (no change)

For more details on testing assertions, see Testing Assertions. Run the tests:

pcl test

Recap

You’ve built a complete assertion:

Set up: Clone the starter repo with correct structure
Write: Create assertion with triggers and validation logic
Test: Verify it blocks attacks and allows normal operations

Video Walkthrough

For a visual walkthrough of assertion development:

Next Steps

Apply Assertions

Deploy your assertions with pcl apply

From Invariant to Assertion

Learn to write complex real-world assertions

Cheatcodes Reference

All available assertion cheatcodes

Assertions Book

More assertion examples

Start Here

Tutorials

How-to Guides

Explanation

Platform

Reference

The Example Contract

Step 1: Set Up Your Project

Step 2: Write the Assertion

How It Works

Key Components

Best Practices

Step 3: Test the Assertion

Key Testing Concepts

Recap

Video Walkthrough

Next Steps

Apply Assertions

From Invariant to Assertion

Cheatcodes Reference

Assertions Book

​The Example Contract

​Step 1: Set Up Your Project

​Step 2: Write the Assertion

​How It Works

​Key Components

​Best Practices

​Step 3: Test the Assertion

​Key Testing Concepts

​Recap

​Video Walkthrough

​Next Steps

Apply Assertions

From Invariant to Assertion

Cheatcodes Reference

Assertions Book

The Example Contract

Step 1: Set Up Your Project

Step 2: Write the Assertion

How It Works

Key Components

Best Practices

Step 3: Test the Assertion

Key Testing Concepts

Recap

Video Walkthrough

Next Steps