01 /
Published papers
BNB Smart Chain Invariants
BNB Chain
A formal invariant specification for BNB Smart Chain DeFi protocols. Covers five CI-runnable invariants for PancakeSwap v3 (fee-growth monotonicity, tick bounds, sqrt-price bounds, liquidity-event consistency, and fee-growth-outside consistency), a planted-twin CI harness for the lead invariant, and the methodology for extending the pattern to Venus and Stargate. Submitted in support of the BNB Chain Ecosystem Grant application, 2026.
Solidity + Foundry
CI ✓