-- Loading...Runtime vs Static Verification
Runtime Contracts
--verify-contracts checks contracts during execution on actual inputs.
Fast, works everywhere, but only catches bugs on tested paths.
Static Verification
ailang verify translates pure functions to SMT-LIB formulas and invokes
the Z3 theorem prover. Proves contracts for all valid inputs at compile time.
What Z3 Proves
For each ensures clause, Z3 searches for a counterexample. If none exists,
the contract is proven correct for every possible input satisfying requires.
What Are Z3 and SMT Solvers?
SMT Solvers theory
Satisfiability Modulo Theories (SMT) solvers decide whether logical formulas over integers, booleans, strings, arrays, and other types have a satisfying assignment. They extend SAT solvers with built-in decision procedures for arithmetic, bit-vectors, and data structures — enabling automated reasoning about real programs, not just propositional logic.
The SMT-LIB standard
defines a common input format that all major solvers understand. AILANG's ailang verify
compiles contracts to SMT-LIB v2 and feeds them to Z3.
Z3 Theorem Prover solver
Z3 is Microsoft Research's high-performance SMT solver, used in production by compilers, operating systems, and security tools worldwide. It combines DPLL(T) search with specialized solvers for linear arithmetic, non-linear arithmetic, strings, sequences, and algebraic datatypes.
When AILANG asks "does this contract hold for all valid inputs?", Z3 either proves it universally or returns a concrete counterexample — the exact input values that break the contract.
Why AILANG Is a Natural Fit language
AILANG's pure func declarations guarantee no side effects — exactly the fragment
Z3 can reason about. Algebraic data types (enums, records) map directly to Z3's datatype theory.
First-class requires/ensures contracts are the specification language,
so there's nothing extra to write — your contracts are your proofs.
Cross-function calls are automatically inlined as Z3 define-fun declarations,
letting the solver verify entire call chains (like the 4-deep billing pipeline above) in one pass.
The Decidable Fragment scope
Z3 can verify pure functions using: int, bool, float,
string, lists, records, and enum ADTs. Arithmetic, comparisons, if/match,
string operations (++, startsWith, find), and list operations
are all supported. Recursive functions are verified via bounded unrolling with
--verify-recursive-depth.
Higher-order functions and effect-ful code are outside the decidable fragment — these get
runtime contract checking via --verify-contracts instead.