What is Sector9?

Sector9 is a Motoko-derived language and verification toolchain for Internet Computer systems. It keeps the actor-oriented feel of Motoko, but adds enough verification syntax, type-system rules, shared-boundary checks, and proof semantics that new code should be treated as Sector9 source, not Motoko with a checker bolted on.

The practical goal is simple: important protocol assumptions should be visible in source code and checked before deployment. That includes local properties such as balances staying non-negative, public-entry properties such as only an owner being able to call an update method, and cross-canister properties such as proof-enabled Sector9 actors calling other proof-enabled Sector9 actors through sr9 shared boundaries.

The Problem with Testing

Testing can only check the specific inputs you choose. A test suite for a token transfer function might verify that transferring 100 tokens works correctly, but it cannot prove the function works for every possible amount. You might miss edge cases like zero transfers, maximum values, or overflow conditions.

For smart contracts handling financial assets, a single missed case can mean catastrophic loss. Testing is necessary but insufficient.

Verification vs Testing

Sector9 uses formal verification to prove written properties over symbolic inputs and modeled execution paths:

Approach	What It Proves
Testing	"These specific test cases passed"
Verification	"This property holds for every input allowed by the specification"

When Sector9 verifies a function in the Viper lane, it proves the specification is satisfied for all values allowed by the preconditions and for the state interference modeled by the verifier. That proof is only as strong as the specification and the trusted base, so Sector9 pushes boundary assumptions into explicit source constructs instead of letting them remain hidden.

How It Works

Sector9 extends and specializes Motoko into its own verification-oriented language. Its annotations specify what your code should do:

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
  };
}

The ensures clauses are contracts: promises your code makes to callers. Sector9 proves these contracts hold for inputs allowed by the specification.

Public methods also distinguish between a logical precondition and a deployed entry check. requires is what verified callers may assume; entry_requires is the runtime guard that screens external IC messages before the method body runs.

The Verification Pipeline

When you run sector9 --verify file.sr9, the system:

1. Parses and type-checks your Sector9 source
2. Extracts contracts (requires, ensures, invariant, etc.)
3. Translates to an intermediate representation (MVIR)
4. Runs analysis passes for effects, permissions, and async handling
5. Generates Viper code (a verification language)
6. Invokes the SMT solver (Z3) to prove or disprove your contracts
7. Reports results mapped back to source locations when available, with generated Viper locations as the fallback

If verification succeeds, your code satisfies its specification under Sector9's verifier model and trusted assumptions. If it fails, Sector9 shows which property could not be proven and can often print a counterexample model.

What You Can Verify

Sector9 supports a rich set of verification constructs:

Contracts

• entry_requires - Runtime entry guards for exported actor methods
• requires - Preconditions callers must satisfy
• ensures - Postconditions the function guarantees
• old() - Capture values at function entry for comparison

State Tracking

• modifies - Declare which fields a function may change
• reads - Declare which fields a function observes
• invariant - Properties that always hold at actor boundaries

Advanced Features

• Ghost state for verification-only tracking
• ghost func and lemmas for proof helpers
• abstract func declarations for contract-only specification placeholders
• Spec collections (Map, Set, Seq, Multiset)
• Quantifiers (forall, exists) for universal properties
• token and opaque module-owned values for asset and handle boundaries
• sr9 shared calls for proof-enabled cross-canister boundaries

Why Sector9 for the Internet Computer

The Internet Computer has unique verification challenges:

Async/Await Boundaries: When your actor awaits a response, other messages can execute. Viper models await interference conservatively for local handler proofs.

Reentrancy: While awaiting, your own public methods can be called again. Sector9 checks that declared invariants hold under conservative reentrancy assumptions.

Verified interoperability: Ordinary actor imports give you a typed remote interface. Sector9 can additionally use proof-enabled sr9 boundaries so verified canisters can carry proof material across calls and reason from downstream verified interfaces instead of treating every remote dependency as opaque trust.

Protocol Schedules: For claims that depend on cross-canister schedules, interleavings, or async failure behavior, Sector9 also has a TLA+ backend. This getting-started section focuses on the Viper/local-correctness lane.

What Sector9 Does Not Do

• Termination proofs: Sector9 verifies partial correctness (if code terminates, it's correct) but not that loops always terminate
• Runtime behavior: Verification applies to logic correctness, not performance or gas costs
• Complete protocol liveness: The Viper lane proves local correctness; schedule-level liveness and multi-canister temporal claims belong in TLA+ models

File Extensions

Sector9 has one source language. Use .sr9 for new files; .mo remains accepted for legacy compatibility. The sr9 token in shared sr9 func is unrelated to the file extension: it marks a caller-verified shared method.

# Canonical extension
my-contract.sr9

# Also supported
my-contract.mo

Summary

• Sector9 is a Motoko-derived language plus verification toolchain for smart contracts and protocols
• It proves written properties hold for all inputs allowed by the specification, not just tested cases
• Contracts (entry_requires, requires, ensures, invariant) specify expected behavior
• The Viper lane translates Sector9 source to Viper and uses Z3 for proof
• It handles local IC-specific challenges like async/await interference
• It supports proof-aware cross-canister boundaries through sr9 shared calls
• TLA+ covers protocol-level scheduling and temporal claims
• Verification catches specification violations before deployment and reduces reliance on tests alone