phylaxsystems · odyslam · May 12, 2026 · May 12, 2026 · May 12, 2026 · May 12, 2026
diff --git a/assertions-book/assertions/aave-v3-suite.mdx b/assertions-book/assertions/aave-v3-suite.mdx
@@ -23,7 +23,7 @@ We have mocked parts of the protocol in order to properly test the assertions an
 
 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.
 
-We would recommend running the assertions in a test environment against old transactions to ensure that the assertions do not trigger false positives or other unexpected behavior. This is standard best practice that should be followed for any protocol upgrades and does not just apply to assertions.
+We recommend running the assertions in a test environment against historical transactions to validate behavior before production promotion. This is standard best practice for protocol upgrades and does not just apply to assertions.
 
 ## Here Be Dragons 🐲
 

diff --git a/assertions-book/assertions/ass08-sum-of-all-positions.mdx b/assertions-book/assertions/ass08-sum-of-all-positions.mdx
@@ -25,7 +25,7 @@ Uses these cheatcodes:
 - `ph.context()` and `ph.callinputAt()`: Inspect the triggered position-modifying call
 - `registerFnCallTrigger()`: Trigger on position-modifying functions
 
-Check the [Modified Keys](/credible/use-case-mappings/unsupported-use-cases/modified-keys) use case for details on what direct position iteration would look like.
+Check [Modified Key Discovery](/credible/use-case-mappings/unsupported-use-cases/modified-keys) for details on what direct position iteration would look like.
 
 For more information about cheatcodes, see the [Cheatcodes Documentation](/credible/cheatcodes-reference).
 

diff --git a/assertions-book/previous-hacks/abracadabra-gmx-v2-exploit.mdx b/assertions-book/previous-hacks/abracadabra-gmx-v2-exploit.mdx
@@ -3,6 +3,8 @@ title: Abracadabra GMX V2 Cauldron Exploit
 description: 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.
@@ -108,4 +110,4 @@ The exploit succeeded because of the growing gap between reported and actual val
 - **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.
+**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.
diff --git a/assertions-book/previous-hacks/abracadabra-hack-3.mdx b/assertions-book/previous-hacks/abracadabra-hack-3.mdx
@@ -3,6 +3,8 @@ title: Abracadabra CauldronV4 Cook Function Exploit
 description: 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.

diff --git a/assertions-book/previous-hacks/abracadabra-rounding-error.mdx b/assertions-book/previous-hacks/abracadabra-rounding-error.mdx
@@ -3,6 +3,8 @@ title: Abracadabra Rounding Error Attack
 description: 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:
@@ -76,4 +78,4 @@ contract AbracadabraRebaseInvariantAssertion is Assertion {
 }
 ```
 
-This assertion ensures that when no assets are owed (elastic = 0), there should be no debt shares (base = 0), thereby preventing the exploit.
+This assertion ensures that when no assets are owed (elastic = 0), there should be no debt shares (base = 0), thereby preventing the exploit.
diff --git a/assertions-book/previous-hacks/balancer-v2-stable-rate-exploit.mdx b/assertions-book/previous-hacks/balancer-v2-stable-rate-exploit.mdx
@@ -3,6 +3,8 @@ title: Balancer V2 Rate Manipulation Exploit
 description: $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.
@@ -16,7 +18,7 @@ This demonstrates how assertions protect protocols by focusing on *what should n
 
 <Warning>
 
-This assertion was developed by analyzing the observable effects of the exploit (drastic rate changes) rather than the root cause (rounding error accumulation). While this approach provides broad protection against rate manipulation attacks, it may not cover all edge cases or could potentially trigger false positives on legitimate operations that we have not yet discovered.
+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.
 
@@ -176,7 +178,7 @@ We chose **3x (300%)** as the threshold based on the following analysis:
 - 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. If false positives occur in production, the threshold can be increased to 5x or higher, though this would reduce sensitivity to smaller manipulation attempts.
+**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.

diff --git a/assertions-book/previous-hacks/bunni-xyz-rounding-error.mdx b/assertions-book/previous-hacks/bunni-xyz-rounding-error.mdx
@@ -3,6 +3,8 @@ title: Bunni XYZ Rounding Error Exploit
 description: 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.

diff --git a/assertions-book/previous-hacks/bybit-safe-ui.mdx b/assertions-book/previous-hacks/bybit-safe-ui.mdx
@@ -3,6 +3,8 @@ title: Bybit - Compromised Safe Wallet UI
 description: 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.

diff --git a/assertions-book/previous-hacks/compound-upgrade-bug.mdx b/assertions-book/previous-hacks/compound-upgrade-bug.mdx
@@ -3,6 +3,8 @@ title: Compound Upgrade Bug
 description: 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 which had a one letter bug on L1217.

diff --git a/assertions-book/previous-hacks/euler-finance-donation-hack.mdx b/assertions-book/previous-hacks/euler-finance-donation-hack.mdx
@@ -3,6 +3,8 @@ title: Euler Finance Donation Hack
 description: 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:

diff --git a/assertions-book/previous-hacks/first-depositor.mdx b/assertions-book/previous-hacks/first-depositor.mdx
@@ -3,6 +3,8 @@ title: First Depositor Bug
 description: 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

diff --git a/assertions-book/previous-hacks/gma-aum-jul25-hack.mdx b/assertions-book/previous-hacks/gma-aum-jul25-hack.mdx
@@ -1,7 +1,10 @@
 ---
 title: GMX v1 AUM Manipulation Hack
+description: 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.
@@ -24,7 +27,7 @@ The critical vulnerability chain:
 
 ### Normal AUM Calculation
 GMX calculates its total value using this formula:
-```
+```text
 AUM = Physical Tokens + Stablecoins + Unrealized Trading Profits + Fees
 ```
 

diff --git a/assertions-book/previous-hacks/hack1-radiant-capital.mdx b/assertions-book/previous-hacks/hack1-radiant-capital.mdx
@@ -3,6 +3,8 @@ title: Radiant Capital Hack
 description: 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/).

diff --git a/assertions-book/previous-hacks/hack2-vestra-dao.mdx b/assertions-book/previous-hacks/hack2-vestra-dao.mdx
@@ -3,6 +3,8 @@ title: Vestra DAO Hack
 description: 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).

diff --git a/assertions-book/previous-hacks/uxlink-multisig-hack.mdx b/assertions-book/previous-hacks/uxlink-multisig-hack.mdx
@@ -3,6 +3,8 @@ title: UxLink Multisig Ownership Compromise
 description: 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.

diff --git a/assertions-book/previous-hacks/vicuna-finance-hack.mdx b/assertions-book/previous-hacks/vicuna-finance-hack.mdx
@@ -3,6 +3,8 @@ title: Vicuna Finance Oracle Manipulation Hack
 description: 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.

diff --git a/credible/apply-assertions.mdx b/credible/apply-assertions.mdx
@@ -3,14 +3,14 @@ title: 'Apply Assertions'
 description: 'Configure assertions and create a release on the platform using `pcl apply`'
 ---
 
-This guide walks you through configuring your assertions in `credible.toml` and creating a release on the platform with `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, configure `credible.toml`, and create a release. Then review and deploy it 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
 
@@ -34,7 +34,7 @@ pcl auth status
 
 ## Step 2: Configure `credible.toml`
 
-Create a `credible.toml` file at `assertions/credible.toml` in your project root. This file declares which assertions protect which contracts:
+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
 environment = "production"
@@ -75,6 +75,10 @@ Each contract address must be unique within the configuration. See the [pcl Refe
 Set `project_id` in your `credible.toml` to skip the interactive project selection prompt. This is especially useful for CI/CD pipelines.
 </Tip>
 
+<Note>
+`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.
+</Note>
+
 ## Step 3: Apply Your Assertions
 
 Create a release on the platform:
@@ -86,7 +90,8 @@ pcl apply
 This command:
 1. Reads your `credible.toml` configuration
 2. Builds and compiles the referenced assertion contracts
-3. Creates a release on the platform
+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:
 
@@ -98,18 +103,19 @@ pcl apply --yes
 `pcl apply` automatically builds your project. You can also run `pcl build` separately to check for compilation errors before applying.
 </Note>
 
-## Step 4: Deploy in the Platform
+## 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. Click "Deployment" tab
 3. Find your assertion and click "Proceed to Review"
-4. Select the target contract and environment (Staging or Production)
-5. Click "Deploy" and sign the transaction
+4. Review the release diff and selected target contracts
+5. Select the target environment (Staging or Production)
+6. Click "Deploy" and sign the transaction
 
 <Note>
-Creating a release through `pcl apply` does not make the assertion active by itself. The assertion becomes active only after you deploy it through the platform and the configured timelock in the on-chain State Oracle contracts expires. Removals follow the same State Oracle timelock flow.
+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.
 </Note>
 
 ## Troubleshooting

diff --git a/credible/architecture-overview.mdx b/credible/architecture-overview.mdx
@@ -153,7 +153,7 @@ flowchart LR
 ## Integration Paths
 
 <CardGroup cols={2}>
-  <Card title="Platform Integration Overview" icon="browser" href="/credible/dapp-integration">
+  <Card title="Plan a Platform Integration" icon="browser" href="/credible/dapp-integration">
     How protocols deploy and manage assertions
   </Card>
   <Card title="Network Integration Overview" icon="sitemap" href="/credible/network-integration">
@@ -217,6 +217,6 @@ For concrete assertion examples and real-world use cases, explore the [Assertion
     Detailed reference for assertion functions
   </Card>
   <Card title="Trust Model" icon="shield-check" href="/credible/trust-model">
-    Guarantees, assumptions, and failure modes
+    Guarantees, scope, and operational model
   </Card>
 </CardGroup>