The verification spectrum

The companion to section 21 of the language-design document. That section specifies the verification layer; this one explains it — every term, why it exists, and how you actually use it, with worked examples. It is a guide, not a spec: where the two disagree, the design document wins.

Makoto is built for systems that must not fail. “Must not fail” is a promise, and a promise is only honest if something can check it. This document is about the machinery that lets you state a guarantee and have the compiler discharge it — from “this handle is used exactly once” all the way up to “this kernel is proved correct” — without any of it leaking onto the code of people who never ask for it.

Everything here obeys the opt-in test (section 1 of the design doc): you only pay for what you summon. There is no verification mode. There is a spectrum of guarantees, each summoned by a decorator or a type, each invisible until you reach for it. A program that wants none of this writes none of it and reads none of it.

---

1. The one idea: the discharge ladder

A guarantee in Makoto is always the same shape: an obligation on a predicate. “This index is in bounds” is the predicate i < len; “this transaction is committed or rolled back” is a predicate on a protocol; “reversing a list twice gives the original” is a predicate on a function. The compiler’s job is to discharge each obligation — to make it true, prove it, check it, or, failing all of that, make you sign for it.

There is a ladder of ways to discharge an obligation, from strongest to weakest:

Rung	How the obligation is discharged	Example
0	Type-level — the bad state cannot be written	a dropped @must_consume; Vec[T, 0].head
1	Comptime fold — the compiler computes the answer	Index[8] with the literal index 3
2	Summoned proof — an extension proves it (SMT, model checker)	dynamic arithmetic refinement, a liveness property
3	Runtime check — a trap on violation	@requires, a refinement that reached runtime
4	Advisory — a warning, no inserted cost	the memory analyzer’s hints
5	Human — you assert it, in writing	assume "…" (section 5)

The single rule that makes this safe:

An obligation that cannot be met at one rung falls to the next one down — never off the ladder.

A refinement the SMT solver cannot prove does not vanish; it becomes a runtime check. A runtime check you cannot afford on a hot path does not vanish; it becomes an assume with your name on it. The guarantee always degrades to the strongest honest form still available, and the language tells you, in the open, exactly which rung you landed on. That honesty is the whole point — the name Makoto (誠, “truth”) is the refusal to hide where a guarantee stops.

The rest of this document is the rungs, one family at a time.

---

2. Ownership: using a thing the right number of times

The terms. Two words from type theory, and they are simpler than they sound:

• Linear — must be used exactly once. Not zero times (forgetting it is a bug), not twice.
• Affine — must be used at most once. It may go unused, but never twice.

Makoto names them for what they do, and keeps the theory word for the docs:

• @must_consume = linear. You must consume this. A database transaction you must either commit or roll back — leaving a scope with it still open is the error.
• @consume_once = affine. You may consume this once. A scratch buffer you may or may not use, but must never free twice.

Why it exists. Section 5 already moves ownership at a boundary: @transfer moves a value out, and a @consume parameter eats its argument. But those live on the use site — a parameter, an expression. Sometimes the discipline belongs to the thing itself, wherever it travels. A connection handle should carry “use me exactly once” in its type, so that no function anywhere can forget it. That is what the type-level decorators add: the same flow-analysis, lifted from the parameter to the decl.

How you use it.

decl Transaction @must_consume { conn: *Connection }   // every Transaction MUST be consumed exactly once
decl Scratch      @consume_once { buf: [*]u8 }          // a Scratch may die unused, but never used twice

fn commit(t: Transaction @consume)   { … }              // consumes it (rung 0: the type is now spent)
fn rollback(t: Transaction @consume) { … }

fn handle(t: Transaction) {
    if ok { commit(t) }
    // ERROR: on the else path, t is never consumed — @must_consume broken
}

The check is section 5’s @transfer analysis run over the value’s whole life: reaching the end of a scope with an unconsumed @must_consume is an error, and a second use of either kind is an error. This is a rung-0 guarantee: the wrong program does not compile, so there is nothing to check at runtime.

Typestate for free. A “state machine in the type” — a file that is Open then Closed, a socket that is Unbound then Listening — is just a @must_consume type indexed by a state value (the value-params of section 10), with functions that walk it:

decl File[s: FileState] @must_consume { fd: i32 }
fn open(path: string) -> File[Open]
fn close(f: File[Open] @consume) -> File[Closed]        // you can only close an Open file, and only once

Calling close on a File[Closed] does not typecheck. No runtime flag, no “already closed” exception — the mistake is unrepresentable.

---

3. Refinements: a type that carries a promise

The term. A refinement type is a type plus a predicate its values are guaranteed to satisfy. A NonEmpty[T] is a List[T] that is additionally never empty. A Balance is an i64 that is never negative. The predicate is part of the type, so once a value has the type, the promise is already kept.

Why it exists. Two reasons. First, it deletes whole categories of runtime checks and Optionals: a function that takes a NonEmpty[T] never has to ask “what if it’s empty?”, because it cannot be. Second, it unifies with the contracts you already have — a @where on a type is a @requires/@ensures (section 14) that travels with the type instead of being pinned to one function.

The binder — and where it comes from. This is the part people get wrong, so it is worth being exact. The predicate needs to name the value it constrains. Makoto does not invent a magic variable for it (no it). It reuses the two devices section 14 already has for naming values:

• Reference-by-type (the default, no binder). Exactly like @ensures(u8 > 0), where the post-condition names the return by its type because the type is the slot:

  alias Balance         = i64   @where(i64 >= 0)
  alias Index[n: usize] = usize @where(usize < n)

• Named slot (when the base type is generic or long). Exactly like a named return -> (lo: u8) in section 14, the slot (xs: List[T]) introduces the name xs, whose type is written right there:

  alias NonEmpty[T] = (xs: List[T]) @where(xs.len > 0)

So xs is not magic and not undeclared — it is bound in (xs: List[T]), the same way lo is bound in -> (lo: u8). The simple case needs no binder at all; only the generic case pays for one.

How it discharges. The predicate is a comptime expression the checker consumes (it is not a stored function). Subtyping follows implication: T @where(P) is a subtype of T @where(Q) exactly when P ⟹ Q, so a NonEmpty[T] flows anywhere a List[T] is wanted, but not the reverse. Inside a guard the checker narrows — after if xs.len > 0 { … }, the xs in the branch has type NonEmpty[T]. And the obligation rides the ladder: decided by comptime folding it is rung 1; needing dynamic arithmetic it falls to the SMT extension (rung 2, section 7) or to a runtime check (rung 3).

fn first[T](xs: NonEmpty[T]) -> T {
    return xs[0]                        // no bounds check, no Optional: the type already proved non-empty
}

let ys: List[int] = read_input()
// first(ys)                            // ERROR: List[int] is not NonEmpty[int]
if ys.len > 0 { first(ys) }             // OK: the guard narrowed ys to NonEmpty[int] in this branch

---

4. Fences: pure and total

The terms.

• A pure function has no side effects: given the same inputs, it always returns the same output and changes nothing outside itself.
• A total function is defined on every input (never gets stuck) and always terminates (never loops forever).

Why they exist. On their own they are useful promises. But their real job is to be the fence around the dependent-type layer (section 6). A type that mentions a computed value — Vec[T, factorial(n)] — is only meaningful if factorial actually finishes computing at compile time. A “proof” that secretly loops forever proves nothing. So purity and totality are the conditions that make type-level computation and proofs sound, and the fence is where the compiler insists on them.

How you use them. They sit in the same slot as @requires/@ensures, and they are inferred by default — the compiler already knows whether your body touches an effect and whether your recursion shrinks its argument. Writing the decorator is you demanding the check (rung 0), the same way @requires declares a pre-condition:

@pure  fn area(r: f64) -> f64 { return 3.14159 * r * r }        // no IO, no allocation, no spawn
@total fn len[T](xs: List[T]) -> usize {                         // structural recursion → terminates
    match xs {
        Nil        => 0
        Cons(_, t) => 1 + len(t)
    }
}

The exhaustiveness half of totality is already free: section 14 forces match to cover every case, so a @total function cannot get stuck; the decorator only adds the termination proof (structural recursion, or a measure that provably decreases). A comptime function used in a type must be @total — that is the rule that stops a type from hanging the compiler, and the reason the dependent layer can be trusted.

---

5. Session types: a protocol the compiler walks

The term. A session type is the script of a conversation over a channel: who sends what, in what order, who gets to choose at each fork, and when it ends. A channel endpoint typed by a session is a linear typestate — you are obligated to follow the script to the end, and the compiler checks that you do.

Why it exists. Section 4 already types a channel’s payload and checks a contract at spawn. But a payload type says what can cross, not in what order — and getting the order wrong (both sides waiting to receive) is a deadlock. A protocol makes the order part of the type, so a mismatch is a compile error instead of a hung process.

No cryptic symbols. Session types come from process-calculus papers full of !, ?, &, +. Makoto uses words, and reuses constructs you already know — match for a choice, loop/continue for recursion, _ for the end:

@protocol decl Auth {                    // describes ONE endpoint (here, the client's view)
    Credentials @sends                   // I send Credentials, then…
    @receives match {                     // …a tag ARRIVES, so the PEER chooses; I must handle every arm
        Ok   => Token  @receives
        Deny => Reason @receives
    }
}

• @sends / @receives are postfix on a type (consistent with *T @consume): Token @receives means “I receive a Token here.”
• The direction on a match says who chooses the branch:
  • @receives match — the tag arrives, so the peer decides and I must handle every arm (this is an external choice: I react to what they picked).
  • @sends match — I emit the tag, so I decide which arm to drive (an internal choice).
• Recursion is loop + continue; the end of the protocol is falling out of the block (or a bare _):

@protocol decl KVServer {
    loop {
        @receives match {                 // the client picks the operation each round
            Get  => { Key @receives;  Value @sends;   continue }
            Put  => { Key @receives;  Value @receives;  Ack @sends;  continue }
            Quit => _                     // no continue → out of the loop → the session ends
        }
    }
}

The other side, for free. You write the protocol once, from one endpoint’s point of view. The other endpoint is its dual — every @sends becomes @receives and vice-versa (including @sends match @receives match). dual is a comptime type-operator (not a decorator — it produces a different type, it does not annotate one), and the spawn contract of section 4 checks that the two ends match:

let c: Channel[Auth]        // the client holds Auth
spawn server(ch)            // ch: Channel[dual Auth] — the compiler derives the mirror and checks it lines up

Mismatched ends simply do not compile, so this class of deadlock is a rung-0 guarantee.

Opt-in, even here. A plain Channel[T] is still just a typed pipe with no session obligation. Only a channel typed by a @protocol — Channel[Auth] — is walked as a session. The simple case stays simple; you summon the discipline exactly where a conversation is worth pinning down.

---

6. Dependent types: types that mention values

The term. A dependent type is a type that depends on a value. Vec[T, 3] (a vector of exactly three Ts) is a type that mentions the number 3. Eq[Nat, x, y] (a proof that x equals y) is a type that mentions two numbers. Once types can mention values, the type checker can enforce facts about values — “these two vectors have the same length”, “this index is below the bound” — at compile time.

Dependent types are not new or experimental. They are decades-old, well-understood theory (Martin-Löf in the 1970s; Coq, Agda, Lean and Idris ship them in production). By the design doc’s own ruler — the stable stays in the core, the volatile becomes an extension (section 20) — they belong in the core, opt-in by use, like @supervisor. Makoto splits them into two tiers.

6.1 The practical tier (available today)

A value-indexed type is just a struct over the value-params section 10 already has:

decl Vec[T, n: usize] { data: [n]T }                                             // a vector whose length n is in its type
fn concat[T, n: usize, m: usize](a: Vec[T, n], b: Vec[T, m]) -> Vec[T, n + m]    // the result length is n + m, checked

There is no new syntax here and no “GADT”: a decl[…] is already sugar for a comptime fn(…) -> type (section 10), so Vec[int, 3] is a compile-time call that produces a concrete struct. This tier already buys length-safety, bounds-safety, and units-of-measure (a Meters and a Seconds that cannot be added). “Non-empty” at this tier is a @where refinement (section 3), not an index.

6.2 The proof tier (five core additions, gated by @proof)

To go from “indexed data” to “proved logic”, the core gains five things — three of grammar, two of the checker — all of which only turn on under @proof:

• D1 — dependent value-param [x: A]. Today a value-param is typed by a concrete type ([n: usize]). D1 lets it be typed by an earlier type-param ([A, x: A]). It is the same […] you already write, one step more general, and it sits right next to the higher-kinded C[_] — both are just kinds of generic parameter. This is what lets a type mention a value of an arbitrary type.
• D2 — a kind on the head, -> Kind. A declaration may state what it produces: decl Vec[T, n: usize] -> type (the -> type is the default and is usually omitted), or @proof decl Eq[…] -> prop. The -> reuses “produces” (a type-former produces a Type, section 10’s -> type); : keeps meaning field-and-parameter binding and nothing else. prop is a new universe next to type: a proposition, a type whose inhabitant is a proof.
• D3 — variants with a result type (indexed families / GADTs). In a dependent decl, a variant may say which index it produces, written with the field and function-type shapes that already exist:

  @proof decl Vec[T, n: usize] -> type {
      Nil:  Vec[T, 0]                                        // the empty vector has length 0
      Cons: fn[m: usize](head: T, tail: Vec[T, m]) -> Vec[T, m + 1]   // adding one makes it m + 1
  }

  This is not a fourth kind of decl; it is the struct-field form (Name: Type) and the function-type form (fn[…](…) -> …) reread as index-refining variants once the head is dependent.
• D4 — definitional equality (a checker power, no new syntax). For any of the above to mean something, the checker must decide when two computed indices are the same type: it normalizes comptime expressions over bound value-params (not just folding literals) and compares up to computation, so Vec[T, add(n, 0)] and Vec[T, n] are one type. This is the actual kernel of dependent typing, and the one research-grade piece — made sound by the @total/@pure fences of section 4.
• D5 — dependent fields (Σ) and dependent parameters (Π). A later field may mention an earlier field’s value, and a later parameter an earlier parameter, reusing struct and parameter grammar untouched:

  decl Sized { n: usize; data: [n]int }      // a "Σ / dependent pair": data's type depends on n
  fn take(n: usize, xs: [n]int) -> [n]int    // a "Π / dependent function": xs's type depends on n

Σ and Π, plainly. A Σ (sigma) type is a pair where the second thing’s type depends on the first thing’s value — “a number n, together with a vector of that length n”. A Π (pi) type is a function whose return type depends on its argument’s value — “give me an n, I return an array of size n”. You have been writing a restricted Π every time you wrote fn zeros[N: usize]() -> [N]int; D5 just lets the dependency cross runtime parameters too.

@proof is the fence, and it draws the line between data and logic. An indexed family used as data is sound in the core with no fence at all — it is no more dangerous than any recursive type. It needs logical consistency (total, pure, strictly-positive) only when you intend to trust it as a proof. That intent is @proof, which implies @total, @pure and strict positivity. Without @proof, Vec is rich data; with it, Eq is trusted logic.

6.3 A proof is a program

Equality is not a built-in; it is an ordinary indexed family (D1–D3), and a proof of it is an ordinary recursive function. This is the Curry–Howard correspondence, stated plainly: a proposition is a type, and a proof of it is a value of that type; to prove a theorem is to write a program that has its type.

@proof decl Eq[A, x: A, y: A] -> prop {
    Refl: fn[a: A]() -> Eq[A, a, a]        // the only way to build an equality is reflexivity: a equals a
}

@proof @total fn zero_right(n: Nat) -> Eq[Nat, add(n, 0), n] {
    match n {
        Zero    => Refl                        // base case: add(0, 0) normalizes to 0 (D4), so Eq[Nat, 0, 0], and Refl fits
        Succ(k) => cong(Succ, zero_right(k))   // step: assume it holds for k, conclude it for k + 1
    }
}

Read the step case as induction, because that is exactly what it is: the induction is the match plus the recursive call, and @total is what guarantees the recursion is well-founded — which is precisely what makes the induction valid. cong (“congruence”: if a = b then f(a) = f(b)) is itself a small @proof fn in a proof-stdlib — a library value, not syntax. There is no theorem keyword and no tactic language in the core; a proof is a function, arms are =>, and that is all.

---

7. Model checking: proving things about a design

The term. Where a proof (section 6) verifies an implementation, model checking verifies a design: it explores the reachable states of a system of communicating processes and checks global, temporal properties — safety (“something bad never happens”: no two leaders at once) and liveness (“something good eventually happens”: every request is eventually answered).

Why it is an extension, not core. This is the one member of the spectrum that lives in an extension (section 20), and for the extension ruler’s exact reason: the engine is volatile. Bounded model checking, state-explosion heuristics, and bridges to external checkers (emitting P or TLA⁺ as a codegen target) change with the state of the art — unlike dependent type theory, which is stable. So model checking adds a decorator, a comptime library, a pass and a codegen target, and touches nothing in the core.

How you use it.

// safety: a plain boolean predicate, "always" is implicit
@spec(count(nodes, |n| n.role == Leader && n.term == cur) <= 1)

// liveness: a temporal formula built from library words, not □/◇ symbols
@spec(spec.always(spec.implies(submitted(req), spec.eventually(committed(req)))))

Safety reads in the vocabulary of @requires/@where. Liveness uses spec.always / spec.eventually / spec.implies / spec.leads_to, which are ordinary comptime library functions (metaprogramming is a library, section 10) rather than the □/◇ of temporal logic. A @spec anchors on a @supervisor (section 8), whose process subtree already bounds what to check; the pass reads the spawn-and-channel graph of that subtree and explores it.

(The umbrella name is @spec, covering both safety and liveness. The obvious @property is taken — it is the property-based-testing decorator of the test extension.)

---

8. Tactics: writing proofs without writing every term

The proof of a real theorem can be a large term. A tactic is a command that builds that term by transforming the current goal (the proposition left to prove, plus the hypotheses in scope): induction n splits the goal into a base case and a step case; simp closes goals that hold by computation; rewrite h uses an equation you already have. Makoto reaches tactics in tiers, and is careful about what, if anything, they cost the core.

• Tier 0 — proof-as-term (today). You write the proof directly, as zero_right in section 6.3. For reflexivity and structural proofs this is short and needs nothing new.
• Tier 1 — tactics as a library. Tactics are comptime functions over a first-class Goal (just as reflect exposes type structure, section 10): induction, simp, rewrite, and the combinators first/try/repeat, each fn(Stack) -> Result[Stack, TacticError]. Composed by hand they need no new grammar — they are ordinary Makoto.
• Tier 2 — @by (deferred). The ergonomic form is a block whose statements thread the goal:

  return @by { induction(xs); simp; rewrite(ih) }

Why @by is a decorator, not a keyword. A keyword by would reserve the identifier in every program — no one could name a variable or function by again. A decorator lives in the @-namespace, so by stays a free identifier; only @by is special. It is written prefix, like @mm(arena) { … } (section 5), because you must know a block is in tactic mode before you read its statements.

Why it is a core delta anyway (not a library). A block whose statements thread an implicit goal is new block semantics, and a library cannot add grammar or semantics (section 20). So @by is either core or a compiler extension — never a plain library. The commitment is kept minimal: @by { s1; s2; … } desugars to threading a library-defined Stack value through the statements, seeded from the expected type and short-circuiting on error. Everything else — Goal, Stack, every tactic, every combinator — is an ordinary library, so the volatile part (which tactics exist, how they compose) churns freely without touching the core.

Where it lands: self-hosting. When the compiler is written in Makoto and importable (use compiler), the AST becomes a normal library data type, and @by becomes a block-bound macro: a decorator that receives its own governed block as comptime AST and returns a value. That restriction is the safety rail — such a macro reinterprets a block it is attached to; it can never invent new top-level syntax — which is what keeps it from becoming the “decorator/DSL hell” the language rejects. Three hard problems come with that era, and are named up front so they are not discovered late:

1. Hygiene — a binding a macro introduces must never capture or collide with a user’s name.
2. AST-API stability — the reflected AST type is now a public contract; changing it breaks every macro.
3. Error attribution — an error inside expanded code must point at the user’s source, not the macro’s.

Until self-hosting, Makoto ships Tier 0 and Tier 1, with the Tier-1 library written in its final shape (Goal, Stack, induction/simp/rewrite, first/try/repeat) so that @by later simply wraps it, with no rework.

---

9. The whole spectrum on one page

Family	You write	Guarantees	Home	Rung it usually lands on
Ownership	@must_consume / @consume_once	used exactly / at most once	core (extends §5)	0
Refinement	@where(pred) on a type	a value satisfies a predicate	core	1 2 3
Fences	@pure / @total	no effects / terminates	core	0
Sessions	@protocol + @sends/@receives + dual	a protocol is followed, no deadlock	core (completes §4)	0
Dependent (practical)	value-params + @where	lengths, bounds, units	core (today)	0–1
Dependent (proof)	@proof + D1–D5	full functional correctness	core, opt-in	0
Model checking	@spec + spec.*	global safety / liveness	extension (§20)	2
Tactics	@by { … } (later)	proof ergonomics	core delta, deferred	—

The through-line: one ladder, obligations discharged as high as they will go, and nothing ever forced on code that did not summon it. The proof assistant is in the core because its theory is old and settled; the model checker is an extension because its engine is not; and no guarantee ever falls off the ladder — it degrades, in the open, to the strongest honest form that is left. 誠.