What is Sector9?
See what Sector9 proves beyond tests and where it fits in an IC development workflow. Learn the problem it solves before writing specs.
Installation and Setup
Install the containerized toolchain without assembling Viper, Z3, OCaml, or Nix by hand. Get to a runnable verifier setup fast.
Your First Verified Program
Write a tiny actor, add a contract, and watch the verifier catch the bug. This is the shortest path from syntax to proof.
Differences From Motoko
A guided article on the language, verification, async, ownership, and protocol-safety differences between Sector9 and standard Motoko.
Verification Output
Read verifier success and failure output without guessing. Learn how to turn diagnostics into the next code or spec change.
Mental Model
Shift from testing examples to proving symbolic behavior. Understand what the verifier knows, assumes, and refuses to assume.
Project Structure
Organize verified programs across modules and packages. Keep examples small while learning how larger Sector9 projects fit together.
Quick Reference Card
Keep the core syntax close while you work. Use this as a compact map of contracts, assertions, ghost code, and verifier commands.