# Using the Assertions Book Source: https://docs.phylax.systems/assertions-book/assertions-book-intro Learn how to use the Assertions Book as a catalog of assertion patterns and a set of exploit case studies The Assertions Book has two jobs: * **Reference**: a catalog of reusable assertion patterns you can adapt to your own protocol * **Explanation**: case studies that explain how real exploits worked and why specific assertions would have blocked them Use this section when you want examples and inspiration. If you want a guided path for writing and deploying assertions, start in the [Credible Layer docs](../credible/credible-introduction). Each entry shows code snippets of assertions accompanied by minimal interfaces for the protocols they protect. Full examples and mock protocol code are available in [credible-std](https://github.com/phylaxsystems/credible-std/tree/master/examples/assertions-book). ## How to Use This Book Use the reference catalog when you already know the type of risk you want to cover. Use the case studies when you want to understand why an exploit worked and what assertion would have stopped it. Review deeper examples that show how assertion coverage can be shaped for a real protocol. Leave the book and follow a tutorial when you want to build your own assertion from scratch. If you have questions or issues, please reach out on telegram [@phylax\_credible\_layer](https://t.me/phylax_credible_layer). If you think an assertion is missing, please don't hesitate to open a PR or reach out. We love digging into new hacks and use cases and writing assertions for them! ## Book Structure This book is organized into three sections: ### Part 1: Protocol Case Studies Explanation pages that show how comprehensive assertion coverage can be designed for real systems. **[View real world protocol suites →](./assertions/aave-v3-suite)** ### Part 2: Previous Hacks Explanation pages that analyze real-world DeFi hacks and show how assertions could have prevented them. **[View the previous hacks analysis →](./previous-hacks/)** ### Part 3: Assertion Patterns Reference pages that catalog reusable assertion patterns by security category. **[View the complete use cases catalog →](./assertions/)** All sections include assertion code examples, explanations of the vulnerability or pattern being addressed, and minimal protocol interfaces for context. # Aave V3 Suite Source: https://docs.phylax.systems/assertions-book/assertions/aave-v3-suite Credible Layer Assertions for Aave V3 We've taken a deep dive into the Aave V3 protocol and have created a suite of assertions that can be used to increase the security of the protocol. In general, the Aave V3 smart contracts are very well written and follow best practices with regard to security. We chose Aave V3 because it's a popular and battle-tested protocol that would serve as a good case study for writing real-world assertions. Link to the Phylax fork of Aave V3: [https://github.com/phylaxsystems/aave-v3-origin/tree/main](https://github.com/phylaxsystems/aave-v3-origin/tree/main) ## Approach One of the most common ways of writing assertions is by expressing the protocol invariants as assertions. Aave V3 has put a lot of effort into invariants, as can be seen in the [Aave V3 Invariants](https://github.com/aave-dao/aave-v3-origin/tree/main/tests/invariants) documentation. Specifically, the [invariants specification](https://github.com/aave-dao/aave-v3-origin/tree/main/tests/invariants/specs) was helpful for writing assertions, and most of the assertions we wrote are based on the invariants. We have mocked parts of the protocol in order to properly test the assertions and ensure that they only revert transactions that break the invariants. The mocks are located in the [mocks](https://github.com/phylaxsystems/aave-v3-origin/tree/main/assertions/mocks) directory. ## Maturity The Aave V3 assertion suite has been tested quite thoroughly given the early stage of the Credible Layer testing capabilities. We feel confident that the production assertions could be added to an Aave V3 deployment and add value to the security and robustness of the protocol. Before production promotion, create a release in the Phylax platform and review its automatic backtesting result. The platform tests the release against transactions from the last 20,000 blocks so you can identify benign activity that the assertion would have invalidated. See [How to Review Backtesting Results](/credible/backtesting). ## Here Be Dragons 🐲 In order to showcase the real power of assertions, we have introduced a bug in the protocol. Anyone borrowing exactly `333e6` tokens will receive double the amount of tokens they would normally receive if they borrowed any other amount. The bug can be found in the [BorrowLogic.sol](https://github.com/phylaxsystems/aave-v3-origin/blob/main/src/contracts/protocol/libraries/logic/BorrowLogic.sol#L137-L141) file. **DO NOT USE THIS VERSION OF AAVE V3 IN PRODUCTION!** ## Key Features * Protocol violation detection * Comprehensive operation coverage (supply, borrow, repay, withdraw, liquidation, flash loans) * Based on Aave's official invariants * Extensive test suite ## Assertion Types ### Production Assertions (High Value) These assertions provide unique value beyond pure Solidity capabilities: * **Cross-transaction validation**: Verify invariants across multiple operations * **Price consistency**: Detect manipulated or inconsistent pricing inputs * **Complex state relationships**: Validate accounting integrity * **Proxy/delegatecall resilience**: Use event logs for robust verification ### Showcase Assertions (Demonstrative) These demonstrate assertion capabilities but could be implemented in Solidity: * **Basic balance validation**: Simple balance change checks * **Health factor validation**: Standard health factor maintenance * **Reserve state validation**: Basic reserve condition checks * **Cap validation**: Supply/borrow cap enforcement ## Assertion Collections ### Production Assertions #### Core Invariants * **[BaseInvariants](https://github.com/phylaxsystems/aave-v3-origin/tree/main/assertions/src/production/BaseInvariants.a.sol)** - Cross-transaction accounting validation: * Debt token supply consistency across operations * AToken supply consistency across operations * Underlying balance invariant validation * Virtual balance sanity checks * Liquidity index integrity verification #### Price Consistency * **[OracleAssertions](https://github.com/phylaxsystems/aave-v3-origin/tree/main/assertions/src/production/OracleAssertions.a.sol)** - Price consistency checks: * Borrow/supply/liquidation price deviation monitoring (5% max) * Price consistency validation across transactions * Manipulated pricing input detection #### Flashloan Protection * **[FlashloanInvariantAssertions](https://github.com/phylaxsystems/aave-v3-origin/tree/main/assertions/src/production/FlashloanInvariantAssertions.a.sol)** - Flashloan security: * Repayment verification (amount + fee) * Fee payment validation * Reserve state integrity #### Robust Verification * **[LogBasedAssertions](https://github.com/phylaxsystems/aave-v3-origin/tree/main/assertions/src/production/LogBasedAssertions.a.sol)** - Proxy/delegatecall resilient validation: * Balance change verification using event logs * Works with complex call patterns ### Showcase Assertions #### Operation Validation * **[LendingInvariantAssertions](https://github.com/phylaxsystems/aave-v3-origin/tree/main/assertions/src/showcase/LendingInvariantAssertions.a.sol)** - Standard supply/withdrawal checks: * Reserve state validation * Supply cap enforcement * Balance change verification * Collateral withdrawal health * **[LiquidationInvariantAssertions](https://github.com/phylaxsystems/aave-v3-origin/tree/main/assertions/src/showcase/LiquidationInvariantAssertions.a.sol)** - Standard liquidation checks: * Health factor thresholds * Grace period validation * Close factor conditions * Deficit accounting * Reserve state requirements #### Health Factor Management * **[HealthFactorAssertions](https://github.com/phylaxsystems/aave-v3-origin/tree/main/assertions/src/showcase/HealthFactorAssertions.a.sol)** - Health factor transitions: * Non-decreasing health factor actions * Healthy to unhealthy transition prevention * Supply/withdraw/repay health maintenance #### Basic Validation * **[BorrowLogicErrorAssertion](https://github.com/phylaxsystems/aave-v3-origin/tree/main/assertions/src/showcase/BorrowLogicErrorAssertion.a.sol)** - Simple balance validation: * Borrow amount matches underlying balance change ## Testing ### Structure * Positive tests: Valid operations pass * Negative tests: Invalid operations fail * Integration tests: Multi-operation sequences * Edge cases: Boundary conditions ### Categories * Individual operation tests * Batch operation tests * Error condition tests * Mock protocol tests ## Intentional Bugs 1. **333e6 Borrow Bug**: Borrowing exactly 333e6 tokens returns double amount * Location: `BorrowLogic.sol` lines 128-144 * Test: `test_BASE_INVARIANT_A_DebtTokenSupply_333e6Bug()` 2. **Mock Protocol**: `BrokenPool.sol` for controlled testing ## Usage ```bash theme={null} # Run all assertion tests FOUNDRY_PROFILE=assertions pcl test # Run specific test file FOUNDRY_PROFILE=assertions pcl test assertions/test/BaseInvariants.t.sol ``` # Implementation Address Change Source: https://docs.phylax.systems/assertions-book/assertions/ass01-impl-addr-change Assert that the address of an implementation has not changed unexpectedly ## When to Use This Pattern Prevents unauthorized changes to proxy implementation addresses, which could allow attackers to replace contract logic with malicious code. Critical for proxy-based upgradeable contracts in DeFi protocols (lending pools, yield aggregators), governance systems with timelocks, and cross-chain bridges. For example, it's possible to define a whitelist of allowed implementations - any other implementation would be considered an invalid state. ## What This Pattern Checks Monitors changes to the implementation address storage slot in proxy contracts using: * `_preTx()` / `_postTx()` with Reshiram snapshot reads: Compare implementation address before and after transaction * `ph.loadStateAt()`: Load the implementation slot at each snapshot * `registerTxEndTrigger()`: Trigger when implementation address changes The assertion performs a direct pre/post comparison of the protected implementation slot. For more information about cheatcodes, see the [Cheatcodes Documentation](/credible/cheatcodes-reference). ## Assertion Pattern ```solidity theme={null} // 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"; contract ImplementationChangeAssertion is Assertion { bytes32 internal constant IMPLEMENTATION_SLOT = bytes32(uint256(0)); constructor() { registerAssertionSpec(AssertionSpec.Reshiram); } function triggers() external view override { registerTxEndTrigger(this.implementationChange.selector); } /// @notice Checks that the implementation slot is unchanged across the transaction. function implementationChange() external view { address adopter = ph.getAssertionAdopter(); PhEvm.ForkId memory preFork = _preTx(); PhEvm.ForkId memory postFork = _postTx(); address preImpl = _loadAddressAt(adopter, IMPLEMENTATION_SLOT, preFork); address postImpl = _loadAddressAt(adopter, IMPLEMENTATION_SLOT, postFork); require(preImpl == postImpl, "Implementation changed"); } function _loadAddressAt(address target, bytes32 slot, PhEvm.ForkId memory fork) internal view returns (address) { return address(uint160(uint256(ph.loadStateAt(target, slot, fork)))); } } ``` Full examples and mock protocol code are available in [credible-std](https://github.com/phylaxsystems/credible-std/tree/master/examples/assertions-book). ## Related Patterns * [Owner Change](/assertions-book/assertions/ass05-ownership-change) * [Timelock Verification](/assertions-book/assertions/ass09-timelock-verification) # KYC Whitelist Assertion Source: https://docs.phylax.systems/assertions-book/assertions/ass04-kyc-whitelist Unified KYC Registry for DeFi Protocols Assert that only KYC-verified addresses can perform privileged actions across multiple dapps using a shared registry ## When to Use This Pattern Since regulated funds and prime brokerages can only gain exposure into regulated products, a DeFi protocol may want to attract greater fund deployment by proving itself as a compliant venue. This assertion is a simple proof-of-concept that demonstrates a single, shared registry that multiple applications can reference. It’s designed such that * Users complete KYC once and gain access to all integrated protocols; no redundant process to verify on each protocol * The protocol can adopt KYC requirements without implementing their own verification systems * Registry owners maintain centralized control over access permissions, the owner may revoke an investor accrediation once and have it impact access for all integrated protocols ## What This Pattern Checks What you should know about this KYC assertion example: * It is triggered on a specific function call. For example, a mint or transfer request on the implementation contract. * When triggered, the assertion references a shared registry contract, here named the `AccreditedInvestorRegistry` which maintains the whitelist of KYC-verified addresses. * The assertion validates that `msg.sender` exists in the KYC registry before allowing execution of protected functions. This prevents non-KYC addresses from interacting with regulated tokens or permissioned protocol functions. * It is assumed the admin that controls the Registry may be different than the integrating protocol’s admin. ## Assertion Pattern ```solidity theme={null} // 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 {OnlyAccreditedCanMint} from "../../src/ass4-only-accredited-can-mint.sol"; import {AccreditedInvestorRegistry} from "../../src/AccreditedInvestorRegistry.sol"; contract OnlyAccreditedCanMintAssertion is Assertion { AccreditedInvestorRegistry public immutable registry; constructor(address registry_) { registerAssertionSpec(AssertionSpec.Reshiram); registry = AccreditedInvestorRegistry(registry_); } function triggers() external view override { registerFnCallTrigger(this.assertOnlyAccreditedMint.selector, OnlyAccreditedCanMint.mint.selector); registerFnCallTrigger(this.assertOnlyAccreditedTransfer.selector, OnlyAccreditedCanMint.transfer.selector); } /// @notice Checks that the caller of `mint` is accredited. function assertOnlyAccreditedMint() external view { _assertMatchingCallersAccredited(OnlyAccreditedCanMint.mint.selector); } /// @notice Checks that the caller of `transfer` is accredited. function assertOnlyAccreditedTransfer() external view { _assertMatchingCallersAccredited(OnlyAccreditedCanMint.transfer.selector); } function _assertMatchingCallersAccredited(bytes4 selector) internal view { PhEvm.TriggerCall[] memory calls = ph.matchingCalls(ph.getAssertionAdopter(), selector, _successfulCalls(), 32); for (uint256 i = 0; i < calls.length; i++) { require(registry.isAccredited(calls[i].caller), "caller is not accredited"); } } function _successfulCalls() internal pure returns (PhEvm.CallFilter memory filter) { filter.callType = 1; filter.successOnly = true; } } ``` Full examples and mock protocol code are available in [credible-std](https://github.com/phylaxsystems/credible-std/tree/master/examples/assertions-book). ## Related Patterns * [Owner Change](/assertions-book/assertions/ass05-ownership-change) * [Timelock Verification](/assertions-book/assertions/ass01-impl-addr-change) # Owner Change Source: https://docs.phylax.systems/assertions-book/assertions/ass05-ownership-change Assert that the owner of a contract has not changed unexpectedly ## When to Use This Pattern Prevents unauthorized ownership transfers, which could allow attackers to take complete control of the protocol. Critical for DeFi protocols with owner-controlled administrative functions, lending protocols, yield aggregators, cross-chain bridges, and governance systems. For example, in the [Radiant Capital hack](/assertions-book/previous-hacks/hack1-radiant-capital), the attacker gained control over 3 signers of the multisig, which allowed them to change ownership of the lending pools and ultimately drain the protocol. This assertion would have prevented such an attack. ## What This Pattern Checks Monitors changes to the owner address storage slot in contracts using: * `_preTx()` / `_postTx()` with Reshiram snapshot reads: Compare owner address before and after transaction * `ph.loadStateAt()`: Load the owner and admin slots at each snapshot * `registerTxEndTrigger()`: Trigger when owner address changes The assertion performs both direct pre/post comparison and verification of all intermediate state changes to detect unauthorized ownership modifications. For more information about cheatcodes, see the [Cheatcodes Documentation](/credible/cheatcodes-reference). ## Assertion Pattern ```solidity theme={null} // 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"; contract OwnerChangeAssertion is Assertion { bytes32 internal constant OWNER_SLOT = bytes32(uint256(0)); bytes32 internal constant ADMIN_SLOT = bytes32(uint256(1)); constructor() { registerAssertionSpec(AssertionSpec.Reshiram); } function triggers() external view override { registerTxEndTrigger(this.assertionOwnerChange.selector); registerTxEndTrigger(this.assertionAdminChange.selector); } /// @notice Checks that the owner slot is unchanged across the transaction. function assertionOwnerChange() external view { address adopter = ph.getAssertionAdopter(); PhEvm.ForkId memory preFork = _preTx(); PhEvm.ForkId memory postFork = _postTx(); address preOwner = _loadAddressAt(adopter, OWNER_SLOT, preFork); address postOwner = _loadAddressAt(adopter, OWNER_SLOT, postFork); require(preOwner == postOwner, "Owner changed"); } /// @notice Checks that the admin slot is unchanged across the transaction. function assertionAdminChange() external view { address adopter = ph.getAssertionAdopter(); PhEvm.ForkId memory preFork = _preTx(); PhEvm.ForkId memory postFork = _postTx(); address preAdmin = _loadAddressAt(adopter, ADMIN_SLOT, preFork); address postAdmin = _loadAddressAt(adopter, ADMIN_SLOT, postFork); require(preAdmin == postAdmin, "Admin changed"); } function _loadAddressAt(address target, bytes32 slot, PhEvm.ForkId memory fork) internal view returns (address) { return address(uint160(uint256(ph.loadStateAt(target, slot, fork)))); } } ``` Full examples and mock protocol code are available in [credible-std](https://github.com/phylaxsystems/credible-std/tree/master/examples/assertions-book). ## Related Patterns * [Implementation Address Change](/assertions-book/assertions/ass01-impl-addr-change) * [Timelock Verification](/assertions-book/assertions/ass09-timelock-verification) # Constant Product Source: https://docs.phylax.systems/assertions-book/assertions/ass06-constant-product Assert that a constant product is maintained in an AMM pool ## When to Use This Pattern Ensures the constant product (k = x \* y) is maintained in AMM pools, preventing unauthorized manipulation of pool reserves and potential flash loan attacks. Critical for Uniswap V2-style AMMs, DEX aggregators, lending protocols using AMM price oracles, and yield farming protocols providing liquidity. The constant product formula is fundamental to many AMM designs - any deviation could indicate a serious security issue or potential exploit. ## What This Pattern Checks Monitors the product of reserves (k) in AMM pools to ensure it remains constant after transactions using: * `_preTx()` / `_postTx()` with Reshiram snapshot reads: Compare reserve product before and after transaction * `ph.loadStateAt()`: Load reserve slots before and after the transaction * Direct validation that k = reserve0 \* reserve1 remains unchanged The assertion verifies both initial/final states and detects potential manipulations during transaction execution. For more information about cheatcodes, see the [Cheatcodes Documentation](/credible/cheatcodes-reference). ## Assertion Pattern ```solidity theme={null} // 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"; contract ConstantProductAssertion is Assertion { bytes32 internal constant RESERVE0_SLOT = bytes32(uint256(0)); bytes32 internal constant RESERVE1_SLOT = bytes32(uint256(1)); constructor() { registerAssertionSpec(AssertionSpec.Reshiram); } function triggers() external view override { registerTxEndTrigger(this.assertionConstantProduct.selector); } /// @notice Checks that the pool's stored reserve product is not reduced by the transaction. function assertionConstantProduct() external view { address pool = ph.getAssertionAdopter(); PhEvm.ForkId memory preFork = _preTx(); PhEvm.ForkId memory postFork = _postTx(); uint256 reserve0Pre = uint256(ph.loadStateAt(pool, RESERVE0_SLOT, preFork)); uint256 reserve1Pre = uint256(ph.loadStateAt(pool, RESERVE1_SLOT, preFork)); uint256 reserve0Post = uint256(ph.loadStateAt(pool, RESERVE0_SLOT, postFork)); uint256 reserve1Post = uint256(ph.loadStateAt(pool, RESERVE1_SLOT, postFork)); require(reserve0Post * reserve1Post >= reserve0Pre * reserve1Pre, "Constant product invariant reduced"); } } ``` Full examples and mock protocol code are available in [credible-std](https://github.com/phylaxsystems/credible-std/tree/master/examples/assertions-book). ## Related Patterns * [Fee Calculations](/assertions-book/assertions/ass14-fee-calculations) * [ERC20 Cumulative Outflow Breaker](/assertions-book/assertions/ass20-erc20-drain) * [Panic State Validation](/assertions-book/assertions/ass17-panic-state-validation) * [ERC20 Cumulative Inflow Breaker](/assertions-book/assertions/ass22-erc20-inflow-breaker) # Lending Health Factor Source: https://docs.phylax.systems/assertions-book/assertions/ass07-lending-health-factor Assert that the health factor of updated positions in a lending protocol is above a certain threshold ## When to Use This Pattern Ensures the health factor of updated positions in lending protocols remains above a threshold, preventing unauthorized liquidations and protocol insolvency. Critical for lending protocols (Aave, Compound, Morpho), margin trading platforms, and any DeFi protocol using health factors for position management. Focuses on core lending operations (supply, borrow, withdraw, repay) while allowing other functions like liquidations to operate as designed. ## What This Pattern Checks Monitors health factors of positions during specific lending operations using: * `getCallInputs()`: Track all function calls to specified protocol functions * `registerFnCallTrigger()`: Trigger on lending operations (supply, borrow, withdraw, repay) * `_postTx()`: Verify health factor after each operation (used by default if no pre-state specified) The assertion checks each lending operation individually to ensure positions affected by these operations remain healthy. For more information about cheatcodes, see the [Cheatcodes Documentation](/credible/cheatcodes-reference). ## Assertion Pattern ```solidity theme={null} // 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"; contract LendingHealthFactorAssertion is Assertion { bytes32 internal constant HEALTH_FACTOR_SLOT = bytes32(uint256(0)); uint256 internal constant MIN_HEALTH_FACTOR = 1e18; constructor() { registerAssertionSpec(AssertionSpec.Reshiram); } function triggers() external view override { registerFnCallTrigger(this.assertionOperationSafety.selector, IMorpho.supply.selector); registerFnCallTrigger(this.assertionOperationSafety.selector, IMorpho.borrow.selector); registerFnCallTrigger(this.assertionOperationSafety.selector, IMorpho.withdraw.selector); registerFnCallTrigger(this.assertionOperationSafety.selector, IMorpho.repay.selector); } /// @notice Checks that the touched account remains healthy after a lending operation. function assertionOperationSafety() external view { PhEvm.TriggerContext memory ctx = ph.context(); PhEvm.ForkId memory postCall = PhEvm.ForkId({forkType: 3, callIndex: ctx.callEnd}); (uint256 marketId,) = abi.decode(_stripSelector(ph.callinputAt(ctx.callStart)), (uint256, uint256)); address account = _matchingCaller(ctx.selector); bytes32 healthSlot = _healthFactorSlot(marketId, account); uint256 healthFactor = uint256(ph.loadStateAt(ph.getAssertionAdopter(), healthSlot, postCall)); require(healthFactor >= MIN_HEALTH_FACTOR, "Operation resulted in unhealthy position"); } function _matchingCaller(bytes4 selector) internal view returns (address) { PhEvm.TriggerCall[] memory calls = ph.matchingCalls(ph.getAssertionAdopter(), selector, _successfulCalls(), 1); require(calls.length == 1, "missing triggered call"); return calls[0].caller; } function _successfulCalls() internal pure returns (PhEvm.CallFilter memory filter) { filter.callType = 1; filter.successOnly = true; } function _healthFactorSlot(uint256 marketId, address account) internal pure returns (bytes32) { return keccak256(abi.encode(account, keccak256(abi.encode(marketId, HEALTH_FACTOR_SLOT)))); } function _stripSelector(bytes memory data) internal pure returns (bytes memory) { bytes memory stripped = new bytes(data.length - 4); for (uint256 i = 4; i < data.length; i++) { stripped[i - 4] = data[i]; } return stripped; } } interface IMorpho { function supply(uint256 marketId, uint256 amount) external; function borrow(uint256 marketId, uint256 amount) external; function withdraw(uint256 marketId, uint256 amount) external; function repay(uint256 marketId, uint256 amount) external; } ``` Full examples and mock protocol code are available in [credible-std](https://github.com/phylaxsystems/credible-std/tree/master/examples/assertions-book). **Extending Assertions:** When new functions are added to the protocol that should maintain healthy positions, you can create a new assertion file (e.g., `LendingHealthFactorExtendedAssertion.sol`) that follows the same pattern. This allows you to: * Keep the original assertions active for existing functions * Add new assertions for new functions without modifying existing code * Maintain clear separation of concerns between different protocol features ## Related Patterns * [Full Aave Assertion Suite](/assertions-book/assertions/aave-v3-suite) * [ERC20 Cumulative Outflow Breaker](/assertions-book/assertions/ass20-erc20-drain) * [Panic State Validation](/assertions-book/assertions/ass17-panic-state-validation) * [Owner Change](/assertions-book/assertions/ass05-ownership-change) # Sum of all positions Source: https://docs.phylax.systems/assertions-book/assertions/ass08-sum-of-all-positions Assert that the sum of all positions is the same as the total supply reported by the protocol ## When to Use This Pattern Verifies that the sum of all individual positions exactly matches the total supply reported by the protocol, preventing supply manipulation, double counting, and accounting discrepancies. Critical for lending protocols, liquidity pools, staking mechanisms, synthetic asset protocols, and fractionalized NFT protocols where accurate position accounting is fundamental to security. Any discrepancy between individual positions and total supply could lead to incorrect calculations, withdrawal failures, or protocol insolvency. ## What This Pattern Checks Since direct iteration over all positions isn't currently supported, this assertion uses a workaround that tracks position changes through function calls: 1. Capture the pre-state total supply before the transaction 2. Monitor all function calls that modify positions (deposit, withdraw) 3. Calculate the sum of changes to these positions 4. Verify that the new total supply equals the pre-state total supply plus the sum of position changes Uses these cheatcodes: * `_preTx()` / `_postTx()` with Reshiram snapshot reads: Capture total supply before and after transaction * `ph.context()` and `ph.callinputAt()`: Inspect the triggered position-modifying call * `registerFnCallTrigger()`: Trigger on position-modifying functions Check [Modified Key Discovery](/credible/use-case-mappings/modified-keys) for the V2 helpers that enumerate mapping entries changed by the current transaction. These helpers do not enumerate every position that has ever existed. For more information about cheatcodes, see the [Cheatcodes Documentation](/credible/cheatcodes-reference). ## Assertion Pattern ```solidity theme={null} // 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"; contract PositionSumAssertion is Assertion { bytes32 internal constant TOTAL_SUPPLY_SLOT = bytes32(uint256(0)); constructor() { registerAssertionSpec(AssertionSpec.Reshiram); } function triggers() external view override { registerFnCallTrigger(this.assertionPositionsSum.selector, ILending.deposit.selector); } /// @notice Checks that a deposit call increases stored total supply by the deposited amount. function assertionPositionsSum() external view { address adopter = ph.getAssertionAdopter(); PhEvm.TriggerContext memory ctx = ph.context(); PhEvm.ForkId memory preCall = PhEvm.ForkId({forkType: 2, callIndex: ctx.callStart}); PhEvm.ForkId memory postCall = PhEvm.ForkId({forkType: 3, callIndex: ctx.callEnd}); uint256 preTotalSupply = uint256(ph.loadStateAt(adopter, TOTAL_SUPPLY_SLOT, preCall)); uint256 postTotalSupply = uint256(ph.loadStateAt(adopter, TOTAL_SUPPLY_SLOT, postCall)); (, uint256 amount) = abi.decode(_stripSelector(ph.callinputAt(ctx.callStart)), (address, uint256)); require(postTotalSupply == preTotalSupply + amount, "Positions sum does not match total supply"); } function _stripSelector(bytes memory data) internal pure returns (bytes memory) { bytes memory stripped = new bytes(data.length - 4); for (uint256 i = 4; i < data.length; i++) { stripped[i - 4] = data[i]; } return stripped; } } interface ILending { function deposit(address user, uint256 amount) external; } ``` Full examples and mock protocol code are available in [credible-std](https://github.com/phylaxsystems/credible-std/tree/master/examples/assertions-book). ## Related Patterns * [Lending Health Factor](/assertions-book/assertions/ass07-lending-health-factor): Ensures user balances are consistent across different views * [Liquidation Health Factor](/assertions-book/assertions/ass16-liquidation-health-factor): Verifies that the total supply doesn't exceed protocol limits # Timelock Verification Source: https://docs.phylax.systems/assertions-book/assertions/ass09-timelock-verification Make sure that a timelock has been correctly triggered for governance actions ## When to Use This Pattern Ensures timelocks are correctly triggered for governance actions, enforcing delays between proposal and execution to allow community review. Critical for DeFi lending protocols, DEX protocols, yield aggregators, cross-chain bridges, and DAOs that use timelocks to prevent flash loan attacks, allow security review periods, and protect against governance attacks. Timelocks provide a buffer against malicious governance actions - without proper enforcement, changes could be executed immediately. ## What This Pattern Checks Verifies timelock integrity by comparing timelock state and parameters before and after transactions: * `_preTx()` / `_postTx()` with Reshiram snapshot reads: Compare timelock state before and after transaction * `registerTxEndTrigger()`: Monitor changes to timelock storage slot * Ensures timelock delay is within acceptable bounds (1 day to 2 weeks) * Confirms timelock activation follows proper procedures The assertion performs both pre/post state comparison and parameter validation to ensure governance changes follow proper timelock procedures. For more information about cheatcodes, see the [Cheatcodes Documentation](/credible/cheatcodes-reference). ## Assertion Pattern ```solidity theme={null} // 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"; contract TimelockVerificationAssertion is Assertion { bytes32 internal constant TIMELOCK_DELAY_SLOT = bytes32(uint256(0)); bytes32 internal constant TIMELOCK_ACTIVE_SLOT = bytes32(uint256(1)); constructor() { registerAssertionSpec(AssertionSpec.Reshiram); } function triggers() external view override { registerTxEndTrigger(this.assertionTimelock.selector); } /// @notice Checks that an activated timelock uses a bounded delay. function assertionTimelock() external view { address adopter = ph.getAssertionAdopter(); PhEvm.ForkId memory preFork = _preTx(); PhEvm.ForkId memory postFork = _postTx(); bool preActive = uint256(ph.loadStateAt(adopter, TIMELOCK_ACTIVE_SLOT, preFork)) != 0; if (preActive) { return; } bool postActive = uint256(ph.loadStateAt(adopter, TIMELOCK_ACTIVE_SLOT, postFork)) != 0; if (postActive) { uint256 delay = uint256(ph.loadStateAt(adopter, TIMELOCK_DELAY_SLOT, postFork)); require(delay >= 1 days && delay <= 2 weeks, "Timelock parameters invalid"); } } } ``` Full examples and mock protocol code are available in [credible-std](https://github.com/phylaxsystems/credible-std/tree/master/examples/assertions-book). ## Related Patterns * [Owner Change](/assertions-book/assertions/ass05-ownership-change) * [Implementation Address Change](/assertions-book/assertions/ass01-impl-addr-change) # Oracle Liveness Validation Source: https://docs.phylax.systems/assertions-book/assertions/ass10-oracle-validation Assert that an oracle is updated within a specified time window ## When to Use This Pattern Ensures oracle data is fresh and updated within an acceptable time window, preventing the use of stale price data that could lead to incorrect valuations and financial losses. Critical for lending protocols (collateral valuation, liquidations), DEXs (price discovery, arbitrage detection), yield farming protocols (reward calculations), insurance protocols (premium calculations), and options/derivatives protocols (settlement). Stale oracle data can indicate service disruption or attacks on oracle infrastructure, potentially leading to significant protocol vulnerabilities. ### Related Case Studies * [Loopscale](https://rekt.news/loopscale-rekt): Hack caused by a stale oracle. It was on Solana, so not relevant to Credible Layer, but the same idea applies. ## What This Pattern Checks Monitors oracle timestamp updates when critical protocol functions are called: * `_postTx()`: Check oracle's last update time after transaction * `registerFnCallTrigger()`: Trigger on functions that rely on oracle data (e.g., DEX swaps) * Verify oracle's last update time is within defined maximum time window Upon functions that rely on oracle data, the assertion ensures transactions only proceed with fresh oracle data, preventing operations with stale pricing information. For more information about cheatcodes, see the [Cheatcodes Documentation](/credible/cheatcodes-reference). ## Assertion Pattern ```solidity theme={null} // 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"; contract OracleLivenessAssertion is Assertion { constructor() { registerAssertionSpec(AssertionSpec.Reshiram); } // Maximum time window (in seconds) that oracle data can be considered fresh // This is a constant that should be adjusted based on the protocol's requirements uint256 public constant MAX_UPDATE_WINDOW = 10 minutes; function triggers() external view override { // Register trigger for the swap function which relies on oracle data registerFnCallTrigger(this.assertionOracleLiveness.selector, IDex.swap.selector); } // Assert that the oracle has been updated within the specified time window function assertionOracleLiveness() external { // Get the assertion adopter address IDex adopter = IDex(ph.getAssertionAdopter()); // Get the current state to check the oracle's last update time PhEvm.ForkId memory postFork = _postTx(); // Check if the oracle has been updated within the maximum allowed window uint256 lastUpdateTime = IOracle(adopter.oracle()).lastUpdated(); uint256 currentTime = block.timestamp; // Verify the oracle data is fresh (updated within the time window) require(currentTime - lastUpdateTime <= MAX_UPDATE_WINDOW, "Oracle not updated within the allowed time window"); } } interface IOracle { function lastUpdated() external view returns (uint256); } interface IDex { function swap(address tokenIn, address tokenOut, uint256 amountIn) external returns (uint256); function oracle() external view returns (IOracle); } ``` Full examples and mock protocol code are available in [credible-std](https://github.com/phylaxsystems/credible-std/tree/master/examples/assertions-book). ## Related Patterns * [Oracle Price Deviation](/assertions-book/assertions/ass28-intra-tx-oracle-deviation) # TWAP Deviation Source: https://docs.phylax.systems/assertions-book/assertions/ass11-twap-deviation Assert that the TWAP price doesn't deviate more than X% from the pre-state TWAP price ## When to Use This Pattern Prevents TWAP (Time-Weighted Average Price) price manipulation by ensuring oracle prices don't deviate more than X% from pre-state TWAP prices. Critical for AMMs and DEXs (price discovery), lending protocols (collateral valuation), yield aggregators (rebalancing), options protocols (settlement), and cross-chain bridges (asset pricing). Sudden price deviations could indicate manipulation through flash loan attacks or oracle failures, potentially leading to protocol insolvency or fund extraction. ## What This Pattern Checks Monitors TWAP price changes using a two-stage approach to ensure price stability: * `_preTx()` / `_postTx()` with Reshiram snapshot reads: Compare post-transaction price against pre-transaction TWAP * `getStateChangesUint()`: Track all price changes during transaction execution * `registerTxEndTrigger()`: Trigger when price storage slot changes The assertion verifies both the final price and any intermediate price updates against the initial TWAP to detect flash loan attacks and price manipulation throughout the transaction. For more information about cheatcodes, see the [Cheatcodes Documentation](/credible/cheatcodes-reference). ## Assertion Pattern ```solidity theme={null} // 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"; contract TwapDeviationAssertion is Assertion { constructor() { registerAssertionSpec(AssertionSpec.Reshiram); } function triggers() external view override { // Register trigger for changes to the current price // We assume that the price is stored in storage slot 0 registerTxEndTrigger(this.assertionTwapDeviation.selector); } // Assert that the current price doesn't deviate more than 5% from the TWAP price function assertionTwapDeviation() external { // Get the assertion adopter address IPool adopter = IPool(ph.getAssertionAdopter()); // Get TWAP price before the transaction (our reference point) PhEvm.ForkId memory preFork = _preTx(); uint256 preTwapPrice = adopter.twap(); // Get price after the transaction PhEvm.ForkId memory postFork = _postTx(); uint256 postPrice = adopter.price(); uint256 maxDeviation = 5; // First check: Compare post-transaction price against pre-transaction TWAP uint256 deviation = calculateDeviation(preTwapPrice, postPrice); require(deviation <= maxDeviation, "Price deviation from TWAP exceeds maximum allowed"); // Second check: If the simple check passes, inspect all price changes in the callstack // This is more expensive but catches manipulation attempts within the transaction uint256[] memory priceChanges = getStateChangesUint( address(adopter), bytes32(uint256(0)) // Current price storage slot ); // Check each price change against the pre-transaction TWAP for (uint256 i = 0; i < priceChanges.length; i++) { deviation = calculateDeviation(preTwapPrice, priceChanges[i]); require(deviation <= maxDeviation, "Price deviation from TWAP exceeds maximum allowed"); } } // Helper function to calculate percentage deviation function calculateDeviation(uint256 referencePrice, uint256 currentPrice) internal pure returns (uint256) { return (((currentPrice > referencePrice) ? currentPrice - referencePrice : referencePrice - currentPrice) * 100) / referencePrice; } } interface IPool { function price() external view returns (uint256); function twap() external view returns (uint256); } ``` Full examples and mock protocol code are available in [credible-std](https://github.com/phylaxsystems/credible-std/tree/master/examples/assertions-book). ## Related Patterns * [Intra-tx Oracle Deviation](/assertions-book/assertions/ass28-intra-tx-oracle-deviation) * [Liquidation Health Factor](/assertions-book/assertions/ass16-liquidation-health-factor) # ERC4626 Assets to Shares Source: https://docs.phylax.systems/assertions-book/assertions/ass12-erc4626-assets-to-shares Make sure that the total shares are not more than the total assets ## When to Use This Pattern Enforces a critical ERC4626 vault invariant: total shares must never exceed total assets converted to shares, preventing share price manipulation and fund loss. Critical for yield aggregators, lending protocols implementing ERC4626, liquidity pools using ERC4626 for LP tokens, and staking protocols with ERC4626 vaults. Any violation could allow unauthorized share minting that dilutes existing holders or enables withdrawal of more assets than deposited, potentially leading to protocol insolvency. ## What This Pattern Checks Verifies the fundamental ERC4626 share-to-asset relationship using a basic approach: * `registerTxEndTrigger()`: Trigger when total supply storage slot changes * Verify total assets are sufficient to back all outstanding shares * Ensure share value is preserved and users can withdraw their assets This ensures there are always enough assets to back all shares, maintaining accurate share values and preventing value extraction from the vault. For more information about cheatcodes, see the [Cheatcodes Documentation](/credible/cheatcodes-reference). ## Assertion Pattern ```solidity theme={null} // 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"; contract ERC4626AssetsSharesAssertion is Assertion { bytes32 internal constant TOTAL_ASSETS_SLOT = bytes32(uint256(0)); bytes32 internal constant TOTAL_SUPPLY_SLOT = bytes32(uint256(1)); constructor() { registerAssertionSpec(AssertionSpec.Reshiram); } function triggers() external view override { registerTxEndTrigger(this.assertionAssetsShares.selector); } /// @notice Checks that stored total assets are sufficient to back stored total shares. function assertionAssetsShares() external view { address vault = ph.getAssertionAdopter(); PhEvm.ForkId memory postFork = _postTx(); uint256 totalAssets = uint256(ph.loadStateAt(vault, TOTAL_ASSETS_SLOT, postFork)); uint256 totalSupply = uint256(ph.loadStateAt(vault, TOTAL_SUPPLY_SLOT, postFork)); require(totalAssets >= totalSupply, "Not enough assets to back all shares"); } } ``` Full examples and mock protocol code are available in [credible-std](https://github.com/phylaxsystems/credible-std/tree/master/examples/assertions-book). ## Related Patterns * [ERC4626 Deposit and Withdraw Share Price](./ass13-erc4626-deposit-withdraw): deposit and withdraw share-price checks # ERC4626 Deposit and Withdraw Share Price Source: https://docs.phylax.systems/assertions-book/assertions/ass13-erc4626-deposit-withdraw Reference pattern for checking ERC4626 deposit and withdraw calls against share-price dilution ## When to Use This Pattern Use this pattern when ERC4626 deposit or withdraw calls must not dilute existing or remaining shares. It applies to yield aggregators, lending protocols with ERC4626 interest-bearing tokens, liquidity pools using ERC4626 shares, and staking protocols with ERC4626 receipt tokens. This pattern checks share-price monotonicity around matched deposit and withdraw calls. It does not cover mint/redeem entry points or batch-wide preview-function validation. ## What This Pattern Checks Checks ERC4626 share-price safety around deposit and withdraw calls: * `registerAssertionSpec(AssertionSpec.Reshiram)`: Registers the assertion as a Reshiram assertion. * `registerFnCallTrigger()`: Runs the assertion around `deposit` and `withdraw` calls. * `ph.context()`: Reads the current call frame. * `PhEvm.ForkId({forkType: 2, callIndex: ctx.callStart})` / `PhEvm.ForkId({forkType: 3, callIndex: ctx.callEnd})`: Reads pre-call and post-call snapshots. * `ph.loadStateAt()`: Loads total assets and total supply at each snapshot. ## Assertion Pattern ```solidity theme={null} // 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"; contract ERC4626DepositWithdrawAssertion is Assertion { bytes32 internal constant TOTAL_ASSETS_SLOT = bytes32(uint256(0)); bytes32 internal constant TOTAL_SUPPLY_SLOT = bytes32(uint256(1)); constructor() { registerAssertionSpec(AssertionSpec.Reshiram); } function triggers() external view override { registerFnCallTrigger(this.assertDepositPreservesSharePrice.selector, IERC4626.deposit.selector); registerFnCallTrigger(this.assertWithdrawPreservesSharePrice.selector, IERC4626.withdraw.selector); } /// @notice Checks that a deposit does not dilute existing shares. function assertDepositPreservesSharePrice() external view { PhEvm.TriggerContext memory ctx = ph.context(); _assertSharePriceNotReduced(ctx.callStart, ctx.callEnd, "ERC4626: deposit diluted shares"); } /// @notice Checks that a withdrawal does not dilute remaining shares. function assertWithdrawPreservesSharePrice() external view { PhEvm.TriggerContext memory ctx = ph.context(); _assertSharePriceNotReduced(ctx.callStart, ctx.callEnd, "ERC4626: withdrawal diluted shares"); } function _assertSharePriceNotReduced(uint256 callStart, uint256 callEnd, string memory reason) internal view { address vault = ph.getAssertionAdopter(); PhEvm.ForkId memory preCall = PhEvm.ForkId({forkType: 2, callIndex: callStart}); PhEvm.ForkId memory postCall = PhEvm.ForkId({forkType: 3, callIndex: callEnd}); uint256 preAssets = uint256(ph.loadStateAt(vault, TOTAL_ASSETS_SLOT, preCall)); uint256 preSupply = uint256(ph.loadStateAt(vault, TOTAL_SUPPLY_SLOT, preCall)); uint256 postAssets = uint256(ph.loadStateAt(vault, TOTAL_ASSETS_SLOT, postCall)); uint256 postSupply = uint256(ph.loadStateAt(vault, TOTAL_SUPPLY_SLOT, postCall)); if (preSupply == 0 || postSupply == 0) { return; } require(postAssets * preSupply >= preAssets * postSupply, reason); } } interface IERC4626 { function deposit(uint256 assets, address receiver) external returns (uint256 shares); function withdraw(uint256 assets, address receiver, address owner) external returns (uint256 shares); } ``` Full examples and mock protocol code are available in [credible-std](https://github.com/phylaxsystems/credible-std/tree/master/examples/assertions-book). ## Related Patterns * [ERC4626 Assets to Shares](./ass12-erc4626-assets-to-shares): simple base invariant check * [Harvest Increases Balance](./ass18-harvest-increases-balance): yield operation validation # Fee Calculations Source: https://docs.phylax.systems/assertions-book/assertions/ass14-fee-calculations Make sure that the fees do not change unexpectedly ## When to Use This Pattern Prevents unauthorized fee manipulation in AMMs and DeFi protocols by using a whitelist approach to control fee changes. Critical for AMMs (Velodrome, Aerodrome, Curve), DEX aggregators, lending protocols with origination fees, yield aggregators with performance fees, and cross-chain bridges with transfer fees. Unexpected fee changes can lead to unauthorized manipulation, protocol revenue loss, user losses, or market manipulation through fee bypasses. ## What This Pattern Checks Uses a whitelist approach to control fee changes: * `registerTxEndTrigger()`: Detect changes to fee storage slot * `ph.loadStateAt()`: Retrieve new fee value after change * Maintains hardcoded allowed fee values for stable pools (0.1%, 0.15%) and non-stable pools (0.25%, 0.30%) When triggered, verifies the new fee matches one of the allowed values, preventing unauthorized modifications while allowing proper protocol updates. For more information about cheatcodes, see the [Cheatcodes Documentation](/credible/cheatcodes-reference). ## Assertion Pattern ```solidity theme={null} // 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"; contract AmmFeeVerificationAssertion is Assertion { bytes32 internal constant FEE_SLOT = bytes32(uint256(1)); bytes32 internal constant STABLE_SLOT = bytes32(uint256(2)); uint256 private constant STABLE_POOL_FEE_1 = 1; uint256 private constant STABLE_POOL_FEE_2 = 15; uint256 private constant NON_STABLE_POOL_FEE_1 = 25; uint256 private constant NON_STABLE_POOL_FEE_2 = 30; constructor() { registerAssertionSpec(AssertionSpec.Reshiram); } function triggers() external view override { registerTxEndTrigger(this.assertFeeVerification.selector); } /// @notice Checks that the post-transaction fee is one of the allowed values. function assertFeeVerification() external view { address pool = ph.getAssertionAdopter(); PhEvm.ForkId memory postFork = _postTx(); bool isStable = uint256(ph.loadStateAt(pool, STABLE_SLOT, postFork)) != 0; uint256 newFee = uint256(ph.loadStateAt(pool, FEE_SLOT, postFork)); bool isAllowed = isStable ? (newFee == STABLE_POOL_FEE_1 || newFee == STABLE_POOL_FEE_2) : (newFee == NON_STABLE_POOL_FEE_1 || newFee == NON_STABLE_POOL_FEE_2); require(isAllowed, "Fee change to unauthorized value"); } } ``` Full examples and mock protocol code are available in [credible-std](https://github.com/phylaxsystems/credible-std/tree/master/examples/assertions-book). ## Related Patterns * [Price Within Ticks](/assertions-book/assertions/ass15-price-within-ticks) # Price Within Ticks Source: https://docs.phylax.systems/assertions-book/assertions/ass15-price-within-ticks Make sure that the price is within the tick range ## When to Use This Pattern Ensures prices remain within valid tick boundaries in concentrated liquidity AMMs, preventing price manipulation and maintaining protocol mathematical validity. Critical for AMMs using concentrated liquidity models (Uniswap V3, PancakeSwap V3), protocols with tick-based price calculations, DeFi protocols interacting with tick-based AMMs, and cross-chain bridges using tick-based price feeds. If attackers could push prices outside valid tick ranges, they could execute trades at invalid prices, manipulate liquidity positions, or cause protocol calculations to fail. ## What This Pattern Checks Implements focused tick integrity verification: * `_preTx()` / `_postTx()` with Reshiram snapshot reads: Capture tick state before and after transaction * `registerTxEndTrigger()`: Monitor changes to tick-related storage slots * Verify ticks stay within global bounds (-887272 to 887272) * Ensure ticks align with pool's tick spacing requirements The assertion maintains proper concentrated liquidity calculations and prevents position management errors by enforcing tick boundaries and spacing rules. For more information about cheatcodes, see the [Cheatcodes Documentation](/credible/cheatcodes-reference). ## Assertion Pattern ```solidity theme={null} // 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"; contract PriceWithinTicksAssertion is Assertion { constructor() { registerAssertionSpec(AssertionSpec.Reshiram); } // Uniswap V3 tick bounds int24 constant MIN_TICK = -887272; int24 constant MAX_TICK = 887272; function triggers() external view override { // Register trigger for changes to the tick storage slot // Assumes tick is stored in slot0 of the pool contract registerTxEndTrigger(this.priceWithinTicks.selector); } // Check that the price is within the tick bounds and that the tick is divisible by the tick spacing function priceWithinTicks() external { // Get the assertion adopter address IUniswapV3Pool adopter = IUniswapV3Pool(ph.getAssertionAdopter()); // Get post-swap state PhEvm.ForkId memory postFork = _postTx(); (, int24 postTick,,,,,) = adopter.slot0(); int24 spacing = adopter.tickSpacing(); // Check 1: Tick must be within global bounds require(postTick >= MIN_TICK && postTick <= MAX_TICK, "Tick outside global bounds"); // Check 2: Tick must be divisible by tickSpacing require(postTick % spacing == 0, "Tick not aligned with spacing"); } } // Uniswap v3 pool style interface interface IUniswapV3Pool { function slot0() external view returns ( uint160 sqrtPriceX96, int24 tick, uint16 observationIndex, uint16 observationCardinality, uint16 observationCardinalityNext, uint8 feeProtocol, bool unlocked ); function tickSpacing() external view returns (int24); } ``` Full examples and mock protocol code are available in [credible-std](https://github.com/phylaxsystems/credible-std/tree/master/examples/assertions-book). ## Related Patterns * [Fee Calculations](/assertions-book/assertions/ass14-fee-calculations) * [Liquidation Health Factor](/assertions-book/assertions/ass16-liquidation-health-factor) # Liquidation Health Factor Source: https://docs.phylax.systems/assertions-book/assertions/ass16-liquidation-health-factor Make sure that liquidations can only happen if the position is unhealthy ## When to Use This Pattern Ensures liquidations only occur when positions are unhealthy, preventing unauthorized liquidations of healthy positions and protecting user funds. Critical for lending protocols (Aave, Compound, Morpho), margin trading platforms with position health monitoring, perpetual futures protocols with liquidation mechanisms, and any DeFi protocol using health factors for position solvency. Incorrect health factor validation could lead to unfair liquidations, protocol insolvency, or market manipulation through targeted liquidations. ## What This Pattern Checks Implements multi-layered liquidation health factor verification: * **Pre-liquidation**: `_preTx()` captures health factor before liquidation, verifies position is actually unhealthy * **Post-liquidation**: `_postTx()` verifies health factor improves after liquidation * **Parameter validation**: `getCallInputs()` monitors liquidation calls, validates seized assets and repaid shares are non-zero, enforces maximum liquidation amounts * `registerFnCallTrigger()`: Triggers on liquidation function calls The assertion ensures only unhealthy positions can be liquidated, liquidations improve position health, and liquidation amounts remain within safe limits for proper protocol risk management. For more information about cheatcodes, see the [Cheatcodes Documentation](/credible/cheatcodes-reference). ## Assertion Pattern ```solidity theme={null} // 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"; contract LiquidationHealthFactorAssertion is Assertion { constructor() { registerAssertionSpec(AssertionSpec.Reshiram); } // Simple health factor constants (no scaling) uint256 constant LIQUIDATION_THRESHOLD = 100; // Below this = liquidatable uint256 constant MIN_HEALTH_FACTOR = 120; // Minimum safe health factor after liquidation function triggers() external view override { // Register trigger for liquidation function calls registerFnCallTrigger(this.assertHealthFactor.selector, ILendingProtocol.liquidate.selector); } // Check that liquidation can't happen if the position is healthy // Check that the health factor is improved after liquidation function assertHealthFactor() external { // Get the assertion adopter address ILendingProtocol adopter = ILendingProtocol(ph.getAssertionAdopter()); // Get all liquidation calls in the transaction PhEvm.CallInputs[] memory callInputs = ph.getAllCallInputs(address(adopter), adopter.liquidate.selector); for (uint256 i = 0; i < callInputs.length; i++) { address borrower; uint256 seizedAssets; uint256 repaidDebt; // Decode liquidation parameters (borrower, seizedAssets, repaidDebt) = abi.decode(callInputs[i].input, (address, uint256, uint256)); // Validate liquidation amounts require(seizedAssets > 0, "Zero assets seized"); require(repaidDebt > 0, "Zero debt repaid"); // Check health factor before liquidation PhEvm.ForkId memory preCallFork = PhEvm.ForkId({forkType: 2, callIndex: callInputs[i].id}); uint256 preHealthFactor = adopter.healthFactor(borrower); require(preHealthFactor <= LIQUIDATION_THRESHOLD, "Account not eligible for liquidation"); // Check health factor after liquidation PhEvm.ForkId memory postCallFork = PhEvm.ForkId({forkType: 3, callIndex: callInputs[i].id}); uint256 postHealthFactor = adopter.healthFactor(borrower); // Verify the liquidation actually improved the position's health require(postHealthFactor > preHealthFactor, "Health factor did not improve after liquidation"); // Ensure the position is now in a safe state above the minimum required health factor require(postHealthFactor >= MIN_HEALTH_FACTOR, "Position still unhealthy after liquidation"); } } } // Simplified lending protocol interface interface ILendingProtocol { function liquidate(address borrower, uint256 seizedAssets, uint256 repaidDebt) external returns (uint256, uint256); function isHealthy(address user) external view returns (bool); function healthFactor(address user) external view returns (uint256); } ``` Full examples and mock protocol code are available in [credible-std](https://github.com/phylaxsystems/credible-std/tree/master/examples/assertions-book). ## Related Patterns * [ERC4626 Assets to Shares](/assertions-book/assertions/ass12-erc4626-assets-to-shares) * [Lending Health Factor](/assertions-book/assertions/ass07-lending-health-factor) # Emergency State Validation Source: https://docs.phylax.systems/assertions-book/assertions/ass17-panic-state-validation Ensure protocol behaves correctly during emergency pause states ## When to Use This Pattern Ensures protocols maintain proper security controls during emergency pause states, allowing existing users to withdraw funds while preventing new deposits. Critical for yield aggregators and vaults (Yearn, Beefy), lending protocols with pause mechanisms, DEXs with emergency circuit breakers, cross-chain bridges with pause functionality, and any protocol with emergency pause capabilities. Improper handling of pause states can lead to fund lockups, unauthorized access, or users being unable to exit during emergencies. ## What This Pattern Checks Monitors protocol balance and pause state to ensure proper emergency behavior using a multi-layered approach: * `_preTx()` / `_postTx()` with Reshiram snapshot reads: Capture protocol state before and after transaction * `ph.loadStateAt()`: Read the pause and balance slots at pre-transaction and post-transaction snapshots * `registerFnCallTrigger()`: Monitor all function calls to the contract * Verify protocol balance can only decrease when paused (allowing withdrawals) * Detect unauthorized modifications during pause periods The assertion ensures users can withdraw funds during emergencies while preventing new deposits and maintaining protocol state consistency. > **Note:** In the future, this assertion could be optimized with a new trigger type that only fires when a specific storage slot has a specific value (e.g., when the pause flag is true). This would reduce unnecessary assertion checks and improve efficiency. For more information about cheatcodes, see the [Cheatcodes Documentation](/credible/cheatcodes-reference). ## Assertion Pattern ```solidity theme={null} // 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"; contract EmergencyStateAssertion is Assertion { bytes32 internal constant PAUSED_SLOT = bytes32(uint256(0)); bytes32 internal constant BALANCE_SLOT = bytes32(uint256(1)); constructor() { registerAssertionSpec(AssertionSpec.Reshiram); } function triggers() external view override { registerTxEndTrigger(this.assertionPanickedCanOnlyDecreaseBalance.selector); } /// @notice Checks that a paused protocol cannot increase its stored balance. function assertionPanickedCanOnlyDecreaseBalance() external view { address adopter = ph.getAssertionAdopter(); PhEvm.ForkId memory preFork = _preTx(); PhEvm.ForkId memory postFork = _postTx(); bool wasPaused = uint256(ph.loadStateAt(adopter, PAUSED_SLOT, preFork)) != 0; if (!wasPaused) { return; } uint256 preBalance = uint256(ph.loadStateAt(adopter, BALANCE_SLOT, preFork)); uint256 postBalance = uint256(ph.loadStateAt(adopter, BALANCE_SLOT, postFork)); require(postBalance <= preBalance, "Balance can only decrease when panicked"); } } ``` Full examples and mock protocol code are available in [credible-std](https://github.com/phylaxsystems/credible-std/tree/master/examples/assertions-book). ## Related Patterns * [Implementation Address Change](/assertions-book/assertions/ass01-impl-addr-change) * [Owner Change](/assertions-book/assertions/ass05-ownership-change) # Harvest Increases Balance Source: https://docs.phylax.systems/assertions-book/assertions/ass18-harvest-increases-balance Make sure that the balance increases after a harvest ## When to Use This Pattern Ensures harvest operations in yield farming protocols maintain integrity by preventing balance decreases and price per share manipulation. Critical for yield farming protocols (Beefy, Yearn, Harvest), liquidity mining programs, staking protocols with reward distribution, and auto-compounding vaults. Incorrect harvest implementations could lead to loss of user funds, price per share manipulation enabling flash loan attacks, or protocol insolvency through improper reward distribution. ## What This Pattern Checks Implements multi-layered approach to verify harvest operations: * `_preTx()` / `_postTx()` with Reshiram snapshot reads: Capture vault balance and price per share before/after harvest * `ph.loadStateAt()`: Read balance and price-per-share slots before and after the harvest call * `registerFnCallTrigger()`: Trigger on harvest function calls * Ensures balance hasn't decreased (can stay same if harvested recently) * Confirms price per share hasn't decreased * Prevents manipulation through multiple harvest calls The assertion verifies each balance change is valid relative to previous state, ensuring no balance decreases occur at any point and maintaining protocol solvency. For more information about cheatcodes, see the [Cheatcodes Documentation](/credible/cheatcodes-reference). ## Assertion Pattern ```solidity theme={null} // 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"; contract BeefyHarvestAssertion is Assertion { bytes32 internal constant BALANCE_SLOT = bytes32(uint256(0)); bytes32 internal constant PRICE_PER_SHARE_SLOT = bytes32(uint256(1)); constructor() { registerAssertionSpec(AssertionSpec.Reshiram); } function triggers() external view override { registerFnCallTrigger(this.assertionHarvestIncreasesBalance.selector, IBeefyVault.harvest.selector); } /// @notice Checks that a harvest does not reduce vault balance or price per share. function assertionHarvestIncreasesBalance() external view { address vault = ph.getAssertionAdopter(); PhEvm.TriggerContext memory ctx = ph.context(); PhEvm.ForkId memory preCall = PhEvm.ForkId({forkType: 2, callIndex: ctx.callStart}); PhEvm.ForkId memory postCall = PhEvm.ForkId({forkType: 3, callIndex: ctx.callEnd}); uint256 preBalance = uint256(ph.loadStateAt(vault, BALANCE_SLOT, preCall)); uint256 postBalance = uint256(ph.loadStateAt(vault, BALANCE_SLOT, postCall)); uint256 prePricePerShare = uint256(ph.loadStateAt(vault, PRICE_PER_SHARE_SLOT, preCall)); uint256 postPricePerShare = uint256(ph.loadStateAt(vault, PRICE_PER_SHARE_SLOT, postCall)); require(postBalance >= preBalance, "Harvest decreased balance"); require(postPricePerShare >= prePricePerShare, "Price per share decreased after harvest"); } } interface IBeefyVault { function harvest(bool badHarvest) external; } ``` Full examples and mock protocol code are available in [credible-std](https://github.com/phylaxsystems/credible-std/tree/master/examples/assertions-book). ## Related Patterns * [ERC4626 Assets to Shares](/assertions-book/assertions/ass12-erc4626-assets-to-shares) * [ERC20 Cumulative Outflow Breaker](/assertions-book/assertions/ass20-erc20-drain) * [Price Within Ticks](/assertions-book/assertions/ass15-price-within-ticks) # Tokens Borrowed Invariant Source: https://docs.phylax.systems/assertions-book/assertions/ass19-tokens-borrowed-invariant Make sure that the tokens borrowed are not more than the tokens deposited ## When to Use This Pattern Ensures the fundamental lending protocol invariant that total tokens borrowed never exceed total tokens deposited, preventing protocol insolvency and ensuring withdrawal requests can be honored. Critical for lending and borrowing platforms (Aave, Compound, Morpho), money markets with deposit/borrow pools, yield aggregators implementing lending strategies, and synthetic asset protocols with collateralized debt positions. Violating this invariant could lead to protocol insolvency, loss of user funds, or destabilization of dependent DeFi ecosystems. ## What This Pattern Checks Implements straightforward verification that total tokens borrowed never exceed total tokens deposited: * `_postTx()`: Capture protocol state after transaction to verify invariant holds * `registerTxEndTrigger()`: Trigger on storage slots tracking supply and borrow totals * Check total supply of assets (tokens deposited) and total borrowed assets * Assert total supply ≥ total borrowed assets The assertion verifies final state after all transaction operations complete, ensuring the invariant holds at transaction boundaries. This is a known limitation - we cannot capture intermediate state changes during execution, only the final result. For more information about cheatcodes, see the [Cheatcodes Documentation](/credible/cheatcodes-reference). ## Assertion Pattern ```solidity theme={null} // 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"; contract TokensBorrowedInvariant is Assertion { bytes32 internal constant TOTAL_SUPPLY_SLOT = bytes32(uint256(0)); bytes32 internal constant TOTAL_BORROW_SLOT = bytes32(uint256(1)); constructor() { registerAssertionSpec(AssertionSpec.Reshiram); } function triggers() external view override { registerTxEndTrigger(this.assertBorrowedInvariant.selector); } /// @notice Checks that total supplied assets cover total borrowed assets after the transaction. function assertBorrowedInvariant() external view { address market = ph.getAssertionAdopter(); PhEvm.ForkId memory postFork = _postTx(); uint256 totalSupplyAsset = uint256(ph.loadStateAt(market, TOTAL_SUPPLY_SLOT, postFork)); uint256 totalBorrowedAsset = uint256(ph.loadStateAt(market, TOTAL_BORROW_SLOT, postFork)); require( totalSupplyAsset >= totalBorrowedAsset, "INVARIANT VIOLATION: Total supply of assets is less than total borrowed assets" ); } } ``` Full examples and mock protocol code are available in [credible-std](https://github.com/phylaxsystems/credible-std/tree/master/examples/assertions-book). ## Related Patterns * [Liquidation Health Factor](/assertions-book/assertions/ass16-liquidation-health-factor) * [ERC20 Cumulative Outflow Breaker](/assertions-book/assertions/ass20-erc20-drain) * [Lending Health Factor](/assertions-book/assertions/ass07-lending-health-factor) # ERC20 Cumulative Outflow Breaker Source: https://docs.phylax.systems/assertions-book/assertions/ass20-erc20-drain Limit cumulative ERC20 outflows with a Reshiram circuit-breaker trigger ## When to Use This Pattern Monitors and limits cumulative token outflows to prevent catastrophic asset loss during exploits, creating a response window for protocol operators. Use it for lending reserves, vault custody, bridge escrows, treasuries, liquidity pools, and other contracts where rapid ERC20 withdrawals are a critical risk. This is a V2 Reshiram circuit-breaker pattern. The trigger/precompile machinery collects token outflow into one bucket per block and evaluates those per-block buckets over the rolling window. The assertion does not need its own storage for this accounting. ## What This Pattern Checks Registers a percentage-based cumulative outflow limit: * `registerAssertionSpec(AssertionSpec.Reshiram)`: Registers the assertion as a Reshiram assertion. * `watchCumulativeOutflow(token, thresholdBps, windowDuration, assertFn)`: Collects ERC20 outflow into one bucket per block and watches the buckets over a rolling window. * `ph.outflowContext()`: Reads the token context inside the triggered assertion. * Reverts when cumulative outflow breaches the configured threshold. The assertion does not manually store balances or rolling counters. The Reshiram circuit-breaker trigger tracks the per-block buckets across the window and invokes the assertion when the limit is exceeded. The current Phylax app and Linea deployment support the V1 assertion specification. Treat this V2 Reshiram pattern as a local or development example until the target deployment supports V2. For more information about cheatcodes, see the [Cheatcodes Documentation](/credible/cheatcodes-reference). ## Assertion Pattern ```solidity theme={null} // 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"; contract ERC20CumulativeOutflowBreakerAssertion is Assertion { address public immutable monitoredToken; uint256 public immutable outflowThresholdBps; uint256 public immutable outflowWindowDuration; constructor(address monitoredToken_, uint256 outflowThresholdBps_, uint256 outflowWindowDuration_) { registerAssertionSpec(AssertionSpec.Reshiram); monitoredToken = monitoredToken_; outflowThresholdBps = outflowThresholdBps_; outflowWindowDuration = outflowWindowDuration_; } function triggers() external view override { watchCumulativeOutflow( monitoredToken, outflowThresholdBps, outflowWindowDuration, this.assertCumulativeOutflow.selector ); } /// @notice Reverts when cumulative token outflow breaches the rolling-window limit. /// @dev The Reshiram trigger tracks the window and calls this function only after breach. function assertCumulativeOutflow() external view { PhEvm.OutflowContext memory ctx = ph.outflowContext(); require(ctx.token == monitoredToken, "ERC20Outflow: wrong token context"); revert("ERC20Outflow: cumulative outflow breaker tripped"); } } ``` Full examples and mock protocol code are available in [credible-std](https://github.com/phylaxsystems/credible-std/tree/master/examples/assertions-book). ## Related documentation * [Circuit breakers](./circuit-breakers) * [`outflowRate` and `inflowRate`](./rate-of-change-circuit-breakers) * [ERC20 Cumulative Inflow Breaker](/assertions-book/assertions/ass22-erc20-inflow-breaker) * [Ether Drain](/assertions-book/assertions/ass21-ether-drain) * [Ownership Change](/assertions-book/assertions/ass05-ownership-change) * [Implementation Address Change](/assertions-book/assertions/ass01-impl-addr-change) # Ether Drain Source: https://docs.phylax.systems/assertions-book/assertions/ass21-ether-drain Make sure that ether is not drained from a contract ## When to Use This Pattern Prevents rapid ETH draining by limiting sudden large withdrawals, giving protocols time to respond to potential exploits. Critical for DeFi lending platforms using ETH as collateral, cross-chain bridges with large ETH reserves, DAOs and protocol treasuries, staking protocols managing ETH deposits, yield aggregators holding ETH, and centralized exchanges. Malicious actors often attempt to extract all available ETH in a single transaction after discovering exploits, leading to catastrophic fund loss. > **Real-world example:** In February 2025, Bybit suffered one of the largest hacks in crypto history, losing approximately \$1.4 billion USD when attackers compromised Safe Wallet's UI and changed the implementation address of their proxy contract. This allowed the attackers to drain all assets without requiring additional approvals from the original owners. ETH drain assertions, especially with whitelist functionality, could have prevented or significantly limited the impact of this attack. See the [Bybit Safe UI attack](/assertions-book/previous-hacks/bybit-safe-ui) for more details. ## What This Pattern Checks Implements tiered protection strategy to detect rapid ETH draining: * `_preTx()` / `_postTx()` with Reshiram snapshot reads: Capture contract's ETH balance and whitelist balances before/after transaction * `registerTxEndTrigger()`: Trigger when ETH balances change * For small withdrawals (below threshold): Allow regardless of destination * For large withdrawals (above threshold): Require destination to be whitelisted address * If no whitelist defined, block all large withdrawals as safety measure The tiered approach ensures normal operations with small withdrawals continue uninterrupted while restricting large withdrawals to trusted addresses. For more information about cheatcodes, see the [Cheatcodes Documentation](/credible/cheatcodes-reference). ## Assertion Pattern ```solidity theme={null} // 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"; contract EtherDrainAssertion is Assertion { constructor() { registerAssertionSpec(AssertionSpec.Reshiram); } // Maximum percentage of ETH that can be drained in a single transaction (10% by default) uint256 public constant MAX_DRAIN_PERCENTAGE = 10; function triggers() external view override { // Register a trigger that activates when the ETH balance of the monitored contract changes registerTxEndTrigger(this.assertionEtherDrain.selector); } // Combined assertion for ETH drain with whitelist logic function assertionEtherDrain() external { // Get the assertion adopter address (this is the contract we're monitoring) address exampleContract = ph.getAssertionAdopter(); // Capture the ETH balance before transaction execution PhEvm.ForkId memory preFork = _preTx(); uint256 preBalance = address(exampleContract).balance; // Capture the ETH balance after transaction execution PhEvm.ForkId memory postFork = _postTx(); uint256 postBalance = address(exampleContract).balance; // Only check for drainage (we don't care about ETH being added) if (preBalance > postBalance) { // Calculate the amount drained and the maximum allowed drain uint256 drainAmount = preBalance - postBalance; uint256 maxAllowedDrain = (preBalance * MAX_DRAIN_PERCENTAGE) / 100; // If drain amount is within allowed limit, allow the transaction if (drainAmount <= maxAllowedDrain) { return; // Small drain, no need to check whitelist } // For large drains, we would need to check whitelist // Since we can't easily access constructor parameters in the new interface, // we'll use a simplified approach that just checks the drain percentage // In a real implementation, this would be more sophisticated revert("Large ETH drain detected - exceeds allowed percentage"); } } } interface IExampleContract {} ``` Full examples and mock protocol code are available in [credible-std](https://github.com/phylaxsystems/credible-std/tree/master/examples/assertions-book). ## Related Patterns * [ERC20 Cumulative Outflow Breaker](/assertions-book/assertions/ass20-erc20-drain) * [Implementation Address Change](/assertions-book/assertions/ass01-impl-addr-change) * [Ownership Change](/assertions-book/assertions/ass05-ownership-change) # ERC20 Cumulative Inflow Breaker Source: https://docs.phylax.systems/assertions-book/assertions/ass22-erc20-inflow-breaker Limit cumulative ERC20 inflows with a Reshiram circuit-breaker trigger ## When to Use This Pattern Use this pattern when unexpected inflows can distort protocol accounting, prices, or risk controls. It applies to lending vault donations, AMM reserve stuffing, bridged-asset accounting, staking receipt-token systems, and other protocols where excessive token inflow over a short window is suspicious. This is a V2 Reshiram circuit-breaker pattern. The trigger/precompile machinery collects token inflow into one bucket per block and evaluates those per-block buckets over the rolling window. The assertion does not need its own storage for this accounting. ## What This Pattern Checks Registers a percentage-based cumulative inflow limit: * `registerAssertionSpec(AssertionSpec.Reshiram)`: Registers the assertion as a Reshiram assertion. * `watchCumulativeInflow(token, thresholdBps, windowDuration, assertFn)`: Collects ERC20 inflow into one bucket per block and watches the buckets over a rolling window. * `ph.inflowContext()`: Reads the token context inside the triggered assertion. * Reverts when cumulative inflow breaches the configured threshold. The assertion does not manually store balances or rolling counters. The Reshiram circuit-breaker trigger tracks the per-block buckets across the window and invokes the assertion when the limit is exceeded. The current Phylax app and Linea deployment support the V1 assertion specification. Treat this V2 Reshiram pattern as a local or development example until the target deployment supports V2. For more information about cheatcodes, see the [Cheatcodes Documentation](/credible/cheatcodes-reference). ## Assertion Pattern ```solidity theme={null} // 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"; contract ERC20CumulativeInflowBreakerAssertion is Assertion { address public immutable monitoredToken; uint256 public immutable inflowThresholdBps; uint256 public immutable inflowWindowDuration; constructor(address monitoredToken_, uint256 inflowThresholdBps_, uint256 inflowWindowDuration_) { registerAssertionSpec(AssertionSpec.Reshiram); monitoredToken = monitoredToken_; inflowThresholdBps = inflowThresholdBps_; inflowWindowDuration = inflowWindowDuration_; } function triggers() external view override { watchCumulativeInflow( monitoredToken, inflowThresholdBps, inflowWindowDuration, this.assertCumulativeInflow.selector ); } /// @notice Reverts when cumulative token inflow breaches the rolling-window limit. /// @dev The Reshiram trigger tracks the window and calls this function only after breach. function assertCumulativeInflow() external view { PhEvm.InflowContext memory ctx = ph.inflowContext(); require(ctx.token == monitoredToken, "ERC20Inflow: wrong token context"); revert("ERC20Inflow: cumulative inflow breaker tripped"); } } ``` Full examples and mock protocol code are available in [credible-std](https://github.com/phylaxsystems/credible-std/tree/master/examples/assertions-book). ## Related documentation * [Circuit breakers](./circuit-breakers) * [`outflowRate` and `inflowRate`](./rate-of-change-circuit-breakers) * [ERC20 Cumulative Outflow Breaker](/assertions-book/assertions/ass20-erc20-drain) * [ERC4626 Assets to Shares](/assertions-book/assertions/ass12-erc4626-assets-to-shares) * [Sum of All Positions](/assertions-book/assertions/ass08-sum-of-all-positions) # Intra-tx Oracle Deviation Source: https://docs.phylax.systems/assertions-book/assertions/ass28-intra-tx-oracle-deviation Assert that oracle price updates stay within an acceptable deviation range ## When to Use This Pattern Monitors oracle price updates to detect and prevent price manipulation within a single transaction, protecting against flash loan attacks and malicious arbitrage. Critical for AMM-based DEXs using oracle prices, lending protocols relying on oracles for collateral valuation, synthetic asset platforms, derivatives protocols using oracles for settlement, and yield farming platforms calculating rewards based on asset prices. Intra-transaction price manipulations can lead to flash loan attacks, theft of funds through manipulated liquidations, or protocol insolvency due to incorrect asset valuations. ## What This Pattern Checks Implements approach to verify oracle price updates using both pre/post state comparison and intra-transaction inspection: * `_preTx()` / `_postTx()` with Reshiram snapshot reads: Capture oracle price before and after transaction, compare for deviations * `getCallInputs()`: Monitor all price update function calls within transaction * `registerFnCallTrigger()`: Trigger when oracle price update is detected * Verify each update's price parameter against initial price * Enforce no price update can deviate more than maximum allowed percentage The assertion ensures oracle prices remain within acceptable deviation range throughout transaction, detecting and preventing flash loan attacks that attempt to manipulate prices. For more information about cheatcodes, see the [Cheatcodes Documentation](/credible/cheatcodes-reference). ## Assertion Pattern ```solidity theme={null} // 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"; contract IntraTxOracleDeviationAssertion is Assertion { constructor() { registerAssertionSpec(AssertionSpec.Reshiram); } // Maximum allowed price deviation (10% by default) uint256 public constant MAX_DEVIATION_PERCENTAGE = 10; function triggers() external view override { // Register trigger for oracle price update calls registerFnCallTrigger(this.assertOracleDeviation.selector, IOracle.updatePrice.selector); } // Check that price updates don't deviate more than the allowed percentage // from the initial price at any point during the transaction function assertOracleDeviation() external { // Get the assertion adopter address IOracle adopter = IOracle(ph.getAssertionAdopter()); // Start with a simple check comparing pre and post state PhEvm.ForkId memory preFork = _preTx(); uint256 prePrice = adopter.price(); // Calculate allowed deviation thresholds (10% by default) uint256 maxAllowedPrice = (prePrice * (100 + MAX_DEVIATION_PERCENTAGE)) / 100; uint256 minAllowedPrice = (prePrice * (100 - MAX_DEVIATION_PERCENTAGE)) / 100; // First check post-state price PhEvm.ForkId memory postFork = _postTx(); uint256 postPrice = adopter.price(); // Verify post-state price is within allowed deviation from initial price require( postPrice >= minAllowedPrice && postPrice <= maxAllowedPrice, "Oracle post-state price deviation exceeds threshold" ); // Get all price update calls in this transaction // Since this assertion is triggered by updatePrice calls, we know there's at least one PhEvm.CallInputs[] memory priceUpdates = ph.getCallInputs(address(adopter), adopter.updatePrice.selector); // Check each price update to ensure none deviate more than allowed from initial price for (uint256 i = 0; i < priceUpdates.length; i++) { PhEvm.ForkId memory postCallFork = PhEvm.ForkId({forkType: 3, callIndex: priceUpdates[i].id}); // Call the price function at the given frame in the call stack uint256 updatedPrice = adopter.price(); // Verify each update is within allowed deviation from initial pre-state price require( updatedPrice >= minAllowedPrice && updatedPrice <= maxAllowedPrice, "Oracle intra-tx price deviation exceeds threshold" ); } } } interface IOracle { function updatePrice(uint256 price) external; function price() external view returns (uint256); } ``` Full examples and mock protocol code are available in [credible-std](https://github.com/phylaxsystems/credible-std/tree/master/examples/assertions-book). ## Related Patterns * [Oracle Validation](/assertions-book/assertions/ass10-oracle-validation) * [TWAP Deviation](/assertions-book/assertions/ass11-twap-deviation) * [Price Within Ticks](/assertions-book/assertions/ass15-price-within-ticks) # Circuit breakers Source: https://docs.phylax.systems/assertions-book/assertions/circuit-breakers Overview of cumulative and rate-of-change circuit breakers for ERC20 balance changes Circuit breakers enforce configured limits on ERC20 balance changes. They can reject a candidate transaction before it settles. This page compares cumulative and rate-of-change controls. ## What they watch * **Adopter:** The contract protected by the assertion. * **Token:** The ERC20 balance being watched. * **Direction:** Tokens entering or leaving the adopter. * **Time:** Balance changes across blocks and transactions. ## Circuit breaker types Limits net tokens leaving the adopter over a rolling window. Limits net tokens entering the adopter over a rolling window. Lets an assertion limit how quickly the watched balance changes. ## How cumulative and rate limits work together Cumulative and rate-of-change limits use different semantics. A cumulative limit measures total net flow over a rolling window, while a rate limit measures how quickly the balance changes. An assertion can enforce either policy or both. Both policies use a matching cumulative watcher to invoke the assertion. For a rate limit, the assertion reads the rolling-window rate data during that callback. | Risk | Circuit breaker | | ---------------------------------------------- | ----------------------------- | | Too many tokens leave over time | Cumulative outflow | | Too many tokens enter over time | Cumulative inflow | | The balance changes too quickly | Rate of change | | Total flow and flow speed must both be bounded | Cumulative and rate of change | When checks are combined, the assertion can reject a transaction when either limit is exceeded. ## Why use a Phylax circuit breaker A protocol-integrated circuit breaker protects the execution paths wired through it. A Phylax circuit breaker runs as an assertion before the transaction settles. It watches the actual ERC20 balance change of the adopter. | | Protocol-integrated circuit breaker | Phylax circuit breaker | | ------------- | ----------------------------------------------------- | -------------------------------------------------------------- | | Coverage | Covers paths integrated with the breaker | Covers observed changes to the adopter's watched ERC20 balance | | Measurement | Defined by the protocol integration | Uses the observed balance change | | Time window | May require counters or buckets in protocol storage | Keeps rolling buckets outside the protected protocol | | Protocol code | Adds hooks, state, and audit surface | Adds no breaker code or storage to the protocol | | User gas | May include breaker calls and storage writes | Adds no protocol-side gas for breaker accounting | | Changes | Integration may require a protocol upgrade or wrapper | Uses an assertion release without changing protocol code | Because enforcement runs as an assertion, the protocol does not need breaker-specific hooks or storage. The assertion can reject a candidate transaction when it exceeds the configured policy. ## Bucket ingestion and balance reconstruction On mainnet, the per-block buckets behind a cumulative watcher are not written while a block is being built. The executor ingests each complete canonical block after it has been executed, using the block's ERC20 `Transfer` logs and the adopter's post-block token balance. Ingestion runs concurrently with block building, so bucket history can lag the chain tip and a candidate transaction can be validated before the buckets for one or more recent blocks exist. Ingested blocks can also land partway through building a block. Each transaction reads the latest ingested history at the time it is validated, so two transactions in the same block can be evaluated against different histories: an earlier one against reconstructed buckets and a later one against exact buckets. We do not expect history to be behind by more than one block on a regular basis, and any practical window is far longer than that. The missing blocks are always the newest blocks before the candidate transaction, so they lie inside the rolling window. The rest of this section assumes that. When the history is behind, the executor still runs the check. It reconstructs the missing buckets for that evaluation only: 1. It derives the adopter's token balance immediately before the candidate transaction from the current state and compares it with the balance recorded in the latest known bucket. 2. It treats the difference as the net flow of the gap and spreads it evenly across the missing blocks, interpolating bucket timestamps between the last known block and the candidate block. If only earlier transactions in the current block are missing, the difference is added to the current block's bucket instead. 3. It evaluates the threshold against the reconstructed window plus the candidate transaction's own transfers. Reconstructed buckets are never persisted. Durable history is updated only by block ingestion, so as soon as the missing blocks are ingested, later transactions are evaluated against the exact per-block data. ### Effect on the circuit breaker trigger When a transaction arrives at block N and the last stored bucket is block M with M \< N-1, the blocks in between are missing. We pick the last stored bucket as the anchor, and we fill the gap like this: 1. Compare the anchor's end-of-block balance with the candidate's pre-transaction balance. 2. Divide the difference evenly across the missing blocks. 3. Splice those fake buckets into a clone of the state and evaluate on it. The fake buckets are thrown away and not persisted. Because the missing blocks lie inside the window, the reconstructed buckets sum exactly to the real net balance change of the gap, and the cumulative check sees the same net flow it would see with complete buckets. **False triggers can only occur at the window boundary.** If a missing block has already aged out of the window, the even split still drops a share of that block's movement into the later gap blocks, which are inside the window. This requires history to be behind by more than the window itself, which we do not expect to happen: ```mermaid theme={null} flowchart LR B1["Bucket 1 · stored anchor
expired"] B2["Bucket 2 · missing
actual: 150 out
reconstructed: 50
expired"] subgraph WINDOW["Active window · buckets 3–5"] direction LR B3["Bucket 3 · missing
actual: 0
reconstructed: 50"] B4["Bucket 4 · missing
actual: 0
reconstructed: 50"] B5["Bucket 5 · candidate
current flow: ε ≥ 0"] B3 --> B4 --> B5 end RESULT["Threshold 100
actual in window: ε · PASS
reconstructed: 100 + ε ≥ 100 · FALSE TRIGGER"] B1 --> B2 B2 -. "150 delta is split evenly
across blocks 2–4" .-> B3 B5 --> RESULT classDef expired fill:#E2E8F0,stroke:#475569,color:#0F172A,stroke-width:1.5px classDef reconstructed fill:#FEF3C7,stroke:#B45309,color:#78350F,stroke-width:2px classDef current fill:#DBEAFE,stroke:#1D4ED8,color:#1E3A8A,stroke-width:1.5px classDef failure fill:#FEE2E2,stroke:#B91C1C,color:#7F1D1D,stroke-width:2px class B1,B2 expired class B3,B4 reconstructed class B5 current class RESULT failure style WINDOW fill:#EFF6FF,stroke:#2563EB,color:#1E3A8A,stroke-width:1px ``` Gross flow is a separate matter. Inflows and outflows that offset each other inside the gap cancel out in the balance difference, so the reconstructed gross outflow is always less than or equal to the real gross outflow. A limit on gross flow can therefore undercount while history is behind. We don't recommend any direct changes to your circuit breaker design for this edge case. ### Effect on trigger context Reconstruction recovers the exact net balance change, but not the individual transfers behind it. Inflows and outflows that offset each other within the gap cancel out and cannot be recovered. | Context fields | Under reconstruction | | ------------------------------------------- | ------------------------------------------------------------------------------ | | `cumulativeOutflow`, `cumulativeInflow` | Exact. Net flow is derived from the balance difference. | | `absoluteOutflow`, `absoluteInflow` | May undercount. Only the net direction of the gap is attributed as gross flow. | | `peakRateBps`, `lastRateBps`, `meanRateBps` | Approximate. Gap flow is spread evenly across the missing blocks. | | `tvlSnapshot`, `windowStart`, `currentBps` | Approximate when the earliest retained bucket falls inside the gap. | An assertion that enforces a limit on `absoluteOutflow` or `absoluteInflow` can miss gross flow that occurred while bucket history was behind, so it may accept a transaction it would reject with complete buckets. If your circuit breaker uses `absoluteOutflow` or `absoluteInflow` to get the total token flow values, please be aware that the values you are reading might be derived from the above mechanism and approximate. Please keep this in mind when designing the limits, as the gross figures can undercount. ## Monitoring and incident response Circuit breakers constrain token flow rather than a specific attack path, so they can limit the impact of different exploit classes, including attacks that begin with oracle manipulation. They bound flow within the configured rolling window; they do not replace monitoring or incident response. Choose a window long enough for your team to receive an invalidation alert, investigate, and apply mitigation before earlier flow ages out of the window. Before production, [validate the threshold and window in staging](../../credible/testing-strategy#monitor-staging-behavior) and [configure invalidation notifications](../../credible/dapp-integrations). # Optimism FMA Suite Source: https://docs.phylax.systems/assertions-book/assertions/optimism-fma-suite Assertions for Optimism's Failure Mode Analysis We've created a comprehensive suite of assertions based on Optimism's Failure Mode Analysis (FMA) framework to prevent critical failure modes identified in the protocol. Optimism's FMA process systematically identifies, analyzes, and mitigates potential failure modes. As documented in their [security design docs](https://github.com/ethereum-optimism/design-docs/tree/main/security), FMAs "shift-left" risk assessment so mitigations can be planned and implemented earlier. We chose Optimism's FMA framework because it represents a comprehensive and well-documented approach to security analysis. The protocol has conducted extensive failure mode analyses across various components including the Interop Portal, ETH Lockbox, Message Passing contracts, and more. This makes it an excellent case study for demonstrating how assertions can prevent specific failure modes identified through systematic security analysis. **Link to the Phylax fork of Optimism: [https://github.com/phylaxsystems/optimism/tree/feat/fma-assertions/packages/contracts-bedrock/assertions](https://github.com/phylaxsystems/optimism/tree/feat/fma-assertions/packages/contracts-bedrock/assertions)** ## Approach Our approach follows the same systematic methodology used in Optimism's FMA process. We analyze each identified failure mode and create assertions that prevent the conditions that could lead to those failures. The key insight is that many failure modes identified in FMAs can be prevented by enforcing invariants at the transaction level. For example, if an FMA identifies that "incorrect state reporting by AnchorStateRegistry" could lead to withdrawal safety failures, we can write assertions that validate state consistency before allowing withdrawal transactions to proceed. ## Assertion Collections Overview ### [FMA ETH Lockbox Assertions](https://github.com/phylaxsystems/optimism/blob/feat/fma-assertions/packages/contracts-bedrock/assertions/src/fma-eth-lockbox-assertions.a.sol) This collection validates the **ETHLockbox** contract's security properties, corresponding to the [ETH Lockbox FMA document](https://github.com/phylaxsystems/optimism/blob/feat/fma-assertions/packages/contracts-bedrock/assertions/fma/fma-eth-lockbox.md): #### Key Checks: * **FM1: Unauthorized Access Protection** - Ensures only authorized portals can call `lockETH` and `unlockETH` functions * **FM2: Drain Prevention** - Prevents the lockbox from being drained to zero balance in a single transaction * **FM3: Proxy Upgrade Protection** - Monitors for unexpected proxy implementation address changes that could indicate buggy upgrades #### Risk Context: These assertions address **CRITICAL** failure modes where unauthorized access or bugs could lead to complete loss of ETH liquidity from the lockbox, with **HIGH** impact but **LOW** likelihood due to access controls and upgrade procedures. ### [FMA Interop Portal Assertions](https://github.com/phylaxsystems/optimism/blob/feat/fma-assertions/packages/contracts-bedrock/assertions/src/fma-interop-portal.a.sol) This collection validates the **OptimismPortal2** and **AnchorStateRegistry** integration, corresponding to the [Interop Portal FMA document](https://github.com/phylaxsystems/optimism/blob/feat/fma-assertions/packages/contracts-bedrock/assertions/fma/fma-interop-portal.md): #### Key Checks: * **FM1: AnchorStateRegistry Integrity** - Validates retirement timestamp updates, respected game type changes, anchor state transitions, and blacklist operations * **FM2: Migration Logic Safety** - Ensures ETH lockbox and portal migrations maintain fund safety and state consistency * **FM4: SuperRoots Toggle Validation** - Validates that `superRootsActive` flag changes follow proper authorization and state requirements #### Risk Context: These assertions address **CRITICAL** failure modes where incorrect state reporting or migration bugs could lead to **Withdrawal Safety Failure** or **Withdrawal Liveness Failure**, with **LOW** likelihood but **HIGH/CRITICAL** impact. ### [FMA L2 Message Passing Assertions](https://github.com/phylaxsystems/optimism/blob/feat/fma-assertions/packages/contracts-bedrock/assertions/src/fma-l2-message-passing.a.sol) This collection validates cross-chain message passing contracts, corresponding to the [Message Passing FMA document](https://github.com/phylaxsystems/optimism/blob/feat/fma-assertions/packages/contracts-bedrock/assertions/fma/fma-message-passing-contracts.md): #### Key Checks: * **FM1: Destination Chain Validation** - Ensures messages aren't sent to invalid destinations (same chain, zero chain ID, etc.) * **FM2: Message Validation Integrity** - Validates message identifiers and parameters for cross-chain message validation * **FM3: Message Relay Completeness** - Ensures sent messages are properly recorded and can be relayed * **FM4: Replay Protection** - Prevents duplicate message execution through proper `successfulMessages` tracking * **FM5: Reentrancy Protection** - Ensures message relay functions are atomic and non-reentrant * **FM6: Repeated Identifier Validation** - Prevents duplicate identifier usage within the same transaction #### Risk Context: These assertions address **CRITICAL** failure modes where message passing bugs could lead to asset theft, duplicate minting, or lost funds, with **MEDIUM** likelihood and **HIGH/CRITICAL** impact depending on the specific failure mode. # outflowRate and inflowRate Source: https://docs.phylax.systems/assertions-book/assertions/rate-of-change-circuit-breakers Reference for the flow-rate context returned by cumulative ERC20 flow triggers `ph.outflowRate()` and `ph.inflowRate()` return rate statistics for the rolling window that caused a cumulative ERC20 flow trigger to invoke an assertion. The getters take no arguments, do not register a trigger, and do not enforce a rate limit. An assertion that calls either getter must register `AssertionSpec.Experimental`; Legacy and Reshiram assertions cannot call them. ## Interface ```solidity theme={null} struct FlowRateContext { address token; uint256 peakRateBps; uint256 lastRateBps; uint256 meanRateBps; uint256 tvlSnapshot; uint256 windowStart; uint256 windowEnd; } function outflowRate() external view returns (FlowRateContext memory ctx); function inflowRate() external view returns (FlowRateContext memory ctx); ``` Use each getter only in the matching cumulative trigger callback: | Getter | Matching trigger | | ------------------ | ----------------------------- | | `ph.outflowRate()` | `watchCumulativeOutflow(...)` | | `ph.inflowRate()` | `watchCumulativeInflow(...)` | ## When it runs After deployment, the cumulative watcher tracks the assertion adopter's balance changes for the configured ERC20 token. It invokes the registered assertion function when net inflow or outflow is strictly greater than `thresholdBps` of the window-start balance. During that invocation, `ph.inflowRate()` or `ph.outflowRate()` returns rate statistics calculated from the same rolling-window data. The getter does not trigger the assertion by itself. ## Directional flow The executor records both inflow and outflow. It derives the directional values as follows: | Context | Per-block flow used for `peakRateBps` and `lastRateBps` | Window flow used for `meanRateBps` | | ------- | ------------------------------------------------------- | ------------------------------------ | | Outflow | `max(blockOutflow - blockInflow, 0)` | `max(totalOutflow - totalInflow, 0)` | | Inflow | `max(blockInflow - blockOutflow, 0)` | `max(totalInflow - totalOutflow, 0)` | Opposite-direction flow therefore offsets the watched direction. The per-block rates clamp each bucket independently, while the mean uses net flow across the entire retained window. ## Rate calculations All three rate fields are integer values measured in basis points of `tvlSnapshot` per second. ### Peak rate For every retained block bucket, the executor calculates: `bucket rate = floor(net block flow × 10,000 ÷ (tvlSnapshot × 10 seconds))` `peakRateBps` is the greatest bucket rate. The denominator always uses 10 seconds; it does not use the chain's actual block interval. ### Latest rate `lastRateBps` is the bucket rate for the most recent retained block. A previous spike can therefore remain in `peakRateBps` while `lastRateBps` falls to a lower value. ### Mean rate The mean uses the active span between the earliest and latest retained buckets: `active span = latest bucket timestamp - earliest bucket timestamp + 10 seconds` `mean rate = floor(net window flow × 10,000 ÷ (tvlSnapshot × active span))` It does not divide by the full configured window when the retained activity covers a shorter span. With one retained bucket, the active span is 10 seconds, so peak, latest, and mean rates are equal. ## Returned fields | Field | Behavior | | ------------- | --------------------------------------------------------------------------------------- | | `token` | Watched ERC20 token. `address(0)` means no matching flow trigger context was available. | | `peakRateBps` | Highest directional block-bucket rate in the retained window. | | `lastRateBps` | Directional rate of the most recent retained block bucket. | | `meanRateBps` | Net directional window flow divided by the active span. | | `tvlSnapshot` | Adopter's token balance immediately before the earliest retained bucket. | | `windowStart` | Timestamp of the earliest retained bucket. | | `windowEnd` | `windowStart + windowDuration`, with saturating addition. | ## Edge cases | Condition | Behavior | | ---------------------------------------------------------------- | ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- | | Getter called without its matching trigger context | Returns a zero-filled `FlowRateContext`. Check `token != address(0)` before using the rate fields. | | Cumulative flow equals the watcher threshold | The watcher does not invoke the assertion. Dispatch requires a strict threshold breach. | | Net directional flow is zero | The watcher does not invoke the assertion, including when its threshold is zero. | | Several changes occur in one block | Their inflow and outflow amounts are accumulated before the block rate is calculated. | | Distinct blocks share the same 10-second period | They remain distinct block buckets, but each rate still uses the fixed 10-second denominator. | | Calculated rate is below `1 bps/s` | Integer division rounds it down to zero. | | `tvlSnapshot` is zero | Nonzero cumulative flow breaches any finite threshold. A nonzero rate calculation returns `type(uint256).max`; a zero-flow bucket still has a zero rate. | | Bucket timestamp equals the window cutoff | The bucket remains in the window because the cutoff is inclusive. | | `windowDuration` is below 10 seconds or does not fit in `uint64` | Trigger registration is rejected. | | Rate multiplication | The executor uses 512-bit intermediate arithmetic before narrowing the result to `uint256`. | | Bucket history lags the block being built | The executor spreads the net balance change of the missing blocks evenly across them, so rate fields are approximate. See [Bucket ingestion and balance reconstruction](./circuit-breakers#bucket-ingestion-and-balance-reconstruction). | ## Calculation example For a `tvlSnapshot` of 100,000 tokens: | Retained outflow | Result | | ---------------------------------- | ------------------------: | | 10,000 tokens in one block | `peakRateBps = 100 bps/s` | | 1,000 tokens in each of ten blocks | `peakRateBps = 10 bps/s` | Both results use the fixed 10-second denominator for each block bucket. The timestamps of the first and last retained blocks determine `meanRateBps`. ## Combined inflow and outflow example This assertion registers both cumulative directions with a low dispatch threshold, reads the matching cumulative and rate contexts, and rejects when either configured limit is exceeded. ```solidity theme={null} theme={null} // 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"; contract ERC20FlowRateCircuitBreakerAssertion is Assertion { // Dispatch early so the assertion can enforce its own cumulative and rate limits. uint256 internal constant DISPATCH_THRESHOLD_BPS = 1; address public immutable monitoredToken; uint256 public immutable windowDuration; uint256 public immutable inflowLimitBps; uint256 public immutable outflowLimitBps; uint256 public immutable inflowPeakRateLimitBps; uint256 public immutable outflowPeakRateLimitBps; constructor( address monitoredToken_, uint256 windowDuration_, uint256 inflowLimitBps_, uint256 outflowLimitBps_, uint256 inflowPeakRateLimitBps_, uint256 outflowPeakRateLimitBps_ ) { registerAssertionSpec(AssertionSpec.Experimental); monitoredToken = monitoredToken_; windowDuration = windowDuration_; inflowLimitBps = inflowLimitBps_; outflowLimitBps = outflowLimitBps_; inflowPeakRateLimitBps = inflowPeakRateLimitBps_; outflowPeakRateLimitBps = outflowPeakRateLimitBps_; } function triggers() external view override { watchCumulativeInflow( monitoredToken, DISPATCH_THRESHOLD_BPS, windowDuration, this.assertInflowWithinLimits.selector ); watchCumulativeOutflow( monitoredToken, DISPATCH_THRESHOLD_BPS, windowDuration, this.assertOutflowWithinLimits.selector ); } function assertInflowWithinLimits() external view { PhEvm.InflowContext memory flow = ph.inflowContext(); PhEvm.FlowRateContext memory rate = ph.inflowRate(); require(flow.token == monitoredToken && rate.token == monitoredToken, "ERC20Flow: bad inflow context"); require(flow.currentBps <= inflowLimitBps, "ERC20Flow: cumulative inflow limit"); require(rate.peakRateBps <= inflowPeakRateLimitBps, "ERC20Flow: peak inflow rate limit"); } function assertOutflowWithinLimits() external view { PhEvm.OutflowContext memory flow = ph.outflowContext(); PhEvm.FlowRateContext memory rate = ph.outflowRate(); require(flow.token == monitoredToken && rate.token == monitoredToken, "ERC20Flow: bad outflow context"); require(flow.currentBps <= outflowLimitBps, "ERC20Flow: cumulative outflow limit"); require(rate.peakRateBps <= outflowPeakRateLimitBps, "ERC20Flow: peak outflow rate limit"); } } ``` Circuit breakers should be paired with invalidation monitoring and an incident-response plan. See [Monitoring and incident response](./circuit-breakers#monitoring-and-incident-response). ## Related documentation * [Circuit breakers](./circuit-breakers) * [ERC20 Cumulative Outflow Breaker](./ass20-erc20-drain) * [ERC20 Cumulative Inflow Breaker](./ass22-erc20-inflow-breaker) * [Circuit-breaker cheatcode reference](../../credible/cheatcodes-reference#circuit-breaker-context) # Assertion Pattern Catalog Source: https://docs.phylax.systems/assertions-book/assertions/use-cases-index Reference catalog of reusable V2 assertion patterns organized by security category Use this page as a reference catalog when you already know the class of risk you want to cover and need a matching assertion pattern. If you want to understand a historical exploit first, use the [hack case studies](../previous-hacks/prev-hacks-index). ## Access Control & Administrative Changes * [**Implementation Address Change**](./ass01-impl-addr-change): Protects against unauthorized changes to proxy implementation addresses, preventing attackers from replacing contract logic with malicious code. * [**KYC Whitelist**](./ass04-kyc-whitelist): Ensures that only KYC accredited users can interact with a contract based on a unified KYC registry. * [**Owner Change**](./ass05-ownership-change): Ensures ownership of a contract cannot be transferred unexpectedly, preventing attackers from gaining administrative control over critical protocol functions. * [**Timelock Verification**](./ass09-timelock-verification): Verifies that administrative actions are executed only after the required timelock period, preventing rushed or malicious changes to protocol parameters. ## Liquidity Pool & AMM Security * [**Constant Product**](./ass06-constant-product): Ensures the constant product formula (k = x \* y) is maintained in AMM pools, preventing price manipulation attacks and unauthorized token drains. * [**Price Within Ticks**](./ass15-price-within-ticks): Verifies that concentrated liquidity positions in AMM protocols maintain prices within expected tick boundaries, protecting against price manipulation. * [**Fee Calculations**](./ass14-fee-calculations): Ensures trading fees are correctly calculated and distributed, preventing fee theft or unexpected losses in AMM protocols. ## Lending Protocol Safety * [**Lending Health Factor**](./ass07-lending-health-factor): Enforces minimum health factor requirements in lending protocols, preventing under-collateralized positions and protecting protocol solvency. * [**Liquidation Health Factor**](./ass16-liquidation-health-factor): Ensures liquidations only occur when health factors fall below the liquidation threshold, protecting borrowers from premature or incorrect liquidations. * [**Sum of All Positions**](./ass08-sum-of-all-positions): Verifies that the sum of all user positions matches the total asset balance, detecting accounting errors or unauthorized fund movements. * [**Tokens Borrowed Invariant**](./ass19-tokens-borrowed-invariant): Enforces that the relationship between borrowed tokens and collateral remains within safe protocol limits, preventing critical invariant violations. ## Oracle Security * [**Oracle Liveness Validation**](./ass10-oracle-validation): Verifies that oracle data is fresh enough for protocol operations that rely on it. * [**TWAP Deviation**](./ass11-twap-deviation): Compares pre-transaction and post-transaction TWAP values and tracks intra-transaction price changes. * [**Intra-tx Oracle Deviation**](./ass28-intra-tx-oracle-deviation): Checks that oracle price updates stay within an allowed deviation range during a transaction. ## Circuit Breakers * [**ERC20 Cumulative Outflow Breaker**](./ass20-erc20-drain): Uses the Reshiram `watchCumulativeOutflow` trigger to collect ERC20 outflow into one bucket per block and limit cumulative outflow over a rolling window. * [**ERC20 Cumulative Inflow Breaker**](./ass22-erc20-inflow-breaker): Uses the Reshiram `watchCumulativeInflow` trigger to collect ERC20 inflow into one bucket per block and limit suspicious cumulative inflow over a rolling window. * [**`outflowRate` and `inflowRate`**](./rate-of-change-circuit-breakers): Reference for the peak, latest, and mean rate contexts exposed to cumulative flow assertions. ## Native Asset Protection * [**Ether Drain**](./ass21-ether-drain): Limits sudden ETH outflows and requires trusted destinations for large withdrawals. ## Vault & ERC4626 Security * [**ERC4626 Assets to Shares**](./ass12-erc4626-assets-to-shares): Verifies correct conversion between assets and shares in ERC4626 vaults, preventing accounting errors that could lead to fund loss. * [**ERC4626 Deposit and Withdraw Share Price**](./ass13-erc4626-deposit-withdraw): Checks that deposit and withdraw calls do not reduce the vault share price across matched call snapshots. * [**Harvest Increases Balance**](./ass18-harvest-increases-balance): Verifies that yield-generating operations like harvests always increase the total balance of vaults, preventing value extraction attacks. ## Emergency & Special Mode Protection * [**Panic State Validation**](./ass17-panic-state-validation): Validates critical protocol state variables during panic or emergency modes, ensuring fallback mechanisms work correctly when normal operations are suspended. *** **Next:** Explore [previous hacks analysis](../previous-hacks/prev-hacks-index) to see how assertions could have prevented real-world exploits. # Abracadabra GMX V2 Cauldron Exploit Source: https://docs.phylax.systems/assertions-book/previous-hacks/abracadabra-gmx-v2-exploit Exploit that drained $13.4M from Abracadabra's GMX V2 Cauldron through accounting manipulation in the RouterOrder system This case study explains how the Abracadabra GMX V2 Cauldron exploit worked and which assertion pattern could have constrained the invalid state transition. ## What Happened This exploit drained \$13.4M from Abracadabra's GMX V2 Cauldron through an accounting bug that created "phantom collateral" - allowing the same tokens to be borrowed against multiple times. **The Core Bug:** The `GmxV2CauldronRouterOrder` contract had two critical functions: * **`sendValueInCollateral()`** - Extracted real tokens during liquidations * **`orderValueInCollateral()`** - Reported collateral value for borrowing calculations Link to the two functions: [https://github.com/Abracadabra-money/abracadabra-money-contracts/blob/dff69a19a219bbff90ab7b752c9f9c0ab5e8fe6f/src/periphery/GmxV2CauldronOrderAgent.sol#L241-L280](https://github.com/Abracadabra-money/abracadabra-money-contracts/blob/dff69a19a219bbff90ab7b752c9f9c0ab5e8fe6f/src/periphery/GmxV2CauldronOrderAgent.sol#L241-L280) When `sendValueInCollateral()` removed tokens, it failed to update internal accounting variables (`inputAmount`, `minOut`, `minOutLong`). This meant `orderValueInCollateral()` continued reporting the original collateral value even after tokens were extracted. **Exploitation Steps:** 1. **Setup**: Attacker creates a failed GMX deposit, leaving tokens in the RouterOrder contract 2. **Exploit Loop**: * Borrow MIM against the reported collateral value * Self-liquidate to extract real tokens via `sendValueInCollateral()` * Internal accounting remains unchanged - same collateral value still reported * Borrow again against the "phantom" collateral * Repeat until all real tokens are drained The attacker could extract real value multiple times while the system's solvency checks continued to pass using stale accounting data. ## Assertion Pattern The core issue was a fundamental violation of a basic invariant: reported collateral values should never exceed actual extractable assets. A simple phantom collateral assertion could have prevented this exploit: ```solidity theme={null} // SPDX-License-Identifier: MIT pragma solidity 0.8.28; import {Assertion} from "../../lib/credible-std/src/Assertion.sol"; import {AssertionSpec} from "../../lib/credible-std/src/SpecRecorder.sol"; import {PhEvm} from "../../lib/credible-std/src/PhEvm.sol"; interface IGmxV2CauldronRouterOrder { function orderValueInCollateral() external view returns (uint256); function shortToken() external view returns (address); function getExchangeRates() external view returns (uint256 shortExchangeRate, uint256 marketExchangeRate); function sendValueInCollateral(address to, uint256 amount) external; } interface IERC20 { function balanceOf(address account) external view returns (uint256); } contract AbracadabraGmxV2Assertion is Assertion { constructor() { registerAssertionSpec(AssertionSpec.Reshiram); } uint256 constant oracleDecimalScale = 1e30; function triggers() public view override { // Trigger on any call to sendValueInCollateral registerFnCallTrigger( this.assertPhantomCollateral.selector, IGmxV2CauldronRouterOrder.sendValueInCollateral.selector ); } function assertPhantomCollateral() external view { IGmxV2CauldronRouterOrder routerOrder = IGmxV2CauldronRouterOrder(ph.getAssertionAdopter()); // Get the reported collateral value from the potentially buggy function uint256 reportedCollateral = routerOrder.orderValueInCollateral(); // Calculate actual extractable value based on real token balance address shortTokenAddr = routerOrder.shortToken(); IERC20 shortToken = IERC20(shortTokenAddr); uint256 actualBalance = shortToken.balanceOf(address(routerOrder)); // Convert to collateral value using the same exchange rates as orderValueInCollateral() (uint256 shortExchangeRate, uint256 marketExchangeRate) = routerOrder.getExchangeRates(); uint256 actualExtractable = (actualBalance * shortExchangeRate * marketExchangeRate) / oracleDecimalScale; // Core invariant: Reported collateral must never exceed actual extractable value require( reportedCollateral <= actualExtractable, "PHANTOM_COLLATERAL: Reported collateral exceeds actual extractable value" ); } } ``` ### How the Assertion Would Have Prevented It This assertion implements a fundamental economic sanity check that would have caught the accounting manipulation: **What it does:** 1. **Captures reported collateral** from the buggy `orderValueInCollateral()` function 2. **Calculates actual extractable value** by checking real token balances 3. **Enforces the invariant** that reported values cannot exceed actual extractable amounts **Why it catches the exploit:** The exploit succeeded because of the growing gap between reported and actual values: * **Before exploit**: RouterOrder has 1000 USDC, `orderValueInCollateral()` returns 1000 USDC equivalent, actual balance = 1000 USDC → **Assertion passes** ✅ * **During exploit**: `sendValueInCollateral()` extracts 500 USDC, but `orderValueInCollateral()` still returns 1000 USDC equivalent, actual balance = 500 USDC → **Assertion fails** ❌ * **After multiple extractions**: All tokens extracted, but `orderValueInCollateral()` still returns 1000 USDC equivalent, actual balance = 0 USDC → **Assertion fails** ❌ **Key insight**: This assertion doesn't need to understand the complex GMX V2 order mechanics or the specific accounting bug. It simply enforces the fundamental principle that "you cannot extract more value than actually exists" - a rule the exploit fundamentally violated. # Abracadabra CauldronV4 Cook Function Exploit Source: https://docs.phylax.systems/assertions-book/previous-hacks/abracadabra-hack-3 Logic flaw in the cook() function allowed bypassing solvency checks, enabling $1.8M in uncollateralized borrowing This case study explains how the Abracadabra CauldronV4 cook function exploit worked and which assertion pattern could have constrained the invalid state transition. ## What Happened A logic flaw in Abracadabra's `cook()` function allowed an attacker to borrow \$1.8M in MIM tokens without posting any collateral. **The Bug:** The `CauldronV4` contract's `cook()` function executes multiple actions in sequence while tracking a `CookStatus` struct. This struct contains a flag indicating whether solvency checks are required. * Action 5 (borrow) sets the solvency check flag to `true` * Action 0 calls `_additionalCookAction()`, which returns a fresh `CookStatus` with all fields set to `false` By chaining \[Action 5, Action 0], the borrow executes and marks that a solvency check is needed. But Action 0 immediately clears this flag before any validation runs. **Exploitation:** 1. Call `cook()` with \[Action 5 (borrow), Action 0] 2. Borrow MIM tokens without collateral 3. Repeat across six cauldron contracts 4. Total stolen: 1,793,755 MIM (\~\$1.8M) ## Assertion Pattern This exploit could have been prevented by enforcing a fundamental invariant: **users cannot borrow without sufficient collateral**. The beauty of this approach is that it doesn't require understanding the exploit's specific mechanism. Developers don't need to know about: * The `CookStatus` struct and how it tracks solvency checks * The `_additionalCookAction()` helper function that resets flags * The specific action sequence \[Action 5, Action 0] that triggers the bug * How the internal solvency check logic works Instead, an assertion simply states the protocol's core rule: after any transaction, if a user's borrow increased, their collateral must cover the debt. This works regardless of which code path led to the borrow or what internal checks were bypassed. **Why This Matters:** Complex protocols like Abracadabra have many functions and execution paths. The `cook()` function alone can execute dozens of different action combinations. Trying to secure each path individually is error-prone - as this exploit demonstrates, one forgotten check or edge case can drain millions. Assertions flip this model. Rather than validating each execution path, you validate the outcome. The protocol can have 100 different ways to borrow, but only one invariant to check: collateral >= required collateral. **Implementation:** ```solidity theme={null} // SPDX-License-Identifier: MIT pragma solidity 0.8.28; import {Assertion} from "credible-std/Assertion.sol"; import {AssertionSpec} from "credible-std/SpecRecorder.sol"; import {PhEvm} from "credible-std/PhEvm.sol"; interface ICauldronV4 { function userBorrowPart(address user) external view returns (uint256); function userCollateralShare(address user) external view returns (uint256); function totalBorrow() external view returns (uint128 elastic, uint128 base); function oracle() external view returns (address); function oracleData() external view returns (bytes memory); function COLLATERIZATION_RATE() external view returns (uint256); function cook( uint8[] calldata actions, uint256[] calldata values, bytes[] calldata datas ) external payable returns (uint256, uint256); } interface IOracle { function peek(bytes calldata data) external view returns (bool success, uint256 rate); } contract AbracadabraCookSolvencyAssertion is Assertion { constructor() { registerAssertionSpec(AssertionSpec.Reshiram); } uint256 constant COLLATERIZATION_RATE_PRECISION = 1e5; function triggers() public view override { registerFnCallTrigger( this.assertUserSolvency.selector, ICauldronV4.cook.selector ); } function assertUserSolvency() external view { ICauldronV4 cauldron = ICauldronV4(ph.getAssertionAdopter()); PhEvm.CallInputs[] memory calls = ph.getCallInputs( address(cauldron), ICauldronV4.cook.selector ); require(calls.length > 0, "No cook calls found"); address caller = calls[0].caller; // Get borrow amount before transaction PhEvm.ForkId memory preFork = _preTx(); uint256 borrowPartBefore = cauldron.userBorrowPart(caller); // Get borrow amount after transaction PhEvm.ForkId memory postFork = _postTx(); uint256 borrowPartAfter = cauldron.userBorrowPart(caller); // Only check if borrow increased if (borrowPartAfter <= borrowPartBefore) { return; } uint256 collateralShare = cauldron.userCollateralShare(caller); (uint128 elastic, uint128 base) = cauldron.totalBorrow(); uint256 userDebt = base > 0 ? (borrowPartAfter * uint256(elastic)) / uint256(base) : 0; address oracle = cauldron.oracle(); bytes memory oracleData = cauldron.oracleData(); (, uint256 exchangeRate) = IOracle(oracle).peek(oracleData); uint256 collateralValue = (collateralShare * exchangeRate) / 1e18; uint256 collateralizationRate = cauldron.COLLATERIZATION_RATE(); uint256 requiredCollateral = (userDebt * COLLATERIZATION_RATE_PRECISION) / collateralizationRate; require( collateralValue >= requiredCollateral, "INSUFFICIENT_COLLATERAL: Borrow exceeds collateral value" ); } } ``` **How It Works:** The assertion triggers on every `cook()` call and: 1. Identifies the caller using `getCallInputs` 2. Compares their borrow amount before (`forkPreTx`) and after (`forkPostTx`) the transaction 3. If borrowing increased, calculates their collateral value using oracle prices 4. Validates that collateral meets the required threshold for their debt 5. Reverts if insufficient collateral is detected This approach validates the outcome rather than the execution path: * **Without assertion**: Developers must remember to add solvency checks in every function that modifies debt, handle complex state transitions, and guard against flag manipulation * **With assertion**: Define the invariant once. It catches any bug that results in undercollateralized positions, whether from flag manipulation, reentrancy, rounding errors, or future code changes # Abracadabra Rounding Error Attack Source: https://docs.phylax.systems/assertions-book/previous-hacks/abracadabra-rounding-error Rounding error in Abracadabra protocol allowed attacker to inflate base value without corresponding adjustment of elastic value This case study explains how the Abracadabra rounding error attack worked and which assertion pattern could have constrained the invalid state transition. ## What Happened The vulnerability stems from an intricate implementation of a RebaseToken mechanism in the Abracadabra protocol: * The protocol used a [RebaseToken](https://github.com/boringcrypto/BoringSolidity/blob/78f4817d9c0d95fe9c45cd42e307ccd22cf5f4fc/contracts/libraries/BoringRebase.sol) with two key components: * Elastic value: Represents the actual assets in debt * Base value: Represents total borrowed shares * The [`User borrow mapping`](https://github.com/Abracadabra-money/abracadabra-money-contracts/blob/cb97c71c8fbfecbd0080e0cfa877f2dc37f56950/src/cauldrons/CauldronV4.sol#L308) only stored borrowed shares per user, not the actual assets * The design appeared to intentionally allow the protocol (or anyone) to modify the assets owed by users by changing the elastic value of the RebaseToken * The [`repayForAll()`](https://github.com/Abracadabra-money/abracadabra-money-contracts/blob/cb97c71c8fbfecbd0080e0cfa877f2dc37f56950/src/cauldrons/CauldronV4.sol#L688) function made this feature accessible to everyone **Attack Mechanism:** 1. A critical rounding error allowed the attacker to inflate the base value without correspondingly adjusting the elastic value 2. This rounding error only manifests when elastic and base values significantly deviate from each other 3. The [`repayForAll()`](https://github.com/Abracadabra-money/abracadabra-money-contracts/blob/cb97c71c8fbfecbd0080e0cfa877f2dc37f56950/src/cauldrons/CauldronV4.sol#L703) function was instrumental in creating this deviation **Exploitation Steps:** 1. Inflate the base value (getting to elastic = 1, base = infinite) 2. Repay the outstanding assets (elastic = 0) 3. Leverage the [first depositor problem](https://github.com/boringcrypto/BoringSolidity/blob/78f4817d9c0d95fe9c45cd42e307ccd22cf5f4fc/contracts/libraries/BoringRebase.sol#L18), when elastic = 0, shares minted will be base = elastic 4. Borrow all assets in the protocol, because of first depositor problem, shares minted will be 1:1. 5. The attacker now has all assets in the protocol, but only owes a negligble share ratio to all outstanding shares. **Vulnerability Details:** * The solvency check [`_isSolvent()`](https://github.com/Abracadabra-money/abracadabra-money-contracts/blob/cb97c71c8fbfecbd0080e0cfa877f2dc37f56950/src/cauldrons/CauldronV4.sol#L203) relied on comparing the attacker's ratio of total borrowed shares * The solvency check implicitly assumed elastic and base values would remain closely aligned * With base set to infinite, the attacker's debt ratio becomes negligible ## Assertion Pattern Assuming the original implementation was well-intentioned but flawed, a simple invariant check could have prevented the attack. The key invariant is: **when no assets are owed (elastic = 0), there should be no debt shares (base = 0)**. ```solidity theme={null} // SPDX-License-Identifier: MIT pragma solidity 0.8.28; import {Assertion} from "credible-std/Assertion.sol"; import {AssertionSpec} from "credible-std/SpecRecorder.sol"; interface ICauldronV4 { function totalBorrow() external view returns (uint128 elastic, uint128 base); } contract AbracadabraRebaseInvariantAssertion is Assertion { constructor() { registerAssertionSpec(AssertionSpec.Reshiram); } function triggers() external view override { // Trigger on any storage change to the cauldron registerTxEndTrigger(this.assertionNoDebtSharesIfNoDebt.selector); } function assertionNoDebtSharesIfNoDebt() external view { ICauldronV4 cauldron = ICauldronV4(ph.getAssertionAdopter()); PhEvm.ForkId memory postFork = _postTx(); (uint128 elastic, uint128 base) = cauldron.totalBorrow(); // Core invariant: if no debt exists, no shares should exist if (elastic == 0) { require(base == 0, "No debt shares should exist when no debt"); } } } ``` This assertion ensures that when no assets are owed (elastic = 0), there should be no debt shares (base = 0), thereby preventing the exploit. # Balancer V2 Rate Manipulation Exploit Source: https://docs.phylax.systems/assertions-book/previous-hacks/balancer-v2-stable-rate-exploit $120m+ lost due to rate manipulation caused by rounding error accumulation This case study explains how the Balancer V2 rate manipulation exploit worked and which assertion pattern could have constrained the invalid state transition. ## What Happened In November 2025, an attacker systematically manipulated exchange rates in Balancer V2 stable pools by exploiting accumulated rounding errors in the stable pool invariant calculation. Through a crafted sequence of 84 alternating batch swaps, the attacker biased the pool's invariant (D) downward by maintaining balances near rounding boundaries. This caused the BPT (Balancer Pool Token) price to change significantly. One pool changed from \~1.027e18 to \~20.189e18 (approximately 20x change). The attacker then extracted value through internal balance withdrawals in a subsequent transaction. **Key Insight:** While the root cause was complex (involving scaled balance calculations, down-rounding operations, and specific balance configurations), the invariant violation was simple: **pool rates should not change drastically within a single transaction**. This demonstrates how assertions protect protocols by focusing on *what should never happen* rather than *how it might happen*. This assertion was developed by analyzing the observable effects of the exploit (drastic rate changes) rather than the root cause (rounding error accumulation). This approach provides broad protection against rate manipulation attacks and should be validated against representative legitimate operations before production use. **Use with caution.** This assertion should undergo extended testing and monitoring in non-production environments before deployment to production systems. The 3x threshold may need adjustment based on real-world transaction patterns. ## The Invariant In Balancer V2 stable pools, the rate represents the price of BPT relative to underlying assets: ```text theme={null} rate = D / totalSupply ``` Where: * `D` is the stable pool invariant (computed from token balances) * `totalSupply` is the circulating supply of BPT **Normal behavior:** During legitimate swaps, rates change minimally (typically \< 10%) due to: * Trading fees * Slight imbalances from large trades * Natural price discovery **Exploit behavior:** The attacker's manipulation caused rates to change by 20x in a single `batchSwap` call, which should never happen for any legitimate operation. ## How the Exploit Worked The exploit consisted of two transactions: ### Transaction 1: Rate Manipulation The attacker executed a single `batchSwap` with 84 swap steps in alternating patterns. These swaps manipulated balances to specific boundaries where `StableMath._calculateInvariant()` accumulated maximum down-rounding bias, causing the invariant D to be underestimated and reducing BPT price. **Observable Effect:** * osETH/WETH-BPT pool rate: approximately 1.027e18 to 20.189e18 (\~19.7x change) * wstETH/WETH-BPT pool rate: approximately 1.051e18 to 3.887e18 (\~3.7x change) ### Transaction 2: Value Extraction The attacker withdrew accumulated internal balances via `manageUserBalance(WITHDRAW_INTERNAL)`. ## Root Cause (Technical Detail) While not necessary for the assertion, understanding the root cause provides context: Balancer V2's `StableMath._calculateInvariant()` uses repeated down-rounding operations on scaled balances: ```solidity theme={null} // Simplified invariant calculation D_P = Math.divDown(Math.mul(D_P, invariant), Math.mul(balances[j], numTokens)); invariant = Math.divDown(...); // Multiple divDown operations compound precision loss ``` Under specific conditions: * Mixed token decimals amplify precision loss * Balances maintained near rounding boundaries maximize bias * Repeated operations in a long `batchSwap` sequence compound the error * The computed invariant D becomes progressively underestimated The attacker's math helper contract (0x679b3) searched for inputs that would push denominators toward zero without triggering reverts. ## Assertion Pattern Rather than attempting to detect the specific exploit mechanism, we assert a simple invariant: **Pool rates must not change drastically within a single `batchSwap` call.** ### Example Assertion ```solidity theme={null} import {AssertionSpec} from "credible-std/SpecRecorder.sol"; contract BatchSwapDeltaAssertion is Assertion { constructor() { registerAssertionSpec(AssertionSpec.Reshiram); } uint256 constant MAX_RATE_CHANGE_MULTIPLIER = 3e18; // 3.0x uint256 constant MIN_RATE_CHANGE_MULTIPLIER = 33e16; // 0.33x function assertionBatchSwapRateManipulation() external { address vault = ph.getAssertionAdopter(); PhEvm.CallInputs[] memory batchSwapCalls = ph.getAllCallInputs( vault, IVault.batchSwap.selector ); for (uint256 i = 0; i < batchSwapCalls.length; i++) { // Decode swap parameters to get affected pools (, IVault.BatchSwapStep[] memory swaps, , , , ) = abi.decode( callInput.input, (IVault.SwapKind, IVault.BatchSwapStep[], IAsset[], IVault.FundManagement, int256[], uint256) ); bytes32[] memory uniquePoolIds = _getUniquePoolIds(swaps); for (uint256 j = 0; j < uniquePoolIds.length; j++) { (address poolAddress, ) = IVault(vault).getPool(uniquePoolIds[j]); // Check rate before and after the swap PhEvm.ForkId memory preCallFork = PhEvm.ForkId({forkType: 2, callIndex: callInput.id}); uint256 preRate = IRateProvider(poolAddress).getRate(); PhEvm.ForkId memory postCallFork = PhEvm.ForkId({forkType: 3, callIndex: callInput.id}); uint256 postRate = IRateProvider(poolAddress).getRate(); uint256 rateChangeMultiplier = (postRate * 1e18) / preRate; // Revert if rate changed by more than 3x require( rateChangeMultiplier <= MAX_RATE_CHANGE_MULTIPLIER && rateChangeMultiplier >= MIN_RATE_CHANGE_MULTIPLIER, "BatchSwap: Extreme pool rate manipulation detected" ); } } } } ``` ### Why This Works The assertion is **root-cause agnostic**: * Detects the known exploit (20x rate change far exceeds 3x threshold) * Would detect any future rate manipulation attack, regardless of technique * Doesn't care about: * How the manipulation was achieved (rounding, overflow, logic bugs) * Whether it's 84 swaps or 10 swaps * The specific math used in the exploit * Helper contracts or preprocessing techniques The assertion simply enforces: **"Pool rates don't drastically change in one transaction"**, a fundamental economic invariant of stable pools. ### Threshold Selection We chose **3x (300%)** as the threshold based on the following analysis: **Normal rate change behavior:** * Single swaps: Cause \< 10% rate changes due to swap fees (1.05x-1.10x maximum) * Proportional joins/exits: Maintain rate constant (1.0x - no change) * Imbalanced joins/exits: Similar to swaps, \< 10% rate change maximum * Multiple operations in a batch: Could accumulate to \~1.5-2.5x in extreme cases with many maximum-sized operations **Exploit behavior:** * The actual exploit showed 20x rate change (far exceeding any legitimate scenario) **Safety margin:** * 3x provides a 1.2x-2x buffer above the most extreme legitimate batch swap scenarios * Significantly below the 20x change observed in the exploit **Potential edge cases:** * Rate provider updates: If a pool uses yield-bearing tokens with rate providers, legitimate rates should change gradually over time. A 3x change in a single transaction would indicate either oracle manipulation or a severe underlying issue (slashing event, de-pegging) that warrants investigation. * Amplification changes: Limited to 2x per day by protocol, causing minimal per-transaction rate impact **Trade-off:** The 3x threshold is aggressive enough to catch exploitation attempts while providing margin for legitimate operations. Teams can tune the threshold upward for protocols whose normal transaction patterns need more room, though this would reduce sensitivity to smaller manipulation attempts. **Disclaimer:** This assertion is conceptual. Based on our analysis of the protocol mechanics, we have not discovered any legitimate operations that would cause rate changes exceeding 3x in a single transaction. However, we cannot guarantee that such edge cases do not exist. Thorough testing and analysis of real-world scenarios and edge cases is required before using this assertion in production. ## Review the release backtest After adding this assertion to a project, create a release with `pcl apply`. The platform automatically tests the release against transactions from the last 20,000 blocks. Review every finding to confirm whether the assertion detected behavior you intend to prevent or would block a benign operation. The platform window moves with the chain, so an older exploit transaction may fall outside the release backtest. Keep a focused regression test for the known exploit and use the platform result to evaluate the release against recent protocol activity. See [How to Review Backtesting Results](/credible/backtesting) for the review workflow. ## Key Takeaways 1. **Invariants > Root Causes:** By focusing on *what should never happen* (drastic rate changes) rather than *how it might happen* (rounding errors, helper contracts, specific exploit techniques), the assertion protects against both known and unknown attack vectors. 2. **Simplicity is powerful:** A simple rate comparison is more effective than trying to detect complex exploit patterns like: * Multi-step swap sequences * Rounding boundary manipulation * Helper contracts * Specific balance configurations 3. **Economic invariants are robust:** The assertion enforces an economic property (pool rates should be stable) that holds true regardless of the underlying implementation details or future protocol changes. 4. **One assertion, multiple protections:** This same assertion would catch: * Oracle manipulation attacks on pool rates * Future rounding error exploits * Integer overflow/underflow affecting rates * Any logic bug causing rate distortion ## References * **Post-Mortem Analysis:** [Coinspect - Balancer Rate Manipulation Exploit](https://www.coinspect.com/blog/balancer-rate-manipulation-exploit/) * **Exploit Transaction (Mainnet):** [0x3e173ab0ba9183efa8a42caa783bdb5ec75daffcc8505cc1302009d11daf1ccf](https://etherscan.io/tx/0x3e173ab0ba9183efa8a42caa783bdb5ec75daffcc8505cc1302009d11daf1ccf) * **Extraction Transaction:** [0xd155207261712c35fa3d472ed1e51bfcd816e616dd4f517fa5959836f5b48569](https://etherscan.io/tx/0xd155207261712c35fa3d472ed1e51bfcd816e616dd4f517fa5959836f5b48569) # Bunni XYZ Rounding Error Exploit Source: https://docs.phylax.systems/assertions-book/previous-hacks/bunni-xyz-rounding-error Sophisticated rounding error exploitation in Bunni AMM led to $8.4M loss through disproportionate liquidity manipulation This case study explains how the Bunni XYZ rounding error exploit worked and which assertion pattern could have constrained the invalid state transition. ## What Happened On September 2, 2025, Bunni was exploited for \$8.4M through a rounding error in the protocol's withdrawal mechanism. The attack affected two pools: weETH/ETH on Unichain and USDC/USDT on Ethereum. ## Why It Worked The attack exploited a rounding error in Bunni's idle balance update mechanism during withdrawals. The vulnerability occurred in `BunniHubLogic::withdraw()`: ```solidity theme={null} // decrease idle balance proportionally to the amount removed { ... uint256 newBalance = balance - balance.mulDiv(shares, currentTotalSupply); ... } ``` **The Flaw:** The `mulDiv` function was intentionally rounded down during development, with the assumption that this would round up the idle balance and round down the active balance. The developers considered this "safe" since lower liquidity meant more price impact during swaps, favoring the pool. **Why This Assumption Failed:** While the rounding direction was safe for individual operations, it became exploitable when combined with multiple operations in sequence. ## Attack Execution The exploit consisted of three steps: ### Step 1: Swap with Flashloaned Funds 1. Attacker flashborrowed 3M USDT from external venues (Uniswap v3 and Morpho) 2. Made multiple swaps from USDT (token1) to USDC (token0) 3. Pushed the pool's spot price tick to 5000 (1 USDC = 1.68 USDT) 4. Pool's active balance in USDC decreased to 28 wei ### Step 2: Exploiting Rounding Errors 1. Attacker made 44 tiny withdrawals in a single transaction that exploited the rounding error 2. USDC active balance decreased from 28 wei to 4 wei (85.7% decrease) 3. This decrease was disproportionate to the amount of liquidity shares being burned 4. Total liquidity decreased by 84.4% from 5.83e16 to 9.114e15 ### Step 3: Sandwich Attack 1. With liquidity artificially decreased, attacker made a large swap from USDT to USDC 2. Spot price tick pushed to 839189 (1 USDC = 2.77e36 USDT) 3. The swap caused total liquidity to increase by 16.8% from 9.114e15 to 1.065e16 4. Attacker made a second swap from USDC to USDT at inflated prices 5. After repaying flashloan, attacker gained 1.33M USDC and 1M USDT ## Why Unichain USDC/USD₮0 Pool Wasn't Exploited The largest Bunni pool (Unichain USDC/USD₮0) was spared due to insufficient flashloan liquidity: * Required 17M flashloan but only 11M was available on Euler * Uniswap v4 couldn't be used due to conflicts with step 2 withdrawals * Pool assets were rehypothecated to Euler, making them unavailable for exploitation ## Root Cause **The Issue:** A rounding direction that's safe for individual operations may not be safe for multiple operations in sequence. **Technical Details:** 1. Bunni uses two estimates of total liquidity and takes the smaller one 2. The series of withdrawals disproportionately reduced `totalLiquidityEstimate0` (USDC-based) 3. The first swap in step 3 caused `totalDensity0X96` to become miniscule (1 wei) 4. This made `totalLiquidityEstimate1` (USDT-based) the chosen estimate, which was larger than the artificially decreased value from step 2 5. The liquidity increase was then sandwiched by the attacker ## Assertion Pattern A withdrawal proportionality assertion could have prevented this attack by ensuring that active balance decreases are proportional to shares burned: ```solidity theme={null} import {AssertionSpec} from "credible-std/SpecRecorder.sol"; contract BunniWithdrawalInvariantAssertion is Assertion { constructor() { registerAssertionSpec(AssertionSpec.Reshiram); } function triggers() external view override { registerFnCallTrigger( this.assertionWithdrawalProportionality.selector, IBunniHub.withdraw.selector ); } /// @notice Ensures withdrawals decrease pool balances proportionally to shares burned function assertionWithdrawalProportionality() external { IBunniHub hub = IBunniHub(ph.getAssertionAdopter()); PhEvm.CallInputs[] memory withdrawals = ph.getCallInputs( address(hub), IBunniHub.withdraw.selector ); for (uint256 i = 0; i < withdrawals.length; i++) { // Decode withdrawal parameters (PoolId poolId, uint256 shares, address to, uint256 deadline) = abi.decode(withdrawals[i].input, (PoolId, uint256, address, uint256)); // Get pool state before withdrawal PhEvm.ForkId memory preCallFork = PhEvm.ForkId({forkType: 2, callIndex: withdrawals[i].id}); uint256 totalSupplyBefore = hub.bunniTokenOfPool(poolId).totalSupply(); uint256 activeBalance0Before = hub.getPoolBalance(poolId, 0); uint256 activeBalance1Before = hub.getPoolBalance(poolId, 1); // Get pool state after withdrawal PhEvm.ForkId memory postCallFork = PhEvm.ForkId({forkType: 3, callIndex: withdrawals[i].id}); uint256 totalSupplyAfter = hub.bunniTokenOfPool(poolId).totalSupply(); // Assuming `getPoolBalance` function exists for simplicity uint256 activeBalance0After = hub.getPoolBalance(poolId, 0); uint256 activeBalance1After = hub.getPoolBalance(poolId, 1); // Calculate expected vs actual changes uint256 sharesBurned = totalSupplyBefore - totalSupplyAfter; require(sharesBurned == shares, "Shares burned mismatch"); // Active balance decreases must be proportional to shares burned uint256 expectedBalance0Decrease = activeBalance0Before * shares / totalSupplyBefore; uint256 expectedBalance1Decrease = activeBalance1Before * shares / totalSupplyBefore; uint256 actualBalance0Decrease = activeBalance0Before - activeBalance0After; uint256 actualBalance1Decrease = activeBalance1Before - activeBalance1After; // Dynamic tolerance: 1% of expected decrease or minimum 1 wei uint256 tolerance0 = expectedBalance0Decrease / 100 + 1; uint256 tolerance1 = expectedBalance1Decrease / 100 + 1; require( actualBalance0Decrease <= expectedBalance0Decrease + tolerance0 && actualBalance0Decrease >= expectedBalance0Decrease - tolerance0, "Token0 active balance decrease not proportional to shares burned" ); require( actualBalance1Decrease <= expectedBalance1Decrease + tolerance1 && actualBalance1Decrease >= expectedBalance1Decrease - tolerance1, "Token1 active balance decrease not proportional to shares burned" ); } } } ``` ### How the Assertion Would Have Prevented It **What it does:** 1. Monitors all withdrawals to the Bunni protocol 2. Calculates expected balance decreases based on shares burned and total supply 3. Uses dynamic tolerance that scales with transaction size (1% of expected decrease + 1 wei minimum) 4. Reverts on disproportionate changes that exceed the tolerance **Why it catches the exploit:** The attacker's 44 tiny withdrawals in a single transaction caused the USDC active balance to decrease from 28 wei to 4 wei (85.7% decrease) while burning only a small amount of shares. This disproportion would trigger the assertion: * Expected decrease: Proportional to shares burned (small amount, e.g., 0.1 wei) * Actual decrease: 24 wei (28 - 4) * Dynamic tolerance: 1% of expected + 1 wei (e.g., 1 wei for tiny withdrawals) * Result: The 24 wei actual decrease vs 0.1 wei expected would exceed the 1 wei tolerance, triggering the assertion **Key insight**: This assertion enforces that withdrawals must decrease pool balances proportionally to shares burned - a rule that the rounding error attack violated. ## Key Takeaways The Bunni attack succeeded because the protocol's rounding assumptions were safe for individual operations but exploitable in combination. The attack demonstrates that mathematical properties must hold not just for individual operations, but across sequences of operations. A proportionality check - ensuring balance decreases match share burns - would have prevented this \$8.4M loss. This principle applies to any DeFi protocol: if accounting doesn't maintain mathematical consistency across operations, the protocol is vulnerable to attacks that exploit the gaps between assumptions and reality. # Bybit - Compromised Safe Wallet UI Source: https://docs.phylax.systems/assertions-book/previous-hacks/bybit-safe-ui Safe Wallet UI was compromised by gaining access to the host machine. This case study explains how the Bybit compromised Safe Wallet UI attack worked and which assertion pattern could have constrained the invalid state transition. ## What Happened Bybit suffered from a security breach in Safe's hosting infrastructure losing 1.4bn USD. The attackers, the lazarus group, gained access to the server and was able to modify the served Safe Wallet frontend. More on the attack: [https://x.com/safe/status/1894768522720350673](https://x.com/safe/status/1894768522720350673) The malicious code was specifically targeting Bybit's next transaction. As of today, it is commonly agreed that the signers of the transaction were shown a fake UI, seeming to be the intended transaction to sign, but in fact it was a malicious transaction. Unfortunately, it is often very hard to verify the correctness of the message that is signed in software or hardware wallets. **Attack steps:** 1. Attackers gained access to the hosting server by compromising a developer's machine. 2. A malicious frontend was uploaded to the server, which targeted Bybit's next transaction. 3. The frontend would show the intended transaction but in fact the message to be signed was malicious 4. The malicious message was a delegate call which would change the implementation of the Safe's proxycontract ## Assertion Pattern In Safe's proxy implementation, the first storage slot is the implementation address. ```solidity theme={null} /** * @title Singleton - Base for singleton contracts (should always be the first super contract) * This contract is tightly coupled to our proxy contract (see `proxies/SafeProxy.sol`) * @author Richard Meissner - @rmeissner */ abstract contract Singleton { // singleton always has to be the first declared variable to ensure the same location as in the Proxy contract. // It should also always be ensured the address is stored alone (uses a full word) address private singleton; } ``` The malicious transaction was executing a delegate call to a malicious contract, effectively changing the implementation address of Bybit's proxy contract. A change of the implementation address allows an attacker to almost completely exchange the logic of the contract. Therefore it was possible to be able to drain all the assets of the Safe without the need of any additional approvals by the original owners. It should be highlighted that even if there is no logic to change the implemenation address in the implementation by safe, delegate calls can modify storage slots of the calling contract. This allows for full flexibility but opens up the possibility for attacks. ### How the Assertion Would Have Prevented It It might be fair to assume that most users of safes would never actually want to change the implementation address of their safe, but they have no way to express their preferences. Assertions give users the ability to express additional invariants on the state of the contract. A change of the implementation address could be prevented by analyzing the state changes within a transaction. PhEvm precompiles used: * *forkPreTx* allowing to fork the state of the contract before a transaction * *load* reading specific storage slots * *getStateChangesAddress* getting all state changes within a transaction for a given slot ```solidity theme={null} // SPDX-License-Identifier: MIT pragma solidity 0.8.28; import {Assertion} from "../../lib/credible-std/src/Assertion.sol"; import {AssertionSpec} from "../../lib/credible-std/src/SpecRecorder.sol"; // Credible Layer precompiles import {Safe} from "../../lib/safe-contracts/src/Safe.sol"; // Safe contract import {PhEvm} from "../../lib/credible-std/src/PhEvm.sol"; contract SafeAssertion is Assertion { Safe safe; constructor(address payable safe_) { registerAssertionSpec(AssertionSpec.Reshiram); safe = Safe(safe_); // Define address of Safe contract } // Define the triggers for the assertions function triggers() public view override { registerTxEndTrigger(this.implementationAddressChange.selector); } function implementationAddressChange() external view { PhEvm.ForkId memory preFork = _preTx(); address preImplementationAddress = address(uint160(uint256(ph.loadStateAt(address(safe), bytes32(0x0), preFork)))); address[] memory addresses = getStateChangesAddress(address(safe), bytes32(0x0)); for (uint256 i = 0; i < addresses.length; i++) { if (addresses[i] != preImplementationAddress) { revert("Implementation address has changed within transaction"); } } } } ``` To even enhance security properties, a complentary assertion could enforce transfers to a whitelist of addresses. In the below example, the assertion checks if the balance of the safe decreased while the balance of the whitelisted addresses increased with the respective amount. ```solidity theme={null} function assertionSafeDrain() external { PhEvm.ForkId memory preFork = _preTx(); uint256 preBalance = address(bybitSafeAddress).balance; uint256[] memory preWhitelistBalances = new uint256[](whitelistedAddresses.length); for (uint256 i = 0; i < whitelistedAddresses.length; i++) { preWhitelistBalances[i] = address(whitelistedAddresses[i]).balance; } PhEvm.ForkId memory postFork = _postTx(); uint256 postBalance = address(bybitSafeAddress).balance; if (postBalance > preBalance) { return; // Balance increased, not a hack } uint256 diff = preBalance - postBalance; for (uint256 i = 0; i < whitelistedAddresses.length; i++) { uint256 postWhitelistBalance = address(whitelistedAddresses[i]).balance; if (postWhitelistBalance == preWhitelistBalances[i] + diff) { return; // Balance increased, not a hack } } // None of the whitelisted addresses have increased in balance, so it's a hack revert("Bybit safe address balance decreased"); } ``` # Compound Upgrade Bug Source: https://docs.phylax.systems/assertions-book/previous-hacks/compound-upgrade-bug Compound comptroller contract had a one letter bug that allowed users to receive massive amounts of COMP rewards This case study explains how the Compound upgrade bug worked and which assertion pattern could have constrained the invalid state transition. ## What Happened Compound upgraded their comptroller contract to [https://etherscan.io/address/0x374abb8ce19a73f2c4efad642bda76c797f19233](https://etherscan.io/address/0x374abb8ce19a73f2c4efad642bda76c797f19233) which had a one letter bug on L1217. The bug occurred when users supplied tokens to markets with zero COMP rewards before initialization. In these cases, the supplyIndex equaled compInitialIndex (1e36), but the reward calculation logic was skipped due to the incorrect comparison operator. ```solidity theme={null} if (supplierIndex == 0 && supplyIndex > compInitialIndex) { // Covers the case where users supplied tokens before the market's supply state index was set. // Rewards the user with COMP accrued from the start of when supplier rewards were first // set for the market. supplierIndex = compInitialIndex; } ``` The bug was caused by using > instead of >= in the check. This meant that when supplyIndex equaled compInitialIndex (1e36), the if block was skipped, leaving supplierIndex at 0. The large difference between supplierIndex (0) and supplyIndex (1e36) caused the protocol to pay out massive unintended rewards. The previous version worked because supplyIndex started at 0 instead of 1e36, though >= would have been more correct. ## Assertion Pattern It would have made sense for the developers to make sure that the COMPS accrual never exceeds the maximum possible rate. This way even if a bug is introduced, it will be caught by the assertion. The assertion below calculates the maximum possible rate of COMP accrual and checks that a distribution does not exceed this rate. The code below is **conceptual pseudo code** to illustrate the invariant that should be enforced. It uses simplified syntax for accessing storage mappings (`compound.compAccrued[supplier]`) that would not compile in actual Solidity. A real implementation would need to use proper getter functions or storage slot calculations via `ph.loadStateAt()`. ```solidity theme={null} // CONCEPTUAL - Verify that COMP accrual never exceeds the maximum possible rate function assertionValidCompAccrual() external view { PhEvm.CallInputs[] memory distributions = ph.getCallInputs( address(comptroller), Comptroller.distributeSupplierComp.selector ); for (uint256 i = 0; i < distributions.length; i++) { // Decode call inputs (selector already stripped by cheatcode) (address cToken, address supplier) = abi.decode(distributions[i].input, (address, address)); // Check COMP accrued before distribution PhEvm.ForkId memory preCallFork = PhEvm.ForkId({forkType: 2, callIndex: distributions[i].id}); uint256 preAccrued = comptroller.compAccrued(supplier); uint256 supplyIndex = comptroller.compSupplyState(cToken).index; uint256 maxDeltaPerToken = supplyIndex - comptroller.compInitialIndex(); uint256 supplierTokens = CToken(cToken).balanceOf(supplier); uint256 maxIncrease = supplierTokens * maxDeltaPerToken; // Check COMP accrued after distribution PhEvm.ForkId memory postCallFork = PhEvm.ForkId({forkType: 3, callIndex: distributions[i].id}); uint256 postAccrued = comptroller.compAccrued(supplier); if (postAccrued > preAccrued) { uint256 increase = postAccrued - preAccrued; require(increase <= maxIncrease, "COMP accrual increase exceeds maximum possible rate"); } } } ``` # Cream Finance 2 Source: https://docs.phylax.systems/assertions-book/previous-hacks/cream-finance-2 Cream Finance suffered a price manipulation hack Cream Finance suffered a 130M USD hack in October 2021. Detailed Analysis: [https://mudit.blog/cream-hack-analysis/](https://mudit.blog/cream-hack-analysis/) ## What Happened The attack stem from a sudden price manipulation of a supported asset (yUSDVault) in the protocol. The attacker built up leveraged positions and then manipulated the price of the asset by donating the underlying into the yUSDVault. ## Assertion Pattern One possible solution is to check price deviations from touched assets in the protocol during the transaction. This would avoid flashloan price manipulation attacks. ```solidity theme={null} uint256 constant MAX_DEVIATION_BPS = 500; // 5% max deviation function assertion_priceDeviation() external view { // Get pre-transaction prices first PhEvm.ForkId memory preFork = _preTx(); PhEvm.Log[] memory logs = ph.getLogs(); // Count relevant logs to size our array uint256 count = 0; for (uint256 i = 0; i < logs.length; i++) { bytes32 topic = logs[i].topics[0]; if (topic == CTokenInterface.Mint.selector || topic == CTokenInterface.Redeem.selector || topic == CTokenInterface.Borrow.selector || topic == CTokenInterface.RepayBorrow.selector) { count++; } } // Collect touched assets and their pre-prices address[] memory touchedAssets = new address[](count); uint256[] memory prePrices = new uint256[](count); uint256 idx = 0; for (uint256 i = 0; i < logs.length; i++) { bytes32 topic = logs[i].topics[0]; address asset; if (topic == CTokenInterface.Mint.selector) { asset = getAssetFromLog(logs[i]); } else if (topic == CTokenInterface.Redeem.selector) { asset = getAssetFromLog(logs[i]); } else if (topic == CTokenInterface.Borrow.selector) { asset = getAssetFromLog(logs[i]); } else if (topic == CTokenInterface.RepayBorrow.selector) { asset = getAssetFromLog(logs[i]); } else { continue; } touchedAssets[idx] = asset; prePrices[idx] = priceOracle.getPrice(asset); idx++; } // Get post-transaction prices and compare PhEvm.ForkId memory postFork = _postTx(); for (uint256 i = 0; i < touchedAssets.length; i++) { uint256 postPrice = priceOracle.getPrice(touchedAssets[i]); uint256 prePrice = prePrices[i]; // Check deviation in both directions uint256 deviation; if (postPrice > prePrice) { deviation = ((postPrice - prePrice) * 10000) / prePrice; } else { deviation = ((prePrice - postPrice) * 10000) / prePrice; } require(deviation <= MAX_DEVIATION_BPS, "Price deviation too high"); } } // Helper to extract asset address from log (implementation depends on log structure) function getAssetFromLog(PhEvm.Log memory log) internal pure returns (address) { // Decode asset address from log topics or data // Implementation depends on the specific event structure return abi.decode(log.data, (address)); } ``` # Drift Admin Takeover Source: https://docs.phylax.systems/assertions-book/previous-hacks/drift-security-council-takeover Reported Drift administrative takeover and assertion patterns for constraining high-impact governance actions This case study explains how a reported administrative takeover can lead to rapid value loss and which assertion patterns could constrain comparable high-impact actions in an EVM protocol. ## What Happened In April 2026, Drift Protocol reported an active attack and suspended deposits and withdrawals. The Record reported that security firms estimated losses above USD 285 million, while other estimates were at least USD 130 million. TechRadar later summarized Drift's public explanation as a sophisticated attack involving durable nonces, misrepresented transaction approvals, and rapid takeover of Drift's Security Council administrative powers. Sources: * [The Record report on the Drift security incident](https://therecord.media/drift-crypto-heist-solana-hacker) * [TechRadar report on the Drift incident](https://www.techradar.com/pro/security/this-is-not-an-april-fools-joke-crypto-platform-drift-suspends-services-after-millions-stolen) Drift is not an EVM protocol. This page uses the incident as an operational-risk case study for comparable EVM systems with emergency councils, admin multisigs, governance executors, or fast-path roles. ## Why It Worked The public reporting describes an attack on the administrative execution layer rather than a conventional smart-contract bug. The relevant risk pattern is that trusted signers or emergency-governance machinery can be induced to execute actions that are valid at the signature layer but unsafe for the protocol. For an EVM protocol, comparable high-impact actions include: * changing owners or role memberships, * lowering multisig thresholds, * upgrading implementation contracts, * minting or moving protocol assets, * pausing or unpausing critical systems, * changing risk parameters, * disabling safety checks or circuit breakers. ## The Invariant The protocol should never enter a state where emergency or admin authority can be rapidly repointed, weakened, or used to move large value without satisfying the protocol's own governance policy. This can be expressed as several enforceable properties: * approved role graph remains intact, * signer threshold stays above a minimum, * new owners or role holders are on an allowlist or pass a timelock, * high-impact functions can only be called through approved governance routes, * protocol outflows stay within configured limits even when an admin action is validly signed. ## Assertion Patterns ### Admin Role-Graph Assertion An assertion can inspect role, owner, and threshold changes in the transaction and reject unsafe transitions. Useful checks include: * threshold cannot be reduced below the approved minimum, * emergency council members cannot be replaced outside an approved set, * admin roles cannot be granted to new addresses without a timelock, * ownership cannot move to an unrecognized executor. ### High-Impact Action Allowlist An assertion can watch sensitive function selectors and require that they are called only through approved governance paths. Useful surfaces include: * `upgradeTo` or proxy implementation changes, * `grantRole`, `revokeRole`, and ownership changes, * minting functions, * treasury transfers, * risk-parameter changes, * emergency pause or unpause operations. ### Outflow Circuit Breaker Even if an attacker reaches an admin role or function, an outflow circuit breaker can prevent rapid value extraction. Useful checks include: * maximum protocol asset outflow per transaction, * maximum outflow across the rolling window's per-block buckets, * tighter limits after admin-role changes, * separate limits for treasury, vault, and user collateral assets. ## How Assertions Would Constrain It For an EVM protocol with comparable emergency-admin powers, assertions could block the unsafe transaction before it settles if the transaction: 1. weakens the signer threshold, 2. adds an unapproved admin, 3. combines an admin change with large asset movement, 4. calls a high-impact function outside the approved route, or 5. moves value beyond the protocol's configured outflow limit. The key point is that the signature can be valid while the state transition is still unsafe. Runtime assertions give protocols a way to define that boundary. ## Key Takeaways Operational security failures should not automatically become total protocol failures. Admin wallets, emergency councils, and governance executors are powerful because they are supposed to respond quickly, but that same power needs explicit runtime limits. Assertions can enforce the protocol's intended governance shape: who can hold authority, how much authority can change at once, and how much value can move when authority changes. # Euler Finance Donation Hack Source: https://docs.phylax.systems/assertions-book/previous-hacks/euler-finance-donation-hack Euler Finance forgot to add a health check to the donation function This case study explains how the Euler Finance donation hack worked and which assertion pattern could have constrained the invalid state transition. ## What Happened The Euler Finance hack exploited two key protocol features: 1. Users could create artificial leverage by minting and depositing assets in the same transaction via `EToken::mint` 2. Users could donate their balance to protocol reserves via `EToken::donateToReserves` without any health checks The attack worked by: 1. Creating an over-leveraged position by minting excess tokens 2. Donating collateral to intentionally make the position under-collateralized 3. Self-liquidating the position to take advantage of the 20% liquidation discount This resulted in the attacker keeping significant "bad debt" while their liquidator account received discounted collateral, profiting from the protocol's liquidation incentives. **Attack Explanation:** The attack was executed through two main contracts: 1. Primary Contract: * Got a 30M DAI flash loan from AAVE V2 * Deployed violator and liquidator contracts * Sent the DAI to the violator 2. Violator Contract: * Deposited 20M DAI to get \~19.56M eDAI * Created artificial leverage twice: * First time: Minted \~195.68M eDAI and 200M dDAI * Second time: Minted another \~195.68M eDAI and 200M dDAI * Repaid 10M DAI to reduce dDAI to 190M * Donated 100M eDAI to reserves This left the violator with: * \~310.93M eDAI * 390M dDAI The key vulnerability was that the donation created an under-collateralized position (more dDAI than eDAI). 3. Liquidator Contract: * Liquidated the violator's position * Due to liquidation discount (20%), got \~310.93M eDAI but only \~259.31M dDAI * Withdrew DAI by burning eDAI at a favorable rate The attacker profited \~8.88M DAI (\~\$8.78M USD) from this attack, with their liquidator contract maintaining a healthy collateralization ratio of \~1.05. Attack was carried out for several different assets, including DAI, WETH, and USDC. ## Assertion Pattern Proper health checks should be performed on the account that is performing the donation. It is worth noting that the below assertion checks for modifications made by the user in the transaction. The user should never be allowed to make changes to their own collateral or debt that brings their positions under water. The code below is **conceptual pseudo code** to illustrate the invariant that should be enforced. The `getModifiedAccounts()` cheatcode does not currently exist. In practice, you would need to identify affected accounts through other means, such as parsing logs with `getLogs()` or tracking call inputs with `getCallInputs()`. ```solidity theme={null} // CONCEPTUAL - getModifiedAccounts() is not a real cheatcode function assertionNoUnsafeDebt() external view { PhEvm.ForkId memory postFork = _postTx(); // Get all accounts that were modified in this tx // NOTE: This cheatcode does not exist - this is conceptual address[] memory accounts = ph.getModifiedAccounts(); for (uint256 i = 0; i < accounts.length; i++) { address account = accounts[i]; // Core invariant: Collateral must always be >= Debt require(euler.healthCheck(account), "Account has more debt than collateral"); } } ``` The key insight is that the **invariant itself is simple**: after any transaction, no account should have more debt than collateral. The challenge is identifying which accounts to check, which in a real implementation might require parsing transaction logs or call inputs. ## Additional Considerations The Euler devs forgot to add a health check to the `donateToReserves` function, so why would they have added an assertion for this? The answer is that they wouldn't. They would have added the assertion way in the beginning when the protocol was deployed first as an additional layer of security. They would have done that to exactly prevent what happened. Someone forgot to perform basic invariant checks at a protocol extension, and that's why the assertion acts as an additional layer of security which enforces protocol wide invariants, exactly to prevent insufficient checks in protocol extensions. In other words, regardless of whether the devs simply forgot to do the checks or if they thought they don't need to do the checks, it shows that extensions are prone to forgetting protocol wide checks. Whereas assertions implicitly check protocol wide assertions by default. # First Depositor Bug Source: https://docs.phylax.systems/assertions-book/previous-hacks/first-depositor First depositor bug in Compound / Aave v2 lending protocols This case study explains how the first depositor bug works and which assertion pattern can constrain the invalid state transition. ## What Happened Background: [https://akshaysrivastav.hashnode.dev/first-deposit-bug-in-compoundv2-and-its-forks](https://akshaysrivastav.hashnode.dev/first-deposit-bug-in-compoundv2-and-its-forks) The First Depositor Attack in Compound / Aave v2 lending protocols: Key points: * First depositor supplies a tiny amount (e.g. 1 wei) of assets * First depositor donates a large amount directly to the lending pool (bypassing supply) * This artificially inflates the exchange rate between shares and assets * Next depositor will receive very few shares for their deposit * If next depositor's amount is smaller than exchange rate, they will receive 0 shares due to rounding error * First depositor owns all shares, so they can withdraw all assets Example: 1. Attacker deposits 1 wei, gets 1 share 2. Attacker donates 1000 tokens directly 3. Exchange rate is now 1000.00..01 tokens : 1 share 4. Victim deposits 100 tokens, gets only \~0.1 shares due to inflated rate -> will be rounded down to 0 5. Attacker withdraws 1 share and gets 1100 tokens, stealing all of victim's deposit ## Why This Matters Traditional prevention: * Attack only makes sense if attacker owns all shares (or close to it) * If he owns all shares, donating tokens to the pool will still be owned by the attacker * Protocols typically deposit with opening the market atomically * This means not all shares are owned by the attacker * Adjustments to the protocol could mint tokens to 0x0 upon first mint/deposit * Many forks fail to combine these actions ## Assertion Pattern * History has shown that an old vulnerability has found its way into many protocols * Many succesfull attacks leveraged this vulnerability * Sonne Finance * Radiant Capital * Hundred Finance * Assertions can be used to easily prevent known vulnerabilities in forked protocols * Enforce existing workarounds * I.e. Sonne Finance planned to execute deploying the market and depositing atomically, however, their governance process let the attacker execute the transactions out of order * Low entry barrier to enable publicly known assertions for famous protocols to your own fork ### Example Assertion: Enforce atomically opening the market and depositing first assets ```solidity theme={null} function assertionHasMinimumSupply() public view { Market market = Market(address(0x1234)); require(market.totalSupply() > MINIMUM_SUPPLY, "Market has no supply"); } ``` ### Example Assertion: Enforce exchange rate \< deposit amount ```solidity theme={null} function assertionExchangeRate() public view { Market market = Market(address(0x1234)); PhEvm.CallInputs[] memory inputs = ph.getCallInputs(address(cToken), cToken.mint.selector); for (uint256 i = 0; i < inputs.length; i++) { PhEvm.CallInputs memory input = inputs[i]; (uint256 amount) = abi.decode(input.input, (uint256)); require(amount / market.exchangeRate() > 0, "Did not receive any shares"); } } ``` # GMX v1 AUM Manipulation Hack Source: https://docs.phylax.systems/assertions-book/previous-hacks/gma-aum-jul25-hack Explanation of the GMX v1 AUM manipulation exploit and assertion patterns that could have constrained it. This case study explains how the GMX v1 AUM manipulation attack worked and which assertion patterns could have constrained the invalid state transition. ## What Happened On July 9, 2025, [GMX v1 lost around \~\$42 million to an attack](https://x.com/GMX_IO/status/1942989975814820347) that exploited how the protocol calculated its total value (Assets Under Management or AUM). This was GMX's second hack of 2025, following a \$13 million loss in March. The attacker used a reentrancy vulnerability to manipulate pricing data, artificially inflating the protocol's apparent value, then immediately withdrew tokens at the inflated price. * [Exploit tx](http://arbiscan.io/tx/0x03182d3f0956a91c4e4c8f225bbc7975f9434fab042228c7acdc5ec9a32626ef) * [Exploiter address Arbitrum](https://arbiscan.io/address/0xdf3340a436c27655ba62f8281565c9925c3a5221) * [Exploiter address Mainnet](https://etherscan.io/address/0xdf3340a436c27655ba62f8281565c9925c3a5221) ## Why It Worked The attack exploited a design flaw where short position operations immediately updated `globalShortAveragePrices`, which directly impacted AUM calculations used for GLP token minting and redemption. The attacker used reentrancy to establish massive short positions within a single transaction, artificially inflating GLP prices. The critical vulnerability chain: 1. **Reentrancy entry point**: `executeDecreaseOrder` accepted a contract address instead of EOA 2. **State manipulation**: Opening short positions immediately updated global averages 3. **AUM inflation**: System counted unrealized short losses as vault "assets" 4. **Value extraction**: Inflated AUM allowed redemption of GLP for excessive assets ## How AUM Calculation Was Exploited ### Normal AUM Calculation GMX calculates its total value using this formula: ```text theme={null} AUM = Physical Tokens + Stablecoins + Unrealized Trading Profits + Fees ``` The "unrealized trading profits" component was the vulnerability. When traders open short positions (betting prices will fall), the protocol tracks: * **Average price** at which all shorts were opened * **Current market price** of the asset * **Difference** = profit/loss for the protocol AUM Calculation ### Key Insight: Short Position Impact The critical part is how short positions affect AUM: * When shorts lose money (current price > average price): Vault profits, AUM increases * When shorts make money (current price \< average price): Vault loses, AUM decreases ### The Manipulation 1. Attacker deposited tokens to mint GLP (liquidity provider tokens) 2. Exploited reentrancy to gain control during a transaction 3. Opened massive short positions at artificially low average prices 4. AUM spiked significantly because the system thought it had huge unrealized profits from shorts 5. Redeemed GLP tokens at the inflated price, withdrawing \$40M+ in real assets ## Critical Invariants That Could Have Prevented the Attack Multiple invariants could have detected this attack, but **AUM manipulation bounds** is probably the most obvious and versatile detection method, because it defines a behavior that should never happen. Here are some invariants that could have prevented the attack: ### 1. AUM Manipulation Bounds Invariant Implement a simple check that AUM changes must be reasonable. This invariant ensures that any change in the protocol's total value is bounded by actual token flows and reasonable market movements. ### 2. Atomic State Consistency Invariant Ensure all state changes affecting token pricing complete atomically before any external calls. This prevents reentrancy-based manipulation of global price averages. ### 3. Price Update Monotonicity Invariant Ensure global average prices update based on actual position changes, not synthetic operations. This maintains mathematical consistency in price calculations. ### 4. Caller Type Restriction Invariant Critical financial operations must originate from externally owned accounts (EOAs) or pre-approved contracts. This prevents malicious contracts from exploiting reentrancy vulnerabilities. ### 5. Position-to-Pool Ratio Invariant Individual positions must not exceed a maximum percentage of total pool value. This limits the impact any single position can have on global averages. ## Assertion Pattern A Credible Layer assertion similar to the one below could have prevented an attack like this. We have simplified the assertion for brevity, but a real world assertion would check for each call in the call stack that the invariant holds. In the example we just show the logic that would be checked for one call. Being able to inspect the call stack is a powerful feature of the Credible Layer and it allows for detection of attacks that are carried out in a single transaction. ```solidity theme={null} function assertSimplifiedAUMBounds() external { // Core principle: AUM should closely track actual token flows // 1. Capture AUM before transaction PhEvm.ForkId memory preFork = _preTx(); uint256 aumBefore = getAumInUsdg(true); // 2. Capture AUM after transaction PhEvm.ForkId memory postFork = _postTx(); uint256 aumAfter = getAumInUsdg(true); // 3. Calculate AUM change uint256 aumChange = aumAfter > aumBefore ? aumAfter - aumBefore : aumBefore - aumAfter; // 4. Calculate percentage change uint256 percentageChange = aumBefore > 0 ? (aumChange * 10000) / aumBefore : 0; // 5. Core invariant: AUM should not change by more than 5% in a single transaction require( percentageChange <= MAX_AUM_DEVIATION_BPS, "SIMPLE_AUM_BOUNDS_VIOLATION: AUM changed by more than 5% in a single transaction" ); // 6. Additional check: If AUM increased significantly, verify it's not artificial if (aumAfter > aumBefore) { uint256 aumIncrease = aumAfter - aumBefore; // If AUM increased by more than $10M, revert require( aumIncrease <= MAX_ABSOLUTE_AUM_DEVIATION, "LARGE_AUM_INCREASE: AUM increased by more than $10M in a single transaction" ); } } ``` ### How the Assertion Would Have Prevented It This assertion implements a simple but powerful economic sanity check that would have prevented the GMX attack: **What it does:** 1. **Captures AUM before and after** the transaction using Phylax's state forking 2. **Calculates the percentage change** in AUM during the transaction 3. **Enforces a 5% maximum deviation** - any AUM change larger than 5% triggers a revert (example value, could be higher or lower depending on the protocol) 4. **Adds an absolute cap** of \$10M for any single AUM increase (example value, could be higher or lower depending on the protocol) **Why it catches the exploit:** The GMX attacker artificially inflated AUM by a massive amount with only a small real deposit. This created an enormous percentage deviation that would immediately trigger the assertion: * **Percentage check**: The artificial AUM increase represented a huge percentage change, far exceeding the 5% limit * **Absolute check**: The artificial increase also exceeded the \$10M absolute cap * **Economic logic**: Real market movements rarely cause such extreme AUM swings in a single transaction **Key insight**: This assertion doesn't need to understand the technical details of the reentrancy attack. It simply enforces the economic principle that "protocol value should match actual assets at any point in the call stack" - a rule that the attack fundamentally violated. ## Key Takeaways The GMX attack succeeded because the protocol trusted its internal accounting without validating that value changes matched actual asset movements. A simple economic sanity check - "did our total value increase by more than our deposits?" - would have prevented this \$42M loss. **Multiple invariants could have detected this attack, but AUM manipulation bounds was the most obvious and effective detection method.** The key insight is that financial protocols must maintain strict mathematical properties throughout all state transitions, with no intermediate states that violate these properties. By defining invariants and protecting against transactions that violate them with something like the Credible Layer assertions, protocols can prevent a wide range of attacks while maintaining intended functionality. This principle applies to any DeFi protocol: **if your system's reported value doesn't match your actual holdings, something is wrong.** # Radiant Capital Hack Source: https://docs.phylax.systems/assertions-book/previous-hacks/hack1-radiant-capital Ownership change of lending pools lead to drain This case study explains how the Radiant Capital hack worked and which assertion pattern could have constrained the invalid state transition. ## What Happened In October 2024, Radiant Capital was hacked. You can read more about the hack on [Rekt](https://rekt.news/radiant-capital-rekt2/). In short, the attacker managed to gain control over 3 signers of the Radiant Capital multisig, which allowed the attacker to change ownership of the lending pools and ultimately drain the pools. Had there been an assertion in place that checked that the ownership of the lending pools didn't change, the hack would have been prevented. ## Why This Matters This use case is a good example of how to use assertions to detect ownership changes. A lot of DeFi protocols have the concept of owners and admins that can change the protocol's behavior. Usually these are controlled by a multisig, which is best practice, but it is not always enough. Especially if the multisig setup is not done in an optimal way. The assertion shown below is easy to generalize and use in any protocol that wants to make sure that the ownership of critical contracts don't change. It would also be possible to define a whitelist of contracts that the ownership can be changed to. By default there is a cooldown period before an assertion can be paused or removed, so protocols need to plan ahead if they don't have a whitelist defined. ## Assertion Pattern This assertions checks if the owner, emergency admin and pool admin of the lending pool have changed. It's a good example of how a simple assertion can be used to prevent disastrous hacks. ```solidity theme={null} // SPDX-License-Identifier: MIT pragma solidity 0.8.28; import {Assertion} from "../lib/credible-std/Assertion.sol"; import {AssertionSpec} from "../lib/credible-std/SpecRecorder.sol"; interface ILendingPoolAddressesProvider { function owner() external view returns (address); function getEmergencyAdmin() external view returns (address); function getPoolAdmin() external view returns (address); } // Radiant Lending Pool on Arbitrum that got hacked and drained contract LendingPoolAddressesProviderAssertions is Assertion { constructor() { registerAssertionSpec(AssertionSpec.Reshiram); } ILendingPoolAddressesProvider public lendingPoolAddressesProvider = ILendingPoolAddressesProvider(0x091d52CacE1edc5527C99cDCFA6937C1635330E4); //arbitrum function triggers() external view override { // Trigger on any storage change to catch ownership modifications registerTxEndTrigger(this.assertionOwnerChange.selector); registerTxEndTrigger(this.assertionEmergencyAdminChange.selector); registerTxEndTrigger(this.assertionPoolAdminChange.selector); } // Check if the owner has changed function assertionOwnerChange() external view { PhEvm.ForkId memory preFork = _preTx(); address prevOwner = lendingPoolAddressesProvider.owner(); PhEvm.ForkId memory postFork = _postTx(); address newOwner = lendingPoolAddressesProvider.owner(); require(prevOwner == newOwner, "Owner has changed"); } // Check if the emergency admin has changed function assertionEmergencyAdminChange() external view { PhEvm.ForkId memory preFork = _preTx(); address prevEmergencyAdmin = lendingPoolAddressesProvider.getEmergencyAdmin(); PhEvm.ForkId memory postFork = _postTx(); address newEmergencyAdmin = lendingPoolAddressesProvider.getEmergencyAdmin(); require(prevEmergencyAdmin == newEmergencyAdmin, "Emergency admin has changed"); } // Check if the pool admin has changed function assertionPoolAdminChange() external view { PhEvm.ForkId memory preFork = _preTx(); address prevPoolAdmin = lendingPoolAddressesProvider.getPoolAdmin(); PhEvm.ForkId memory postFork = _postTx(); address newPoolAdmin = lendingPoolAddressesProvider.getPoolAdmin(); require(prevPoolAdmin == newPoolAdmin, "Pool admin has changed"); } } ``` # Vestra DAO Hack Source: https://docs.phylax.systems/assertions-book/previous-hacks/hack2-vestra-dao Unchecked isActive flag in maturity This case study explains how the Vestra DAO hack worked and which assertion pattern could have constrained the invalid state transition. ## What Happened In December 2024, VestraDAO was hacked. The hacker exploited a vulnerability in the `unStake` function which allowed users to stake and unstake without waiting for the maturity period. For an in-depth analysis of the hack, you can read this [post](https://x.com/_czepluch/status/1866112404242743590). In a nutshell, there was an `isActive` flag that was set to `false` correctly in the `unStake` function. However, the `isActive` flag was never checked if someone called the `unStake` function again. This resulted in an attacker being able to repeatedly call `unStake` and get additional yield from the protocol until it was drained. It should be noted that there were no tests for the code base and the code was not audited. However, with an assertion it would be possible to patch the vulnerability until a new version of the code is deployed. The assertion would simply check if the `isActive` flag is `false` before calling the `unStake` function. ## Why This Matters In this hack, a simple require statement would have been enough to prevent the vulnerability. Usually, a contract redeployment is needed to fix a vulnerability like this. With an assertion, it is possible to patch this directly and make sure that all calls to the `unStake` function check the `isActive` flag. This is a very powerful concept and can be useful in many situations. Imagine a security researcher reports a vulnerability in a protocol before anyone has exploited it. In that case the protocol can publish an assertion that guards against the vulnerability until the team has had the time to fix the vulnerability in the best way possible. ## Assertion Pattern This assertions checks if the `isActive` flag is `false` before calling the `unStake` function if it's false the transaction will not be included in the block. Alternatively, there could be an assertion that checks that the `totalStaked` is always equal to the sum of all `stakeAmount` in the `stakes` mapping. This would require a way to iterate over all the stakes and sum them up, which is not yet supported by a cheatcode. ```solidity theme={null} // SPDX-License-Identifier: MIT pragma solidity 0.8.28; import {Assertion} from "../lib/credible-std/Assertion.sol"; import {AssertionSpec} from "../lib/credible-std/SpecRecorder.sol"; // VestraDAO interface interface IVestraDAO { struct Stake { uint64 startTime; uint256 stakeAmount; uint256 yield; uint256 penalty; uint64 endTime; bool isActive; } mapping(address => mapping(uint8 => Stake)) public stakes; function unStake(uint8 maturity) external; } contract VestraDAOHack is Assertion { constructor() { registerAssertionSpec(AssertionSpec.Reshiram); } IVestraDAO public vestraDAO = IVestraDAO(address(0xbeef)); function triggers() external view override { registerFnCallTrigger(this.assertionExample.selector, vestraDAO.unStake.selector); } // Check that user was actively staked before unstaking // This prevents double-unstaking by ensuring isActive was true before the call function assertionExample() external view { PhEvm.CallInputs[] memory unStakes = ph.getCallInputs(address(vestraDAO), vestraDAO.unStake.selector); for (uint256 i = 0; i < unStakes.length; i++) { uint8 maturity = abi.decode(unStakes[i].input, (uint8)); address from = unStakes[i].caller; // Check BEFORE the unstake that the stake was active PhEvm.ForkId memory preCallFork = PhEvm.ForkId({forkType: 2, callIndex: unStakes[i].id}); (,,,,,bool wasActive) = vestraDAO.stakes(from, maturity); require(wasActive, "User was not actively staked for this maturity"); } } } ``` # KelpDAO / rsETH LayerZero Configuration Incident Source: https://docs.phylax.systems/assertions-book/previous-hacks/kelpdao-rseth-layerzero-configuration Reported cross-chain verification failure affecting KelpDAO rsETH and assertion patterns that could constrain similar inflow risk This case study explains how a reported cross-chain verification failure could create unsafe asset inflows and which assertion patterns could constrain the resulting state transition. ## What Happened In April 2026, TechRadar reported that Lazarus Group stole roughly \$290 million from KelpDAO through its LayerZero integration. The report described attackers compromising infrastructure used to verify cross-chain transactions and feeding false data that caused fraudulent transfers to be approved. The same report said LayerZero characterized the incident as isolated to KelpDAO's rsETH configuration and attributed it to a single-DVN setup. KelpDAO disputed that the incident was solely the result of its configuration. Sources: * [TechRadar report on the KelpDAO / LayerZero incident](https://www.techradar.com/pro/security/north-koreas-lazarus-makes-off-with-usd290m-crypto-in-kelp-dao-heist-after-siphoning-funds-using-fraudulent-transactions) The public root-cause record is disputed. This page focuses on the observable risk class: a cross-chain configuration or verification failure can create unsafe inflows into protocols that depend on the asset, even when those downstream protocols did not make the configuration change themselves. ## Why It Matters Cross-chain assets can become dependencies for lending markets, vaults, and other protocols. If an upstream bridge, messaging layer, or token issuer accepts invalid messages, the downstream protocol may see apparently valid token balances or inflows even though the underlying backing assumptions have changed. The dangerous state is not only "a bridge was compromised." For a dependent protocol, the dangerous state is: * a supported asset's supply increases faster than expected, * the asset's backing no longer matches protocol assumptions, * a market accepts deposits from a newly unsafe origin, or * risk exposure grows before the protocol team can update parameters. ## Assertion Patterns ### Cross-Chain Inflow Circuit Breaker An inflow circuit breaker can collect bridged or restaked asset inflow into one bucket per block and limit the cumulative inflow across those per-block buckets over a rolling window. Useful checks include: * maximum inflow per block, hour, or day, * maximum inflow from a specific bridge, origin chain, or endpoint, * maximum increase in a market's exposure to the asset, * stricter limits when the asset is newly listed or recently reconfigured. This would not need to prove exactly which cross-chain message was invalid. It would constrain the downstream impact by preventing unusually large inflows from being accepted all at once. ### Backing and Supply Parity Assertion For assets whose safety depends on backing, the protocol can assert that minted or accepted supply remains within a tolerated range of verified backing data. Useful checks include: * total accepted supply does not exceed verified backing plus a tolerance, * bridge-minted supply on a destination chain does not jump without matching source-side accounting, * lending-market collateral value is capped when backing data is stale or inconsistent. ### Message-Security Configuration Assertion If the protocol relies on a cross-chain asset or endpoint with configurable verification policy, an assertion can watch configuration surfaces. Useful checks include: * verifier or DVN sets remain in an approved configuration, * quorum or threshold values do not drop below a safe minimum, * endpoint changes pass through expected governance or timelock paths, * high-risk configuration changes trigger lower asset-flow caps until reviewed. ## How Assertions Would Constrain It For an EVM protocol accepting an asset like rsETH as collateral or vault input, the assertions would not need to understand every LayerZero or KelpDAO internal detail. They would enforce local safety boundaries: 1. The protected market cannot accept more than a configured amount of the asset across the rolling window's per-block buckets. 2. The market cannot grow exposure if asset backing or message-security data is stale, disputed, or outside policy. 3. The protocol cannot silently continue with the same risk parameters after a critical upstream configuration changes. The core idea is to turn external dependency risk into enforceable local limits. ## Key Takeaways The incident shows why protocols need protections around assets and dependencies they do not fully control. A lending market, vault, or structured product can be harmed by decisions made upstream by a bridge, restaking protocol, verifier set, or token issuer. Runtime assertions are useful because they can enforce the downstream protocol's own risk boundaries even when the external root cause is complex or disputed. # KiloEx Price Oracle Manipulation Source: https://docs.phylax.systems/assertions-book/previous-hacks/kiloex-price-manipulation-hack Access control vulnerability in price oracle implementation led to $7.5M loss across multiple chains ## What Happened Background: [https://x.com/SlowMist\_Team/status/1911991384254402737](https://x.com/SlowMist_Team/status/1911991384254402737) The vulnerability stemmed from a critical access control flaw in KiloEx's price oracle implementation: * The protocol used a chain of contracts for price updates: * KiloPriceFeed: Main oracle contract * Keeper: Contract responsible for price updates * PositionKeeper: Contract managing positions * MinimalForwarder: Contract handling transaction forwarding * The access control chain was implemented as follows: * KiloPriceFeed trusted Keeper * Keeper trusted PositionKeeper * PositionKeeper trusted MinimalForwarder * MinimalForwarder had no access controls **Attack Mechanism:** 1. The attacker exploited the MinimalForwarder's lack of access controls 2. They were able to forge signatures and bypass the entire access control chain 3. This allowed direct manipulation of the KiloPriceFeed contract **Exploitation Steps:** 1. Attacker funded their wallet through Tornado Cash 2. Used the MinimalForwarder to bypass access controls 3. Manipulated ETH price down to \$100 4. Opened leveraged long positions 5. Manipulated price up to \$10,000 6. Closed positions for profit 7. Repeated across multiple chains (Base, BNB Chain, Taiko) **Vulnerability Details:** * The MinimalForwarder contract lacked signature validation * No checks were performed on the caller's identity * The entire access control chain relied on each component trusting the next * The protocol had been audited 5 times since June 2023, but the vulnerability remained undetected ## Assertion Pattern ### Price Deviation Assertion With an assertion very similar to the [Price Deviation Assertion](/assertions-book/assertions/ass28-intra-tx-oracle-deviation), this attack could have been prevented. The example assertion below could with very few changes have caught the large price deviations in the attack and prevented the transaction. ```solidity theme={null} // 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"; contract IntraTxOracleDeviationAssertion is Assertion { constructor() { registerAssertionSpec(AssertionSpec.Reshiram); } // Maximum allowed price deviation (10% by default) uint256 public constant MAX_DEVIATION_PERCENTAGE = 10; function triggers() external view override { // Register trigger for oracle price update calls registerFnCallTrigger(this.assertOracleDeviation.selector, IOracle.updatePrice.selector); } // Check that price updates don't deviate more than the allowed percentage // from the initial price at any point during the transaction function assertOracleDeviation() external { // Get the assertion adopter address IOracle adopter = IOracle(ph.getAssertionAdopter()); // Start with a simple check comparing pre and post state PhEvm.ForkId memory preFork = _preTx(); uint256 prePrice = adopter.price(); // Calculate allowed deviation thresholds (10% by default) uint256 maxAllowedPrice = (prePrice * (100 + MAX_DEVIATION_PERCENTAGE)) / 100; uint256 minAllowedPrice = (prePrice * (100 - MAX_DEVIATION_PERCENTAGE)) / 100; // First check post-state price PhEvm.ForkId memory postFork = _postTx(); uint256 postPrice = adopter.price(); // Verify post-state price is within allowed deviation from initial price require( postPrice >= minAllowedPrice && postPrice <= maxAllowedPrice, "Oracle post-state price deviation exceeds threshold" ); // Get all price update calls in this transaction // Since this assertion is triggered by updatePrice calls, we know there's at least one PhEvm.CallInputs[] memory priceUpdates = ph.getCallInputs(address(adopter), adopter.updatePrice.selector); // Check each price update to ensure none deviate more than allowed from initial price for (uint256 i = 0; i < priceUpdates.length; i++) { PhEvm.ForkId memory postCallFork = PhEvm.ForkId({forkType: 3, callIndex: priceUpdates[i].id}); // Call the price function at the given frame in the call stack uint256 updatedPrice = adopter.price(); // Verify each update is within allowed deviation from initial pre-state price require( updatedPrice >= minAllowedPrice && updatedPrice <= maxAllowedPrice, "Oracle intra-tx price deviation exceeds threshold" ); } } } interface IOracle { function updatePrice(uint256 price) external; function price() external view returns (uint256); } ``` Specifically, the assertion could have been configured to: 1. Trigger on all calls to the `setPrices` function in the KiloPriceFeed contract 2. Enforcing a maximum price deviation of 5% per update 3. Reverting if the price deviation exceeds this threshold This would have prevented the attack in two ways: 1. When the attacker tried to set ETH price to $100 (from the then ~$2000), the assertion would have detected this \~95% deviation and reverted the transaction 2. When they later tried to set the price to \$10,000, the assertion would have again detected this extreme deviation and reverted 3. If this was all done in a single transaction, the assertion would have caught the large deviation and reverted the entire transaction Note: In a real implementation, this assertion should be: * Run for each token in the protocol * Consider token-specific deviation thresholds * Handle multiple price updates in a single transaction ### Access Control Assertion The root cause of the vulnerability was the MinimalForwarder's lack of access controls. A simple assertion could have prevented this by ensuring the MinimalForwarder is only called by authorized addresses in the expected call chain (Keeper → PositionKeeper → MinimalForwarder): * **Trigger**: Register for all calls to `MinimalForwarder.execute()` * **Assertion**: * Maintain a whitelist of authorized callers (specifically the PositionKeeper) * Verify the caller is in the whitelist * Revert if unauthorized This simple assertion would have prevented the attack by ensuring that only the PositionKeeper could trigger price updates through the MinimalForwarder. While fixing the access control in the contract itself would be the better solution, this assertion could have served as a safety net to catch unauthorized access attempts. # Hack Case Studies Source: https://docs.phylax.systems/assertions-book/previous-hacks/prev-hacks-index Explanation-focused case studies of real-world hacks and the assertions that would have prevented them Use this section when you want to understand why a real exploit worked and which assertion pattern would have blocked it. If you already know the kind of invariant you want and just need examples, use the [assertion pattern catalog](../assertions/use-cases-index). These pages analyze real-world hacks and demonstrate how assertions could have prevented them. They show how assertions work as a safety net by catching failures that might slip through audits and testing. Each analysis includes: * Detailed explanation of the attack mechanism * Root cause analysis of the vulnerability * Specific assertion patterns, and code examples where they have been implemented and tested ## Cross-Chain, Runtime, and Operational Risk Recent incidents show that protocol risk often comes from external dependencies, bridge configuration, operational controls, and asset-flow assumptions rather than only from a bug in the protected contract itself. Runtime assertions are useful in these cases because they can enforce outcome-based limits around what state should never be reached. ### [KelpDAO / rsETH LayerZero Configuration Incident](/assertions-book/previous-hacks/kelpdao-rseth-layerzero-configuration) **Attack Type:** Cross-chain Configuration + Message Verification Failure **Loss:** Reported \$290M USD **Root Cause:** Reported compromise or misuse of cross-chain verification infrastructure, with public dispute over whether KelpDAO's rsETH LayerZero configuration was the direct cause **Prevention:** Cross-chain inflow circuit breakers, backing/supply parity assertions, and message-security configuration assertions ### [Drift Admin Takeover](/assertions-book/previous-hacks/drift-security-council-takeover) **Attack Type:** Operational Security + Administrative Takeover **Loss:** Reported \$280M+ USD **Root Cause:** Reported misrepresented approvals and durable nonce abuse enabled takeover of emergency administrative powers **Prevention:** Admin role-graph assertions, high-impact action allowlists, and protocol outflow circuit breakers ## Access Control & Administrative Vulnerabilities ### [Bybit - Compromised Safe Wallet UI](/assertions-book/previous-hacks/bybit-safe-ui) **Attack Type:** UI Compromise + Implementation Change **Loss:** \$1.4B USD **Root Cause:** Compromised frontend showed fake transactions while changing proxy implementation **Prevention:** Implementation address change assertions and transaction validation ### [Radiant Capital Hack](/assertions-book/previous-hacks/hack1-radiant-capital) **Attack Type:** Ownership Takeover **Loss:** \$58M+ USD **Root Cause:** Attackers gained control of multisig signers and changed ownership of lending pools **Prevention:** Owner change assertions with proper validation and whitelisting ### [UxLink Multisig Ownership Compromise](/assertions-book/previous-hacks/uxlink-multisig-hack) **Attack Type:** Private Key Compromise + Multisig Manipulation **Loss:** \$39.3M USD **Root Cause:** Compromised private keys enabled rapid multisig reconfiguration and threshold reduction **Prevention:** Threshold protection assertions, owner whitelisting, and cooling periods ## Arithmetic & Calculation Errors ### [Balancer V2 Rate Manipulation Exploit](/assertions-book/previous-hacks/balancer-v2-stable-rate-exploit) **Attack Type:** Rounding Error Accumulation **Loss:** \$120M+ USD **Root Cause:** Accumulated rounding errors in stable pool invariant calculation manipulated exchange rates **Prevention:** Rate change bounds assertions detecting drastic pool rate changes within single transactions ### [Bunni XYZ Rounding Error Exploit](/assertions-book/previous-hacks/bunni-xyz-rounding-error) **Attack Type:** Rounding Error + Liquidity Manipulation **Loss:** \$8.4M USD **Root Cause:** Rounding error in withdrawal mechanism led to disproportionate liquidity decreases **Prevention:** Withdrawal proportionality assertions ensuring balance decreases match share burns ### [Abracadabra Rounding Error Attack](/assertions-book/previous-hacks/abracadabra-rounding-error) **Attack Type:** Rounding Error Exploitation **Loss:** \$6.5M USD **Root Cause:** Rounding error in RebaseToken mechanism allowed base value inflation **Prevention:** Invariant checks ensuring debt shares consistency ### [Vestra DAO Hack](/assertions-book/previous-hacks/hack2-vestra-dao) **Attack Type:** Unchecked State Flag **Loss:** Protocol drained **Root Cause:** Missing validation of `isActive` flag in unstake function **Prevention:** State flag validation assertions ### [Compound Upgrade Bug](/assertions-book/previous-hacks/compound-upgrade-bug) **Attack Type:** Logic Error in Upgrade **Loss:** \$280K USD (limited by quick response) **Root Cause:** One-letter bug (`>` instead of `>=`) in reward calculation **Prevention:** Maximum reward rate validation assertions ## Oracle & Price Manipulation ### [GMX v1 AUM Manipulation Hack](/assertions-book/previous-hacks/gma-aum-jul25-hack) **Attack Type:** Reentrancy + AUM Manipulation **Loss:** \$42M USD **Root Cause:** Reentrancy vulnerability allowed artificial AUM inflation **Prevention:** AUM manipulation bounds assertions and atomic state consistency ### [KiloEx Price Oracle Manipulation](/assertions-book/previous-hacks/kiloex-price-manipulation-hack) **Attack Type:** Access Control + Price Manipulation **Loss:** \$7.5M USD **Root Cause:** Lack of access controls in MinimalForwarder allowed price manipulation **Prevention:** Price deviation assertions and access control validation ### [Vicuna Finance Oracle Manipulation](/assertions-book/previous-hacks/vicuna-finance-hack) **Attack Type:** LP Token Oracle Manipulation **Loss:** \$700K USD **Root Cause:** LP tokens priced using simple sum formula instead of fair pricing **Prevention:** Price deviation assertions monitoring oracle changes per call ### [Cream Finance 2](/assertions-book/previous-hacks/cream-finance-2) **Attack Type:** Price Manipulation **Loss:** \$130M USD **Root Cause:** Sudden price manipulation through asset donation to vault **Prevention:** Price deviation monitoring assertions ## Protocol Logic Vulnerabilities ### [Abracadabra GMX V2 Cauldron Exploit](/assertions-book/previous-hacks/abracadabra-gmx-v2-exploit) **Attack Type:** Accounting Bug **Loss:** \$13.4M USD **Root Cause:** Phantom collateral created when tokens extracted without updating order value **Prevention:** Collateral tracking assertions ensuring borrowed amounts never exceed actual collateral ### [Abracadabra CauldronV4 Cook Function Exploit](/assertions-book/previous-hacks/abracadabra-hack-3) **Attack Type:** Logic Flaw in Action Sequencing **Loss:** \$1.8M USD **Root Cause:** Action sequence \[5, 0] allowed solvency check flag to be set then immediately cleared **Prevention:** Post-transaction solvency assertions enforcing outcome-based validation ### [Euler Finance Donation Hack](/assertions-book/previous-hacks/euler-finance-donation-hack) **Attack Type:** Missing Health Check **Loss:** \$197M USD **Root Cause:** Donation function lacked health factor validation **Prevention:** Health factor assertions after all state changes ### [Visor Finance Unrestricted Mint](/assertions-book/previous-hacks/visor-finance-unrestricted-mint) **Attack Type:** Unrestricted Token Minting **Loss:** Protocol funds **Root Cause:** Anyone could mint reward tokens without proper validation **Prevention:** Collateralization ratio assertions ### [First Depositor Bug](/assertions-book/previous-hacks/first-depositor) **Attack Type:** Share Price Manipulation **Loss:** Various protocols affected **Root Cause:** First depositor can manipulate exchange rate through donation **Prevention:** Minimum supply assertions and exchange rate validation # UxLink Multisig Ownership Compromise Source: https://docs.phylax.systems/assertions-book/previous-hacks/uxlink-multisig-hack Compromised private keys led to \$10M+ drain from UxLink multisig through threshold manipulation and owner replacement This case study explains how the UxLink multisig ownership compromise worked and which assertion pattern could have constrained the invalid state transition. ## What Happened On September 22, 2025, UxLink's multisig was compromised through private key theft, resulting in \$11.3M direct theft plus unauthorized minting of 10 trillion tokens worth \~\$28M. Attackers manipulated the multisig configuration to drain funds and gain token minting privileges. ## Why It Worked The attack exploited two weaknesses: 1. **Compromised Private Keys**: Attackers gained access to UxLink's multisig owner private keys 2. **Unrestricted Multisig Configuration**: Safe contract allowed threshold reduction and owner changes without security checks 3. **Token Minting Access**: Compromised multisig gained Manager privileges over the UXLINK token contract **Attack Vector:** Compromised private keys enabled execution of multisig transactions without validation or rate limiting. ## Attack Analysis ### Attack Sequence **Phase 1: Multisig Compromise** Attackers used compromised private keys to revoke admin privileges, add themselves as owners, and reduce the multisig threshold to 1, gaining full control. **Phase 2: Treasury Drainage** Drained \$11.3M in assets (USDT, USDC, WBTC, ETH) and converted them across chains. **Phase 3: Token Exploitation** Used multisig control to mint unlimited UXLINK tokens, causing a price crash and significant market cap loss. ### Root Causes 1. **Private Key Compromise**: Compromised private keys due to poor operational security 2. **No Multisig Protection**: No safeguards against rapid configuration changes 3. **No Rate Limiting**: Multisig changes executed immediately without cooling periods 4. **Missing Access Controls**: No whitelisting for owner changes ## Assertion Pattern Multisig protection assertions could have prevented this attack by enforcing governance invariants: ```solidity theme={null} // SPDX-License-Identifier: MIT pragma solidity 0.8.28; import {Assertion} from "../../lib/credible-std/src/Assertion.sol"; import {AssertionSpec} from "../../lib/credible-std/src/SpecRecorder.sol"; import {PhEvm} from "../../lib/credible-std/src/PhEvm.sol"; import {ISafe} from "@safe-global/safe-contracts/contracts/interfaces/ISafe.sol"; contract UxLinkMultisigProtectionAssertion is Assertion { constructor() { registerAssertionSpec(AssertionSpec.Reshiram); } // Minimum threshold that must be maintained uint256 constant MIN_THRESHOLD = 2; // Whitelisted addresses that can become owners (set at deployment) address constant ALLOWED_OWNER_1 = 0x1111111111111111111111111111111111111111; address constant ALLOWED_OWNER_2 = 0x2222222222222222222222222222222222222222; address constant ALLOWED_OWNER_3 = 0x3333333333333333333333333333333333333333; function triggers() external view override { registerFnCallTrigger( this.assertThresholdProtection.selector, ISafe.changeThreshold.selector ); registerFnCallTrigger( this.assertOwnerAddition.selector, ISafe.addOwnerWithThreshold.selector ); registerFnCallTrigger( this.assertOwnerRemoval.selector, ISafe.removeOwner.selector ); } /// @notice Prevents threshold reduction below minimum function assertThresholdProtection() external view { ISafe safe = ISafe(ph.getAssertionAdopter()); PhEvm.CallInputs[] memory calls = ph.getCallInputs( address(safe), ISafe.changeThreshold.selector ); for (uint256 i = 0; i < calls.length; i++) { uint256 newThreshold = abi.decode(calls[i].input, (uint256)); // Never allow threshold below minimum require(newThreshold >= MIN_THRESHOLD, "Threshold cannot go below minimum"); } } /// @notice Validates new owner additions against whitelist function assertOwnerAddition() external view { ISafe safe = ISafe(ph.getAssertionAdopter()); PhEvm.CallInputs[] memory calls = ph.getCallInputs( address(safe), ISafe.addOwnerWithThreshold.selector ); for (uint256 i = 0; i < calls.length; i++) { (address newOwner, uint256 threshold) = abi.decode(calls[i].input, (address, uint256)); // Basic validation require(newOwner != address(0), "Invalid owner address"); // Check whitelist require( newOwner == ALLOWED_OWNER_1 || newOwner == ALLOWED_OWNER_2 || newOwner == ALLOWED_OWNER_3, "New owner not whitelisted" ); // Never allow threshold below minimum require(threshold >= MIN_THRESHOLD, "Threshold cannot go below minimum"); } } /// @notice Validates owner removals don't reduce threshold below minimum function assertOwnerRemoval() external view { ISafe safe = ISafe(ph.getAssertionAdopter()); PhEvm.CallInputs[] memory calls = ph.getCallInputs( address(safe), ISafe.removeOwner.selector ); for (uint256 i = 0; i < calls.length; i++) { (, , uint256 threshold) = abi.decode(calls[i].input, (address, address, uint256)); // Never allow threshold below minimum require(threshold >= MIN_THRESHOLD, "Threshold cannot go below minimum"); } } } ``` Assertions cannot track state across transactions (e.g., cooling periods). The original attack used rapid sequential transactions, which would require off-chain monitoring or timelocked governance contracts to fully prevent. However, the assertions above still provide strong protection by enforcing minimum thresholds and owner whitelisting. ### How the Assertions Would Have Prevented It **What they do:** 1. **Threshold Protection**: Prevents threshold from dropping below a safe minimum (e.g., 2) 2. **Owner Whitelisting**: Only allows pre-approved addresses to become owners 3. **Removal Validation**: Ensures owner removals don't reduce threshold below minimum **How they prevent the attack:** * **Step 1**: `assertThresholdProtection()` blocks any attempt to reduce threshold to 1 * **Step 2**: `assertOwnerAddition()` blocks attacker addresses that aren't whitelisted * **Step 3**: `assertOwnerRemoval()` ensures threshold stays above minimum even when removing owners * **Result**: Attacker cannot gain solo control of the multisig **Key insight**: While these assertions can't prevent private key compromise or enforce time delays between transactions, they establish hard boundaries that attackers cannot cross regardless of how many keys they control. ## Key Takeaways The UxLink attack shows that multisig security requires both operational security (private key protection) and protocol-level protections (configuration validation). The \$39.3M total impact (\$11.3M direct + \$28M token minting) demonstrates how compromised private keys can lead to complete protocol takeover when governance controls are missing. Credible Layer assertions can enforce governance invariants: maintaining reasonable thresholds, validating owner changes, and preventing rapid reconfiguration. This approach ensures operational security failures don't lead to complete protocol compromise. # Vicuna Finance Oracle Manipulation Hack Source: https://docs.phylax.systems/assertions-book/previous-hacks/vicuna-finance-hack Vicuna Finance lost $700K due to LP token oracle manipulation that ignored invariant-based pricing This case study explains how the Vicuna Finance oracle manipulation hack worked and which assertion pattern could have constrained the invalid state transition. ## What Happened The Vicuna Finance hack resulted in a \$700K loss through oracle manipulation of Beets LP tokens used as collateral on the Sonic chain. The Core Bug was that LP tokens were priced using a simple sum formula: `price_lp = price_token1 * amount_token1 + price_token0 * amount_token0` instead of fair pricing that accounts for the underlying pool's constant product formula. **Exploitation Steps:** 1. **Pool Manipulation**: Attacker swapped large amounts from token0 to token1, artificially inflating the LP token's oracle-reported price 2. **Over-Collateralization**: Deposited the overvalued LP tokens as collateral and borrowed assets against the inflated value 3. **Price Deflation**: Reversed the swap (token1 back to token0), deflating the LP price and creating bad debt in the protocol The attack was executed across two markets - the `$S` market and the stablecoin market - draining approximately \$700K in total. The fundamental issue was that the oracle treated LP tokens like regular assets without considering that their value should reflect extractable value, not just the sum of underlying token values. ## Assertion Pattern A targeted price deviation check on all calls could have prevented this oracle manipulation attack. The assertion function monitors how each call affects oracle prices and reverts if any single call causes price swings exceeding 5%: ```solidity theme={null} function assertPriceDeviation() external view { BeetsLP assertionAdopter = BeetsLP(ph.getAssertionAdopter()); PhEvm.ForkId memory preFork = _preTx(); uint256 preOraclePrice = oracle.getPrice(token); // Get the price before the transaction // Using swap calls as an example, but any call that affects price should be checked PhEvm.CallInputs[] memory calls = ph.getCallInputs(address(assertionAdopter), assertionAdopter.swap.selector); for (uint256 i = 0; i < calls.length; i++) { PhEvm.ForkId memory postCallFork = PhEvm.ForkId({forkType: 3, callIndex: calls[i].id}); uint256 postOraclePrice = oracle.getPrice(token); // Calculate deviation and require change is within range uint256 deviation = ((postOraclePrice - preOraclePrice) * 10000) / preOraclePrice; require(deviation <= MAX_DEVIATION_BPS, "ORACLE_PRICE_MANIPULATION: Token price changed by more than 5% in single transaction"); } } ``` ## How the Assertion Would Have Prevented It This assertion function detects oracle price manipulation by monitoring how each call affects prices. **How it works:** 1. **Captures baseline**: Uses `_preTx()` with a Reshiram snapshot read to get the oracle price before any calls 2. **Monitors each call**: Iterates through calls (like swaps) that could affect the oracle price 3. **Checks price impact**: Uses a post-call `ForkId` with `ph.loadStateAt()` to see how each call changed the oracle price 4. **Enforces limits**: Reverts if any single call causes >5% price deviation from the baseline Using Phylax cheatcodes allows checking the oracle price at every call in the transaction, detecting price manipulation as it happens and preventing attacks that rely on temporary price distortions. ## Related Resources * [Oracle Manipulation Example](/assertions-book/assertions/ass28-intra-tx-oracle-deviation) # Visor Finance Unrestricted Mint Source: https://docs.phylax.systems/assertions-book/previous-hacks/visor-finance-unrestricted-mint Visor Finance allowed anyone to mint rewardTokens This is a fairly simple bug that let anyone mint rewardTokens. Background: [https://x.com/storming0x/status/1473321779250802693](https://x.com/storming0x/status/1473321779250802693) ## What Happened * The deposit function lets anyone mint rewardTokens if * the from address is a contract and has an owner and where msg.sender == owner * It is intended that the from address sends the underlying token to this contract * But it does not check whether delegatedTransferERC20 is implemented correctly * it can be a noop * The attacker can mint rewardTokens to himself ## Assertion Pattern While this is an obvious bug, an invariant could have prevented an exploit of the bug. Invariant: ```solidity theme={null} function assertionIsSolvent() public view { require(visr.balanceOf(address(adopter)) >= vvisr.totalSupply(), "Reward tokens are undercollateralized"); } ``` Alternatively, the assertion could test the correct behavior of the previous transaction. The assertion could be triggered by a call to the deposit function. ```solidity theme={null} function assertion_triggerDeposit_remainsSolvent() public view { // Get pre-transaction state PhEvm.ForkId memory preFork = _preTx(); uint256 preBalanceCollateral = visr.balanceOf(address(adopter)); uint256 preTotalSupplyRewards = vvisr.totalSupply(); // Get post-transaction state PhEvm.ForkId memory postFork = _postTx(); uint256 postBalanceCollateral = visr.balanceOf(address(adopter)); uint256 postTotalSupplyRewards = vvisr.totalSupply(); // Compare ratios using cross-multiplication to avoid precision loss // preBalance / preSupply >= postBalance / postSupply // => preBalance * postSupply >= postBalance * preSupply require( preBalanceCollateral * postTotalSupplyRewards >= postBalanceCollateral * preTotalSupplyRewards, "Reward tokens are undercollateralized" ); } ``` # Agentic PCL Source: https://docs.phylax.systems/credible/agentic-pcl Use an AI coding agent to create, test, and deploy Credible Layer assertion projects with pcl This guide shows you how to equip an AI coding agent to operate `pcl`, from creating an assertion project through deploying it with the Phylax platform. Phylax publishes reusable instructions in the [agent-skills repository](https://github.com/phylaxsystems/agent-skills). These skills give compatible agents the project structure, safety boundaries, and `pcl` workflows needed to complete a task instead of relying on a large one-off prompt. ## Prerequisites Before you begin, make sure you have: * [`pcl` installed](./credible-install) * An agent that supports the [Agent Skills format](https://agentskills.io), such as Codex or Claude Code * A local protocol repository the agent can inspect and edit * Clearly defined protocol invariants For deployment, you also need a target chain, an RPC endpoint, and access to the protocol manager wallet. Authenticate with the platform for your target network before starting the agent. See [How to Deploy Projects Through Agentic PCL](./agentic-pcl-deploy#1-authenticate-manually) for the Linea and Ethereum commands. An agent can edit code, create platform resources, and broadcast on-chain transactions. Review its plan and local changes before authorizing remote mutations. Require a successful dry run and explicit approval before any production deployment. ## Install the Phylax agent skills Install the two PCL workflow skills from GitHub: ```bash Codex theme={null} npx github:phylaxsystems/agent-skills#851cd274972efa6047393eaa61a935ed56f66b3b install pcl-assertion-workflow --agent codex npx github:phylaxsystems/agent-skills#851cd274972efa6047393eaa61a935ed56f66b3b install deploy-credible-assertions --agent codex ``` ```bash Claude Code theme={null} npx github:phylaxsystems/agent-skills#851cd274972efa6047393eaa61a935ed56f66b3b install pcl-assertion-workflow --agent claude-code npx github:phylaxsystems/agent-skills#851cd274972efa6047393eaa61a935ed56f66b3b install deploy-credible-assertions --agent claude-code ``` The commit pin ensures that both commands install the reviewed skill versions shown in this guide. The [agent-skills repository](https://github.com/phylaxsystems/agent-skills) also includes focused skills for invariant design, assertion implementation, testing, trigger optimization, and troubleshooting. Restart your agent after installation if it does not discover the new skills in the current session. ## Choose the workflow | Goal | Skill | What the agent should do | | --------------------------- | ---------------------------- | -------------------------------------------------------------------------------------------------------------------------------------------- | | Create an assertion project | `pcl-assertion-workflow` | Inspect the protocol, create the assertion project structure, configure dependencies, and run local tests | | Deploy through the platform | `deploy-credible-assertions` | Use the existing authentication, check RPC configuration, create or resolve the platform project, create a release, and activate it on-chain | Use the skill name in your request so the intended workflow is unambiguous. ## Start with a high-level prompt You can describe the intended outcome and let the skills determine the required `pcl` workflow. Include the protocol, target environment, authoritative sources, release contents, and verification boundary. For example: ```text theme={null} Use the Agentic PCL skills to deploy an Aave V3 Horizon project end to end on staging. Find and verify the authoritative deployed contract addresses on-chain. Create credible.toml using the latest reviewed Aave V3 assertions. Create the platform project and release. Verify that the release is correct, then set the project profile image from the specified official brand asset and deploy it. RPC: Signer: Project branding: Do not print, copy, or commit signing credentials. Ask for clarification if sources conflict or any requested project metadata is ambiguous. ``` ## Orient the agent with the installed CLI Current versions of `pcl` expose machine-readable guidance for agents. Include this instruction in your prompt: ```text theme={null} Before acting, inspect the installed pcl version, its machine-readable agent guide, and the help for the relevant workflow command. Treat the installed CLI as the source of truth. Prefer top-level workflow commands, structured JSON output, and the next actions returned by pcl. ``` This prevents the agent from inventing flags or relying on a workflow from another `pcl` version. ## Keep a human in the approval loop Authenticate with the target platform yourself before starting the deployment agent. Then give the agent autonomy for inspection, local file changes, builds, and tests. Require it to pause for: * Any choice between staging and production * Access to a signer or keystore * Platform mutations * On-chain broadcasts Do not paste a private key into the conversation or commit it to the repository. Prefer a Foundry keystore and provide its password through a file outside the project. Bootstrap and validate an assertion project locally Create a platform project and activate a release on-chain # How to Create a PCL Project with an Agent Source: https://docs.phylax.systems/credible/agentic-pcl-create-project Guide an AI coding agent through creating and testing a Credible Layer assertion project This guide shows you how to use the `pcl-assertion-workflow` skill to create a local assertion project in an existing protocol repository and verify it with `pcl`. ## Prerequisites Before you begin, make sure you have: * Completed the [Agentic PCL setup](./agentic-pcl) * [`pcl` installed](./credible-install) * A Foundry-based protocol repository * Written definitions of the invariants you want to protect ## 1. Start the agent in the protocol repository Give the agent access to the repository that contains the protocol contracts. Do not give it deployment credentials for this task; project creation and testing are local operations. Ask it to inspect the existing Foundry configuration, dependency layout, contracts, tests, and invariant documentation before proposing changes. ## 2. Request the project Use a prompt like this: ```text theme={null} Use the pcl-assertion-workflow skill to create a Credible Layer assertion project in this repository. The invariants are defined in: The protected contracts are: Before editing: 1. Inspect the repository and current Foundry configuration. 2. Explain which invariants are suitable for external-state assertions. 3. Propose the smallest project structure and test plan. 4. Ask before making any choice that changes the intended invariant. Create the assertion contracts, focused positive and negative tests, required Foundry profiles, remappings, and assertions/credible.toml. Run the relevant pcl tests and report the exact results. Do not authenticate, create platform resources, or deploy anything. ``` The explicit boundary at the end keeps project creation separate from deployment. ## 3. Review the proposed invariants Before allowing implementation, confirm that each proposed assertion: * Protects a security-relevant property * Observes external state rather than duplicating a local `require` * Names the contracts and state transitions it covers * Has a narrow trigger strategy * Can be exercised by both passing and failing tests If an invariant is ambiguous, refine it before the agent writes Solidity. ## 4. Review the generated project The exact structure should follow the host repository, but a typical result includes: ```text theme={null} assertions/ ├── credible.toml ├── src/ │ └── ExampleAssertion.a.sol └── test/ └── ExampleAssertion.t.sol ``` The agent may also update `foundry.toml`, `remappings.txt`, or dependency files. Review those changes for overlap with existing profiles and remappings. ## 5. Verify the project Give the agent this verification prompt: ```text theme={null} Run the complete assertion test suite through pcl, not Forge alone. Report the exact command, exit status, passing and failing tests, and any warnings. Do not continue to deployment. ``` Review the test output and ask the agent to summarize: * Which assertion functions executed * Which protected calls were tested * How each negative test proves the assertion invalidates a transaction * Any invariant or execution path that remains untested Passing tests do not prove that the chosen invariant is correct or complete. Review the assertion logic and threat model before moving to deployment. ## 6. Prepare for deployment Before handing the project to a deployment agent: * Commit or otherwise preserve the reviewed local changes * Confirm that `assertions/credible.toml` names every protected contract and assertion * Decide on staging or production * Identify the target chain and protocol manager wallet Continue with [How to Deploy Projects Through Agentic PCL](./agentic-pcl-deploy). # How to Deploy Projects Through Agentic PCL Source: https://docs.phylax.systems/credible/agentic-pcl-deploy Guide an AI coding agent through creating a platform project and deploying assertions on-chain This guide shows you how to deploy a project through Agentic PCL using the `deploy-credible-assertions` skill. The agent creates or resolves a Phylax platform project, creates an assertion release, and activates it on-chain with `pcl`. ## Prerequisites Before you begin, make sure you have: * Completed the [Agentic PCL setup](./agentic-pcl) * A reviewed assertion project that passes `pcl test` * A configured `assertions/credible.toml` * An authenticated `pcl` session for the target platform * The target chain ID and an RPC endpoint * Access to the protocol manager wallet through a Foundry keystore Confirm that your installed CLI supports the agentic deployment command: ```bash theme={null} pcl deploy --help ``` Deployment creates remote platform state and can broadcast an on-chain transaction. Start with staging unless you explicitly intend to deploy to production, and do not approve a broadcast until you have reviewed the dry-run result. ## 1. Authenticate manually Complete authentication yourself before giving the agent the deployment task. The platform URL selects the target network: ```bash Linea theme={null} pcl auth login ``` ```bash Ethereum theme={null} pcl auth -u https://ethereum.phylax.systems login ``` The default `https://app.phylax.systems` platform targets Linea. After login, `pcl` remembers the selected platform and uses it as the default for subsequent platform commands. Confirm the session before starting the agent: ```bash theme={null} pcl auth status ``` ## 2. Request a deployment plan Start with a prompt that provides the required choices and sets a clear approval boundary: ```text theme={null} Use the deploy-credible-assertions skill to prepare this assertion project for deployment. Target platform: Target chain ID: RPC: Environment: staging Signer: Foundry keystore Inspect the repository and credible.toml, then check the installed pcl command surface. Confirm the existing authentication and explain every remote or on-chain mutation that would be required. Do not create a project, create a release, access signing credentials, or broadcast a transaction until I explicitly approve the deployment. Never print, store, or commit secrets. ``` Use `production` only when that is your deliberate deployment target. ## 3. Review `credible.toml` For a new platform project, `assertions/credible.toml` needs a project name and no `project_id`: ```toml theme={null} environment = "staging" project_name = "my-protocol-assertions" [contracts.my_contract] address = "0x1234...5678" name = "My Contract" [[contracts.my_contract.assertions]] file = "src/MyAssertion.a.sol" ``` On the first approved deployment, `pcl deploy` creates the platform project and writes its `project_id` back to `credible.toml`. Review and commit that change after deployment. ## 4. Require a dry run Ask the agent to build and verify the project without changing remote or on-chain state: ```text theme={null} Do a dry run of the project deployment and verify the correctness of credible.toml. ``` Review the result for: * The protected contract addresses * The assertions and constructor arguments * Any warnings or failed verification The dry run returns after building and verifying the release payload. It does not authenticate, resolve a platform project, validate a chain, or inspect the protocol manager. Confirm those values separately from your authenticated session, `credible.toml`, and deployment prompt before continuing. ## 5. Approve the deployment After you approve the dry-run result, use a separate prompt: ```text theme={null} Deploy the project according to the credible.toml specification and broadcast the deployment transactions to the specified RPC endpoints. ``` The deployment workflow: 1. Creates or resolves the platform project 2. Verifies or sets the protocol manager 3. Builds and verifies the assertions 4. Creates or resumes the release 5. Waits for deployment-blocking checks 6. Broadcasts the activation transaction 7. Confirms the deployment with the platform `pcl deploy` observes existing state before each step. If an interruption occurs, ask the agent to inspect the structured error and rerun the same command; the workflow resumes rather than intentionally creating a duplicate release. ## 6. Verify the result Require the agent to report: * Project ID * Release ID * Environment * Transaction hash, if a transaction was broadcast * Deployment outcome * Any remaining timelock or activation step Keep these identifiers with your deployment record. You can inspect the project and release through the platform or the corresponding `pcl projects` and `pcl releases` commands. Review commands, configuration, and machine output Review the browser-assisted platform workflow # Apply Assertions Source: https://docs.phylax.systems/credible/apply-assertions Configure assertions and create a release on the platform using `pcl apply` This guide shows you how to configure your assertions in `credible.toml` and create a release on the platform with `pcl apply`. **Prerequisites**: * [pcl installed](/credible/credible-install) * An assertion [written](/credible/write-first-assertion) and [tested](/credible/testing-assertions) * A [project created](/credible/deploy-assertions-dapp#step-2-create-a-project) in the platform **What you'll do**: Authenticate, declare the desired assertion state in `credible.toml`, and create a release. Then review and deploy that release in the platform. ## Step 1: Authenticate Before deploying, authenticate with the Credible Layer: ```bash theme={null} pcl auth login ``` `pcl` displays a device code and verification URL. Press Enter to open the URL in your browser, authenticate with your wallet, email, Google, or GitHub, and approve the request. `pcl` then detects the completed authentication. Your account must be linked to the wallet address that owns the contracts listed in `credible.toml`. The platform verifies on-chain ownership (via the admin verifier, typically `owner()`) before allowing assertion deployment. See [Ownership Verification](/credible/ownership-verification) for details. Check your status anytime: ```bash theme={null} pcl auth status ``` ## Step 2: Configure `credible.toml` Create a `credible.toml` file at `assertions/credible.toml` in your project root. This file declares the desired release state for your project: which contracts are in scope and which assertion files should protect them. ```toml theme={null} environment = "production" [contracts.my_contract] address = "0xYOUR_CONTRACT_ADDRESS" name = "MyContract" [[contracts.my_contract.assertions]] file = "assertions/src/MyAssertion.a.sol" ``` To protect multiple contracts, add more entries: ```toml theme={null} environment = "production" [contracts.vault] address = "0xVAULT_ADDRESS" name = "Vault" [[contracts.vault.assertions]] file = "assertions/src/VaultAssertion.a.sol" [contracts.token] address = "0xTOKEN_ADDRESS" name = "Token" [[contracts.token.assertions]] file = "assertions/src/TokenDrainAssertion.a.sol" ``` Each contract address must be unique within the configuration. See the [pcl Reference](/credible/cli-reference#credibletoml-configuration) for all available fields. Set `project_id` in your `credible.toml` to skip the interactive project selection prompt. This is especially useful for CI/CD pipelines. `credible.toml` is declarative. If a later release removes a contract or assertion from the manifest, the platform treats that as a requested removal from the project when the release is reviewed, deployed, and the State Oracle timelock expires. ## Step 3: Apply Your Assertions Create a release on the platform: ```bash theme={null} pcl apply ``` This command: 1. Reads your `credible.toml` configuration 2. Builds and compiles the referenced assertion contracts 3. Previews the release changes against the current project state 4. Creates a pending release on the platform after you confirm You'll be prompted to confirm before applying. Use `--yes` to skip the confirmation prompt: ```bash theme={null} pcl apply --yes ``` `pcl apply` automatically builds your project. You can also run `pcl build` separately to check for compilation errors before applying. ## Step 4: Review and Deploy in the Platform After applying, complete deployment in the [Phylax platform](https://app.phylax.systems) using the [Deploy Assertions guide](/credible/deploy-assertions-dapp#step-4-deploy-the-assertion): 1. Navigate to your project 2. Select **Releases** 3. Choose the release created by `pcl apply` 4. Review the release diff and selected target contracts 5. Review **Assertion verification**, **Source code**, and **Backtesting**. See [Release Review Checks](./release-review-checks) for details. 6. Confirm the target environment declared in `credible.toml` 7. Connect the protocol manager wallet, select **Deploy to Staging** or **Deploy to Production**, and sign the transaction Creating a release through `pcl apply` does not make the assertion active by itself. The release is pending until an authorized protocol admin, also called a manager, signs the deployment transaction in the platform. The assertion becomes active only after that transaction is accepted on-chain and the configured timelock in the State Oracle contracts expires. Removals follow the same State Oracle timelock flow. ## Troubleshooting ### Authentication Issues | Error | Solution | | ------------------------ | ---------------------------------------- | | "Not authenticated" | Run `pcl auth login` | | "Authentication expired" | Run `pcl auth login` to refresh | | Browser doesn't open | Manually visit the URL shown in terminal | ### Apply Issues | Error | Solution | | ---------------------------- | -------------------------------------------------------------------------------------- | | "credible.toml not found" | Check that the file exists at `assertions/credible.toml` or specify the path with `-c` | | "duplicate contract address" | Each contract address must be unique in `credible.toml` | | "Project not found" | Create the project in the platform first, or set `project_id` in `credible.toml` | | Build failures | Run `pcl build` separately to diagnose compilation errors | ## Next Steps Complete deployment in the platform Full command reference Test before deployment Common issues and solutions # General Design Source: https://docs.phylax.systems/credible/architecture-overview How the Credible Layer components work together to enforce security rules This page provides an overview of the Credible Layer architecture, how the components fit together and interact to enforce security rules for smart contracts. Looking for a non-technical introduction? Start with the [Credible Layer Overview](/credible/credible-layer-overview). ## System Overview The Credible Layer consists of four core components: 1. **[Assertions](/credible/assertions-overview)**: Security rules written in Solidity that define states that should never occur 2. **[Assertion Enforcer](/credible/assertion-enforcer)**: Sidecar that validates transactions against assertions during block production 3. **[Credible Layer Contracts](/credible/credible-layer-contracts)**: On-chain registry that maps assertions to protected contracts 4. **[Assertion DA](/credible/assertion-da)**: Storage layer for assertion bytecode and source code ## How the Credible Layer Works The Credible Layer is a **sidecar security infrastructure** that validates transactions against developer-defined security rules (assertions) before they are included in blocks. As a sidecar, it runs alongside the L2 network's main components, intercepting transactions during block building and ensuring they don't violate any deployed security rules. The Assertion Enforcer is operated by the network's block builder or sequencer. Networks that integrate the Credible Layer run this sidecar as part of their block production infrastructure. This means enforcement does not rely on external execution services beyond the network you already trust to include transactions. ### System Architecture ```mermaid theme={null} --- title: Credible Layer System Architecture --- flowchart LR subgraph dev["Development Tools"] direction TB CLI["pcl"] PLATFORM["Phylax Platform"] end subgraph storage["Storage"] DA["Assertion DA"] end subgraph network["Network"] direction LR VALIDATOR["Block Builder / Sequencer"] REGISTRY["Credible Layer
Contracts"] end subgraph enforcer["Assertion Enforcer (Sidecar)"] direction TB SPACER_E[" "] PhEVM["PhEVM"] end CLI -->|"Create release"| PLATFORM PLATFORM -->|"Store"| DA PLATFORM -->|"Coordinate lifecycle"| REGISTRY VALIDATOR -->|"Candidate Tx"| PhEVM PhEVM -->|"Valid/Invalid"| VALIDATOR PhEVM -.->|"Fetch"| DA PhEVM -.->|"Check"| REGISTRY classDef dev fill:#388e3c,stroke:#1b5e20,stroke-width:2px,color:#fff classDef storage fill:#ff9800,stroke:#e65100,stroke-width:2px,color:#fff classDef network fill:#0288d1,stroke:#01579b,stroke-width:2px,color:#fff classDef sidecar fill:#7b1fa2,stroke:#4a148c,stroke-width:2px,color:#fff classDef invisible fill:none,stroke:none class CLI,PLATFORM dev class DA storage class VALIDATOR,REGISTRY network class PhEVM sidecar class SPACER_E invisible ``` The diagram shows two main flows: **Development Flow**: Developers use [`pcl`](/credible/apply-assertions) to develop, test, and prepare assertions for deployment. Running `pcl apply` compiles assertion code and creates a release on the [Phylax platform](https://app.phylax.systems), which handles storing it in [Assertion DA](/credible/assertion-da). An on-chain lifecycle action, such as `pcl deploy` or the platform deployment flow, then activates the release through the [Credible Layer Contracts](/credible/credible-layer-contracts). **Runtime Flow**: The block builder or sequencer sends transactions to the [Assertion Enforcer](/credible/assertion-enforcer) during block production. The enforcer uses its registry snapshot (from on-chain events) and cached assertion bytecode (from [Assertion DA](/credible/assertion-da)) to execute relevant assertions via [PhEVM](/credible/phevm). The network integration applies its inclusion policy to the resulting validation report. ### How It Works 1. **Assertion Release and Activation**: Developers write assertions and create a release with `pcl apply`. The platform stores the artifact in Assertion DA; a separate on-chain lifecycle action activates it 2. **Transaction Validation**: The network sends transactions to the Assertion Enforcer during block production 3. **Assertion Execution**: The Assertion Enforcer simulates each transaction and validates it against relevant assertions using PhEVM 4. **Validation Results**: The Assertion Enforcer returns valid/invalid results to the block builder or sequencer 5. **Network Policy**: The network integration uses the validation result when deciding whether to include the transaction ## Transaction Flow When a user submits a transaction, it goes through the following validation process: ```mermaid theme={null} --- title: Transaction Validation Flow --- flowchart LR USER["User"] -->|"Submits Transaction"| MP["Mempool"] MP --> BUILDER["Block Builder / Sequencer"] BUILDER -->|"Candidate Tx"| SIDECAR["Assertion Enforcer
(Sidecar)"] SIDECAR -->|"Validation report"| BUILDER BUILDER -->|"Apply inclusion policy"| DECISION{"Include?"} DECISION -->|"Yes"| BLOCK["Block"] DECISION -->|"No"| EXCLUDE["Excluded"] classDef user fill:#9e9e9e,stroke:#616161,stroke-width:2px,color:#fff classDef mempool fill:#64b5f6,stroke:#1976d2,stroke-width:2px,color:#fff classDef sidecar fill:#7b1fa2,stroke:#4a148c,stroke-width:2px,color:#fff classDef valid fill:#388e3c,stroke:#1b5e20,stroke-width:2px,color:#fff classDef invalid fill:#d32f2f,stroke:#b71c1c,stroke-width:2px,color:#fff class USER user class MP mempool class SIDECAR sidecar class BLOCK valid class EXCLUDE invalid ``` 1. **Transaction Submission**: User submits a transaction to the network 2. **Mempool Entry**: Transaction enters the mempool awaiting selection 3. **Block Builder Selection**: The block builder picks transactions from the mempool 4. **Assertion Validation**: Each transaction is validated against deployed assertions 5. **Inclusion Decision**: The network applies its inclusion policy to the validation report The Assertion Enforcer is integrated with the block builder. During block production, the block builder invokes the Assertion Enforcer to validate transactions before including them. ## Invalidation Lifecycle (Public View) When an assertion is violated, the invalidation is recorded and exposed for transparency and alerts. ```mermaid theme={null} --- title: Invalidation Lifecycle --- flowchart LR ENFORCER["Assertion Enforcer"] --> PLATFORM["Phylax Platform"] PLATFORM --> DASH["The Phylax Explorer"] PLATFORM --> ALERTS["Slack/PagerDuty Alerts"] classDef enforcer fill:#7b1fa2,stroke:#4a148c,stroke-width:2px,color:#fff classDef platform fill:#388e3c,stroke:#1b5e20,stroke-width:2px,color:#fff classDef output fill:#0288d1,stroke:#01579b,stroke-width:2px,color:#fff class ENFORCER enforcer class PLATFORM platform class DASH,ALERTS output ``` ## Integration Paths How protocols deploy and manage assertions How networks and sequencers integrate enforcement High-level component boundaries and dependencies For details on the assertion validation process, see [Assertion Enforcer](/credible/assertion-enforcer#validation-process). ## System Components ### Assertion Enforcer The [Assertion Enforcer](/credible/assertion-enforcer) is a sidecar that orchestrates transaction validation. It identifies which assertions apply to incoming transactions and invokes PhEVM to execute them. The network integration applies its inclusion policy to the resulting validation report. ### PhEVM (Phylax EVM) [PhEVM](/credible/phevm) is the execution engine that runs assertion bytecode. It extends the standard EVM with [cheatcodes](/credible/glossary#cheatcodes) for state inspection, enabling assertions to compare pre-transaction and post-transaction states. ### Assertion DA [Assertion Data Availability](/credible/assertion-da) stores assertion bytecode and source code, making them accessible to Assertion Enforcers and providing transparency for users and auditors. ### Credible Layer Contracts The [Credible Layer Contracts](/credible/credible-layer-contracts) are on-chain smart contracts that manage the assertion registry. The State Oracle coordinates protocol admins with network operators and serves as the source of truth for which assertions protect which contracts. ### Developer Tools * **[Phylax platform](https://app.phylax.systems)**: Web interface for deploying, managing, and viewing assertions * **[`pcl`](/credible/apply-assertions)**: Command-line tool for writing, testing, and deploying assertions * **[`credible-std`](/credible/credible-std-overview)**: Standard library exposing cheatcodes and testing utilities ## Network Integrations The Credible Layer can be implemented on different networks. The core concepts remain the same, but implementation details vary by network architecture. For specific implementation details, see: * [OP Stack Implementation](/credible/network-integrations/architecture-op-stack) *** For concrete assertion examples and real-world use cases, explore the [Assertions Book](/assertions-book/assertions-book-intro). ## Next Steps Write and deploy your first assertion Set up your development environment Comprehensive guide to writing assertions Detailed reference for assertion functions Guarantees, scope, and operational model # Assertion Data Availability Source: https://docs.phylax.systems/credible/assertion-da How assertion bytecode is stored and accessed in the Credible Layer [Assertion Data Availability (Assertion DA)](/credible/glossary#assertion-da-data-availability) is the storage layer that maintains [assertion bytecode](/credible/glossary#assertion-bytecode) and source code, making it accessible to [Assertion Enforcers](/credible/glossary#assertion-enforcer) and providing transparency for users and auditors. Assertion DA is managed by the platform. When you run [`pcl apply`](/credible/cli-reference#apply), the platform handles storing your assertion bytecode in Assertion DA automatically. You do not need to interact with Assertion DA directly. ## Purpose Assertion DA serves two primary functions: 1. **Persistent Storage**: Maintains EVM bytecode of assertions in an accessible location 2. **Integrity Verification**: Binds an assertion ID to its deployable creation data ## Key Concepts Before diving into how Assertion DA works, it's important to understand two key concepts: the Assertion ID and the DA Prover Signature. ### Assertion ID The assertion ID is deterministically derived from deployable creation data: ``` Assertion ID = Keccak256(Creation_Bytecode ++ Encoded_Constructor_Arguments) ``` The bytecode and encoded constructor arguments are stored separately in Assertion DA and combined to reconstruct the deployment data. This ensures: * Each unique assertion has a unique identifier * Assertion integrity can be verified by recomputing the hash * Submission compiles the Solidity source in a Dockerized `solc` environment before the artifact is stored ### Assertion DA Prover Signature The Assertion DA prover signature is generated by Assertion DA when an assertion is stored. This proof is used during deployment of the assertion to guarantee that the assertion bytecode is available on Assertion DA. ## Current Implementation The current implementation is operated by Phylax Systems with a highly available infrastructure: * **Storage**: Off-chain server stores assertion bytecode and source code * **Access**: Publicly accessible for transparency and verification * **Integration**: Works with [`pcl`](/credible/glossary#pcl-cli) and the [Phylax platform](https://app.phylax.systems). See the [Architecture Overview](/credible/architecture-overview) for details. ## How It Works ### Storing Assertions When you create a release using [`pcl apply`](/credible/cli-reference#apply), the platform handles storage in Assertion DA: 1. `pcl apply` compiles assertion contracts to EVM bytecode 2. The platform uploads flattened source code and compiler options to Assertion DA 3. An assertion ID (the Keccak256 hash of creation bytecode plus encoded constructor arguments) and DA prover signature are generated Only authorized admins can deploy, modify, or remove assertions for their contracts. This is enforced on-chain by the Credible Layer smart contracts, which verify administrative authority (such as owner-based checks) before allowing assertion management operations. The on-chain State Oracle contracts also enforce the configured timelock for both adding and removing assertions. Ownership verification will be expanded and improved in future versions to support additional ownership patterns. See [Ownership Verification](/credible/ownership-verification) for details. ### Retrieving Assertions Assertion Enforcers fetch assertions from Assertion DA upon on-chain deployment: 1. **On-Chain Deployment Event**: When an assertion is deployed on-chain, the `AssertionAdded` event is emitted 2. **Fetch Bytecode**: Assertion Enforcers detect the event and fetch the assertion bytecode from Assertion DA using the assertion ID 3. **Cache Internally**: Store assertion bytecode in internal cache for future use During transaction validation, Assertion Enforcers use the cached bytecode directly—no fetching occurs on the hot path. This ensures high-performance validation without network latency. See the [Architecture Overview](/credible/architecture-overview#assertion-validation-process) for details on how assertions are executed during validation. ## Complete Lifecycle The complete flow from assertion development to enforcement involves multiple steps: 1. **Development**: Write and test assertions locally using `pcl` 2. **Apply**: Run `pcl apply` to create a release on the platform. The platform stores assertion bytecode in Assertion DA and returns the assertion ID 3. **Deployment**: Review the assertion in the platform, link it to specific contract addresses, choose Staging or Production environment, and sign the transaction to deploy it on-chain 4. **Marked for Enforcement/Staging**: After the deployment transaction is accepted on-chain, the State Oracle timelock begins. During that period, the assertion is marked for enforcement (production) or marked for staging (staging environment) 5. **Enforced/Staged**: After the timelock expires, Assertion Enforcers fetch assertions from Assertion DA and execute them during block production. Assertions become enforced or staged If you later remove the assertion, that removal is also delayed by the configured State Oracle timelock before the assertion stops applying to transactions. For a detailed view of how these components interact, see the [System Architecture](/credible/architecture-overview#system-architecture) section in the Architecture Overview. ## Design Rationale ### Why Off-Chain Storage? * **Cost Efficiency**: EVM bytecode can be large; on-chain storage would be prohibitively expensive * **Performance**: Faster retrieval and caching for high-frequency validation * **Flexibility**: Enables future improvements without base layer changes * **Additional Metadata**: Supports metadata that wouldn't be feasible on-chain, such as instant source code verification for transparency and auditing ### Why Compilation Happens Off-Chain Assertion DA compiles submitted Solidity source off-chain, then the on-chain lifecycle uses the resulting deployment-data hash and availability signature. This keeps compilation and artifact storage outside the State Oracle while binding the on-chain assertion identifier to the exact creation data that enforcers later retrieve. ## Security Considerations **Availability**: The highly available infrastructure ensures consistent uptime. Assertion Enforcers cache assertion bytecode locally, so existing enforced assertions continue operating even during potential downtime. Only new assertion deployments require Assertion DA connectivity. **Integrity**: The Keccak256 hash verification ensures assertions haven't been modified. Each assertion ID uniquely corresponds to its creation bytecode and encoded constructor arguments. **Transparency**: Assertions can be retrieved via Assertion DA, enabling users and auditors to verify security measures. **Incentive Alignment**: Invalid assertions only harm the developer who submitted them, as they will fail execution deterministically. ## Next Steps Learn how to deploy assertions with pcl apply Complete reference for pcl commands Understand how Assertion DA fits into the system Learn more about Assertion DA terminology # Assertion Enforcer Source: https://docs.phylax.systems/credible/assertion-enforcer The sidecar component that orchestrates assertion validation during block production The Assertion Enforcer is a sidecar component that validates transactions against [assertions](/credible/glossary#assertion) during block production. It operates alongside the network's [sequencer](/credible/glossary#sequencer) or [block builder](/credible/glossary#block-builder), reporting which candidate transactions violate active assertions. ## Role in the System The Assertion Enforcer operates inside the block production pipeline: 1. Receives candidate transactions from the block builder or sequencer 2. Identifies which assertions apply to each transaction 3. Invokes [PhEVM](/credible/phevm) to execute assertions against transaction states 4. Returns validation results to the network 5. The network integration applies its inclusion policy to those results Depending on the network integration, validation can run synchronously before inclusion or through a bounded optimistic path where the builder checkpoints execution, runs assertions in parallel worker capacity, and rolls back if a transaction invalidates. ## Sidecar Architecture As a [sidecar](/credible/glossary#sidecar), the Assertion Enforcer: * **Operates independently** from the main L2 infrastructure * **Integrates alongside block builders** without changing core protocol rules * **Scales separately** from the main network components * **Preserves network continuity** by keeping block production policy under the network operator's integration This design allows networks to adopt the Credible Layer without modifying their core infrastructure. ## Validation Process When a transaction arrives for validation, the Assertion Enforcer orchestrates the following process: ```mermaid theme={null} --- title: Assertion Validation Detail --- flowchart LR TX["Transaction"] STATE1["Pre-Transaction State
(State1)"] subgraph simulation["EVM Simulation"] EVM["Execute Transaction"] end STATE2["Post-Transaction State
(State2)"] subgraph validation["PhEVM Assertion Validation"] PhEVM["Validate Against Assertions"] end ASSERTIONS["Deployed Assertions"] RESULT["Valid/Invalid"] TX --> EVM STATE1 --> EVM EVM --> STATE2 TX -.-> PhEVM STATE1 -.-> PhEVM STATE2 -.-> PhEVM ASSERTIONS --> PhEVM PhEVM --> RESULT classDef state fill:#e91e63,stroke:#880e4f,stroke-width:2px,color:#fff classDef evm fill:#0288d1,stroke:#01579b,stroke-width:2px,color:#fff classDef phevm fill:#f57c00,stroke:#e65100,stroke-width:2px,color:#fff classDef assertions fill:#388e3c,stroke:#1b5e20,stroke-width:2px,color:#fff classDef tx fill:#7b1fa2,stroke:#4a148c,stroke-width:2px,color:#fff classDef result fill:#ffa726,stroke:#e65100,stroke-width:2px,color:#fff class STATE1,STATE2 state class EVM evm class PhEVM phevm class ASSERTIONS assertions class TX tx class RESULT result ``` ### Step-by-Step 1. **Identify Relevant Assertions**: The Assertion Enforcer consults registry data (indexed from [on-chain events](/credible/credible-layer-contracts)) to find which assertions apply to the contracts the transaction interacts with 2. **Fetch Assertion Bytecode**: Assertion bytecode is retrieved from internal cache (populated from [Assertion DA](/credible/assertion-da) when assertions are deployed) 3. **Simulate Transaction**: The transaction is executed against pre-transaction state to produce the post-transaction state 4. **Execute Assertions**: [PhEVM](/credible/phevm) runs all relevant assertions with access to: * The transaction itself * Pre-transaction state (State1) * Post-transaction state (State2) 5. **Return Result**: * If any assertion reverts → transaction is invalid * If all assertions pass → transaction is valid ## Block Building Integration The Assertion Enforcer integrates with block builders so that the network can apply assertion-validation results during block production: * The block builder or sequencer receives validation results for candidate transactions * The network integration determines how those results affect inclusion * Block production continues normally with validated transactions ### Invalidation Handling When an assertion invalidates a candidate transaction, the integration applies the network's documented inclusion policy. In the usual production path, the invalid transaction is excluded before settlement and the platform records an invalidation. Some integrations may use optimistic execution to keep assertion work out of the serial block-building path. In that model, the builder creates a rollback checkpoint before speculative execution. If a transaction invalidates, the builder rolls back to the checkpoint before that transaction, excludes the invalid transaction, and replays later transactions within the configured speculative window. Rollback and replay cost must be bounded by policy. Integrations should define the speculative window, publication boundary, timeout behavior, and what happens when assertion workers fall behind. ## Performance Model The Assertion Enforcer is designed to keep the synchronous block-building path small. In the common case, the block builder pays for routing work such as metadata collection, assertion selection, checkpoint creation, and work submission. Assertion execution itself can run separately from that serial path, depending on the integration. The hot path should stay limited to the work required to route, schedule, and account for assertion execution: * collect the trace or metadata needed for assertion routing * select relevant assertions from the registry snapshot * create rollback checkpoints where the integration uses optimistic execution * submit bounded work to assertion workers * apply the validation result before the publication boundary The important performance constraint is keeping assertion work bounded and predictable for the transaction workload. Integrations use bounded queues, publication policies, fine-grained triggers, deterministic gas or runtime limits, and bounded execution surfaces to keep validation predictable. The enforcer also avoids network fetches on the transaction hot path. Assertion bytecode is fetched after deployment events and cached before validation. The primary performance risk is assertion tail latency. Production monitoring should track trigger rate, p95, p99, and maximum assertion execution time, invalidation behavior, worker backlog, and timeout rates. ## Production Admission and Resource Limits Production execution uses the active assertion set admitted through the configured registry and review process. Production assertion admission should account for: * Protected protocol areas and trigger conditions * Expected trigger frequency * Maximum gas or runtime budget * Expected read footprint * Deterministic behavior and read-only execution * Platform release-backtesting and staging behavior * Suitability for common acceleration paths, such as compact trace summaries or native helper functions These controls keep block-building resources predictable and help protocol teams understand which assertions are ready to promote from staging to production. ## Resource Isolation and Griefing Controls Assertions should not automatically consume production block-building resources just because they were published. Production admission and resource limits protect the network from broad, expensive, or poorly scoped assertions. Common controls include: * Authorization or review before an assertion enters the production execution set * Trigger scoping so assertions run only for relevant contracts, selectors, or state changes * Runtime and read-footprint limits * Dedicated worker capacity for assertion execution * Timeout behavior with clear inclusion-policy consequences * Staging and platform release-review requirements before production promotion Ingress filtering can also reduce repeated invalid submissions. When a transaction invalidates, the integration can record short-lived fingerprints for exact replays or repeated attempts against the same assertion and target contract or function. Broad fingerprints should use conservative TTLs and thresholds. ## Operational Expectations (Public) * **Non-invasive**: Runs alongside existing block builders without changing consensus rules * **Deterministic**: Given the same state, transaction, and assertion code, validation results are deterministic * **Staging support**: Networks can validate assertions before enforcing them in production * **Transparent outcomes**: Invalidations are visible in the platform and The Phylax Explorer ## Assertion Caching To ensure high-performance validation, the Assertion Enforcer maintains an internal cache of assertion bytecode: * **On deployment**: When an assertion is deployed on-chain, the Assertion Enforcer detects the event and fetches bytecode from [Assertion DA](/credible/assertion-da) * **During validation**: Assertions are loaded from cache. No network requests occur on the hot path. This caching strategy keeps assertion data retrieval out of the block-production hot path. ## Learn More High-level integration for networks and sequencers Guarantees, scope, and operational model # Overview Source: https://docs.phylax.systems/credible/assertions-overview Understanding Credible Layer assertions An [assertion](/credible/glossary#assertion) is a function that checks if a transaction violates a rule. If the rule is violated, the transaction is dropped during block building and never enters a block. Assertions are most useful when they describe an invalid effect, not every possible path that could produce it. A protocol may not know whether a future failure comes from an oracle issue, signer compromise, integration bug, rounding error, or governance action, but it can still define the state transition that should not be allowed. ## Assertion Specifications * **Legacy (V1)** exposes the original PhEVM precompiles, including mutable fork switching with `forkPreTx`, `forkPostTx`, and `forkPostCall`. * **Reshiram (V2)** replaces mutable fork switching with immutable `ForkId` snapshot reads and adds newer transaction and call inspection precompiles. Do not use Reshiram features on Linea yet. The current Linea deployment supports only Legacy (V1); wait until Linea is upgraded to support Reshiram (V2). ## How Assertions Work When a transaction is submitted to the network: * The system identifies which assertions apply to the contracts being interacted with * Assertions are configured with [triggers](/credible/glossary#trigger) that specify when they should execute (on specific function calls, storage changes, or balance changes) * The [PhEVM](/credible/glossary#phevm-phylax-evm) simulates the transaction and creates [pre/post state](/credible/glossary#pre-statepost-state) snapshots * All relevant assertions execute against these states * If all assertions pass → transaction is included; if any fail → transaction is dropped ## Example: Prevent Unauthorized Ownership Changes ```solidity theme={null} function checkOwnershipChange() external view { PhEvm.ForkId memory preTx = _preTx(); PhEvm.ForkId memory postTx = _postTx(); address ownerBefore = address(uint160(uint256(ph.loadStateAt(address(protocol), bytes32(uint256(0)), preTx)))); address ownerAfter = address(uint160(uint256(ph.loadStateAt(address(protocol), bytes32(uint256(0)), postTx)))); require(ownerBefore == ownerAfter, "Owner cannot change"); } ``` When a transaction tries to change the owner, this assertion runs. If the owner changed, the transaction is dropped. ## What They Can Do That Regular Solidity Can't **Enforce effects instead of hooks** Contract-level checks usually protect the code paths where they were added. Assertions can protect based on the resulting transaction effects, such as balance deltas, storage changes, nested calls, or debt changes. This helps cover paths that were not anticipated when the protocol contracts were originally written. **Compare before/after states** Regular Solidity only sees the current state during execution. Assertions can compare values before and after a transaction using [cheatcodes](/credible/glossary#cheatcodes) like `ph.loadStateAt` with explicit `ForkId` snapshots. You can also inspect state around a specific matched call by combining `ph.context()` with call-scoped `ForkId` values. **Protect immutable contracts** You can add assertions to contracts without modifying them. No redeployment needed. **Keep policy separate from protocol mechanics** Assertions let teams review security rules separately from accounting, settlement, permissioning, and integration logic. This can make it easier to audit what the rule is meant to prevent and to update the rule without upgrading the protected contract. **Check across multiple contracts** An assertion can read and validate state across multiple contracts in a single check, even if those contracts are in different protocols. **Run off-chain with higher gas limits** Assertions run [off-chain](/credible/glossary#off-chain-execution) with higher gas limits than typical on-chain operations, allowing for complex computations that would be too expensive in regular smart contracts. ## Common Use Cases * Prevent unauthorized parameter changes (owner, implementation addresses) * Enforce proportionality rules (withdrawals match shares burned) * Validate collateralization ratios in lending protocols * Monitor oracle price deviations * Check balance invariants (total supply equals sum of balances) * Enforce compliance rules (KYC/AML) * Validate cross-contract dependencies ## Constraints **Gas Limit** Assertion execution has a default limit of 3,000,000 gas. Node operators can configure this limit. If an assertion exceeds the active limit, the transaction is dropped. This bound keeps validation predictable under adversarial inputs. Transactions that exhaust the assertion gas budget are treated as invalid, preserving the enforcement invariant. Stay mindful of gas consumption: * Use [triggers](/credible/triggers) to run assertions only when needed * Account for variable gas costs in cheatcodes such as `getCallInputs()`, where input lengths can vary * Optimize your assertion logic to stay within the gas limit * Test with realistic data volumes - see [Gas Limits in Testing](/credible/testing-assertions#gas-limits) ## Hacks Assertions Would Have Prevented * **[Radiant Capital](/assertions-book/previous-hacks/hack1-radiant-capital)** (\$58M) - Owner takeover via compromised multisig * **[Bybit](/assertions-book/previous-hacks/bybit-safe-ui)** (\$1.4B) - Implementation change through compromised UI * **[Bunni](/assertions-book/previous-hacks/bunni-xyz-rounding-error)** (\$8.4M) - Withdrawal proportionality rounding error * **[Euler Finance](/assertions-book/previous-hacks/euler-finance-donation-hack)** (\$197M) - Missing health factor validation * **[Cream Finance](/assertions-book/previous-hacks/cream-finance-2)** (\$130M) - Price manipulation through donations * **[Balancer](/assertions-book/previous-hacks/balancer-v2-stable-rate-exploit)** (\$120M) - Rounding error accumulation See more examples in the [Previous Hacks Index](/assertions-book/previous-hacks/prev-hacks-index). ## Next Steps Step-by-step guide to writing your first assertion Tools available for writing assertions Learn about assertion triggers and optimization Real-world examples and implementations # How to Review Backtesting Results Source: https://docs.phylax.systems/credible/backtesting Review historical transactions that your assertions would have invalidated before you deploy a release This guide shows you how to review the automatic backtest for a release, inspect a matched historical transaction, and decide whether an assertion is ready to deploy or needs further tuning. **Prerequisites**: * A project in the Phylax platform * A release created with [`pcl apply`](./apply-assertions) * Access to review that project's releases ## What backtesting checks Backtesting is included in the platform's pre-release checks. When you create a release and open it for review, the platform tests every assertion in the release against transactions from the last 20,000 blocks. The results identify historical transactions that would have been prevented from settling if the current assertion set had been active. Use these findings to measure how an assertion behaves against real protocol activity before you deploy it. This is especially important for probabilistic or threshold-based protections, such as outflow circuit breakers and anomaly detection, where a threshold that is too restrictive can block benign behavior and one that is too permissive can miss harmful behavior. ## Open the release In the platform, open your project, select **Releases**, and choose the release you want to review. The release overview shows the proposed assertion changes and three pre-release checks: assertion verification, source code, and backtesting. See [Release Review Checks](./release-review-checks) for the fields and purpose of each check. Review the release diff first so you know which contracts and assertions are included. Then check the status beside **Backtesting**. A passed check means the backtest found no historical transaction that the release would have invalidated. **Issue found** means at least one transaction needs your review. Release overview for the MetaMorpho Top 5 Vaults project with assertion verification, source code, and backtesting checks ## Review a backtesting finding Select **Backtesting** to open the complete result. The summary shows the tested block range and whether the assertions invalidated any historical transactions. When the backtest finds an invalidation, the result identifies the matched transaction hash, assertion ID, block number, assertion adopter, and all assertion IDs watched during the replay. Start with the **Matched TX Hash**, **Matched Assertion ID**, and **Matched Assertion Adopter**. Together, these fields tell you which transaction was rejected, which assertion failed, and which protected contract it was evaluating. The attempt history records when the check ran, while **Transactions With Assertions** shows how many transactions in the range exercised the assertion set. Backtesting result for a release showing one historical transaction that would have been invalidated ## Inspect the invalidated transaction Copy the **Matched TX Hash** and paste it into the block explorer for the project's network. Review the sender and recipient, decoded function call, calldata, transferred value, token transfers, event logs, and internal calls. Compare that activity with the assertion's intended invariant and the matched adopter address. The goal is to explain why the assertion would have rejected a transaction that previously settled: the transaction might contain behavior you want to prevent, or it might reveal a legitimate protocol operation that the assertion does not yet handle. Next, inspect the **Matched Incident Payload** in the backtesting result. The failure entry maps the revert data to the assertion function, assertion ID, and adopter address. For assertions that depend on cumulative flows, an outflow window, or anomaly-detection context, also expand the previous transactions and review the block environment. The matched transaction alone may look benign even though the preceding activity caused the assertion's threshold or model to fire. Matched incident payload with revert data, assertion metadata, and previous transactions from the backtest ## Decide what to do next If the matched transaction represents behavior the assertion is intended to prevent, record why the finding is expected and continue reviewing the other release checks. A historical match can be useful evidence that the assertion detects the targeted behavior, but it does not prove that the assertion covers every harmful transaction. If the matched transaction is benign, treat it as a false positive. Adjust the assertion's thresholds, trigger scope, time window, or handling of normal protocol operations, then add the transaction as a regression case in your assertion tests. Create a new release with `pcl apply`; the platform will run the pre-release checks and backtest the updated assertion set again. If the matched transaction and assertion metadata do not explain the finding, inspect the **Matched Incident Payload** and expand the previous transactions. Decode the revert data, review the block environment, and confirm that the assertion ran against the intended adopter and state. Do not deploy the release until you can explain the finding from the transaction, assertion, and platform evidence. See [Troubleshooting](./troubleshooting) for common assertion failures. When the backtest passes, finish reviewing assertion verification and source code, then deploy the release to staging. Continue monitoring staging invalidations before promoting the assertion to production. A passing backtest confirms that the tested historical activity did not trigger the release; it is not a substitute for focused tests, known-exploit coverage, or staging observation. ## Next steps Add focused and regression tests before creating another release Create a new release after tuning an assertion Deploy a reviewed release to staging Review assertion verification, source code, and backtesting # Cheatcodes Source: https://docs.phylax.systems/credible/cheatcodes-overview Understanding cheatcodes in the Phylax Credible Layer and why they exist Cheatcodes are specialized testing and assertion utilities in the Phylax Credible Layer that extend beyond traditional EVM capabilities. Implemented as native code (Rust) rather than EVM bytecode, they provide developers with powerful tools for writing and testing assertions by offering deep inspection into transaction execution, storage changes, call traces, and blockchain state. ## Main Capabilities Cheatcodes enable functionality that would be impossible or impractical with standard Solidity: * **Snapshot state access**: Access blockchain state before or after a transaction or call with explicit `ForkId` snapshots * **Callstack introspection**: Inspect call traces and execution flow in ways not possible with standard EVM tools * **State change tracking**: Monitor specific storage slots and track how they change during transaction execution * **Triggering assertions**: Define precise conditions for when assertions should execute with `onFnCall` and `onTxEnd` triggers * **Cumulative flow tracking**: Register circuit-breaker triggers that collect ERC20 inflows or outflows into one bucket per block and evaluate the buckets over rolling windows ## Why Cheatcodes Exist Standard Solidity doesn't provide access to transaction execution history, call traces, or the ability to compare pre and post-transaction states. Cheatcodes fill this gap by providing native functions that can: * Compare values before and after a transaction * Track how storage slots change during execution * Identify which functions were called and in what order * Access logs and events from the transaction This makes it possible to write assertions that enforce security properties that would otherwise be impossible to check. You may notice the terms "precompiles" and "cheatcodes" used interchangeably in some contexts. We use the term "cheatcodes" as it's more familiar to Solidity developers who are already using testing frameworks like Foundry or Hardhat. Both terms refer to native functions that extend the EVM's capabilities, but "cheatcodes" better reflects their role in the developer experience. ## When to Use Cheatcodes Use cheatcodes when you need to: * **Compare state changes**: Check if values changed correctly (e.g., "balance decreased by exactly the withdrawal amount") * **Validate call patterns**: Ensure functions were called in the correct order or with expected parameters * **Monitor storage**: Track changes to specific storage slots that represent critical protocol state * **Limit cumulative flows**: Collect ERC20 inflows or outflows into one bucket per block and trigger checks when cumulative flow across the buckets exceeds configured rolling-window thresholds * **Optimize performance**: Use triggers to run assertions only when relevant state changes occur New to assertions? Check out [What are Assertions?](/credible/assertions-overview) to understand how cheatcodes fit into the bigger picture of writing security rules. ## Snapshot Read Guidance Not all assertions require checking both pre- and post-state. Understanding when to use each makes assertions more efficient. The current Phylax app and Linea deployment support the V1 assertion specification. `pcl` warns when an assertion uses the V2 Reshiram specification. Treat Reshiram-only precompile and trigger examples as local or development references until the target deployment supports V2. Prefer Reshiram snapshot reads for new assertions. Use explicit `PhEvm.ForkId` values with `ph.loadStateAt()` for transaction-wide comparisons, or `ph.context()` with call-scoped `ForkId` values inside an `onFnCall` assertion. ### When to Use Pre-State * Comparing values before and after a transaction * Building on top of specific state to verify invariants hold * Verifying that certain values remain constant ### When to Skip Pre-State * Only final values matter * Checking conditions that only matter after execution * Pre-state is irrelevant to your invariant See the [Cheatcodes Reference](/credible/cheatcodes-reference) for complete API documentation. ## Next Steps Ready to use cheatcodes in your assertions? Complete API reference for all available cheatcodes Learn how to write assertions using cheatcodes See practical examples of cheatcodes in action Real-world assertion examples and implementations # Cheatcodes API Reference Source: https://docs.phylax.systems/credible/cheatcodes-reference Reference for deprecated, legacy, and Reshiram cheatcodes in the Phylax Credible Layer New to cheatcodes? Start with [What are Cheatcodes?](./cheatcodes-overview) to understand what they are and why they exist. This reference lists the Credible Layer cheatcodes exposed through `credible-std`. Cheatcodes are grouped by API status: * **Legacy precompiles**: existing precompiles from before the Reshiram update. They remain available for legacy assertions. * **Reshiram precompiles**: newer APIs based on explicit `ForkId` snapshot reads, call context, richer log and call inspection, and protection-suite helpers. * **Deprecated cheatcodes**: legacy fork-switching APIs. Do not use them in new assertions. The current Phylax app and Linea deployment support the V1 assertion specification. `pcl` warns when an assertion uses the V2 Reshiram specification. Do not assume Reshiram-only precompiles or `onFnCall` and `onTxEnd` triggers are available until the target deployment supports V2. ## Assertion Specs `credible-std` defines assertion specs in `SpecRecorder.sol`. ```solidity theme={null} enum AssertionSpec { Legacy, Reshiram, Experimental } ``` | Spec | Availability | | -------------- | --------------------------------------------------------------------------------------------------------------- | | `Legacy` | Standard pre-Reshiram precompile set. Reshiram-only precompiles are unavailable. | | `Reshiram` | Reshiram precompiles plus the non-deprecated shared APIs. Legacy-only fork-switching selectors are unavailable. | | `Experimental` | Unrestricted access to all available precompiles. May include untested or dangerous behavior. | Register the spec in the assertion constructor: ```solidity theme={null} import {AssertionSpec} from "credible-std/SpecRecorder.sol"; constructor() { registerAssertionSpec(AssertionSpec.Reshiram); } ``` ## Common Types ### `ForkId` Identifies an immutable transaction snapshot. ```solidity theme={null} struct ForkId { uint8 forkType; uint256 callIndex; } ``` | `forkType` | Snapshot | | ---------- | --------------------- | | `0` | `PreTx` | | `1` | `PostTx` | | `2` | `PreCall(callIndex)` | | `3` | `PostCall(callIndex)` | Construct `ForkId` values explicitly: ```solidity theme={null} PhEvm.ForkId memory preTx = _preTx(); PhEvm.ForkId memory postTx = _postTx(); PhEvm.ForkId memory preCall = PhEvm.ForkId({forkType: 2, callIndex: callId}); PhEvm.ForkId memory postCall = PhEvm.ForkId({forkType: 3, callIndex: callId}); ``` ### `Log` Represents an Ethereum log emitted during transaction execution. ```solidity theme={null} struct Log { bytes32[] topics; bytes data; address emitter; } ``` ### `LogQuery` Filters logs by emitter and signature. ```solidity theme={null} struct LogQuery { address emitter; bytes32 signature; } ``` `address(0)` matches any emitter. `bytes32(0)` matches any topic0 signature. ### `CallInputs` Represents call input data recorded during transaction execution. ```solidity theme={null} struct CallInputs { bytes input; uint64 gas_limit; address bytecode_address; address target_address; address caller; uint256 value; uint256 id; } ``` Use `id` with call-scoped APIs such as `PhEvm.ForkId({forkType: 2, callIndex: id})`, `PhEvm.ForkId({forkType: 3, callIndex: id})`, `callinputAt(id)`, `callOutputAt(id)`, and `getLogsForCall(query, id)`. ## Legacy Precompiles Legacy precompiles are the standard cheatcodes from before the Reshiram update. Some are still useful, but prefer the Reshiram equivalents when you need explicit snapshot selection or call-scoped behavior. ### `getLogs` Returns all logs emitted during the assertion-triggering transaction. ```solidity theme={null} function getLogs() external returns (Log[] memory logs); ``` Use `getLogsQuery(query, fork)` when you need emitter or signature filtering, or `getLogsForCall(query, callId)` when you need call-scoped logs. ### `getAllCallInputs` Gets call inputs for a target and selector across `CALL`, `STATICCALL`, `DELEGATECALL`, and `CALLCODE`. ```solidity theme={null} function getAllCallInputs( address target, bytes4 selector ) external view returns (CallInputs[] memory calls); ``` Prefer the opcode-specific functions below when you need to avoid double counting through proxies. ### `getCallInputs` Gets call inputs for `CALL` opcodes only. ```solidity theme={null} function getCallInputs( address target, bytes4 selector ) external view returns (CallInputs[] memory calls); ``` ### `getStaticCallInputs` Gets call inputs for `STATICCALL` opcodes only. ```solidity theme={null} function getStaticCallInputs( address target, bytes4 selector ) external view returns (CallInputs[] memory calls); ``` ### `getDelegateCallInputs` Gets call inputs for `DELEGATECALL` opcodes only. ```solidity theme={null} function getDelegateCallInputs( address target, bytes4 selector ) external view returns (CallInputs[] memory calls); ``` ### `getCallCodeInputs` Gets call inputs for `CALLCODE` opcodes only. ```solidity theme={null} function getCallCodeInputs( address target, bytes4 selector ) external view returns (CallInputs[] memory calls); ``` Internal Solidity calls are not EVM calls and are not recorded by the call tracer. Calls made through `this.someFunction()` are external calls and can be recorded. ### `getStateChanges` Returns the sequence of values for a storage slot during transaction execution. ```solidity theme={null} function getStateChanges( address contractAddress, bytes32 slot ) external view returns (bytes32[] memory stateChanges); ``` The returned array includes the initial value as the first element. The length is either `0` or at least `2`. ### State Change Helpers `StateChanges.sol` provides typed helpers for reading slot changes as common Solidity types. ```solidity theme={null} function getStateChangesUint( address target, bytes32 slot ) internal view returns (uint256[] memory); function getStateChangesAddress( address target, bytes32 slot ) internal view returns (address[] memory); function getStateChangesBool( address target, bytes32 slot ) internal view returns (bool[] memory); function getStateChangesBytes32( address target, bytes32 slot ) internal view returns (bytes32[] memory); ``` The helper family also includes mapping-key and mapping-key-with-offset variants. ### `getAssertionAdopter` Returns the assertion adopter contract address associated with the current transaction. ```solidity theme={null} function getAssertionAdopter() external view returns (address); ``` This cheatcode is available in `triggers()` and assertion functions. It is not available in the constructor because assertion contracts have no state during deployment. ### `console.log` Prints debug information during local assertion testing. ```solidity theme={null} function console.log(string memory message) external; ``` Import it from `credible-std/Console.sol`. ## Legacy Trigger Registration Legacy trigger registration functions are internal helpers on `Assertion`. ### `registerCallTrigger` Registers an assertion function to run when the adopter receives a call. ```solidity theme={null} function registerCallTrigger( bytes4 assertionFnSelector ) internal view; function registerCallTrigger( bytes4 assertionFnSelector, bytes4 triggerSelector ) internal view; ``` The one-argument overload triggers on any call to the adopter. The two-argument overload triggers on calls matching `triggerSelector`. ### `registerStorageChangeTrigger` Registers an assertion function to run when adopter storage changes. ```solidity theme={null} function registerStorageChangeTrigger( bytes4 assertionFnSelector ) internal view; function registerStorageChangeTrigger( bytes4 assertionFnSelector, bytes32 slot ) internal view; ``` The one-argument overload triggers on any storage slot change. The two-argument overload triggers on a specific slot. ### `registerBalanceChangeTrigger` Registers an assertion function to run when the adopter's ETH balance changes. ```solidity theme={null} function registerBalanceChangeTrigger( bytes4 assertionFnSelector ) internal view; ``` ## Reshiram Precompiles Reshiram precompiles use explicit snapshot reads instead of global fork switching. In `credible-sdk`, these live under `crates/assertion-executor/src/inspectors/precompiles/reshiram/`. ### State Access #### `loadStateAt` Reads a storage slot from a snapshot fork. ```solidity theme={null} function loadStateAt( bytes32 slot, ForkId calldata fork ) external view returns (bytes32 value); function loadStateAt( address target, bytes32 slot, ForkId calldata fork ) external view returns (bytes32 value); ``` The first overload reads from the current assertion adopter. The second overload reads from any target account. #### `staticcallAt` Executes a read-only call against a snapshot fork. ```solidity theme={null} struct StaticCallResult { bool ok; bytes data; } function staticcallAt( address target, bytes calldata data, uint64 gas_limit, ForkId calldata fork ) external view returns (StaticCallResult memory result); ``` `data` contains return data when `ok` is `true` and revert data when `ok` is `false`. ### Logs #### `getLogsQuery` Returns logs matching an emitter/signature query from a snapshot fork. ```solidity theme={null} function getLogsQuery( LogQuery calldata query, ForkId calldata fork ) external view returns (Log[] memory logs); ``` #### `getLogsForCall` Returns logs matching a query from one recorded call frame. ```solidity theme={null} function getLogsForCall( LogQuery calldata query, uint256 callId ) external view returns (Log[] memory logs); ``` ### Call Inspection #### `callinputAt` Returns the raw calldata for a traced call. ```solidity theme={null} function callinputAt( uint256 callId ) external view returns (bytes memory input); ``` #### `callOutputAt` Returns the raw return or revert bytes for a traced call. ```solidity theme={null} function callOutputAt( uint256 callId ) external view returns (bytes memory output); ``` #### `matchingCalls` Returns recorded calls matching target, selector, and filter criteria. ```solidity theme={null} struct CallFilter { uint8 callType; uint32 minDepth; uint32 maxDepth; bool topLevelOnly; bool successOnly; } struct TriggerCall { uint256 callId; uint256 parentCallId; address caller; address target; address codeAddress; bytes4 selector; uint32 depth; uint8 callType; bool success; uint256 value; bytes input; } function matchingCalls( address target, bytes4 selector, CallFilter calldata filter, uint256 limit ) external view returns (TriggerCall[] memory calls); ``` `callType` uses `0` for any, `1` for `CALL`, `2` for `STATICCALL`, `3` for `DELEGATECALL`, and `4` for `CALLCODE`. ### Trigger Context #### `context` Returns context for the current `registerFnCallTrigger` invocation. ```solidity theme={null} struct TriggerContext { bytes4 selector; uint256 callStart; uint256 callEnd; } function context() external view returns (TriggerContext memory); ``` This reverts outside an assertion function triggered by `registerFnCallTrigger`. ### ERC20 Introspection #### `Erc20TransferData` Decoded ERC20 `Transfer` event data. ```solidity theme={null} struct Erc20TransferData { address token_addr; address from; address to; uint256 value; } ``` #### `getErc20Transfers` Returns decoded ERC20 transfers for one token in a snapshot fork. ```solidity theme={null} function getErc20Transfers( address token, ForkId calldata fork ) external view returns (Erc20TransferData[] memory transfers); ``` #### `getErc20TransfersForTokens` Returns decoded ERC20 transfers across multiple tokens in a snapshot fork. ```solidity theme={null} function getErc20TransfersForTokens( address[] calldata tokens, ForkId calldata fork ) external view returns (Erc20TransferData[] memory transfers); ``` #### `changedErc20BalanceDeltas` Returns all transfer records involving a token in a snapshot fork. ```solidity theme={null} function changedErc20BalanceDeltas( address token, ForkId calldata fork ) external view returns (Erc20TransferData[] memory deltas); ``` #### `reduceErc20BalanceDeltas` Aggregates transfers into net balance deltas per unique `(from, to)` pair. ```solidity theme={null} function reduceErc20BalanceDeltas( address token, ForkId calldata fork ) external view returns (Erc20TransferData[] memory deltas); ``` ### Mapping Tracing #### `changedMappingKeys` Returns canonical Solidity key encodings for mapping entries written during the transaction. ```solidity theme={null} function changedMappingKeys( address target, bytes32 baseSlot ) external view returns (bytes[] memory keys); ``` This is a best-effort trace heuristic. Custom assembly or precomputed hashed slots can produce false negatives. #### `mappingValueDiff` Returns pre-transaction and post-transaction values for one mapping entry. ```solidity theme={null} function mappingValueDiff( address target, bytes32 baseSlot, bytes calldata key, uint256 fieldOffset ) external view returns (bytes32 pre, bytes32 post, bool changed); ``` ### Transaction Object #### `getTxObject` Returns data from the original assertion-triggering transaction. ```solidity theme={null} struct TxObject { address from; address to; uint256 value; uint64 chain_id; uint64 gas_limit; uint128 gas_price; bytes input; } function getTxObject() external view returns (TxObject memory txObject); ``` ### Protection Suite Helpers #### `forbidChangeForSlot` Checks that one adopter storage slot was not modified. ```solidity theme={null} function forbidChangeForSlot( bytes32 slot ) external returns (bool ok); ``` #### `forbidChangeForSlots` Checks that none of the listed adopter storage slots were modified. ```solidity theme={null} function forbidChangeForSlots( bytes32[] calldata slots ) external returns (bool ok); ``` #### `conserveBalance` Checks that an account's ERC20 balance is unchanged between two forks. ```solidity theme={null} function conserveBalance( ForkId calldata fork0, ForkId calldata fork1, address token, address account ) external returns (bool); ``` #### `oracleSanity` Checks oracle price consistency across all fork points. ```solidity theme={null} function oracleSanity( address target, bytes calldata data, uint256 bpsDeviation ) external returns (bool); ``` #### `oracleSanityAt` Checks oracle price consistency between two specific forks. ```solidity theme={null} function oracleSanityAt( address target, bytes calldata data, uint256 bpsDeviation, ForkId calldata initialFork, ForkId calldata currentFork ) external returns (bool); ``` #### `assetsMatchSharePrice` Checks ERC4626 share price consistency across all fork points. ```solidity theme={null} function assetsMatchSharePrice( address vault, uint256 toleranceBps ) external returns (bool); ``` #### `assetsMatchSharePriceAt` Checks ERC4626 share price consistency between two forks. ```solidity theme={null} function assetsMatchSharePriceAt( address vault, uint256 toleranceBps, ForkId calldata fork0, ForkId calldata fork1 ) external returns (bool); ``` ### Circuit Breaker Context #### `outflowContext` Returns context for an assertion triggered by `watchCumulativeOutflow`. ```solidity theme={null} struct OutflowContext { address token; uint256 cumulativeOutflow; uint256 absoluteOutflow; uint256 currentBps; uint256 tvlSnapshot; uint256 windowStart; uint256 windowEnd; } function outflowContext() external view returns (OutflowContext memory ctx); ``` #### `inflowContext` Returns context for an assertion triggered by `watchCumulativeInflow`. ```solidity theme={null} struct InflowContext { address token; uint256 cumulativeInflow; uint256 absoluteInflow; uint256 currentBps; uint256 tvlSnapshot; uint256 windowStart; uint256 windowEnd; } function inflowContext() external view returns (InflowContext memory ctx); ``` On mainnet, bucket history is ingested concurrently with block building and can lag it, including partway through a block. When it does, the executor reconstructs net flow from the latest known balance and the current state, so `absoluteOutflow` and `absoluteInflow` may undercount gross flow. See [Bucket ingestion and balance reconstruction](../assertions-book/assertions/circuit-breakers#bucket-ingestion-and-balance-reconstruction). #### `FlowRateContext` Contains rate-of-change statistics for an assertion triggered by a cumulative-flow watcher. Rate fields are basis points of `tvlSnapshot` per second. ```solidity theme={null} struct FlowRateContext { address token; uint256 peakRateBps; uint256 lastRateBps; uint256 meanRateBps; uint256 tvlSnapshot; uint256 windowStart; uint256 windowEnd; } ``` #### `outflowRate` Returns rate-of-change context for an assertion triggered by `watchCumulativeOutflow`. The assertion must register `AssertionSpec.Experimental`. ```solidity theme={null} function outflowRate() external view returns (FlowRateContext memory ctx); ``` Returns a zeroed context when the assertion was not invoked by a matching cumulative-outflow trigger. In a zeroed context, `token == address(0)`. #### `inflowRate` Returns rate-of-change context for an assertion triggered by `watchCumulativeInflow`. The assertion must register `AssertionSpec.Experimental`. ```solidity theme={null} function inflowRate() external view returns (FlowRateContext memory ctx); ``` Returns a zeroed context when the assertion was not invoked by a matching cumulative-inflow trigger. In a zeroed context, `token == address(0)`. For calculations and edge cases, see [`outflowRate` and `inflowRate`](../assertions-book/assertions/rate-of-change-circuit-breakers). ### Math Helpers #### `mulDivDown` Computes `(x * y) / denominator`, rounded down, using 512-bit intermediates. ```solidity theme={null} function mulDivDown( uint256 x, uint256 y, uint256 denominator ) external pure returns (uint256 result); ``` #### `mulDivUp` Computes `(x * y) / denominator`, rounded up, using 512-bit intermediates. ```solidity theme={null} function mulDivUp( uint256 x, uint256 y, uint256 denominator ) external pure returns (uint256 result); ``` #### `normalizeDecimals` Scales an amount from one decimal base to another. ```solidity theme={null} function normalizeDecimals( uint256 amount, uint8 fromDecimals, uint8 toDecimals ) external pure returns (uint256 result); ``` #### `ratioGe` Compares two ratios with basis-point tolerance. ```solidity theme={null} function ratioGe( uint256 num1, uint256 den1, uint256 num2, uint256 den2, uint256 toleranceBps ) external pure returns (bool); ``` ### Reshiram Trigger Registration Reshiram trigger registration functions are internal helpers on `Assertion`. #### `registerFnCallTrigger` Registers an assertion that fires once per matching adopter call. Use `ph.context()` inside the assertion to inspect the matched call context. ```solidity theme={null} function registerFnCallTrigger( bytes4 fnSelector, bytes4 triggerSelector ) internal view; ``` #### `registerTxEndTrigger` Registers an assertion that fires once after the transaction completes. ```solidity theme={null} function registerTxEndTrigger( bytes4 fnSelector ) internal view; ``` #### `registerErc20ChangeTrigger` Registers an assertion that fires when a token's balances change. ```solidity theme={null} function registerErc20ChangeTrigger( bytes4 fnSelector, address token ) internal view; ``` #### `watchCumulativeOutflow` Registers a circuit breaker trigger that collects ERC20 outflow from the assertion adopter into one bucket per block. ```solidity theme={null} function watchCumulativeOutflow( address token, uint256 thresholdBps, uint256 windowDuration, bytes4 fnSelector ) internal view; ``` The trigger evaluates the per-block buckets over the configured rolling window. `thresholdBps` is measured against the TVL snapshot taken at the start of that window. `1000` is `10%`. #### `watchCumulativeInflow` Registers a circuit breaker trigger that collects ERC20 inflow into the assertion adopter into one bucket per block. ```solidity theme={null} function watchCumulativeInflow( address token, uint256 thresholdBps, uint256 windowDuration, bytes4 fnSelector ) internal view; ``` The trigger evaluates the per-block buckets over the configured rolling window. `thresholdBps` is measured against the TVL snapshot taken at the start of that window. `1000` is `10%`. ## Deprecated Cheatcodes Do not use these cheatcodes in new assertions. They mutate the active fork globally and are replaced by Reshiram's explicit `ForkId`-based `loadStateAt` API. ### `forkPreTx` Switches the active fork to the state before the assertion-triggering transaction. ```solidity theme={null} function forkPreTx() external; ``` Use `loadStateAt(..., _preTx())` instead. ### `forkPostTx` Switches the active fork to the state after the assertion-triggering transaction. ```solidity theme={null} function forkPostTx() external; ``` Use `loadStateAt(..., _postTx())` instead. ### `forkPreCall` Switches the active fork to the state before a specific call execution. ```solidity theme={null} function forkPreCall(uint256 id) external; ``` Use `loadStateAt(..., PhEvm.ForkId({forkType: 2, callIndex: id}))` instead. ### `forkPostCall` Switches the active fork to the state after a specific call execution. ```solidity theme={null} function forkPostCall(uint256 id) external; ``` Use `loadStateAt(..., PhEvm.ForkId({forkType: 3, callIndex: id}))` instead. ### `load(address, bytes32)` Loads a storage slot from an address on the current active fork. ```solidity theme={null} function load( address target, bytes32 slot ) external view returns (bytes32 data); ``` Use `loadStateAt(target, slot, fork)` instead. ## Related Pages Conceptual overview of cheatcodes Tutorial for writing an assertion Examples of assertion capabilities How to test assertions locally # CI/CD Integration Source: https://docs.phylax.systems/credible/ci-cd-integration Automate assertion testing in your CI/CD pipeline You can set up CI/CD workflows to ensure all assertion tests pass before merging code. The setup is very similar to standard Foundry/Forge workflows, with the addition of installing `pcl` and running `pcl test` for testing. ## GitHub Actions Example ```yaml theme={null} name: Phylax Assertion Tests on: pull_request: branches: [main, develop] paths: - "assertions/**" - "src/**" workflow_dispatch: env: FOUNDRY_PROFILE: assertions jobs: test: runs-on: ubuntu-latest steps: - name: Checkout code uses: actions/checkout@v4 with: submodules: recursive - name: Setup Foundry uses: foundry-rs/foundry-toolchain@v1 with: version: nightly - name: Install pcl run: | LATEST_VERSION=$(curl -fsSL https://api.github.com/repos/phylaxsystems/pcl/releases/latest | jq -r '.tag_name') curl -fsSL "https://github.com/phylaxsystems/pcl/releases/download/${LATEST_VERSION}/pcl-${LATEST_VERSION}-linux-x86_64.tar.gz" | tar -xz sudo install -m 0755 pcl/pcl /usr/local/bin/pcl - name: Run tests run: | pcl test ``` This workflow: * **Triggers on pull requests** to main/develop branches when assertion or source files change * **Supports manual runs** with `workflow_dispatch` * **Uses the assertions profile** via `FOUNDRY_PROFILE: assertions` * **Installs the latest pcl** from GitHub releases * **Runs all assertion tests** with `pcl test` Use the `FOUNDRY_PROFILE: assertions` environment variable to ensure the correct Foundry profile is used for testing assertions. ## Foundry Profile Configuration Foundry profiles allow you to configure different compilation and testing settings for different parts of your project. For assertions, you typically want separate profiles for unit and fuzz tests so slower suites do not run every time you want quick local feedback. This configuration goes in your project's `foundry.toml` file, which you should be familiar with if you have used Foundry before. ### Recommended Profile Structure Organize your tests into separate folders and create profiles for each test type: ``` assertions/ ├── src/ # Assertion source code └── test/ ├── unit/ # Fast unit tests └── fuzz/ # Fuzz tests (slower) ``` ### Example foundry.toml ```toml theme={null} [profile.default] src = "src" out = "out" libs = ["lib"] solc = "0.8.29" optimizer = true optimizer_runs = 200 # General assertions profile (runs all tests) [profile.assertions] src = "assertions/src" test = "assertions/test" out = "assertions/out" libs = ["lib"] solc = "0.8.29" optimizer = true optimizer_runs = 200 # Unit tests only (fast, for local development) [profile.unit-assertions] src = "assertions/src" test = "assertions/test/unit" out = "assertions/out" libs = ["lib"] solc = "0.8.29" optimizer = true optimizer_runs = 200 # Fuzz testing profile [profile.fuzz-assertions] src = "assertions/src" test = "assertions/test/fuzz" out = "assertions/out" libs = ["lib"] solc = "0.8.29" optimizer = true optimizer_runs = 10000 # Fuzz configuration (applies to all profiles) [fuzz] runs = 256 max_test_rejects = 65536 ``` ### Profile Benefits * **Unit tests (`unit-assertions`)** - Fast feedback during development * **Fuzz tests (`fuzz-assertions`)** - Run separately when testing edge cases * **General (`assertions`)** - Runs all tests for comprehensive validation When using `pcl test` or setting `FOUNDRY_PROFILE=`, Foundry uses that profile's configuration instead of the default one. ## Running Tests Locally with Profiles You can set the `FOUNDRY_PROFILE` environment variable to use specific profiles: ```bash theme={null} # Run only fast unit tests (recommended for local development) FOUNDRY_PROFILE=unit-assertions pcl test # Run fuzz tests FOUNDRY_PROFILE=fuzz-assertions pcl test # Run all assertion tests FOUNDRY_PROFILE=assertions pcl test ``` If nothing is specified, the default profile is used. ## Best Practices 1. **Run tests on PR** - Catch issues before merging 2. **Use path filters** - Only run tests when relevant files change 3. **Cache dependencies** - Speed up CI runs (Foundry toolchain action handles this) 4. **Separate profiles** - Keep assertion compilation separate from main project 5. **Pin versions** - Consider pinning the `pcl` version for reproducibility **Learn More:** * [Testing Assertions](/credible/testing-assertions) - Basic testing guide * [Fuzz Testing](/credible/fuzz-testing) - Test with random inputs * [Review Backtesting Results](/credible/backtesting) - Review the automatic backtest attached to a platform release * [Foundry Book - Testing](https://book.getfoundry.sh/forge/tests) # pcl CLI Reference Source: https://docs.phylax.systems/credible/cli-reference Reference documentation for `pcl` commands, options, configuration, and environment variables `pcl` is the Credible CLI for building, testing, verifying, deploying, and downloading Credible Layer assertions. New to `pcl`? Start with the [Quickstart Tutorial](/credible/pcl-quickstart) to learn the workflow. ## Version This reference matches [`pcl 1.8.0`](https://github.com/phylaxsystems/pcl/releases/tag/1.8.0). ```bash theme={null} pcl 1.8.0 Commit: f7ae8817db2f Build Timestamp: 2026-08-03T23:19:40Z ``` ## Syntax ```bash theme={null} pcl [OPTIONS] COMMAND ``` ## Global Options | Option | Description | | --------------- | -------------------------------------------------- | | `-j, --json` | Emit strict JSON output for programmatic consumers | | `--llms` | Print the CLI-native LLM usage guide and exit | | `-h, --help` | Print help | | `-V, --version` | Print version | ## Assertion Development Commands The commands below cover the assertion development workflow documented on this page. Run `pcl --help` for the complete command list for your installed version. | Command | Description | | --------------------------- | ----------------------------------------------------------------------- | | [`pcl test`](#test) | Run tests using Phorge | | [`pcl apply`](#apply) | Preview and apply declarative deployment changes from `credible.toml` | | [`pcl deploy`](#deploy) | Create or resolve a project, create a release, and activate it on-chain | | [`pcl auth`](#auth) | Authenticate the CLI with your Credible Layer Platform account | | [`pcl config`](#config) | Manage CLI configuration | | [`pcl build`](#build) | Build contracts using Phorge | | [`pcl verify`](#verify) | Verify assertions locally before deployment | | [`pcl download`](#download) | Download assertion source code for a protocol | ## `test` Runs tests using Phorge. ```bash theme={null} pcl test [OPTIONS] [PATH] ``` `[PATH]` is the contract file to test. It is a shortcut for `--match-path`. ### Common `test` Options | Option | Description | | ---------------------------------- | ----------------------------------------------------------- | | `-v, --verbosity...` | Increase log verbosity. Pass multiple times, such as `-vvv` | | `-q, --quiet` | Do not print log messages | | `--json` | Format log messages as JSON | | `--md` | Format log messages as Markdown | | `--color COLOR` | Set log color mode: `auto`, `always`, or `never` | | `-s, --suppress-successful-traces` | Show traces only for failures | | `--junit` | Output test results as a JUnit XML report | | `-l, --list` | List tests instead of running them | | `--summary` | Print a test summary table | | `--detailed` | Print a detailed test summary table | | `--gas-report` | Print a gas report | | `--fail-fast` | Stop after the first failure | | `--rerun` | Re-run recorded failures from the last run | | `-w, --watch [PATH...]` | Watch files or directories for changes | ### Test Filtering | Option | Description | | --------------------------- | ------------------------------------------- | | `--match-test REGEX` | Only run test functions matching the regex | | `--no-match-test REGEX` | Exclude test functions matching the regex | | `--match-contract REGEX` | Only run tests in matching contracts | | `--no-match-contract REGEX` | Exclude tests in matching contracts | | `--match-path GLOB` | Only run tests in matching source files | | `--no-match-path GLOB` | Exclude tests in matching source files | | `--no-match-coverage REGEX` | Exclude matching files from coverage output | ### EVM and Build Options `pcl test` supports many Forge-compatible EVM, fork, compiler, linker, cache, project, and watch options. Use `pcl test --help` for the complete option list. `pcl test` uses Phorge for test execution. Some Forge options may differ from upstream Foundry behavior. Use `pcl test --help` as the authoritative option list for your installed `pcl` version. ## `apply` Previews and applies declarative deployment changes from `credible.toml`. ```bash theme={null} pcl apply [OPTIONS] ``` `pcl apply` reads [`credible.toml`](#credibletoml-configuration), builds and verifies referenced assertion contracts, previews release changes against the platform, and creates a release after confirmation. ### `apply` Options | Option | Description | | ----------------------- | -------------------------------------------------------------------------------------------------------------------------------------------- | | `--root ROOT` | Project root directory. Default: `.` | | `-c, --config CONFIG` | Path to `credible.toml`, relative to root or absolute. Default: `assertions/credible.toml` | | `--json` | Emit machine-readable output for this command | | `--yes` | Apply without interactive confirmation | | `--auto-approve` | Alias for `--yes` | | `--dry-run` | Build and verify the release payload without calling the platform API | | `-u, --api-url API_URL` | Base URL for the platform API. Uses `PCL_API_URL` when set; otherwise, uses the platform remembered from the last login or network selection | | `-h, --help` | Print help | ### `apply` Behavior * If `project_id` is omitted from `credible.toml`, `pcl apply` prompts you to select a project interactively. * If JSON output is enabled, `project_id` is required in `credible.toml`. * If there are no release changes, the command exits without creating a release. * If `--yes` is omitted, the command prompts for confirmation before applying changes. ### `apply` Examples ```bash theme={null} pcl apply pcl apply --root ./my-project pcl apply --root ./my-project -c path/to/credible.toml pcl apply --yes pcl apply --json --yes ``` ## `deploy` Creates or resolves a platform project, verifies or sets its protocol manager, creates a release, activates the release on-chain, and confirms the deployment. ```bash theme={null} pcl deploy [OPTIONS] ``` ### `deploy` Options | Option | Description | | --------------------------------------- | -------------------------------------------------------------------------------------------------------------------------------------------- | | `--root ROOT` | Project root directory. Default: `.` | | `-c, --config CONFIG` | Path to `credible.toml`, relative to root or absolute. Default: `assertions/credible.toml` | | `--yes`, `--auto-approve` | Proceed without interactive confirmations | | `--dry-run` | Build and verify locally, report which steps would act, and make no changes | | `-u, --api-url API_URL` | Base URL for the platform API. Uses `PCL_API_URL` when set; otherwise, uses the platform remembered from the last login or network selection | | `--private-key PRIVATE_KEY` | Hex-encoded private key used to sign transactions and challenges. Can also be set with `PCL_PRIVATE_KEY` | | `--account ACCOUNT` | Foundry keystore name from `~/.foundry/keystores` | | `--keystore-password KEYSTORE_PASSWORD` | Foundry keystore password. Can also be set with `PCL_KEYSTORE_PASSWORD` | | `--keystore-password-file PATH` | File containing the Foundry keystore password. Can also be set with `PCL_KEYSTORE_PASSWORD_FILE` | | `--rpc-url RPC_URL` | RPC endpoint used to broadcast transactions. Can also be set with `PCL_RPC_URL` | | `--confirmations CONFIRMATIONS` | Confirmations to wait for after broadcasting. Values below the platform requirement are rejected | | `--tx-timeout-secs SECONDS` | Transaction confirmation timeout. Default: `300` | | `--project-name PROJECT_NAME` | Project name used when `credible.toml` has no `project_id`; overrides `project_name` in the file | | `--chain-id CHAIN_ID` | Chain ID used when creating a project. Existing project chains are read from the platform | | `--skip-protocol-manager` | Skip protocol-manager verification or configuration | | `--check-timeout-secs SECONDS` | Timeout for deployment-blocking release checks. Default: `600` | | `-j, --json` | Emit strict JSON output | | `--llms` | Print the CLI-native LLM usage guide and exit | | `-h, --help` | Print help | ### `deploy` Behavior * `--dry-run` returns after building and verifying the local release payload. It does not authenticate, resolve a project, validate a chain, or inspect the protocol manager. * Without `--dry-run`, the command requires authentication, project information, an RPC endpoint, and a signer unless the relevant step is already complete or explicitly skipped. * If `credible.toml` has no `project_id`, provide a project name and chain ID so the command can create the project. * Existing projects use the chain recorded by the platform. * If `--yes` is omitted, the command requests confirmation before mutations and broadcasts. * The command observes existing state before each step so an interrupted workflow can resume. ### `deploy` Examples ```bash theme={null} pcl deploy --dry-run pcl deploy --account protocol-manager --rpc-url https://example-rpc.invalid pcl deploy --project-name my-protocol --chain-id 84532 --account protocol-manager --rpc-url https://example-rpc.invalid --yes --json ``` ## `auth` Authenticates the CLI with your Credible Layer Platform account. ```bash theme={null} pcl auth [OPTIONS] COMMAND ``` ### `auth` Commands | Command | Description | | --------- | ----------------------------------------------------------------- | | `ensure` | Confirm that authentication is usable or return a login challenge | | `login` | Login to PCL | | `poll` | Poll a pending device-login session once | | `refresh` | Refresh authentication or return a login challenge | | `logout` | Logout from PCL | | `status` | Check current authentication status | | `help` | Print help | ### `auth` Options | Option | Description | | ------------------------- | ------------------------------------------------------------------------------------------------------------------------------------------------------- | | `-u, --auth-url AUTH_URL` | Base URL for authentication. Resolution order: `PCL_AUTH_URL`, `PCL_API_URL`, the URL remembered from the last login, then `https://app.phylax.systems` | | `-h, --help` | Print help | `pcl auth login` displays a device code, then opens a browser after you press Enter. Use `--no-wait` with `--json` to return the login challenge without waiting for verification. ## `config` Manages CLI configuration. ```bash theme={null} pcl config COMMAND ``` ### `config` Commands | Command | Description | | ---------------------- | ---------------------------------------------------------------- | | `show` | Display the current configuration | | `delete` | Delete the current configuration | | `set-rpc CHAIN_ID URL` | Store the RPC endpoint used to broadcast transactions on a chain | | `unset-rpc CHAIN_ID` | Remove the stored RPC endpoint for a chain | | `help` | Print help | Configuration is stored in `~/.config/pcl/config.toml` by default and includes authentication state, the remembered platform URL, and per-chain RPC settings. ## `build` Builds contracts using Phorge. ```bash theme={null} pcl build [OPTIONS] ``` ### `build` Options | Option | Description | | ------------- | ----------------------------- | | `--root ROOT` | Root directory of the project | | `-h, --help` | Print help | ## `verify` Verifies assertions locally before deployment. ```bash theme={null} pcl verify [OPTIONS] [ASSERTION] ``` `[ASSERTION]` can be a contract name or `file:contract`. If omitted, `pcl verify` verifies all assertions from `credible.toml`. ### `verify` Options | Option | Description | | --------------------- | ------------------------------------------------------------------------------------------ | | `--root ROOT` | Project root directory. Default: `.` | | `-c, --config CONFIG` | Path to `credible.toml`, relative to root or absolute. Default: `assertions/credible.toml` | | `--args ARGS...` | Constructor arguments for the assertion | | `--json` | Emit machine-readable JSON output | | `-h, --help` | Print help | ### `verify` Behavior * When `[ASSERTION]` is omitted, constructor arguments come from each assertion's `args` field in `credible.toml`. * `--args` can only be used when verifying a specific assertion. * Constructor arguments are ABI-encoded against the assertion contract constructor. * The command exits with code `1` if any assertion fails verification. ### Verification Statuses | Status | Meaning | | ------------------------ | ---------------------------------------------------------------------------- | | `success` | The assertion verified successfully | | `deployment_failure` | The assertion failed during deployment in the local verification environment | | `no_triggers` | The assertion did not expose any triggers | | `missing_assertion_spec` | The assertion is missing the required assertion specification | | `invalid_assertion_spec` | The assertion specification is invalid | ### `verify` Examples ```bash theme={null} pcl verify pcl verify OwnableAssertion pcl verify assertions/src/OwnableAssertion.a.sol:OwnableAssertion pcl verify OwnableAssertion --args 0x75634113D6A2fbfF5e65151ce1572195bE1d001A pcl verify --json ``` ## `download` Downloads assertion source code for a protocol. ```bash theme={null} pcl download [OPTIONS] ``` ### `download` Options | Option | Description | | ----------------------------- | -------------------------------------------------------------------------------------------------------------------------------------------- | | `--project-id PROJECT_ID` | Project UUID to download assertions from | | `-o, --output-dir OUTPUT_DIR` | Output directory for `.sol` files. Default: `PROJECT_NAME-assertions/` | | `--json` | Emit machine-readable output for this command | | `-u, --api-url API_URL` | Base URL for the platform API. Uses `PCL_API_URL` when set; otherwise, uses the platform remembered from the last login or network selection | | `-h, --help` | Print help | ### `download` Behavior * `--project-id` is required. * The command requires authentication. Run `pcl auth login` first. * By default, files are written to a directory named after the project: `PROJECT_NAME-assertions/`. * Downloaded files use the pattern `CONTRACT_NAME_ASSERTION_ID_PREFIX.sol`. * Assertions without available source are skipped. ### `download` Examples ```bash theme={null} pcl download --project-id 550e8400-e29b-41d4-a716-446655440000 pcl download --project-id 550e8400-e29b-41d4-a716-446655440000 -o ./downloaded-assertions pcl download --project-id 550e8400-e29b-41d4-a716-446655440000 --json ``` ## `credible.toml` Configuration The `credible.toml` file defines assertion deployment configuration for `pcl apply` and `pcl verify`. **Default location:** `assertions/credible.toml`, relative to the project root. ### Format ```toml theme={null} environment = "production" project_id = "550e8400-e29b-41d4-a716-446655440000" [contracts.my_contract] address = "0x1234567890abcdef1234567890abcdef12345678" name = "MyContract" [[contracts.my_contract.assertions]] file = "assertions/src/MyAssertion.a.sol" args = ["0x75634113D6A2fbfF5e65151ce1572195bE1d001A", "42"] ``` ### Root Fields | Field | Type | Required | Description | | ------------- | ------ | -------- | ---------------------------------------------------------------- | | `environment` | string | Yes | Deployment environment name, such as `"production"` | | `project_id` | UUID | No | Platform project ID. Required when `pcl apply` emits JSON output | | `contracts` | map | Yes | Named contract definitions | ### Contract Fields | Field | Type | Required | Description | | ------------ | ------ | -------- | ------------------------------------ | | `address` | string | Yes | Contract address on-chain | | `name` | string | Yes | Human-readable contract name | | `assertions` | array | Yes | Assertions to apply to this contract | ### Assertion Fields | Field | Type | Required | Description | | ------ | --------------- | -------- | --------------------------------------------------------------------------------------------------------------------- | | `file` | string | Yes | Assertion contract file path. Use `file.sol:ContractName` when the contract name cannot be inferred from the filename | | `args` | array or scalar | No | Constructor arguments for the assertion. Values are converted to strings before ABI encoding | ### Contract Name Inference `pcl` infers assertion contract names from `file` in this order: | `file` value | Inferred contract | | ---------------------------------------------------- | ------------------- | | `assertions/src/MyAssertion.a.sol:ExplicitAssertion` | `ExplicitAssertion` | | `assertions/src/MyAssertion.a.sol` | `MyAssertion` | | `assertions/src/MyAssertion.sol` | `MyAssertion` | ### Validation * Contract addresses must be unique within the file. * `pcl verify` returns an error if `credible.toml` contains no assertions. * `pcl apply --json` returns an error if `project_id` is missing. ## Environment Variables | Variable | Used by | Description | Default | | -------------- | --------------------- | --------------------------------------- | ------------------------------------------------------------------------------- | | `PCL_AUTH_URL` | `pcl auth` | Base URL for the authentication service | `PCL_API_URL`, then the remembered login URL, then `https://app.phylax.systems` | | `PCL_API_URL` | Platform API commands | Base URL for the platform API | Platform remembered from the last login or network selection | ## Configuration File `pcl` stores CLI configuration in `~/.config/pcl/config.toml` by default. Use `pcl config show` to view the current configuration and `pcl config delete` to delete it. ## Next Steps Learn how to create an assertion release with `pcl apply` Step-by-step tutorial for your first assertion Install pcl Deploy assertions to protect your contracts # Installation Source: https://docs.phylax.systems/credible/credible-install This page explains how to install the Phylax Credible Layer (`pcl`) CLI tool `pcl` is the command-line tool for building, testing, storing, and submitting assertions to the Phylax Credible Layer. ## Installation ### Option 1: Install with Brew (Recommended) The fastest and easiest way to install `pcl` is using Brew: ```bash theme={null} brew install phylax/pcl/phylax ``` This will install the `pcl` binary. ## Verifying Installation To verify that `pcl` is installed correctly, run: ```bash theme={null} pcl --version ``` You should see the version number of the installed `pcl` CLI. ## Installing the `credible-std` Library If you're looking to add the `credible-std` library to your existing project for writing assertions, see the [credible-std Library Overview](/credible/credible-std-overview) for the package name, stable dependency, and remapping reference. ## Next Steps Now that you have `pcl` installed, you can learn how to [get started](/credible/pcl-quickstart) with the Credible Layer. # Introduction Source: https://docs.phylax.systems/credible/credible-introduction Block exploits before they execute by linking security rules to your smart contracts on-chain. Use this page to understand what the Credible Layer is and choose the right documentation path for your goal. ## What is the Credible Layer? The Credible Layer is security infrastructure that enables developers to link security rules to their smart contracts on-chain. Then, the network validates every transaction that interacts with their smart contracts against their security rules, dropping any invalidating transaction. Use this page to choose the right kind of documentation for what you need next: * Learn by doing: [Quickstart Tutorial](./pcl-quickstart) * Complete a specific task: [How-to Guides](./credible-install) * Understand the system: [High-Level Overview](./credible-layer-overview) * Look up commands and APIs: [Reference](./cli-reference) ## How It Works Write assertions—security rules that define states your protocol should never reach. No contract modifications required. The network checks each transaction against your assertions before inclusion in a block. Transactions that violate your rules are dropped by the network and never execute. ## Choose the Right Path Follow a guided tutorial to write, test, and deploy your first assertion end to end. Jump straight to task-focused guides for installation, deployment, testing, and operations. Read the explanation docs for architecture, trust model, assertions, and the platform. Use the reference docs for commands, cheatcodes, glossary entries, and use-case mappings. ## By Audience See the adoption path for writing assertions, deploying them, and monitoring invalidations. See the high-level integration path for enforcement during block building. Browse pattern catalogs and exploit case studies in the Assertions Book. Inspect deployed assertions, invalidations, and public protocol coverage. ## Key Benefits * **Pre-execution prevention** — Exploits are blocked before they execute, not detected after * **No contract changes** — Add protection to any contract, including immutable ones * **Transparent & verifiable** — All rules are public Solidity, auditable by anyone * **Readable security posture** — Understand circuit breakers and verifiable operational risks through clear, plain-English breakdowns * **No external execution services** — Enforcement runs within the network’s block-building flow * **Deterministic decisions** — Binary enforcement based on your rules, not opaque scoring ## Community & Support Have questions or want to connect with the Phylax community? * Join our [Telegram](https://t.me/phylax_credible_layer) * Follow us on [X/Twitter](https://x.com/phylaxsystems) * Explore our [GitHub](https://github.com/phylaxsystems) * Visit the [Phylax Website](https://phylax.systems) ## Learn More For the visual learners, here's a video introduction to the Credible Layer: