Authoring Checklist

Before publishing a contract:

• parse and verify it;
• run authoring diagnostics;
• inspect compiler report;
• inspect storage layout;
• check static cost;
• run local runtime tests;
• run ledger tests for posting effects;
• review all @tx entrypoints for guard-before-effect discipline.

Contract Review

Ask:

• Is the syntax in the implemented subset?
• Are all guards before writes and effects?
• Are ctx.* fields real?
• Are intrinsics real?
• Does post(...) use the correct operation kind?
• Does the ledger AllowedEdge graph allow the route?
• Is business state separated from ledger balances?
• Are map/vector bounds sensible?

Invariants (`@invariant`)

An @invariant function runs after every @tx, on the post-write storage. If it returns false the entire transaction is reverted ([LE-160]).

Rules:

• Declare with @invariant; no parameters; return type must be bool.
• Invariants are not part of the ABI — callers cannot invoke them directly.
• Keep invariants cheap: they run on every @tx, so complex invariants add cost to all mutations.
• Invariants do not run after @view calls.
• Multiple invariants are checked in declaration order; the first failure reverts and stops.

Good uses:

• Solvency constraints: self.total_liabilities <= self.total_assets
• Referential integrity: self.borrower != "" after origination
• Monotonic counters: self.sequence >= self.last_confirmed_sequence

Avoid:

• Invariants that query external contracts (no cross-contract calls inside invariants).
• Invariants with side effects (writes, events) — they run on a scratch execution and their effects are discarded.