Let’s start from Motoko’s type system. When you typecheck your code, the compiler does static analysis. It checks that the types across your program line up, and it puts boundaries around values so they cannot be used in ways that do not fit those types. That eliminates whole classes of errors.
You notice this even without AI. You add a new field to a record, run the compiler, and the typechecker goes through your code and tells you exactly where something no longer fits. It can make programs a bit harder to write at first, but once the types check, a lot of basic mistakes are gone. What remains are usually logical errors.
SR9’s verification syntax feels like the next layer of that idea.
Types let you say:
balance : Nat
SR9 lets you say things like:
balance < 20
or:
amount <= balance
or:
result == old(balance) - amount
It gives you a way to place more boundaries around your program. Not just type boundaries, but logical boundaries.
Take this simple example:
persistent actor {
var balance : Nat = 10;
public func withdraw(amount : Nat) : async Nat
modifies balance
{
balance -= amount;
balance
};
}
SR9 rejects it:
verification failed (1 issue)
Assert might fail. Assertion 0 <= $Self.fld$balance - amount might not hold.
Counterexample: balance=38, amount=39
The verifier found a real problem. If the balance is 38 and the withdrawal amount is 39, then mathematically the new balance would be -1. But balance is a Nat, and a Nat cannot represent negative numbers. In Motoko, that subtraction can trap.
So the verifier gives your agent fast feedback: this function is not safe for every possible input.
The agent can fix it by adding a boundary:
persistent actor {
var balance : Nat = 10;
public func withdraw(amount : Nat) : async Nat
modifies balance
entry_requires amount <= balance;
requires amount <= balance;
{
balance -= amount;
balance
};
}
Now the function says: this method is only valid when the requested withdrawal is less than or equal to the current balance. That is the missing logical boundary.
This example is trivial, but the idea scales.
Imagine there is more business logic inside. There are loops, switches, branches, intermediate values, and noisy refactors. It becomes much harder to tell by looking at the code whether balance always stays safe.
Here is a deliberately noisy example that still verifies:
persistent actor {
type Mode = { #same; #double; #weird };
var balance : Nat = 10;
public func withdraw(amount : Nat) : async Nat
modifies balance
ensures balance < 20;
{
let normalized : Nat = if (balance < 20) { balance } else { 19 };
assert normalized < 20;
balance := normalized;
let mode : Mode = if (amount == 0) { #same } else { #weird };
var i : Nat = 0;
var raw : Nat = 0;
var capped : Nat = 0;
var debit : Nat = 0;
while (i < amount) { loop:invariant i <= amount; loop:invariant balance < 20; loop:invariant raw == 0; loop:invariant capped == 0; loop:invariant debit == 0; i += 1; };
raw := switch (mode) { case (#same) amount; case (#double) amount + amount; case (#weird) if (i == amount) { i } else { amount } };
capped := if (raw <= balance) { raw } else { switch (mode) { case (#double) balance; case (_) balance } };
debit := if (capped == raw) { raw } else { capped };
assert balance < 20;
assert debit <= balance;
assert balance - debit < 20;
balance -= debit;
balance
};
}
This verifies for all possible amount values and all modeled starting states of balance.
A test can only try a few examples. The verifier builds a logical model of the program and asks an SMT solver to prove the property for every case covered by that model.
The important line is:
ensures balance < 20;
That is the contract. The function is obligated to return only after leaving balance below 20.
The assert statements in this example are not runtime traps. In SR9, plain assert is a proof step for the verifier. If you want a runtime check, you use runtime:assert or trap.
That is one of the few breaking changes from Motoko syntax, but it makes sense for verification. AI was getting confused when the same word meant both “prove this statically” and “check this at runtime.”
There are limitations today. You cannot just write arbitrary code and expect the verifier to understand everything. You often need to structure code in a narrow way, add loop invariants, add intermediate assertions, or use library models that the verifier understands.
But for AI coding, that is exactly the point.
Your agent can try an implementation, run verification, get a counterexample, and adjust the code. The verification layer becomes another feedback loop. It keeps the runtime code inside the boundaries you wrote down.
Actor invariants make this even more interesting.
For example:
persistent actor {
var apples : Nat = 0;
var oranges : Nat = 0;
invariant apples >= oranges;
// ...
}
Every verified method that can change apples or oranges has to prove that this invariant still holds.
Your canister might have 200 modules involved in calculations around apples and oranges. Someone reading the contract does not need to manually inspect every path to know the intended rule. If it verifies, then every verified path that touches this state has preserved the invariant.
That is the executive value of SR9: it turns important business rules into machine-checked obligations.
The typechecker keeps your values shaped correctly. The verifier keeps your logic inside the rules you declared.
For human developers, this is hard to write today. Even with AI, it takes tinkering and experimentation.
But if the future is AI writing more of the code, then this kind of boundary becomes much more practical. You do not want to rely only on the agent sounding confident. You want the agent to prove that the code it wrote still satisfies the rules. SR9 becomes a guardrail system for canister logic.
It lets you turn “I hope this is true” into “the verifier checked that every modeled path keeps this true.”
), look forward to learn more on your experience building it this far 