Solidity Property Testing Framework

A comprehensive, commercial-grade framework for writing and testing properties (invariants) in Solidity smart contracts.

Overview

This framework provides:

• Taxonomy of 12+ property categories with 40+ subcategories
• Structured Schema for machine-readable property representation
• 28 Protocol-Specific Checklists covering DEX, Lending, CDP, Vault, Governance, Streaming, Options, Bridge, Rebasing Tokens, and more
• 10 Protocol Invariant Libraries with Chimera-compatible code
• 15 Advanced Implementation Patterns in Appendix A
• Detection Patterns for AI-assisted property discovery
• 60 Campaign Analyses from leading security firms

Quick Start

1. Identify your protocol type (DEX, Lending, CDP, Vault, etc.)
2. Use the property taxonomy to find relevant categories
3. Apply protocol templates as a starting point
4. Implement using provided patterns
5. Validate with fuzzing tools

Documents

Document	Description
00_MASTER_CAMPAIGN_LIST.md	List of 60+ public fuzzing campaigns
01_PROPERTY_CLASSIFICATION_TAXONOMY.md	Complete property categorization system
02_PROPERTY_SCHEMA.md	JSON/YAML schema for properties
03_COMPREHENSIVE_FRAMEWORK.md	Main operational manual
research/theoretical_foundations.md	Academic & industry research
research/campaigns/	Individual campaign analyses

Property Categories

Category	Code	Focus
Accounting	ACC	Sum equality, balance consistency
Collateralization	COL	Health ratios, liquidation
State Machine	STM	Transitions, lifecycle
Boundary	BND	Caps, minimums, ranges
Directional	DIR	Operation effects
Temporal	TMP	Time-based restrictions
ERC Compliance	ERC	Standard conformance
Oracle	ORC	Price feed reliability
Access Control	ACL	Permissions

Property Type Hierarchy

INVARIANTS          - Must hold across ALL states
  └─ GPOST          - Must hold after ANY action
      └─ HSPOST     - Must hold after SPECIFIC actions
          └─ PRECONDITIONS - Must be true BEFORE action

Protocol Checklists (28 Types)

Core Protocols	DeFi Primitives	Advanced
DEX/AMM	Rebasing Token	Async Vault (ERC-7540)
Lending	Wrapped Token	Credit Position
CDP	Yield Strategy Vault	RWA Token
ERC4626 Vault	Extended Governance	Reward Distribution
Governance	Data Structures	Cross-Chain Vault
Streaming Payments	Multi-Role Stablecoin	Message Aggregator
Options/Derivatives	Vesting/Escrow	Multi-Strategy Vault
Self-Repaying Loans	Institutional Lending	Staking Protocol
Bridge	Multi-Ilk Lending	Voting Escrow
	Concentrated Liquidity AMM

Example Property (JSON Schema)

{
  "id": "AAVE_BASE_INV_01",
  "name": "Supply-Balance Equality",
  "category": "accounting",
  "type": "invariant",
  "description": "Total supply equals sum of all balances",
  "specification": "totalSupply == Σ balanceOf(user)",
  "assertion": {
    "type": "approx_eq",
    "left": "totalSupply()",
    "right": "sum(balances)",
    "tolerance": { "absolute": "2 * actorCount" }
  },
  "severity": "critical"
}

Sources

Campaigns Analyzed

• Trail of Bits (Uniswap V4, Bunni, Curvance)
• Enigma Dark (Aave V3, Euler Vault Kit)
• Perimeter Security (Origin Protocol, Drips)
• Recon (Liquity, Centrifuge, Superform)
• Antonio Viggiano (BadgerDAO eBTC)

Academic Research

• SMARTINV (IEEE S&P 2024)
• Demystifying Invariant Effectiveness (FSE 2024)
• PropertyGPT (NDSS 2025)

Industry Documentation

• Trail of Bits: Building Secure Contracts
• Certora CVL Documentation
• Foundry Invariant Testing

Tools Supported

• Echidna - Grammar-based fuzzing
• Medusa - Coverage-guided parallel fuzzing
• Foundry - Rust-based invariant testing
• Certora - Formal verification

Directory Structure

property_framework/
├── README.md
├── 00_MASTER_CAMPAIGN_LIST.md
├── 01_PROPERTY_CLASSIFICATION_TAXONOMY.md
├── 02_PROPERTY_SCHEMA.md
├── 03_COMPREHENSIVE_FRAMEWORK.md
└── research/
    ├── theoretical_foundations.md
    ├── campaigns/
    │   ├── 01_uniswap_v4_tob.md
    │   ├── 02_aave_v3_enigma.md
    │   ├── 03_euler_vault_kit.md
    │   ├── 04_badger_ebtc.md
    │   ├── 05_origin_ousd.md
    │   └── 06_liquity_gov_recon.md
    ├── frameworks/
    └── patterns/

License

This framework is provided for educational and security research purposes.

Contributing

Contributions welcome. Please add:

• New campaign analyses
• Additional property patterns
• Protocol-specific templates
• Tool configuration examples

---

Version: 4.1 | Framework: Chimera-Compatible | Last Updated: January 2026