Skip to main content

Property Violation

What it detects​

Smart contracts sometimes include assertions to enforce invariants such as token balances or state transitions. When these properties are violated—either due to bugs or malicious input—the contract may enter an invalid state. This detector surfaces failed asserts or explicit property checks.

Typical symptoms​

  • assert statements that can be triggered by user input
  • Commented assumptions contradicted by code

Solidity snippet (v0.8.25)​

pragma solidity ^0.8.25;

contract Property {
    uint256 public count;

    function dec() external {
        count -= 1;
        // Violates invariant that count should never underflow
        assert(count >= 0);
    }
}

Why it matters on EVM​

Property violations can expose deeper design flaws and be exploited to drain funds or corrupt contract state.