Cure
Verification-First Programming
Verification-First Programming
Modern software systems are growing increasingly complex, with state machines, concurrent processes, and intricate data dependencies. Traditional testing approaches—while valuable—cannot exhaustively verify all possible execution paths and states. This is where Satisfiability Modulo Theories (SMT) solvers become indispensable tools for formal verification.
The Cure language, with its built-in support for finite state machines (FSMs), dependent types, and refinement types, is uniquely positioned to benefit from SMT-based verification. This document explores how SMT solvers, particularly Z3, can dramatically improve code quality and provide mathematical guarantees about program correctness.
Imagine a puzzle where certain rules must always be obeyed, and the goal is to find out if there’s any way to make all the pieces fit without breaking any rules. SMT-solvers, short for Satisfiability Modulo Theories solvers, are special computer programs designed to solve these rule-based puzzles automatically12.
In practical terms, SMT-solvers answer questions like: "Given all the rules (mathematical, logical, or data-related), is there any combination of values that keeps everything true and consistent?" For example, they can check if a set of formulas describing a piece of software will ever run into errors, if a digital circuit will always work correctly, or even if a robot can safely move given complicated obstacles and instructions1.
What makes SMT-solvers powerful is that rather than just working with basic true/false logic, they also understand deeper mathematical topics—like arithmetic, relationships between data, and more. They look at every part of the puzzle, combining logic and math, to figure out whether a solution exists or not. If the puzzle can’t be solved, they can even help you pinpoint exactly why it fails12.
SMT-solvers are computational systems that determine whether statements involving variables and constraints are satisfiable under a range of mathematical theories (such as arithmetic, arrays, bit-vectors, and more)34.
SMT-solvers generalize SAT-solvers (Boolean satisfiability) to additional, expressive theories. This enables the automated analysis of formulas that capture constraints and properties found in realistic software, hardware, and business systems.34
See below for more detailed description.
SMT-solvers are fundamental in modern software and systems engineering, particularly for safety-critical and high-assurance domains:
A foundational resource for using SMT-solvers in system verification is Alessandro Gianola’s work, especially his dissertation “SMT-based Safety Verification of Data-Aware Processes: Foundations and Applications.”3
Currently, Z3 from Microsoft Research is seen as the most advanced and robust SMT-solver:
A SAT (Boolean Satisfiability) solver determines whether a Boolean formula can be satisfied—that is, whether there exists an assignment of variables that makes the formula true. For example:
(A ∨ B) ∧ (¬A ∨ C) ∧ (¬B ∨ ¬C)
A SAT solver would find that A = true, B = false, C = true satisfies this formula.
SMT (Satisfiability Modulo Theories) solvers extend SAT solvers to handle richer logical theories beyond pure Boolean logic. These theories include:
x + 2y ≤ 5, 3a - b = 7select(store(a, i, v), i) = vSMT solvers typically employ a lazy SMT approach:
This architecture combines the efficiency of modern SAT solvers with the expressiveness of domain-specific theories.
Z3 is a high-performance SMT solver developed by Microsoft Research. It has become the de facto standard for program verification, symbolic execution, and formal methods research.
┌─────────────────────────────────────────────┐
│ User Interface (APIs) │
├─────────────────────────────────────────────┤
│ SMT-LIB 2.0 Parser │
├─────────────────────────────────────────────┤
│ Preprocessing & Simplification │
├─────────────────────────────────────────────┤
│ Core SAT Solver (DPLL) │
├───────────┬─────────────┬───────────────────┤
│ Arithmetic│ Arrays │ Datatypes │
│ Theory │ Theory │ Theory │
│ Solver │ Solver │ Solver │
└───────────┴─────────────┴───────────────────┘
Testing Formal Verification
│ │
├─── Unit Tests │
├─── Integration Tests │
├─── Property-Based Tests │
├─── Symbolic Execution ────────────────────┐ │
│ │ │
│ ▼ ▼
│ SMT Solver
│ │
└───────────────────────────────────────────────┘
Partial Coverage Complete Guarantees
Traditional testing explores a finite set of execution paths. SMT-based verification considers all possible paths symbolically.
Example: Verifying array bounds (below is pseudocode)
# Without SMT: Hope you tested enough edge cases
def access_array(arr: Vector(Int, n), idx: Int): Int =
arr[idx] # Runtime check: idx < n ?
# With SMT: Compile-time guarantee
def access_array(arr: Array(Int, n), idx: {i: Int | 0 <= i < n}): Int =
arr[idx] # Provably safe - no runtime check needed!
SMT solvers excel at finding corner cases that humans miss.
[TODO] Fins an example for that
Instead of finding bugs, SMT can prove no bugs exist under specified conditions.
Example: Division by zero
# Without SMT: Runtime check required
def divide(x: Int, y: Int): Int =
match y == 0 do
true -> error("Division by zero")
false -> ok(x / y)
end
# With SMT: Compile-time guarantee via guard
def safe_divide(x: Int, y: Int): Int when y != 0 = x / y
# SMT solver verifies y != 0 before allowing division
Cure uses SMT solvers to verify that function guards cover all possible input values:
Example: Complete guard coverage
# Guards for sign function
def sign(x: Int): Int when x > 0 = 1
def sign(x: Int): Int when x == 0 = 0
def sign(x: Int): Int when x < 0 = -1
# SMT verification: (x > 0) ∨ (x == 0) ∨ (x < 0) ≡ true ✓
# Compiler proves all Int values are covered
Example: Detecting unreachable clauses
# Redundant guard warning
def classify(x: Int): String when x >= 0 = "non-negative"
def classify(x: Int): String when x > 10 = "large" # Unreachable!
def classify(x: Int): String = "negative"
# SMT detection: (x >= 0) subsumes (x > 10)
# Compiler warning: Second clause will never execute
Implementation: See cure_guard_smt.erl for:
- Guard completeness checking
- Subsumption detection
- Counterexample generation
- Inconsistent guard detection
type NonZero = x: Int when x != 0
def safe_divide(a: Int, b: NonZero): Int =
a / b # Provably safe - Z3 verifies b /= 0 always holds
Compilers can use SMT to verify that optimizations preserve semantics.
# Original
def compute_original(x: Int): Int =
(x + 1) * (x + 1) - x * x - 2 * x
# Optimized
def compute_optimized(x: Int): Int =
1
# SMT verification: ∀x. compute_original(x) = compute_optimized(x) ✓
SMT verifies implementations match formal specifications.
# Specification: sorting produces ordered array with same elements
spec def is_sorted(v: Vector(Int, n)): Bool =
∀i j. 0 <= i < j < n → v[i] <= v[j]
spec def same_multiset(v1: Vector(Int, n), v2: Vector(Int, n)): Bool =
∀x. count(v1, x) = count(v2, x)
# Implementation must satisfy both properties
def sort(arr: Vector(Int, n)): Vector(Int, n)
ensures is_sorted(result) ∧ same_multiset(arr, result)
= ...
"Verification of Data-Aware Processes via Satisfiability Modulo Theories" by Alessandro Gianola presents a comprehensive framework for verifying systems that combine:
This is precisely the problem domain that Cure FSMs inhabit.
A data-aware process consists of:
- A finite set of control states (FSM states)
- A data schema (variables, types, constraints)
- Transition guards (conditions on data)
- Actions (data transformations)
This maps directly to Cure's FSM model:
record TrafficPayload do
cycles_completed: Int # Data schema
timer_events: Int
emergency_stops: Int
end
fsm TrafficPayload{...} do
Red --> |timer| Green # Control states and transitions
Green --> |timer| Yellow
Yellow --> |timer| Red
end
Gianola identifies critical verification problems:
The book presents algorithms that reduce these problems to SMT queries:
Reachability(s0, sf):
∃ path. path[0] = s0 ∧ path[n] = sf ∧
∀i. valid_transition(path[i], path[i+1])
Safety(s0, bad):
¬∃ path. path[0] = s0 ∧ ∃i. path[i] ∈ bad
Liveness(s0, good):
∀ path from s0. ∃i. path[i] ∈ good
Z3 can solve these queries even with complex data constraints.
For infinite-state systems, bounded model checking explores up to depth k:
Reachable_k(s0, sf):
Check all paths of length ≤ k from s0 to sf
If no bug found up to depth k, increase k. SMT solvers efficiently handle increasing bounds.
Gianola describes techniques to automatically discover invariants—properties that hold in all reachable states:
# Synthesized invariant for traffic light
invariant TrafficLight:
∀ state. cycles_completed >= 0 ∧
timer_events >= cycles_completed * 3 ∧
emergency_stops >= 0
Z3's quantifier reasoning helps discover such invariants automatically.
Cure's design makes it ideal for SMT-based verification:
Problem: Can state S be reached from the initial state?
Cure Example (from 07_fsm_verification.cure):
fsm LightState{cycle_count: 0} do
Red --> |timer| Green {cycle_count = cycle_count + 1}
Green --> |timer| Yellow
Yellow --> |timer| Red
Red --> |emergency| Red
Green --> |emergency| Red
Yellow --> |emergency| Red
end
# Verification query:
# Is Yellow reachable from Red?
# Answer: Yes, via path Red → Green → Yellow
Z3 Encoding:
(declare-datatypes () ((State Red Green Yellow)))
(declare-fun step (State) State)
(assert (or
(= (step Red) Green)
(= (step Red) Red)))
(assert (or
(= (step Green) Yellow)
(= (step Green) Red)))
(assert (= (step Yellow) Red))
(assert (= Yellow (step (step Red)))) ; Can reach Yellow in 2 steps?
(check-sat) ; sat → yes, reachable
Problem: Is there a state with no outgoing transitions?
Cure Example:
fsm CounterState{count: 0, max_count: 5} do
Counting --> |increment| Counting {count = count + 1}
Counting --> |check| Done {when count >= max_count}
# Done state has no outgoing transitions → DEADLOCK
end
Z3 Encoding:
(declare-datatypes () ((State Counting Done)))
(declare-fun next (State) State)
; Define transitions
(assert (or
(= (next Counting) Counting)
(= (next Counting) Done)))
; Check if Done is a deadlock
(assert (= (next Done) Done)) ; No real transition, self-loop
(assert (distinct Done (next Done))) ; Try to find different next state
(check-sat) ; unsat → deadlock confirmed
Problem: Can we reach a "bad" state?
Cure Example (from 07_fsm_verification.cure):
record DoorState do
is_locked: Int # 1 = locked, 0 = unlocked
alarm_active: Int # 1 = active, 0 = inactive
end
fsm DoorState{is_locked: 1, alarm_active: 0} do
Locked --> |unlock| Unlocked {is_locked = 0, when alarm_active = 0}
Unlocked --> |lock| Locked {is_locked = 1}
Locked --> |activate_alarm| LockedWithAlarm {alarm_active = 1}
LockedWithAlarm --> |deactivate_alarm| Locked {alarm_active = 0}
# NO transition from LockedWithAlarm to Unlocked
end
# Safety property: ¬(is_locked = 0 ∧ alarm_active = 1)
# "Never unlocked while alarm is active"
Z3 Verification:
(declare-datatypes () ((State Locked Unlocked LockedWithAlarm)))
(declare-fun is_locked (State) Int)
(declare-fun alarm_active (State) Int)
; Define state invariants
(assert (= (is_locked Locked) 1))
(assert (= (alarm_active Locked) 0))
(assert (= (is_locked Unlocked) 0))
(assert (= (alarm_active Unlocked) 0))
(assert (= (is_locked LockedWithAlarm) 1))
(assert (= (alarm_active LockedWithAlarm) 1))
; Check safety property violation
(declare-const s State)
(assert (and (= (is_locked s) 0) (= (alarm_active s) 1)))
(check-sat) ; unsat → safety property holds!
Problem: Do we eventually reach a desired state?
Cure Example:
fsm WorkflowState{tasks_completed: 0, total_tasks: 3} do
Pending --> |start| InProgress {tasks_completed = 0}
InProgress --> |complete_task| InProgress {
tasks_completed = tasks_completed + 1
}
InProgress --> |finish| Completed {
when tasks_completed >= total_tasks
}
end
# Liveness property: ◇Completed
# "Eventually reach Completed state"
Z3 Encoding (using bounded model checking):
; Check if Completed is reachable within k steps
(declare-datatypes () ((State Pending InProgress Completed)))
(declare-fun state (Int) State)
(declare-fun tasks (Int) Int)
; Initial state
(assert (= (state 0) Pending))
(assert (= (tasks 0) 0))
; Transition constraints for k=10 steps
(define-fun transition ((i Int)) Bool
(or
(and (= (state i) Pending)
(= (state (+ i 1)) InProgress)
(= (tasks (+ i 1)) 0))
(and (= (state i) InProgress)
(= (state (+ i 1)) InProgress)
(= (tasks (+ i 1)) (+ (tasks i) 1)))
(and (= (state i) InProgress)
(>= (tasks i) 3)
(= (state (+ i 1)) Completed))))
; Check if Completed is reachable
(assert (exists ((i Int)) (and (<= 0 i) (<= i 10) (= (state i) Completed))))
(check-sat) ; sat → liveness holds
Problem: Do data constraints always hold?
Cure Example:
record CounterData do
count: Int
max_count: Int
end
fsm CounterData{count: 0, max_count: 10} do
Active --> |increment| Active {
count = count + 1,
when count < max_count # Guard prevents overflow
}
end
# Invariant: ∀ state. 0 <= count <= max_count
Z3 Verification:
(declare-const count_before Int)
(declare-const max_count Int)
(declare-const count_after Int)
; Initial invariant
(assert (= count_before 0))
(assert (= max_count 10))
(assert (<= 0 count_before))
(assert (<= count_before max_count))
; Transition preserves invariant
(assert (< count_before max_count)) ; Guard
(assert (= count_after (+ count_before 1))) ; Action
; Check invariant after transition
(assert (or (< count_after 0) (> count_after max_count)))
(check-sat) ; unsat → invariant preserved!
Cure supports refinement types (from refinement_types.cure):
type Positive = Int when x > 0
type NonZero = Int when x /= 0
type Percentage = Int when x >= 0 and x =< 100
def safe_divide(a: Int, b: NonZero): Int =
a / b
Z3 Verification of Type Safety:
(declare-const a Int)
(declare-const b Int)
; Precondition: b is NonZero
(assert (not (= b 0)))
; Division is safe
(declare-const result Int)
(assert (= result (div a b)))
; Check if division by zero is possible
(assert (= b 0))
(check-sat) ; unsat → division is safe
record BankAccount do
balance: Int
overdraft_limit: Int
end
fsm BankAccount{balance: 1000, overdraft_limit: 500} do
Active --> |withdraw| Active {
balance = balance - amount,
when balance - amount >= -overdraft_limit
}
end
Z3 Verification: Prove balance never exceeds overdraft limit
(declare-const balance_before Int)
(declare-const overdraft_limit Int)
(declare-const amount Int)
(declare-const balance_after Int)
; Initial condition
(assert (= balance_before 1000))
(assert (= overdraft_limit 500))
; Transition guard
(assert (>= (- balance_before amount) (- overdraft_limit)))
; Action
(assert (= balance_after (- balance_before amount)))
; Verify invariant: balance >= -overdraft_limit
(assert (< balance_after (- overdraft_limit)))
(check-sat) ; unsat → invariant holds
Original FSM:
fsm TrafficLight1{...} do
Red --> |timer| Green
Green --> |timer| Yellow
Yellow --> |timer| Red
end
Refactored FSM:
fsm TrafficLight2{...} do
State0 --> |timer| State1
State1 --> |timer| State2
State2 --> |timer| State0
end
Z3 Verification: Prove both FSMs are isomorphic
; Define mapping: Red ↔ State0, Green ↔ State1, Yellow ↔ State2
(declare-fun map (State1) State2)
(assert (= (map Red) State0))
(assert (= (map Green) State1))
(assert (= (map Yellow) State2))
; Verify transitions are preserved
(assert (= (map (transition1 Red)) (transition2 (map Red))))
; ... (similar for all transitions)
(check-sat) ; sat → FSMs are equivalent
record SharedCounter do
value: Int
end
fsm Counter1{value: 0} do
Idle --> |increment| Idle {value = value + 1}
end
fsm Counter2{value: 0} do
Idle --> |increment| Idle {value = value + 1}
end
# Both FSMs share the same `value` variable
# Can concurrent increments lead to lost updates?
Z3 Verification:
(declare-const value_initial Int)
(declare-const value_fsm1 Int)
(declare-const value_fsm2 Int)
(declare-const value_final Int)
(assert (= value_initial 0))
; FSM1 increments
(assert (= value_fsm1 (+ value_initial 1)))
; FSM2 increments (reads initial value due to race)
(assert (= value_fsm2 (+ value_initial 1)))
; Final value (last write wins)
(assert (or (= value_final value_fsm1) (= value_final value_fsm2)))
; Check if final value could be 1 instead of 2
(assert (= value_final 1))
(check-sat) ; sat → race condition detected!
; Model: both FSMs read value=0, both write value=1, last write wins
Integrate Z3 into the Cure compiler pipeline:
Cure Source Code
│
▼
Lexer/Parser
│
▼
Type Checker ◄───────┐
│ │
▼ │
FSM Analyzer │
│ │
▼ │
Generate Z3 Queries │
│ │
▼ │
Z3 Solver │
│ │
├──────────────────┘
│ (unsat → verify next property)
▼
Report Errors/Proofs
│
▼
Code Generation
unsat → Property holds ✓sat → Counterexample found ✗unknown → Timeout or undecidable%% In cure_fsm_verifier.erl
-export([verify_fsm/1, check_deadlock/1, check_safety/2, check_liveness/2]).
verify_fsm(FSM) ->
%% Extract FSM structure
States = extract_states(FSM),
Transitions = extract_transitions(FSM),
Guards = extract_guards(FSM),
%% Generate Z3 context
Z3Context = z3:mk_context([]),
%% Encode FSM in Z3
StateSort = encode_states(Z3Context, States),
TransitionAssertions = encode_transitions(Z3Context, StateSort, Transitions),
%% Check properties
DeadlockResult = check_deadlock(Z3Context, StateSort, Transitions),
SafetyResult = check_safety_properties(Z3Context, FSM),
LivenessResult = check_liveness_properties(Z3Context, FSM),
%% Report
{DeadlockResult, SafetyResult, LivenessResult}.
check_deadlock(Z3Context, StateSort, Transitions) ->
Solver = z3:mk_solver(Z3Context),
%% For each state, check if it has outgoing transitions
lists:map(fun(State) ->
HasTransition = has_outgoing_transition(State, Transitions),
case HasTransition of
false -> {deadlock, State};
true -> ok
end
end, get_all_states(StateSort)).
For large FSMs, use Z3's incremental solving:
verify_incremental(FSM) ->
Z3Ctx = z3:mk_context([]),
Solver = z3:mk_solver(Z3Ctx),
%% Add base constraints
z3:solver_assert(Solver, base_constraints(FSM)),
%% Check properties incrementally
lists:map(fun(Property) ->
z3:solver_push(Solver), % Save state
z3:solver_assert(Solver, property_constraint(Property)),
Result = z3:solver_check(Solver),
z3:solver_pop(Solver), % Restore state
{Property, Result}
end, properties_to_check(FSM)).
Provide real-time verification feedback in development:
┌─────────────────────────────────────────────┐
│ fsm DoorLock{...} do │
│ Locked --> |unlock| Unlocked │
│ LockedWithAlarm --> |unlock| Unlocked │ ⚠️ Safety violation
│ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ │ Can unlock with
│ Warning: Violates safety property │ alarm active
│ end │
└─────────────────────────────────────────────┘
Generate test cases from Z3 counterexamples:
generate_test_from_counterexample(FSM, Property, Counterexample) ->
%% Z3 provides: [Red, Green, Yellow, Failure]
TestSteps = lists:map(fun(State) ->
Event = get_transition_event(State, Counterexample),
{send_event, Event, expect_state, State}
end, Counterexample),
%% Generate EUnit test
generate_eunit_test(FSM, Property, TestSteps).
"Verification of Data-Aware Processes via Satisfiability Modulo Theories" by Alessandro Gianola
- Comprehensive treatment of SMT-based verification for stateful systems
- Covers reachability, safety, liveness, and deadlock detection
- Presents decision procedures and complexity results
- Essential reading for understanding Cure FSM verification
"The Calculus of Computation" by Aaron R. Bradley and Zohar Manna
- Foundations of program verification
- SMT-based verification techniques
- Temporal logic and model checking
"Decision Procedures" by Daniel Kroening and Ofer Strichman
- In-depth treatment of SAT and SMT algorithms
- Theory solvers and their combination
- Practical implementation details
"Z3: An Efficient SMT Solver" by Leonardo de Moura and Nikolaj Bjørner
- Architecture and algorithms of Z3
- Performance optimizations
"Satisfiability Modulo Theories: Introduction and Applications" by Clark Barrett et al.
- Overview of SMT landscape
- Applications in verification
"Temporal Verification of Reactive Systems: Safety" by Zohar Manna and Amir Pnueli
- Safety properties and their verification
- Temporal logic foundations
SMT solvers, particularly Z3, represent a transformative technology for ensuring software correctness. By integrating Z3 into the Cure compiler, we can:
As Cure evolves, SMT-based verification will become increasingly valuable, especially for mission-critical systems where correctness is paramount. The combination of Cure's expressive type system, built-in FSMs, and Z3's powerful reasoning capabilities creates a uniquely robust platform for building reliable concurrent systems.
The insights from Gianola's "Verification of Data-Aware Processes via Satisfiability Modulo Theories" provide a solid theoretical foundation for implementing these verification techniques in Cure. By following the frameworks and algorithms presented in that work, we can build a world-class verification system that makes Cure a leader in verified systems programming for the BEAM.
For questions or contributions to Cure's verification infrastructure, please see the project repository and documentation.
Sudoku and Satisfiability Modulo Theories: Layman’s Example ↩↩↩
Alessandro Gianola, "SMT-based Safety Verification of Data-Aware Processes: Foundations and Applications," PDF. ↩↩↩↩↩↩↩↩↩↩
Alessandro Gianola et al., “SMT-based Safety Verification of Data-Aware Processes,” CEUR Workshop Proceedings. PDF. ↩↩↩↩↩↩↩↩↩