Skip to content
STIMSMITH

Invariant

Concept WIKI v1 · 5/29/2026

An invariant is a condition or property used by analysis, verification, or runtime-guarding techniques to constrain or characterize system behavior. In the supplied evidence, invariants restrict starting states in Interval Property Checking, describe program conditions shared across software versions, and serve as guards for smart-contract transaction monitoring.

Definition

An invariant is a condition or property used to characterize allowed behavior or state in a system. The evidence describes invariants in three technical settings: formal hardware verification, software-version analysis, and smart-contract security.

Use in Interval Property Checking

In Interval Property Checking (IPC), safety properties are checked over bounded intervals using SAT-based reasoning. IPC differs from the original form of bounded model checking by starting from an arbitrary state rather than only an initial state. If a property holds from an arbitrary state, it also holds from any reachable state, giving an exhaustive verification result for that property.[1]

Because arbitrary starting states can include unreachable states, IPC can produce counterexamples that are not real executions of the design. The cited work describes these as false negatives, and states that they are removed by adding invariants that restrict the starting state.[2]

In the hardware-verification setting, the design is modeled as a finite-state machine with inputs, states, initial states, transition relation, and outputs. A safety property can be translated into a Boolean function, and IPC searches for counterexamples by solving a SAT instance formed from the unrolled transition relation over a bounded time interval together with the property encoding.[3]

Version invariants

In software-version analysis, the paper Invariant Diffs defines version invariants as program conditions that are common across program versions. It also defines invariant churns to describe changes in program conditions between versions, analogous to how source-code diffs report common code and code churn. The approach reports invariant diffs at matched program points and correlates invariant diffs with source diffs to explain which source-code changes led to property changes.[4]

Runtime and security invariants

In smart-contract security, invariants are used by runtime monitoring and guarding mechanisms to validate expected behavior and stop anomalous transactions. The Trace2Inv work studied invariant templates and dynamically generated contract-specific invariants from historical transaction data. In its evaluation, combining multiple invariant guards blocked up to 23 of 27 benchmark exploits with a false-positive rate reported as low as 0.32%.[5]

Practical significance

Across these uses, invariants act as explicit behavioral constraints: in IPC they rule out unreachable starting states, in invariant diffs they summarize program conditions across versions, and in smart-contract monitoring they function as guards against anomalous or exploit-like transactions.

LINKED ENTITIES

1 links
Interval Property Checking USES

CITATIONS

5 sources
5 citations
[1] IPC checks safety properties over bounded intervals using SAT-based reasoning and uses an arbitrary starting state rather than the initial state used in bounded model checking. Generating an Efficient Instruction Set Simulator from a Complete Property Suite
[2] In IPC, counterexamples can arise from unreachable starting states; the cited work says these false negatives are removed by adding invariants that restrict the starting state. Generating an Efficient Instruction Set Simulator from a Complete Property Suite
[3] The IPC formalization models a synchronous circuit as a finite-state machine, translates safety properties to Boolean functions, and searches for counterexamples using a SAT instance over an unrolled transition relation. Generating an Efficient Instruction Set Simulator from a Complete Property Suite
[4] Invariant Diffs defines version invariants as program conditions common across versions and invariant churns as changes in program conditions between versions; it correlates invariant diffs with source diffs. Invariant Diffs
[5] Smart-contract runtime monitoring and guarding mechanisms validate invariants to stop anomalous transactions; Trace2Inv dynamically generates contract-specific invariants from historical transaction data and, in the reported evaluation, combinations of guards blocked up to 23 of 27 benchmark exploits with false-positive rates as low as 0.32%. Demystifying Invariant Effectiveness for Securing Smart Contracts