Trusted Modifier
The trusted modifier marks a deliberate verification boundary: callers must prove the function's preconditions, and the verifier assumes its postconditions without proving the implementation.
Signature-Only Decls
Bodyless verifier placeholders are written with abstract. Use bodyless trusted only for permanent assumptions that belong in the trusted base.
Abstract Functions
Abstract functions are contract-only declarations for verification-driven development. They have requires and ensures clauses, but no body yet, so their postconditions are assumptions until the declaration is refined.
The Trusted Base
Understanding what Sector9 trusts without proof: prelude axioms, primitive collections, core-library boundaries, and user-defined trusted code.