Numeric Verification

Prove arithmetic without being surprised by bounds or division. Use numeric modes and guards to keep math obligations explicit.

Overflow Checking Mode

Verified Sector9 code uses checked fixed-width integer arithmetic. Potential

Proving that fixed-width integer values stay within their valid ranges during arithmetic operations.

Division and modulo operations in contracts require explicit non-zero guards.