Denaria launched its perpetual trading infrastructure with a clear requirement: ensure that no trade, liquidation, or liquidity operation can push the system into uncollateralized bad debt.
Perpetual markets are structurally fragile. Leverage amplifies small pricing errors. Liquidations depend on timely execution. Profit and loss calculations must reconcile exactly with collateral accounting. A single invariant failure can cascade into insolvency.
To prevent this class of failure at the sequencer level, Denaria integrated the Credible Layer and deployed a runtime assertion that blocks bad debt before it is ever included in a block.
Here is how Denaria protects $50k of user funds in their alpha program with runtime enforcement.
The Credible Layer
The Credible Layer introduces a new security primitive: assertions. Rather than attempting to enumerate every exploit path, assertions define states that must never occur.
Core concept: Assertion: State → {true, false}
Assertions execute off-chain in the PhEVM and run as part of the sequencer’s validation pipeline. If a transaction would violate a protocol-defined invariant, it is rejected before block inclusion.
For Denaria, the invariant is simple and uncompromising: no user may cause bad debt to themselves as a result of their transaction. In other words, Denaria’s assertions ensures that bad debt and liquidations can be rightfully caused by market risk, but bad debt caused by contract logic errors are prevented.
About Denaria
Denaria operates a perpetual trading pair contract that supports:
- Leveraged directional trades
- Liquidity provisioning and removal
- Auto-close thresholds
- Liquidations
- Realized PnL settlement
Each of these functions can materially change a trader’s collateral or exposure. That means each can potentially introduce insolvency if accounting assumptions break.
To formalize this risk surface, Denaria completed invariant mapping around user collateral and PnL dynamics and implemented a bad-debt assertion.
Security Assertion Deployed
1. Bad Debt Prevention Invariant
Focus: Preventing any transaction from creating negative equity (bad debt) for any user.
What the assertion protects:
In leveraged perpetual systems, bad debt occurs when a trader’s losses exceed posted collateral. This can happen due to:
- Incorrect PnL calculation
- Incorrect liquidation sizing
- Race conditions around price updates
- Edge cases in liquidity movement
- Bugs in trade sizing or leverage enforcement
If collateral < loss, the protocol absorbs the deficit. Over time, that can wipe liquidity providers or force emergency shutdowns.
How the assertion protects:
- To ensure that the assertion checks every transaction that involves user exposure, a variety of methods are registered to trigger the assertion: trade, closeAndWithdraw, addLiquidity, removeLiquidity, liquidate, and enableAutoClose.
- When a qualifying transaction is found, the Enforcer simulates its post-transaction state;
- Extracts the affected user directly from emitted events;
- Reads current collateral via getCollateral(user);
- Computes real-time PnL using calcPnL(user, getPrice()).
Enforces the invariant:
pnl <= collateral OR pnl is positive
In other words:
- If the user is profitable, no restriction applies.
- If the user is at a loss, that loss must never exceed posted collateral.
If a transaction would produce a state where losses exceed collateral, it is rejected at the sequencer level. Dig into the assertion on the transparency dashboard here.
The Integration
Denaria deployed the bad-debt assertion as a standalone smart contract. No contract upgrades were required. No trading downtime occurred.
The assertion is referenced directly by the sequencer sidecar. Denaria’s production code continues to execute exactly as written, but critical functions are now protected by a solvency invariant.
The result is structural protection against a fundamental failure mode of leveraged markets.
All active assertions are publicly verifiable through the Credible Layer transparency interface. Traders, liquidity providers, and allocators can inspect the exact invariant protecting capital.
For perpetual markets, solvency is not optional. With runtime enforcement, Denaria ensures it is non-negotiable.