Protocol Invariant Checker (PIC) is a command-line framework that loads a DeFi protocol's state from a JSON file, runs a defined set of security invariants against it, and produces a structured audit report — each finding tagged with a severity level, category, description, and recommendation.
The framework is designed around a single abstraction: every protocol implements the same Protocol trait. The CLI, engine, and reporting layers never reference a specific protocol directly. Adding a new protocol means implementing one trait and registering it in one line — nothing else in the codebase changes.
pic check --protocol erc4626 state.json
pic simulate --protocol erc4626 state.json slash.json
pic explain erc4626
DeFi protocols are built on invariants — mathematical properties that must hold at all times, regardless of what actions users take. When they break, funds are at risk.
| Protocol | Invariant | Consequence if Broken |
|---|---|---|
| ERC-4626 Vault | total_assets >= total_liabilities |
Users cannot redeem — vault is insolvent |
| ERC-4626 Vault | Σ user.shares == total_shares |
Phantom shares allow double-spending |
| Uniswap V2 | reserve0 × reserve1 >= k |
Arbitrage drains the pool |
| Staking Pool | total_staked == Σ user.stake |
Reward accounting breaks |
These invariants are routinely checked during manual audits. PIC provides a way to define them once as code, run them against any state snapshot, and simulate how they respond to actions — turning a reasoning exercise into a repeatable, automatable check.
- Modular protocol registry — protocols are registered, not hardcoded; the CLI is unaware of any specific implementation
- Structured findings — every violation is a typed
Findingwith severity, category, description, and recommendation - State simulation — apply a protocol action (deposit, withdraw, slash, mint, redeem) and immediately check post-state invariants
pic explain— inline documentation for every invariant, including the attack vector it guards against- CI-ready —
--strictflag exits with code 1 on any failure, suitable for integration into automated pipelines - Zero unsafe code — entirely safe Rust
The codebase is organised into strict vertical layers. Each layer has one responsibility and communicates with the layer below through a defined interface.
┌──────────────────────────────────────────┐
│ CLI (src/cli/) │
│ list · check · simulate · explain │
└─────────────────────┬────────────────────┘
│
┌─────────────────────▼────────────────────┐
│ main.rs (dispatch) │
└─────────────────────┬────────────────────┘
│
┌─────────────────────▼────────────────────┐
│ engine/registry.rs │
│ maps protocol id → dyn Protocol │
└─────────────────────┬────────────────────┘
│ &dyn Protocol
┌─────────────────────▼────────────────────┐
│ protocols/<name>/mod.rs │
│ impl Protocol for <Name>Protocol │
│ ├── state.rs (data model) │
│ ├── invariants.rs (check logic) │
│ └── simulator.rs (state transitions) │
└─────────────────────┬────────────────────┘
│ Vec<CheckOutcome>
┌─────────────────────▼────────────────────┐
│ reporting/mod.rs │
│ (terminal rendering) │
└──────────────────────────────────────────┘
pub trait Protocol {
fn id(&self) -> &'static str;
fn name(&self) -> &'static str;
fn description(&self) -> &'static str;
fn check(&self, state: &Value) -> Result<Vec<CheckOutcome>>;
fn simulate(&self, state: &Value, action: &Value) -> Result<Value>;
fn explain(&self) -> Vec<InvariantDoc>;
}engine/registry.rs is the only file that imports a concrete protocol type. Every other component operates on &dyn Protocol.
src/
├── main.rs
├── cli/mod.rs # Command definitions (clap)
├── engine/
│ ├── mod.rs # Protocol trait · CheckOutcome · InvariantDoc
│ └── registry.rs # Protocol registry
├── protocols/
│ ├── mod.rs
│ └── erc4626/
│ ├── mod.rs # Erc4626Protocol — Protocol impl + INV-5, INV-6
│ ├── state.rs # VaultState
│ ├── invariants.rs # INV-1 through INV-4
│ └── simulator.rs # apply_action
├── reporting/mod.rs # Coloured terminal output
└── shared/
├── finding.rs # Finding struct
└── severity.rs # Severity enum
examples/erc4626/
├── healthy.json # All invariants pass
├── broken.json # Insolvency + phantom shares
├── inflation_attack.json # First-depositor attack scenario
├── withdraw.json # Safe withdraw action
└── slash.json # Drain — triggers insolvency
| ID | Invariant | Severity | Category |
|---|---|---|---|
| INV-1 | total_assets >= total_liabilities |
Critical | Accounting |
| INV-2 | total_shares > 0 IFF total_assets > 0 |
Critical | Accounting |
| INV-3 | Exchange rate has not dropped more than 10% from snapshot | High | Pricing |
| INV-4 | total_shares == 0 OR total_shares >= 1,000 |
Medium | Economic Security |
| INV-5 | Σ user[i].shares == total_shares |
Critical | Accounting |
| INV-6 | convertToAssets(convertToShares(x)) <= x and vice versa |
High | Rounding |
Run pic explain erc4626 for the full description and example attack vector for each invariant.
| Version | Status | Scope |
|---|---|---|
| v0.1 — ERC-4626 Vault | ✅ Complete | 6 invariants · simulation · explain · CI mode |
| v0.2 — Constant Product AMM | Planned | Uniswap V2: constant-product, reserve sanity, price manipulation |
| v0.3 — Staking Protocols | Planned | Reward accounting, slashing invariants |
| v0.4 — State Diff | Planned | pic diff before.json after.json |
| v0.5 — Fuzzing | Planned | Random action sequences to surface invariant violations |
| v0.6 — Solana Vaults | Planned | SPL token account invariants |
git clone https://github.com/Sourav-IIITBPL/protocol-invariant-checker
cd protocol-invariant-checker
cargo build --releaseThe compiled binary is placed at ./target/release/pic.
Requirement: Rust 1.85 or later. Install via rustup.rs.
pic listLists every registered protocol with its identifier and description.
pic check --protocol <id> <state.json>
pic check --protocol erc4626 examples/erc4626/healthy.json
pic check --protocol erc4626 examples/erc4626/broken.json --strictRuns all invariants for the given protocol against the state file. --strict exits with code 1 if any check fails.
State JSON format:
{
"total_assets": 1000000,
"total_shares": 1000000,
"total_liabilities": 1000000,
"previous_exchange_rate": 1.0,
"users": [
{ "name": "Alice", "shares": 600000 },
{ "name": "Bob", "shares": 400000 }
]
}previous_exchange_rate and users are optional — the checks that depend on them (INV-3 and INV-5) are skipped gracefully when absent.
pic simulate --protocol <id> <state.json> <action.json>
pic simulate --protocol erc4626 examples/erc4626/healthy.json examples/erc4626/slash.jsonApplies one action to the given state, then runs all invariants on the resulting state.
Action JSON format:
{ "type": "deposit", "assets": 500000 }
{ "type": "withdraw", "assets": 200000 }
{ "type": "mint", "shares": 100000 }
{ "type": "redeem", "shares": 50000 }
{ "type": "slash", "assets": 300000 }slash reduces assets without touching shares or liabilities — it models a direct loss event such as an exploit or bad debt.
pic explain <id>
pic explain erc4626Prints every invariant for the protocol with its formula, severity, reasoning, and an example of the attack it guards against.
Contributions are welcome. The most useful areas are:
- New protocol modules (Uniswap V2, Aave, Curve, SPL Token programs)
- Additional invariants for existing protocols (donation attacks, fee accounting)
- Output formats (JSON report, SARIF, Markdown)
- Integration tests using real on-chain state snapshots
To add a protocol, implement the Protocol trait in src/protocols/<name>/ and register it with one line in src/engine/registry.rs. Open an issue before starting on large changes to align on the design.