Static Assertions
The assert statement declares a property that the verifier must prove. It has no runtime effect.
Runtime Assertions
The runtime:assert statement both proves a condition at verification time and traps at runtime if the condition is false.
Trap Conditions
The trap statement marks an error condition as unreachable. It traps at runtime if the condition is true, and the verifier proves the condition cannot be true at that program point.
Choosing Assertions
Sector9 provides three assertion forms with distinct verification and runtime behavior. This guide helps you choose the right one.