Your First Verified Program

This page walks through a tiny counter actor, then shows what Sector9 proves and what it deliberately does not infer for you. The important habit is to read the function header as the proof interface: return guarantees go in ensures, state effects go in reads and modifies, and public entry assumptions go in entry_requires.

A Simple Counter

Let's create a counter with contracts that the verifier can check. This is a persistent actor with a count variable:

counter.sr9

// Your first verified program
// A simple counter with a postcondition

persistent actor {
  var count : Nat = 0;

  // The `ensures` clause proves the return value equals count
  public func get() : async Nat
    reads count
    ensures result == count;
  {
    count
  };

  // Proves that count increases by exactly 1
  public func increment() : async Nat
    modifies count
    ensures count == old(count) + 1;
    ensures result == count;
  {
    count += 1;
    count
  };
}

This actor has two methods:

• get() returns the current count
• increment() increases the count by 1 and returns the new value

Both methods are small, but they already show Sector9's central idea: the implementation is checked against a written contract for all modeled states, not only against example inputs.

What Makes This "Verified"?

The key verification features in this program are:

1. Postconditions with ensures

The ensures clause specifies what must be true when a function returns. In get():

ensures result == count;

This proves that the return value (result) equals the current count on every modeled return path.

2. Capturing Previous State with old()

In increment():

ensures count == old(count) + 1;

The old() expression captures the value of count at method entry. This postcondition proves that count increases by exactly 1 for all entry states allowed by the specification.

3. Declaring Field Access with reads and modifies

Actor methods must declare which actor fields they access:

• reads count - The function reads count but does not change it
• modifies count - The function may change count

These declarations enable the verifier to prove that unmentioned actor fields remain unchanged (the "frame condition"). Local variables and fresh local values do not need reads or modifies.

Running Verification

Step 1: Type Check

Start with a quick type check to catch syntax errors:

sector9 --check counter.sr9

If successful, there is no output and the exit code is 0.

Step 2: Verify

Run full verification to prove the checked contracts:

sector9 --verify counter.sr9

Successful output:

✓ verification succeeded

The verifier has proven these checked properties under the current specification:

• get() always returns the current count
• increment() always increases count by exactly 1
• increment() always returns the new count value

It has not proven unrelated claims. For example, there is no claim here about a maximum counter value, authorization, or liveness. Add those as actor invariants, preconditions, or protocol-level models when they matter.

When Verification Fails

Let's see what happens when the code has a bug. Consider this incorrect version:

counter-bug.sr9

// A buggy counter - verification will fail
// The postcondition claims result == count, but we return BEFORE incrementing

persistent actor {
  var count : Nat = 0;

  // BUG: Returns the old count, not the new count
  public func increment() : async Nat
    modifies count
    ensures count == old(count) + 1;
    ensures result == count;  // This is wrong!
  {
    let old_count = count;
    count += 1;
    old_count  // Returns old value, but ensures claims result == count
  };
}

The postcondition claims result == count, but the function returns the saved old value instead of the value after incrementing. Running verification:

sector9 --verify counter-bug.sr9

Typical output:

✗ verification failed (1 issue)

[1] Postcondition of increment might not hold
  Postcondition of increment might not hold.
  method: increment
  hint:
    - Strengthen the implementation or weaken the ensures.

The exact snippet and location may be a source span or, when source mapping is unavailable, a generated Viper span. To debug:

1. Read the message - "Postcondition ... might not hold" tells you the issue type
2. Check the method and snippet - The failing obligation is the ensures result == count clause
3. Trace the logic - The function returns old_count, so result is the old value while count is the new value

Getting More Information

Add --counterexample to ask for concrete values that cause the failure:

sector9 --verify --counterexample counter-bug.sr9

When a model is available, this shows example values where the contract fails, helping you understand the bug. Internal names such as $Res may appear when the counterexample comes from the generated Viper model.

Understanding the Verification Output

Output	Meaning
✓ verification succeeded	Checked contracts proven for all inputs allowed by their preconditions
✗ verification failed	At least one obligation could not be proven
Exit code 0	Success
Exit code 1	Verification failure

For a deeper explanation of source spans, generated Viper locations, and model output, continue to Understanding Verification Output.

Try It Yourself

1. Create counter.sr9 with the correct code above
2. Run sector9 --verify counter.sr9 and confirm it succeeds
3. Change count += 1 to count += 2 and verify again
4. Observe the failure message and fix the postcondition

Common Beginner Mistakes

Wrong postcondition value

// WRONG: Off by one
ensures result == n + 2;
// But function returns n + 1

Missing modifies clause

// WRONG: Modifies count but doesn't declare it
public func increment() : async ()
  ensures count == old(count) + 1;
{
  count += 1  // Error: undeclared modification
}

Using old() in preconditions

// WRONG: old() in requires doesn't make sense
requires old(count) > 0  // Error: old() not allowed here

old() captures state at method entry, so it is only meaningful in postconditions (ensures) where you compare final state to initial state.

Confusing Public Preconditions with Entry Guards

// WRONG for a public method: external callers do not prove requires clauses
public func withdraw(amount : Nat) : async ()
  requires amount <= balance;
{ ... }

// CORRECT: runtime guard plus logical proof fact
public func withdraw(amount : Nat) : async ()
  entry_requires amount <= balance;
  requires amount <= balance;
{ ... }

Use entry_requires for facts that must be checked at the external IC boundary. Use requires for the logical fact that verified callers and the verifier may rely on inside the body.

Next Steps

• Learn about Understanding Verification Output for debugging failures
• See Preconditions with requires to restrict function inputs
• See Entry Guards before adding preconditions to public actor methods
• Explore Actor Invariants for properties that always hold

Summary

• Use ensures to specify what must be true when a function returns
• Use result in postconditions to refer to the return value
• Use old(expr) to capture values at method entry
• Declare field access with reads and modifies
• Run sector9 --verify to prove contracts hold for all inputs allowed by their preconditions
• Verification failures show exactly which contract failed and where