Verification

Makoto is a language for systems that must not fail, and the honest way to earn “must not fail” is to let the programmer state a guarantee and have the compiler discharge it. This section is the spectrum of guarantees: ownership disciplines, refinements, session protocols, effect and termination fences, dependent types and proofs, and model checking. None of it is a mode you switch the language into; each is opt-in (section 1), summoned by a decorator or a type and invisible to code that does not ask. The spine is a single idea — the discharge ladder — and everything else is one rung of it.

The discharge ladder

Every guarantee in Makoto is an obligation on a predicate, and every obligation is discharged at the highest rung that can carry it. This is section 5’s “borrow-checker you consult” generalized: the analysis is advice with teeth, and the language always tells you, in the open, where a given guarantee actually stops.

The rungs, from strongest to weakest:

• Rung 0 — type-level. The type makes the bad state unrepresentable. A @must_consume handle that is dropped is a compile error; a Vec[T, 0] has no head. Nothing to check at runtime, because the wrong program did not typecheck.
• Rung 1 — comptime fold. The predicate is decided by the compiler folding known values (Index[8] where the index is the literal 3). Rung 0’s engine, applied to values instead of shapes.
• Rung 2 — summoned discharge. An extension (SMT for arithmetic refinements, a model checker for temporal properties) proves the obligation. Opt-in behind a flag or use; see @spec below and section 20.
• Rung 3 — runtime check. The obligation could not be proved statically, so it becomes a check that traps on violation (@requires/@ensures, a refinement that survived to runtime).
• Rung 4 — advisory. The checker cannot decide and will not insert a cost; it warns (the memory analyzer’s dica/warning layers).
• Rung 5 — human. assume (section 5): you assert the predicate on your own authority, in writing, and own the consequence.

The rule that makes the ladder safe: an obligation that cannot be discharged at a rung falls to the next rung down, never off the ladder. A refinement that SMT cannot prove becomes a runtime check; a runtime check you cannot afford becomes an assume you signed. The guarantee never silently disappears; it degrades, visibly, to a weaker-but-honest form.

Ownership as a type discipline: @must_consume, @consume_once

(extends section 5; valid on the existing flow-analysis.) Section 5 already moves ownership at the boundary with @transfer (a value-position move) and @consume (a parameter that eats its argument). Two type-level decorators lift the same flow-analysis from the parameter to the type, so a resource carries its discipline wherever it goes:

decl Transaction @must_consume { conn: *Connection }   // linear: every instance MUST be consumed exactly once
decl Scratch      @consume_once { buf: [*]u8 }          // affine: consumed at most once (may simply die)

@must_consume is linearity (exactly once — dropping it without consuming is an error, so a transaction cannot be silently forgotten). @consume_once is affinity (at most once — it may go unused, but never used twice, so a freed buffer cannot be freed again). The check is the @transfer flow-analysis run over the type’s lifetime: reaching the end of a scope with an unconsumed @must_consume value is the error; a second use of either is the error. Typestate composes with this for free through the value-params of section 10 — File[Open] and File[Closed] are one @must_consume type indexed by a state, and fn close(f: File[Open] @consume) -> File[Closed] walks it. (The user docs name the theory: @must_consume is linear, @consume_once is affine.)

Refinement types: @where

(new core delta: a type may carry a predicate.) A refinement is a type plus a predicate its values satisfy. It unifies with the contracts of section 14 — a @where on a type is a @requires/@ensures that travels with the type instead of sitting on one function — and it uses section 14’s own device for naming the value. There are two forms, and the simple one carries no binder at all:

alias Balance         = i64   @where(i64 >= 0)              // reference-by-type: the value is its type, like @ensures(u8 > 0)
alias Index[n: usize] = usize @where(usize < n)             // same, with a value-param in scope

alias NonEmpty[T]     = (xs: List[T]) @where(xs.len > 0)    // named slot: (xs: List[T]) declares xs, exactly like a named return

The reference-by-type form is the default and mirrors @ensures(u8 > 0), where the post-condition names the return by its type because the type is the slot. The named-slot form is the same move as a named return -> (lo: u8) in section 14: when the base type is generic or verbose, (xs: List[T]) introduces the name xs whose type is written right there — no magic variable, no it. There is no third meaning for :; it is field-and-parameter binding as always.

The predicate is a comptime expression the checker consumes (like @requires), not a stored function value. Subtyping follows implication — T @where(P) is a subtype of T @where(Q) exactly when P ⟹ Q — and inside a guard the checker narrows: after if xs.len > 0, an xs flows at NonEmpty. Discharge rides the ladder: a refinement decided by comptime folding is rung 1; one that needs dynamic arithmetic falls to the SMT extension (rung 2) or to a runtime check (rung 3). The payoff is that bounds checks and Optional disappear where the type already proved them.

Fences: @pure, @total

(new core delta: two checker analyses.) Two decorators state promises about how a function computes, in the same slot as @requires/@ensures, checked by the compiler and invisible to code that does not read them:

• @pure — effect analysis: no @mm(alloc/free), no spawn or channel, no FFI, no IO, no external mutation, no runtime.panic. The body is a mathematical function of its inputs.
• @total — termination and totality. Section 14 already forces match to be exhaustive, so the “defined on every input” half is free; @total adds the other half, termination (structural recursion or a well-founded decreasing measure), and rejects a loop with no decreasing measure.

Both are inferred by default and demanded by the decorator: the compiler already knows whether a body touches an effect and whether a recursion is structural, so writing @pure/@total is you declaring the obligation (rung 0) for the compiler to verify, exactly as @requires declares a pre-condition. They are mandatory on any comptime function used in type position: a type like Vec[T, factorial(n)] is only sound if factorial terminates at compile time, so the fence is what stops a comptime function from hanging the compiler and, at the same time, what makes the dependent layer below sound.

Session types: @protocol, @sends, @receives, dual

(new core delta; completes section 4.) A channel connects two processes, and section 4 already checks a contract at spawn. A protocol promotes a channel’s endpoint to a linear typestate: a script of sends and receives the checker walks and forces you to complete. It is written with words, never the !/?/&/+ of process-calculus papers, and it reuses match, loop, continue and _ from the core:

@protocol decl Auth {                    // describes ONE endpoint; the peer gets the mirror automatically
    Credentials @sends                   // I send Credentials, then...
    @receives match {                     // ...I RECEIVE the tag → the PEER chooses; I handle each arm (external choice)
        Ok   => Token  @receives
        Deny => Reason @receives
    }
}

@protocol decl KVServer {
    loop {
        @receives match {                 // the client chooses the operation (external choice for the server)
            Get  => { Key @receives;  Value @sends;   continue }
            Put  => { Key @receives;  Value @receives;  Ack @sends;  continue }
            Quit => _                     // no continue → falls out of the loop → end
        }
    }
}

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

dual Auth is a comptime type-operator that produces the mirrored endpoint — every @sends becomes @receives and vice-versa, including @sends match @receives match. You write the protocol once; the other side is derived:

let c: Channel[Auth]        // the client sees Auth
spawn server(ch)            // ch: Channel[dual Auth] — the compiler generates and checks the mirror

dual is an operator and not a decorator for the reason dual produces a different type (a decorator only annotates what a thing already is; dual transforms it), the same distinction that keeps type-computation like List[T] out of the decorator space. Crucially, the discipline is opt-in inside the core: a plain Channel[T] stays an ordinary pipe with no session obligation; only a channel typed by a protocol (Channel[Auth]) is walked as a session. The simple case stays simple.

Dependent types: @proof and the practical tier

Dependent types — types that mention values — are old, stable theory (Martin-Löf, 1970s; Coq, Agda, Lean, Idris in production), and so, by the “the stable stays, the volatile becomes an extension” ruler of section 20, they belong in the core, opt-in by use like @supervisor. Makoto splits them into a practical tier that needs almost nothing new, and a proof tier gated by a fence.

The practical tier (valid today). A value-indexed type is a plain struct over the value-params section 10 already has:

decl Vec[T, n: usize] { data: [n]T }                                  // length-indexed vector; n is a comptime value-param
fn concat[T, n: usize, m: usize](a: Vec[T, n], b: Vec[T, m]) -> Vec[T, n + m]   // n + m is an Expr in type-arg position

This is not a GADT and needs no new grammar: Vec[int, 3] is a comptime call producing a concrete struct (a decl[…] is sugar for a comptime fn(…) -> type, section 10). Length-safety, bounds-safety and units-of-measure are already expressible; “non-empty” at this tier is a @where refinement, not an index.

The proof tier (five deltas, all gated by @proof). Full dependent types add, on top of the practical tier:

• D1 — dependent value-param [x: A]. A value-param may be typed by an earlier type-param of the same […], not only by a concrete type. It generalizes the existing value-param and is symmetric with the HKT C[_]; both are just forms of a generic parameter. A pure dependent value-param is sound without @proof (it is a monomorphized comptime value, like [n: usize]).
• D2 — a kind on the declaration head, via -> Kind. decl Vec[T, n: usize] -> type { … } (the -> type is the default and may be omitted); @proof decl Eq[A, x: A, y: A] -> prop { … }. The -> reuses “produces” (a type-former produces a Type or a prop, section 10’s -> type); : gains no third meaning. prop is a new universe alongside type (a proposition whose inhabitant is a proof).
• D3 — a variant with an explicit result type (indexed families / GADTs). Inside a dependent decl, a variant may declare the index it produces, written with the field and function-type forms that already exist — a nullary Name: ResultType, or a constructor Name: fn[…](…) -> ResultType:

  @proof decl Vec[T, n: usize] -> type {
      Nil:  Vec[T, 0]
      Cons: fn[m: usize](head: T, tail: Vec[T, m]) -> Vec[T, m + 1]
  }

  It is not a fourth kind of decl; it is the struct-field and function-type shapes reread as index-refining variants when the head is dependent.
• D4 — symbolic comptime normalization (definitional equality). The checker normalizes comptime expressions over bound value-params — not merely folding literals — and compares types up to computation, so Vec[T, add(n, 0)] and Vec[T, n] are the same type. This has no surface syntax; it is the kernel that makes D1–D3 mean anything, and it is the one research-grade piece, made sound by the fences.
• D5 — dependent fields (Σ) and dependent runtime parameters (Π). A later field’s type may mention an earlier field’s value, and a later parameter’s type may mention an earlier parameter, reusing the struct and parameter grammar wholesale:

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

@proof is the fence, and it implies @total, @pure and strict positivity. The distinction it draws is between data and logic: an indexed family used as data is sound in the core with no fence, exactly like any recursive type; it needs logical consistency (total, pure, strictly-positive) only when it is trusted as logic — a proposition whose inhabitant you believe. Under @proof, the compiler forces that discipline; without it, the same family is just rich data.

Equality and its proof are then an ordinary indexed family, not a primitive — they fall out of D1–D4:

@proof decl Eq[A, x: A, y: A] -> prop {
    Refl: fn[a: A]() -> Eq[A, a, a]
}

@proof @total fn zero_right(n: Nat) -> Eq[Nat, add(n, 0), n] {
    match n {
        Zero    => Refl                        // add(0, 0) normalizes to 0 (D4) ⇒ Eq[Nat, 0, 0], which Refl inhabits
        Succ(k) => cong(Succ, zero_right(k))   // the induction IS the match plus the recursion; @total makes it well-founded
    }
}

A proof is a program (Curry-Howard): a @proof @total fn that returns a proposition, built with match (arms are =>) and recursion. cong is itself a @proof fn in a small proof-stdlib — a library value, not syntax. There is no theorem keyword and no tactic language in the core.

Model checking: @spec (extension)

(extension, section 20.) Where the proof tier verifies an implementation, model checking verifies a design: global and temporal properties of a system of processes (no split-brain, eventual delivery). It is the one member of this section that is an extension, and for the section-20 reason — the engine is volatile (bounded model checking, state-explosion heuristics, a bridge that emits P or TLA⁺ as a codegen target), even though the theory it checks is stable. It adds a decorator, a comptime library, a pass and a codegen target, and changes nothing in the core.

@spec(count(nodes, |n| n.role == Leader && n.term == cur) <= 1)                       // safety: a bare predicate, "always" implicit
@spec(spec.always(spec.implies(submitted(req), spec.eventually(committed(req)))))     // liveness: a temporal formula

Safety is a plain boolean predicate in the vocabulary of @requires/@where; liveness uses spec.always/spec.eventually/spec.implies/spec.leads_to, which are comptime library words (metaprogramming is a library, section 10) rather than the □/◇ of temporal logic. A @spec anchors on a @supervisor (section 8), whose subtree already bounds the system to check; the pass extracts the transition system from the spawn-and-channel graph. (@spec is the umbrella for both safety and liveness; the name @property is unavailable — it is the property-based-testing decorator of the test extension.)

Tactics: proof-as-term now, @by later

A proof term for a real theorem can be large, and tactic scripts build it by transforming a goal. Makoto reaches this in tiers:

• Tier 0 — proof-as-term (today). With D1–D5, you write the proof directly as a total recursive function, as zero_right above. This is the floor and needs no tactics.
• Tier 1 — tactics as a library. Tactics are comptime functions over a first-class Goal (as reflect exposes type-data, 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.
• Tier 2 — @by (deferred, a core delta). The ergonomic form is a block whose statements thread the goal:

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

  @by is a decorator, not a keyword — a keyword would reserve the identifier by in every program; a decorator lives in the @-namespace and leaves by free for user names. It is prefixed like @mm(arena) { … } (the mode must be known before the block is read), and it is a genuine core delta because a goal-threading block is new block semantics — not something a library can add, since a library cannot extend grammar (section 20).

The core commitment @by needs is deliberately 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, and the whole tactic vocabulary — Goal, Stack, the tactics, the combinators — is an ordinary library. When the compiler is self-hosted and importable (use compiler), the AST is itself a 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 never invents top-level syntax — so it buys tactic ergonomics without the decorator/DSL hell the language rejects. Three problems come with that era and are named here so they are not discovered late: hygiene (a macro-introduced binding must not capture a user name), AST-API stability (the reflected AST type is a public contract), and error attribution (an error inside expanded code must point at the user’s source). Until then the language ships Tier 0 and Tier 1, with the Tier-1 library written in its final shape so that @by later wraps it with no rework.

Core, delta, extension

Feature	Form	Where	New grammar?
Ownership discipline	@must_consume / @consume_once on decl	core (extends section 5)	no — decorator
Refinement	@where on a type	core	small — a type carries a predicate
Session types	@protocol decl + @sends/@receives + dual	core (completes section 4)	yes — protocol body, dual
Fences	@pure / @total	core	no — checker analyses
Dependent, practical	value-params + @where	core	no — valid today
Dependent, proof	@proof + D1–D5	core, opt-in by use	yes — D1–D3 grammar, D4–D5 semantics
Model checking	@spec + spec.* + pass + P/TLA⁺	extension (section 20)	no — engine is volatile
Tactics @by	goal-threading block decorator	core delta, deferred to self-hosting	yes — when summoned

The mental model. A guarantee is an obligation on a predicate, and the compiler discharges it as high as it will go — unrepresentable if it can, proven if it must, checked if it cannot be proven, and, at the last, signed by you. Ownership, refinements, sessions, fences and dependent types are rungs of that one ladder, each summoned by a decorator or a type and each invisible until you reach for it. The proof assistant lives in the core because its theory is decades old; the model checker lives in an extension because its engine is not; and no obligation ever falls off the ladder — it only degrades, in the open, to the strongest honest form left. 誠.