The Verification Mental Model

How verification differs from testing: proving properties over symbolic inputs, not just the ones you test.

The Fundamental Shift

Testing and verification answer different questions:

Approach	Question Answered
Testing	"Do these specific test cases pass?"
Verification	"Does this property hold for every input allowed by the specification?"

When you write a test for a function add(a, b), you check specific values: maybe add(1, 2) == 3 and add(0, 0) == 0. If both pass, you gain confidence but no guarantee. The function might fail for add(MAX_INT, 1) or any other untested input.

When you verify the same function with an ensures contract such as ensures result == a + b, the verifier proves this property for all values of a and b allowed by the function's types, preconditions, and arithmetic mode. Not ten cases, not a million cases, but the whole symbolic input space.

Contracts as Specifications

A contract is a specification, not an assertion. It describes what must be true, and the verifier proves it:

public func increment(n : Nat) : async Nat
  entry_requires n < 1000;
  requires n < 1000;
  ensures result == n + 1;
{
  n + 1
}

This contract says: "For any natural number n less than 1000, the result equals n + 1." The entry_requires guard is the runtime entry check for an exported actor method, and the logical requires is the verifier precondition. The verifier does not run the function with sample inputs. It analyzes the code symbolically and proves the postcondition follows from the implementation for all valid inputs.

Symbolic Reasoning

The verifier treats inputs as symbolic values rather than concrete numbers. When verifying increment, it doesn't substitute n = 5 or n = 999. Instead, it reasons about a symbolic n that represents any natural number satisfying n < 1000.

This is why a single verification covers infinite cases:

symbolic-reasoning.sr9

// Symbolic reasoning: one verification covers infinite cases
// The verifier proves abs() returns non-negative for ALL integers in range

persistent actor {
  public func abs(x : Int) : async Int
    entry_requires x >= -1000 and x <= 1000;
    requires x >= -1000 and x <= 1000;
    ensures result >= 0;
    ensures result == x or result == -x;
  {
    if (x < 0) { -x } else { x }
  };
}

The verifier proves result >= 0 holds for all x in [-1000, 1000]. It doesn't enumerate 2001 cases. It symbolically determines that if (x < 0) -x else x always produces a non-negative value.

Loop Invariants: Inductive Proofs

Loops present a challenge: they can execute any number of times. Testing might run a loop 10 or 100 times, but verification must cover unbounded iterations.

The solution is inductive reasoning via loop invariants:

loop-invariant.sr9

// Loop invariant: inductive proof covers all iterations
// One proof covers n=0, n=100, n=1000000 - any value

persistent actor {
  public func sumTo(n : Nat) : async Nat
    ensures 2 * result == n * (n + 1);
  {
    var i : Nat = 0;
    var sum : Nat = 0;

    while (i < n) {
      loop:invariant i <= n;
      loop:invariant 2 * sum == i * (i + 1);

      i := i + 1;
      sum := sum + i;
    };

    sum
  };
}

The verifier proves three things:

1. Initialization: The invariant holds before the loop starts (i = 0, sum = 0, and 2 * 0 == 0 * 1)
2. Preservation: If the invariant holds at iteration start and the condition is true, it holds after the body
3. Conclusion: When the loop exits, the invariant plus the negated condition imply the postcondition

This inductive proof covers ALL possible values of n. Whether n is 0, 100, or 1 million, the same proof applies.

Universal Quantification

The forall expression makes "for all" reasoning explicit:

forall-example.sr9

// Universal quantification: property holds for ALL values
// The forall proves every valid index has a non-negative element

persistent actor {
  public func checkPositive() : async () {
    let arr : [Nat] = [1, 2, 3, 4, 5];
    let size : Nat = arr.size();

    ghost {
      // For ALL indices i, if i < size, then arr[i] >= 0
      assert forall<Nat>(pure func (i : Nat) : Bool =
        (i < size) ==> (arr[i] >= 0));
    };
  };
}

The assertion forall<Nat>(pure func (i) = i < size ==> arr[i] >= 0) says: "For every natural number i, if i is a valid index, then arr[i] is non-negative."

The guard i < size bounds the property to valid indices. Without it, the verifier would try to prove the property for indices beyond the array, which would fail.

Counterexamples: When Proofs Fail

When verification fails, --counterexample asks the verifier to print a counterexample model: concrete values that violate the contract when a model is available.

counterexample_unsat.sr9

// Counterexample: concrete values that violate the contract
// The postcondition claims result == a + b + 1, but implementation returns a + b

persistent actor {
  public func add(a : Int, b : Int) : async Int
    ensures result == a + b + 1;  // Wrong: off by one
  {
    a + b  // Returns a + b, not a + b + 1
  };
}

Running sector9 --verify --counterexample on this file produces:

Counterexample summary
  - return: a=0, b=0, $Res=0

The counterexample shows that when a=0 and b=0, the function returns 0, but the postcondition expects 1. This is not just a sampled test failure; it is a concrete model showing why the proof obligation cannot be established. Generated names such as $Res mean "the returned result" in the Viper model.

The Contract as Interface

Contracts enable modular reasoning. When you call a function, you only need to know its contract, not its implementation:

// Caller only sees the contract:
//   requires amount <= balance
//   ensures balance == old(balance) - amount;

public func pay(amount : Nat) : async () {
  let paid =
    try {
      await withdraw(amount);  // Must satisfy: amount <= balance
      true
    } catch (_) {
      false
    };
  if (paid) {
    // Success path: balance decreased by exactly amount
  }
}

The caller must establish the precondition. In return, the caller can assume the postcondition on the success path. If the awaited call is caught, the catch path must provide its own safe fallback facts. The verifier checks both sides independently, enabling local reasoning about each function.

Invariants: Global Properties

Actor invariants express properties that hold across ALL public method calls:

invariant-example.sr9

// Actor invariant: must hold at entry and exit of every public method
// The balance can never go negative

persistent actor {
  var balance : Int = 0;

  invariant balance >= 0;

  public func deposit(amount : Nat) : async () modifies balance
    ensures balance == old(balance) + amount;
  {
    balance += amount;
  };

  public func withdraw(amount : Nat) : async Bool modifies balance
    ensures result == (old(balance) >= amount);
    ensures result ==> balance == old(balance) - amount;
    ensures (not result) ==> balance == old(balance);
  {
    if (balance >= amount) {
      balance -= amount;
      true
    } else {
      false
    }
  };
}

The invariant balance >= 0 must hold:

• After initialization
• At entry and exit of every public method
• Before every await

Every method that modifies balance must preserve this property. The verifier checks this automatically for all methods.

What Verification Guarantees

When Sector9 reports ✓ verification succeeded, it means the verifier established:

1. All ensures clauses hold whenever the function returns, for any input satisfying requires
2. All invariant declarations are preserved by every method
3. All assert statements are valid at their locations
4. All loop invariants are inductive and maintained

This is a mathematical proof relative to the written specification, verifier model, and trusted assumptions. The checked properties hold for modeled executions, not just the ones you happened to test.

What Verification Does Not Guarantee

Verification proves correctness with respect to the specification. It does not guarantee:

• The specification is what you intended (you might specify the wrong property)
• Termination (loops might run forever; Sector9 proves partial correctness)
• Runtime behavior outside the model (memory limits, timing, environment failures)
• Cross-canister schedule properties in the Viper lane; use TLA+ when the claim depends on message ordering or temporal behavior
• Properties you didn't specify

A function with no contracts verifies trivially. Verification is only as strong as your specifications.

Thinking in Contracts

To use verification effectively, adopt this mental model:

1. Specify first: What property should hold? Write the ensures before the implementation.
2. Think universally: Ask "does this hold for all allowed inputs?" not "does this work for my test cases?"
3. Trust the contracts: When calling a function, rely on its postcondition. Don't peek at the implementation.
4. Strengthen when needed: If verification fails, either fix the code or add preconditions to rule out invalid cases.
5. Use invariants for state: Actor invariants capture properties that span multiple operations.

Summary

• Verification proves properties for symbolic inputs allowed by the specification, not specific test cases
• Contracts (requires, ensures) are specifications the verifier proves mathematically
• The verifier uses symbolic reasoning to cover infinite cases simultaneously
• Loop invariants enable inductive proofs over unbounded iterations
• Counterexamples show concrete values when proofs fail
• Contracts enable modular reasoning: analyze each function independently
• Verification establishes correctness with respect to your specification and verifier model