Termination
Sector9 verifies partial correctness only: it proves properties hold if
Deep Aliasing
Sector9 supports basic aliasing
Runtime Traps
System-level failures like out-of-memory (OOM), garbage collection failures, inter-canister errors, and stable memory issues are outside the verification model. This page explains what Sector9 does and does not verify about runtime failures.
Cross-Canister Scheduling
Sector9's Viper lane does not model cross-canister message ordering or FIFO
Verified Subset Boundaries
Verified code runs under a stricter, sound subset of Sector9. Sector9 is a