Complete Syntax Reference
This reference documents Sector9 verification syntax: function headers, contracts, ghost code, abstract declarations, assertions, invariants, proof collections, and common actor forms.
Error Code Reference
Complete reference for all Sector9 error codes with explanations and solutions.
Viper Encoding Reference
This reference documents how Sector9 language constructs are translated to Viper for formal verification. Sector9 is derived from Motoko, so many inherited constructs look familiar, but the verified source language is Sector9. Understanding this encoding helps when debugging verification failures or interpreting Viper output.
Example Gallery
A curated collection of complete, runnable examples demonstrating Sector9 verification patterns. Each example is self-contained and can be verified independently.
Verified Restrictions
This reference collects the current Sector9 restrictions and soundness model, including how verification models memory, effects, and async behavior.