Important Note: AI tools can make mistakes when generating assertions. Always review AI-generated code carefully and test your assertions thoroughly before deployment. The goal of AI is to accelerate the development process, not replace manual verification.

​
Guide for generating assertions with AI

AI tools can significantly enhance your workflow when defining protocol invariants and assertions. By leveraging AI assistants like Claude, GPT-4, or Cursor AI, you can quickly generate assertion templates that follow Phylax best practices and patterns.
Note: This guide focuses on using Cursor as the AI-powered IDE. If you’re using a different AI coding assistant, you’ll need to adjust the setup steps accordingly while following the same assertion generation principles.
As the number of example assertions grows, we expect the quality of the generated assertions to improve. Similarly, we hope that more and more protocols will start clearly documenting their invariants, as it’s both an important step towards better security in general and towards more efficient assertions generation.

​
Setup

  • We assume you’ve already installed the Credible Layer CLI (pcl) and have a project set up. If you don’t have one set up yet, you can follow the pcl quickstart guide to get started.
  • Open your project in Cursor and configure Cursor settings:
The Phylax documentation is optimized to work well with AIs and expose both llms.txt and llms-full.txt files.

​
Creating Effective Prompts

To generate high-quality assertions, your prompts should include:
  1. Contract Context: Share the relevant contract code that needs protection
  2. Invariant Description: Clearly state what invariants you want to protect
  3. Pattern Reference: Ask for assertions that follow Phylax’s established patterns
  4. Specific Requirements: Mention specific functions, state variables, or edge cases

​
Prompt Template

Create Phylax assertions to protect my protocol. Here's the context:

1. Contract: [paste your contract code or describe its function]

2. Invariants I want to protect:
   - [Invariant 1: e.g., "Owner should never change without authorization"]
   - [Invariant 2: e.g., "Total supply should never exceed maximum cap"]
   - [Invariant 3: e.g., "User balances should never decrease unexpectedly"]

3. Please generate assertions that follow the patterns and best practices from the Phylax assertion examples in the @phylax-docs:
   - Proper imports from credible-std
   - A clean interface to interact with my contract
   - A triggers() function registering appropriate triggers (call, storage, balance)
   - Assertion functions using ph.forkPreState() and ph.forkPostState() to compare values
   - Use of getCallInputs() and getStateChanges() when appropriate to detect invariant breaches in the callstack
   - Clear require statements with descriptive error messages
   - Assertion function names should start with "assertion" prefix (e.g., assertionOwnershipChange)

The assertions should focus on detecting undesired protocol states rather than trying to cover every possible edge case. Follow the pattern from Phylax assertion examples.

​
Example: Origin Protocol

Note: The assertions and tests presented in this section were generated with AI directly from the Origin Protocol codebase as a first version. They are provided as illustrative examples without further refinement and may not fully work in their current form without adjustments. However, they give a practical demonstration of how assertions could be implemented and tested for a real protocol. A developer familiar with Origin Protocol could likely adapt these examples to be production-ready with relatively minimal effort.
We’ll demonstrate using Origin Protocol’s contracts as an example. These contracts are well-documented and include clear invariant definitions in their token logic documentation.

​
Sample Prompt

Create Phylax assertions for Origin Protocol's token contract. 

1. Context: Origin Protocol's OUSD token has rebasing and non-rebasing accounts. It needs to ensure that specific invariants are maintained during operations.

2. Invariants I want to protect:
   - Account state (rebasing/non-rebasing) should only change through authorized functions
   - Yield delegation relationships must maintain bidirectional links
   - Balance changes during rebase opt-in/out should preserve user value
   - Total supply should equal the sum of rebasing and non-rebasing supplies
   - Credits and tokens should maintain correct mathematical relationships

3. Please generate assertions that follow the patterns and best practices from the Phylax assertion examples in the @phylax-docs:
   - A triggers() function registering appropriate triggers
   - Clear use of ph.forkPreState() and ph.forkPostState() to compare values
   - Use of getCallInputs() or getStateChanges() to track relevant operations in the callstack
   - Descriptive error messages
   - Assertion function names should start with "assertion" prefix
   - Focus on detecting undesired states rather than covering every possible scenario

The assertions should check critical state changes before and after transactions to prevent potential exploits.

​
Generated Assertions

Using AI, we can generate assertions like this example (simplified for clarity): 
// SPDX-License-Identifier: MIT
pragma solidity 0.8.28;

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

interface IOUSD {
    function rebaseState(address) external view returns (uint8);
    function balanceOf(address) external view returns (uint256);
    function totalSupply() external view returns (uint256);
    function nonRebasingSupply() external view returns (uint256);
    function rebaseOptIn() external;
    function rebaseOptOut() external;
}

contract OUSDAssertions is Assertion {
    IOUSD public ousd;
    
    constructor(IOUSD _ousd) {
        ousd = _ousd;
    }
    
    function triggers() external view override {
        // Trigger on rebase opt-in/out calls
        registerCallTrigger(
            this.assertionBalancePreservation.selector,
            IOUSD.rebaseOptIn.selector
        );
        registerCallTrigger(
            this.assertionBalancePreservation.selector,
            IOUSD.rebaseOptOut.selector
        );
        
        // Trigger on any state changes that affect total supply
        registerStorageChangeTrigger(this.assertionTotalSupplyInvariant.selector);
    }

    // Ensure balances are preserved during rebase opt-in/out
    function assertionBalancePreservation() external {
        // Get all calls to rebaseOptIn or rebaseOptOut
        PhEvm.CallInputs[] memory calls = ph.getCallInputs(
            address(ousd),
            IOUSD.rebaseOptIn.selector
        );
        
        if (calls.length == 0) {
            calls = ph.getCallInputs(
                address(ousd),
                IOUSD.rebaseOptOut.selector
            );
        }
        
        if (calls.length > 0) {
            address account = calls[0].caller;
            
            ph.forkPreState();
            uint256 preBalance = ousd.balanceOf(account);
            
            ph.forkPostState();
            uint256 postBalance = ousd.balanceOf(account);
            
            require(
                preBalance == postBalance,
                "Balance must be preserved during rebase state changes"
            );
        }
    }

    // Verify total supply equals sum of all balances
    function assertionTotalSupplyInvariant() external {
        ph.forkPostState();
        uint256 totalSupply = ousd.totalSupply();
        uint256 nonRebasingSupply = ousd.nonRebasingSupply();
        
        require(
            nonRebasingSupply <= totalSupply,
            "Non-rebasing supply cannot exceed total supply"
        );
    }
}

​
Refining Generated Assertions

AI-generated assertions often need refinements:
  1. Add Protocol-Specific Logic: Tailor the assertions to your protocol’s unique requirements
  2. Focus on Undesired States: Remember that assertions should focus on detecting states you don’t want your protocol to reach, not covering every possible scenario
  3. Optimize Gas Usage: Simplify complex checks to reduce gas costs
  4. Improve Error Messages: Make error messages clear and actionable
  5. Follow Naming Conventions: Ensure functions start with “assertion” prefix and files use the .a.sol extension
One of the powerful aspects of assertions is that you don’t need to worry about how the undesired state might be reached - you only need to define what that undesired state looks like. This makes assertions much simpler to reason about than trying to predict all possible exploit paths.

​
Generating Test Cases with AI

Testing assertions is critical to ensure they correctly identify both valid and invalid states. AI can also help generate comprehensive test suites for your assertions.

​
Creating Test Prompts

When creating prompts for test generation, include:
  1. Assertion Code: Share the assertion code you want to test
  2. Protocol Contract: Include the protocol contract the assertion protects
  3. Test Scenarios: Describe scenarios that should pass and fail
  4. PCL Testing Patterns: Ask for tests that follow Phylax’s testing practices

​
Test Prompt Template

I need to create test cases for my Phylax assertion. Here's the context:

1. Protocol Contract:
[paste your protocol contract code]

2. Assertion Contract:
[paste your assertion contract code]

3. Please generate test cases that:
   - Import the proper testing libraries (forge-std/Test and credible-std/CredibleTest)
   - Set up the testing environment correctly
   - Test both positive scenarios (assertions should pass) and negative scenarios (assertions should fail)
   - Use cl.addAssertion() to associate assertions with contracts
   - Use cl.validate() to test the assertions against specific transactions
   - Include clear test function names that describe what's being tested
   - Use vm.prank() and other testing utilities as needed

Follow the testing patterns from the Phylax documentation.

​
Example: Testing OUSD Assertions

Building on our OUSD assertion example, here’s a sample prompt for generating tests: 
I need to create test cases for my OUSD assertions. Here's the context:

1. Protocol Contract: [abbreviated OUSD contract]

2. Assertion Contract: [paste the OUSDAssertions contract generated earlier]

3. Please generate test cases that verify:
   - Balance preservation during rebase opt-in/out operations
   - Total supply invariant validation
   - Both valid operations (assertions pass) and invalid operations (assertions fail)

Follow the Phylax documentation testing patterns and include comprehensive setup for realistic testing scenarios.

​
Generated Test Cases

Using AI, we can generate test cases like this example: 
// SPDX-License-Identifier: MIT
pragma solidity 0.8.28;

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

contract TestOUSDAssertions is CredibleTest, Test {
    // Contract state variables
    OUSD public token;
    address public admin = address(0xdead);
    address public user1 = address(0x1111);
    address public user2 = address(0x2222);
    
    function setUp() public {
        // Initialize the OUSD token
        token = new OUSD(admin);
        
        // Setup test accounts
        vm.deal(admin, 100 ether);
        vm.deal(user1, 10 ether);
        vm.deal(user2, 10 ether);
        
        // Mint some tokens to users
        vm.prank(admin);
        token.mint(user1, 1000 * 10**18);
        
        vm.prank(admin);
        token.mint(user2, 500 * 10**18);
    }
    
    function test_assertionBalancePreservation_Pass() public {
        address tokenAddress = address(token);
        string memory label = "Balance preserved during rebase opt-in";
        
        // Associate the assertion with the protocol
        cl.addAssertion(label, tokenAddress, type(OUSDAssertions).creationCode, abi.encode(token));
        
        // User1 opts out then back in with the same balance
        vm.startPrank(user1);
        
        // First, opt out - this should preserve the balance
        cl.validate(label, tokenAddress, 0, abi.encodePacked(token.rebaseOptOut.selector));
        
        // Then, opt back in - this should also preserve the balance
        cl.validate(label, tokenAddress, 0, abi.encodePacked(token.rebaseOptIn.selector));
        
        vm.stopPrank();
    }
    
    function test_assertionBalancePreservation_Fail() public {
        address tokenAddress = address(token);
        string memory label = "Balance not preserved during rebase opt-in";
        
        // Create a malicious mock implementation
        MaliciousOUSD maliciousToken = new MaliciousOUSD(admin);
        vm.prank(admin);
        maliciousToken.mint(user1, 1000 * 10**18);
        
        // Associate the assertion with the malicious implementation
        cl.addAssertion(
            label, 
            address(maliciousToken), 
            type(OUSDAssertions).creationCode, 
            abi.encode(maliciousToken)
        );
        
        // This should revert because the balance would change
        vm.prank(user1);
        vm.expectRevert("Assertions Reverted");
        cl.validate(
            label, 
            address(maliciousToken), 
            0, 
            abi.encodePacked(maliciousToken.rebaseOptIn.selector)
        );
    }
    
    function test_assertionTotalSupplyInvariant_Pass() public {
        address tokenAddress = address(token);
        string memory label = "Total supply invariant maintained";
        
        // Associate the assertion with the protocol
        cl.addAssertion(label, tokenAddress, type(OUSDAssertions).creationCode, abi.encode(token));
        
        // Admin mints tokens - this should maintain the invariant
        vm.prank(admin);
        cl.validate(
            label,
            tokenAddress,
            0,
            abi.encodePacked(token.mint.selector, abi.encode(user1, 500 * 10**18))
        );
    }
    
    function test_assertionTotalSupplyInvariant_Fail() public {
        address tokenAddress = address(token);
        string memory label = "Total supply invariant violated";
        
        // Create a malicious mock that would violate the invariant
        MaliciousOUSD maliciousToken = new MaliciousOUSD(admin);
        
        // Associate the assertion with the malicious implementation
        cl.addAssertion(
            label, 
            address(maliciousToken), 
            type(OUSDAssertions).creationCode, 
            abi.encode(maliciousToken)
        );
        
        // This should revert due to invariant violation
        vm.prank(admin);
        vm.expectRevert("Assertions Reverted");
        cl.validate(
            label,
            address(maliciousToken),
            0,
            abi.encodePacked(maliciousToken.violateSupplyInvariant.selector)
        );
    }
}

// Mock malicious contract for testing failure cases
contract MaliciousOUSD is OUSD {
    constructor(address admin) OUSD(admin) {}
    
    // Override rebaseOptIn to change the balance (violating our assertion)
    function rebaseOptIn() external override {
        // Malicious implementation that would change the balance
        _balances[msg.sender] = _balances[msg.sender] * 99 / 100; // Lose 1%
        super.rebaseOptIn();
    }
    
    // Function that would violate the supply invariant
    function violateSupplyInvariant() external {
        _nonRebasingSupply = _totalSupply + 1; // Violates invariant
    }
}

​
Tips for AI-Generated Tests

  1. Include Both Positive and Negative Tests: Test cases should verify that assertions pass for valid operations and fail for invalid ones.
  2. Create Mock Implementations: Generate mock contracts that violate invariants to test failure scenarios.
  3. Test Each Assertion Function: Create separate test cases for each assertion function.
  4. Simulate Realistic Scenarios: Set up the test environment with realistic token balances, user accounts, and permissions.
  5. Use Clear Test Function Names: Name tests to clearly indicate what they verify (e.g., test_assertionBalancePreservation_Pass).
  6. Leverage Forge Testing Utilities: Use vm.prank, vm.expectRevert, and other utilities to create comprehensive tests.
  7. Test Edge Cases: Include tests for boundary conditions and edge cases that might trigger assertion failures.

​
Testing Workflow

After generating test cases:
  1. Review and adjust the tests to match your specific protocol behavior
  2. Add additional edge cases that might not be covered
  3. Run the tests with pcl test
  4. Fix any failing tests that should pass, or adjust assertions if needed
  5. Iterate on both your assertions and tests until you have confidence in their correctness

​
Next Steps

Head over to the PCL Quickstart guide for more detailed information and check out the rest of the documentation, particularly the Assertions Book for more examples of common assertion patterns.