Differences From Motoko

Sector9 is derived from Motoko, but it is no longer just Motoko with extra comments or a verification command on the side. Motoko gives you an actor language for the Internet Computer. Sector9 keeps the actor model and familiar syntax, then changes the language around one central goal: important protocol claims should be written in source and checked by tools.

That one goal explains most of the differences. Motoko has no built-in deductive verification system. Sector9 has one. It adds contracts, proof-only state, explicit state footprints, verified async rules, specification collections, quantifiers, trusted-boundary tracking, and protocol-analysis surfaces. It also rejects some legal Motoko programs when the verifier cannot give them a sound meaning.

If you already know Motoko, the useful mental model is:

1. Read the actor and module syntax as familiar.
2. Read every function header as a proof interface.
3. Read ghost, lemma, spec collections, and quantifiers as proof language.
4. Read await, shared calls, tokens, and upgrades as boundaries where hidden assumptions must become explicit.

For the general verification mindset, start with The Fundamental Shift. This page focuses on what changed from Motoko and where to continue reading.

A Sector9 Function Header Is A Contract Boundary

In Motoko, a function signature mainly describes types. In Sector9, the header also describes the proof contract. requires states what a verified caller must establish, ensures states what the function promises on return, and result names the returned value inside postconditions.

Public actor methods have an additional distinction that standard Motoko does not have. entry_requires is the runtime entry guard for external messages; requires is the logical precondition used by the verifier. Sector9 rejects public methods that ask the verifier to assume caller-controlled facts without an entry guard, because an external IC caller is not a verified caller.

This is the first major shift: contracts are not comments and not tests. They are the interface that other verified code relies on. Multiple clauses are combined as described in Combining Requires and Ensures, and callbacks can carry their own contracts through Function Type Contracts. When a contracted function value flows through subtyping, Sector9 checks contract preservation instead of silently erasing obligations.

State Effects Are Part Of The Interface

Motoko lets a method read or write actor fields directly. Sector9 makes those effects explicit. modifies declares the fields a function may write; reads declares the fields it may read. Together they give the verifier permission to access state and give callers a frame: fields outside the write set can be preserved through the call when the caller has permission to mention them.

This is not bureaucracy. It is what makes modular proofs possible. If a helper declares only modifies nonce, a caller can keep facts about balance without opening the helper body. The deeper mechanics are covered by Frame Conditions and Effect Inference.

The same discipline applies to ghost fields, runtime fields, private helpers, public methods, and contract-typed callbacks. If state matters to the proof, Sector9 wants that dependency in the boundary.

Invariants Turn Protocol Intent Into Obligations

Motoko actors can maintain invariants by convention. Sector9 lets you state them as actor-level invariant clauses. The verifier checks them after initialization, at public method boundaries, and around suspending await points. This is how durable protocol facts become obligations that every public transition must preserve.

Loops get the same treatment. A Motoko loop is executable control flow; a Sector9 loop may need loop:invariant annotations so the verifier can prove an unbounded number of iterations. When a postcondition needs the entry value of a field or expression, use old(). Its forbidden contexts are documented in Old Expression Restrictions.

The practical rule is simple: use function contracts for one transition, actor invariants for facts that every transition must preserve, and loop invariants for facts that must survive every iteration.

Assertions Separate Proof From Runtime Defense

Motoko has runtime assertions and traps. Sector9 splits intent more carefully. A plain assert is a proof obligation and is erased from runtime output. A runtime:assert is both verified and emitted as a runtime check. A trap is for paths that should be unreachable under the verified assumptions and still trap if reached at runtime.

This distinction keeps proof scaffolding out of deployed code while preserving real runtime guards where you intentionally want defense in depth. Use Choosing the Right Assertion when deciding which form belongs at a boundary.

Pure Functions, Lemmas, Abstracts, And Trusted Code Are Different Tools

Motoko helpers can freely mix computation and effects. Sector9 introduces proof-specific helper forms.

pure functions are specification-callable mathematical helpers. They can appear in contracts, invariants, assertions, and ghost code, but they cannot mutate state or await. Their contract usage is covered in Pure Functions in Contracts, and the restrictions are listed in Pure Function Restrictions.

lemma declarations are proof steps. Use them when the solver needs a named argument, a loop step, or a reusable bridge between facts. For verification-driven development, abstract signature-only declarations let you specify an interface before implementing it. trusted is different: it is an explicit unchecked assumption and expands the trusted base. The trusted-base cost is explained in The Trusted Base.

The essence: pure defines, lemma proves, abstract defers, and trusted assumes.

Ghost Code Lets You Model What Runtime Should Not Store

Standard Motoko has runtime state. Sector9 also has proof-only state. ghost var fields can track histories, summaries, ownership models, or conservation laws that do not need to exist in the deployed actor. ghost { } blocks update proof state and run proof steps; they are erased from runtime.

This is how many real proofs become manageable. A ledger might store balances in a runtime map but prove conservation with a ghost summary. An access-control module might keep deployable role state and mirror it into a ghost model for quantified permission facts. The boundary is strict: ghost blocks cannot mutate runtime fields, and ghost facts cannot be the only runtime source of authorization.

Specification Collections Are Proof Models, Not Storage

Motoko collections are runtime data structures. Sector9 separates runtime collections from mathematical proof collections. The ghost/spec collection modules Map, Set, Seq, and Multiset are proof vocabulary. They model balances, domains, ordering, membership, and permutation facts inside specifications; they are not deployed storage.

When the program needs executable storage, use runtime library structures such as pure BMap or mutable MBMap, then connect them to proof models through Spec.model contracts. The same pattern appears in larger helpers such as MapSummary and SimpleLedger.

The deeper collection proof rules cover threading updates, old() with collections, and spec-immutable element restrictions.

Quantifiers Give The Language A Solver Vocabulary

Motoko has loops and iterators, but no SMT quantifiers in the language. Sector9 adds verifier-facing forall and exists for properties like "every listed account remains solvent" or "there is a witness for this transition chain." These are powerful, but they are solver-facing constructs, so the shape of the predicate matters.

When quantifiers get expensive or the solver cannot find the right instantiation, Sector9 exposes triggers and practical quantifier patterns. This is another difference from ordinary Motoko: you are not just writing a loop that executes; you are writing a formula the solver can use.

Async Is Checked Against Interference, Not Just Typed

Sector9 inherits Motoko's async actor model, but gives it proof semantics. At a suspending await, the verifier assumes other messages may run before execution resumes. The interference model havocs actor state that public methods may write and keeps only facts justified by invariants, frames, local freshness, or explicit rechecks.

That is why exact pre-await values often disappear after an await. The right patterns are: preserve what you need in invariants, re-check conditions after await, keep public write effects narrow, and avoid carrying actor-rooted mutable aliases across suspension. The companion pages on atomicity, commit points, local vs shared state, and async frames explain the proof model.

async*/await* is also more precise than a surface reading suggests. It is not a consensus bypass. It is a computation form: await* continues through the callee and only creates an interference boundary if that callee may reach a real suspension.

Error Handling Is Narrower In Verified Code

Motoko supports throw, try, catch, and finally. Sector9 supports the syntax, but verification mode narrows the surface. Verified code rejects throw; suspending awaits must have explicit catch-all recovery; error values cannot escape verified code; and finally cannot suspend or transfer control outward.

This is not just a limitation. It makes failure paths visible to the proof. A verified async result has a success path and a fallback path, and both need facts strong enough for the function's postcondition and invariant obligations. For impossible failures, use trap. For protocol-level failures, use a domain result type rather than hidden thrown control flow.

Shared Boundaries Carry Proof Meaning

Motoko shared functions describe IC message boundaries. Sector9 keeps shared functions, then adds proof-aware rules at those boundaries. Update methods use entry guards, queries have their own query verification rules, and caller identity should be bound with shared({caller}) rather than passed as a normal argument.

Sector9 also tightens shared type reasoning. Shared signatures must contain serializable, stable shapes; functions, mutable arrays, and modules do not cross ordinary shared boundaries. Actor references are allowed through shared interfaces. The practical rules are covered in update shared type restrictions and async shared type requirements.

Verified Actors Can Compose Across Canisters

One of the biggest differences from ordinary Motoko is that Sector9 is designed for verified actors to build on other verified actors, not only to prove one isolated canister at a time. Motoko can type-check that an imported actor has a shared method shape. It does not carry a proof that the remote canister was checked against the contracts and protocol assumptions you are relying on.

Sector9's sr9 boundary is the interoperability layer for that problem. In proof-enabled builds, a verified canister stores proof material and attaches it to outbound sr9 calls. The receiving sr9 method validates the caller proof, rejects non-canister or invalid callers before token conversion, and exposes caller identity through the proof, principal, module-hash, and CHASH surface. The high-level flow is described in Proof-Enabled Call Flow, and the identity side is covered in Module Hash and Token Identity.

That changes the shape of multi-canister contracts. A Sector9 actor can import another Sector9 actor interface, call it downstream, and reason from the downstream contract while the shared boundary checks that proof-enabled calls come from verified participants. This does not make arbitrary remote code trusted by magic; the dependency still has to be expressed through explicit contracts, shared types, sr9 boundaries, module identity, and protocol assumptions. But it solves the hard part that ordinary Motoko leaves outside the language: tying cross-canister interoperability to verifiable actor interfaces instead of treating every remote call as opaque trust.

Persistence And Upgrades Are Part Of The Proof Story

Motoko and the IC already provide orthogonal persistence. Sector9 treats it as a verified state boundary. In a persistent actor, fields are stable by default, and transient marks state that resets on upgrade. Upgrade safety is covered by compatibility rules.

For method verification, stable and transient fields both participate in reads, modifies, invariants, and await interference. Stability controls upgrade persistence; it does not make a field magically stable across a suspending await. That distinction is covered in state across await points and verification with stable fields.

The Type System Is More Protocol-Aware

Sector9 keeps many Motoko-like type forms, but verification adds structure and restrictions. Function subtyping becomes contract-aware, structural subtyping is limited to spec-immutable record and module shapes, and mutable identity coercions are restricted to avoid unsound aliasing.

Sector9 also adds type operators that are especially useful for protocol surfaces: type spread, omit, and pick. They let you build public views, callback interfaces, and proof-facing module surfaces without duplicating every field by hand.

The file and import story also shifts toward Sector9 as its own source language. .sr9 is the canonical extension, while .mo remains legacy compatible. The project docs cover file extensions and import syntax.

Numeric Safety Is Proved, Not Assumed

Motoko has fixed-width integer types and runtime arithmetic behavior. Sector9 asks the verifier to prove fixed-width operations stay in range. The default integer mode is checked, so overflow and underflow require guards, contracts, or assertions.

The language docs cover natural-number underflow, integer division safety, fixed-width overflow and underflow, and division guards. The style implication is concrete: a subtraction, increment, division, array index, or conversion may need a guard because Sector9 is proving the operation for all allowed inputs, not only for examples that tests happened to cover.

Digital Assets Get Language-Level Ownership Tools

Motoko can represent token-like values with records and modules, but it does not have verifier-enforced asset ownership or proof-aware shared conversion. Sector9 adds token and opaque types for module-owned values. Token-bearing shared methods use sr9 boundaries so token wrappers, module identity, and proof checks are handled at the shared boundary.

Runtime.moduleHash() lets asset definitions bind identity to the module that defines them, and the core fungible token module builds on that rule. Pair this with token conservation patterns and access control patterns when modeling real ledgers.

Runtime Projection Keeps Proofs Out Of The Binary

Sector9 source contains proof-only constructs that must not become deployed behavior. Runtime projection erases ghost declarations, proof-only assertions, and lemma calls while rejecting runtime roots that depend on proof-only values. That boundary is described in Code Identity and Runtime Projection and the proof-dependency check.

CHASH gives Sector9 a runtime-projection-aware identity surface. It filters many proof-only edits while keeping runtime-relevant declarations, entry_requires, and runtime assertions in the hashed surface. The current behavior and limits are documented in CHASH: Runtime Code Identity.

Sector9 Has A Protocol Lane Beyond Local Verification

The Viper/Silicon lane proves local deductive obligations: contracts, frames, permissions, invariants, and await boundaries. Sector9 also has a TLA+/TLC lane for protocol-level temporal checking. The important point is not "two identical proofs"; it is one authored program feeding two different analysis lanes.

The Semantic Bridge explains how Viper-owned semantic facts and protocol catalogs are combined into PIR and emitted to TLA+. The core protocol/lib module gives users a typed way to declare endpoints, roles, state bindings, call bindings, and temporal properties. Use this lane when the claim depends on message ordering, temporal behavior, participant roles, or protocol schedules rather than only one handler's local postcondition.

Some Legal Motoko Shapes Are Rejected

Sector9 intentionally rejects some Motoko programs. The reason is not parser incompatibility; it is proof soundness. Closures that hide state effects, mutable aliases that escape across await, proof-only collections in runtime code, non-shared values in public signatures, unguarded arithmetic, and ambiguous callback contracts can all be legal-looking code but bad verification surfaces.

The current boundaries are collected in Verified Restrictions and Soundness Notes. Focused pages cover aliasing limits, scheduling limits, runtime limits, and the verified subset.

The Workflow Produces Proof Artifacts, Not Just Binaries

Motoko compilation produces executable artifacts. Sector9 also produces proof artifacts. Use sector9 --check for source hygiene, sector9 --verify for full Viper verification, and sector9 --viper to inspect generated Viper. The pipeline from Sector9 to MVIR to Viper to SMT is summarized in Understanding the Pipeline.

When verification fails, debugging is also different from ordinary compiler debugging. Start with reading verifier errors, then use precondition debugging, intermediate assertions, loop invariant discovery, and counterexamples.

How To Read Sector9 If You Know Motoko

Read Sector9 as Motoko-shaped code with a proof interface. entry_requires tells you what external callers are allowed to send. requires tells you what verified callers must establish. ensures tells you what the callee gives back. reads and modifies tell you what state can be mentioned or changed. invariant tells you what every public transition must preserve. ghost, lemma, spec collections, and quantifiers tell you which parts exist only for proof. sr9, token, opaque, CHASH, and protocol schemas mark boundaries where identity and shared behavior matter.

That is the essence of the change. Motoko asks whether the program is a valid IC actor program. Sector9 asks a stronger question: can this protocol transition be proved under the written contracts, explicit state effects, IC async interleavings, upgrade behavior, shared-boundary rules, and trusted assumptions?