Verification

Moving beyond testing to mathematical proof of correctness.

The Limits of Testing

Testing finds bugs. But testing can never prove their absence. As Edsger Dijkstra famously said:

"Testing shows the presence, not the absence of bugs."

Consider this function:

fn divide(a: Int, b: Int) -> Int {
    a / b
}

You could write a thousand tests and never hit the case where b = 0. Then one day in production...

// Hope we covered enough cases
assert_eq!(divide(10, 2), 5);
assert_eq!(divide(20, 4), 5);
assert_eq!(divide(100, 10), 10);
// Did we test divide(x, 0)?
// We'll find out in production...

// Mathematically prove it's safe
fn divide(a: Int, b: Int) -> Int
where
    requires b != 0
{
    a / b
}
// Compiler PROVES b is never 0

Nova doesn't just test — it proves. When you write a contract, the compiler mathematically verifies that every possible execution path satisfies it.

Contracts: Specifications in Code

Nova uses contracts to specify what functions require and guarantee. There are two main clauses:

fn function_name(params) -> ReturnType
where
    requires precondition     // What must be true BEFORE the call
    ensures postcondition      // What will be true AFTER the call
{
    // function body
}

• requires — Preconditions the caller must satisfy
• ensures — Postconditions the function guarantees

Examples of Contracts

// Safe division: caller must provide non-zero divisor
fn divide(a: Int, b: Int) -> Int
where
    requires b != 0
    ensures result * b == a  // Return value times b equals a
{
    a / b
}

// Safe array access: index must be in bounds
fn get(arr: [T], index: Int) -> T
where
    requires index >= 0
    requires index < arr.len()
{
    arr[index]
}

// Absolute value: result is always non-negative
fn abs(x: Int) -> Int
where
    ensures result >= 0
    ensures result == x || result == -x
{
    if x >= 0 { x } else { -x }
}

// Sorting: output is a permutation of input, and is sorted
fn sort(arr: [Int]) -> [Int]
where
    ensures result.len() == arr.len()
    ensures is_sorted(result)
    ensures is_permutation(result, arr)
{
    // ... sorting implementation
}

How Verification Works

Nova's verifier translates your code and contracts into mathematical formulas, then uses an SMT solver to check if there's any way the contracts can be violated.

What's an SMT Solver?

SMT stands for Satisfiability Modulo Theories. It's a tool that can answer questions like:

• "Is there any integer x where x > 5 AND x < 3?" → No (unsatisfiable)
• "Is there any integer x where x > 0 AND x * x == 4?" → Yes, x = 2

Nova uses Z3, a powerful SMT solver developed by Microsoft Research. When you compile Nova code, the verifier:

Verification in Action

Let's trace through verifying the abs function:

fn abs(x: Int) -> Int
where
    ensures result >= 0
{
    if x >= 0 { x } else { -x }
}

The verifier considers two paths:

Both paths satisfy the postcondition, so the function is verified!

What the Verifier Can Prove

Nova's verifier can reason about:

• Arithmetic — Inequalities, equalities, modular arithmetic
• Arrays — Bounds, element properties, length constraints
• Loops — With loop invariants (properties that hold on each iteration)
• Recursion — With proper termination measures
• Algebraic data types — Pattern matching completeness

Loop Invariants

Loops are tricky to verify because they execute an unknown number of times. Nova uses loop invariants — properties that are true before the loop, maintained by each iteration, and true after.

fn sum(arr: [Int]) -> Int
where
    ensures result == arr.fold(0, |a, b| a + b)
{
    let mut total = 0;
    let mut i = 0;

    while i < arr.len()
    invariant i <= arr.len()
    invariant total == arr[0..i].fold(0, |a, b| a + b)
    {
        total = total + arr[i];
        i = i + 1;
    }

    total
}

The invariants tell the verifier:

• i is always within bounds
• total is always the sum of elements we've seen so far

Verification Failures

When verification fails, Nova shows you exactly what went wrong:

fn bad_divide(a: Int, b: Int) -> Int {
    a / b  // No precondition on b!
}

error[V0001]: potential division by zero
  --> main.nova:2:5
   |
2  |     a / b
   |     ^^^^^ division may fail if b == 0
   |
   = note: counterexample found: a = 1, b = 0
   = help: add a precondition: requires b != 0

The verifier found a counterexample — specific values that violate the safety property. This is incredibly useful for debugging!

Capabilities: Security Through Verification

Nova extends verification to capabilities — permissions that must be explicitly granted. This prevents entire classes of security vulnerabilities.

// FileSystem is a capability that must be passed explicitly
fn read_file(path: String, fs: cap FileSystem) -> String {
    fs.read(path)
}

// This function can't secretly access the filesystem
fn process_data(data: String) -> String {
    // No FileSystem capability = can't do file I/O
    data.to_uppercase()
}

// Main must explicitly pass capabilities
fn main(fs: cap FileSystem) {
    let content = read_file("data.txt", fs);
    let processed = process_data(content);
    // process_data can't leak data to files
}

The type system tracks which functions have which capabilities. A function without cap Network literally cannot make network requests — it's mathematically impossible.

The Verification Levels

Not every project needs full formal verification. Nova offers graduated levels:

Real-World Verification

Formal verification isn't just academic. It's used in:

• seL4 — A formally verified operating system kernel used in helicopters, cars, and defense systems
• CompCert — A formally verified C compiler that guarantees the compiled code matches the source
• AWS — Uses formal methods to verify S3, IAM, and other critical infrastructure
• Ethereum smart contracts — Formal verification prevents million-dollar bugs

Nova brings these industrial-strength techniques to everyday programming.

What's Next?

We've covered how Nova checks your code. The final step is turning that verified code into something that actually runs. In the next lesson, we'll explore code generation — how Nova produces WebAssembly from your verified source code.