Declarations & Keywords

Sema has roughly thirty declaration keywords. That is not vocabulary for its own sake: each one replaces a piece of harness you would otherwise hand-roll — a prompt builder, a retry loop, a config loader, a policy check. This page is the contrast map: what each form declares, when to reach for it, and the smallest legal spelling of each. Every example on this page parses with sema check and runs under SEMA_STRICT=1.

The examples share one cast: a writer model, a Note struct, and friends — so you can read any row against the others.

The 30-second rule of thumb

• Plain data → struct (product) or enum (sum). The struct is the wire schema — there is no separate schema keyword.
• A behavior contract over many types → trait, conformed to with impl.
• A computation you can write → def.
• A computation you can only describe → simulate def — the model is the implementation, your contracts are the boundary.
• Math as math → equation. Pure by construction, ^ means power.
• A model actor with tools and a budget → agent.
• Deterministic orchestration of agents → circuit.
• Authority — who may do what → policy. Effects declare what code can do; policies decide what is allowed.
• Declarative infrastructure — prompts, config, DI, telemetry, events, remote interfaces — → the suite kinds (template, context, config, container, collector, event, service, …). Declare it; the runtime wires it.
• Proof it works → test, graded by assure.

Top-level forms

Every cell in the Minimal example column is verbatim-verified. Nearly every form accepts a Python-style one-line body; equation is the one exception (block body required — footnote below).

Form	Declares	Use when	Minimal example (one line)
Callable
def	A function with typed params, effect row, contracts	Any computation you can write out	def slug(title: str) -> str !{}: return title.strip().lower()
simulate def	A function whose body a model provides	You can specify it, not implement it	simulate def headline(article: str) -> str by writer: sem "A short, faithful headline"
stream def	A generator producing Stream[T] via yield	Data that must never be resident at once	stream def beats() -> Stream[int] !{}: yield 1
provide	A DI factory with a lifetime (transient, scoped(x), singleton)	Constructing a dependency for a container	provide default_note() -> Note lifetime singleton: return Note(body="")
operator	Overload of a fixed operator token for your types	Your type has a natural algebra	operator +(a: Note, b: Note) -> Note !{}: return Note(body=a.body + b.body)
operator infix	A custom string-named infix operator with a precedence class	The algebra has no built-in token	operator infix "<~>" precedence add (a: str, b: str) -> str !{}: return a + " " + b
simulate operator	An operator whose semantics a model provides	Semantic algebra — compose, remove meaning	simulate operator -(a: str, b: str) -> str by writer: sem "Remove the meaning of b from a"
equation	Pure math — ^ is power, no effects, CAS-backed	Formulas, symbolic work, argmin, proofs	equation kinetic(m: any, v: any) -> any: †
Data & types
struct	A product type; doubles as the wire schema	Records, payloads, model output shapes	struct Note: body: str
enum	A sum type with variants	Closed sets of alternatives	enum Grade: bronze | silver | gold
trait	A behavior contract (methods + optional laws)	Shared behavior over unrelated types	trait Renderer: def render(self) -> str
impl	Conformance (impl Trait for Type) or inherent methods (impl Type)	Making a type satisfy a trait	impl Renderer for Note: def render(self) -> str !{}: return self.body
Agents & orchestration
agent	A model actor: sem mission, use tools, budget	One model doing one job with bounded authority	agent triager(note: str) -> str by writer: sem "Route the note to the right queue"
circuit	Deterministic multi-agent orchestration with a shared budget	Fan-out/fan-in over agents, durable workflows	circuit fan_out(notes: list[str]) -> list[str] !{model.invoke}: return parallel [triager(n) for n in notes]
Declarative suites
policy	Named authority: allow/forbid rules over effects	Confining what code (and models) may do	policy Confined: allow clock
monitor	Distribution tracking on a function’s inputs/outputs	Keeping statistical(α) guarantees honest	monitor headline_drift on headline: capture article, result
collector	Typed telemetry channels fed by the |> tap	Metrics without logging noise	collector Metrics: latency: f32 mode series retention ring(1000)
protocol	A session-type state machine	Legal orderings of a multi-turn exchange	protocol Handshake: hello: str -> done
template	A typed prompt builder returning Prompt[T]	Reusable prompts with roles and provenance	template terse() -> Prompt[str]: role system: text "Be terse."
context	A stateful prompt state machine over slots	Multi-turn model state with auditable diffs	context Session: model writer
args	The CLI as typed data	Flags and options without argparse plumbing	args Cli: dry_run: bool = flag("--dry-run")
config	A typed config tree with ordered sources	Files/env/CLI merged with validation	config Limits: source env prefix "APP_"
container	The dependency graph: bind, expose	Wiring providers to entrypoints	container App: bind Runtime
component	An injectable object with field injection	A bundle of dependencies passed as one value	component Runtime: lifetime scoped(run)
service	A typed remote interface at a named endpoint	Cross-process calls with visible remoteness	service Scorer at endpoints.scorer: def score(text: str) -> f32
worker	An execution profile for parallel … by	Tuning lanes and batching, not logic	worker Pool: lane best_effort
event	A typed domain signal	Decoupled reactions, journaled delivery	event Spike: value: f64
subscriber	A handler for an event with a queue policy	Reacting to events off the hot path	subscriber log_spike on Spike: handle event: pass
bridge	A membrane to foreign code (python.inline, python.isolated, js.component, js.host, node.host, c.abi, cpp.abi)	Calling Python/JS/C with contracts at the edge	bridge python.inline features from "foreign/features.py": expose def word_count(text: str) -> int !{ffi.call}
model	A pinned model binding as a first-class value	Naming the model a by clause refers to	model writer = model("qwen3-4b-instruct", role=generator)
Verification
test	An executable spec run by sema assure	Every observable contract you rely on	test "slug lowercases": ensure slug("A B") == "a b"
assure	The module’s verification grade (bronze/silver/gold)	Setting how much proof this module owes — at silver the checker starts requiring things, e.g. an agent must declare budget model_calls=…	assure silver
policy attach	Module-wide policy attachment	Confining a whole module at once	policy attach Confined
Imports & constants
import	A Sema module, optionally aliased	Using another module’s public names	import std.cache as cache
from … import	Selected names, optionally aliased	You want two names, not a namespace	from std.collections import join_str
native import	A bound foreign library — never translated	NumPy-class ecosystem dependencies	native import python.isolated.json as pyjson
ported def	Foreign source translated to Sema, gated by differential tests	Small self-contained algorithms worth owning	ported def count_words(text: str) -> int from "vendor/wc.py": ensure result >= 0
(bare) NAME = expr	A module constant	Shared literals	MAX_RETRIES = 3

† equation is the only form that refuses a one-line body — the indented block is the construct:

equation kinetic(m: any, v: any) -> any:
    return 1 / 2 * m * v^2

Modifiers

Modifier	Means	Legal on
pub	Exported from the module; module-private is the default	Any top-level declaration (pub def, pub struct, pub trait, …)
mut	A rebindable local: mut best = xs[0]	Local bindings only. mut def does not parse — mutability is a property of bindings, not functions
simulate	The model is the implementation	def, stream def, operator
stream	The body is a generator; yield produces elements	def (also combined: simulate stream def)
native	Bind foreign code as-is over the C-ABI / embedded host — never translated	import
ported	Translate foreign source into Sema; the source stays the differential oracle	def … from "path", import "path" as name

Inside a function body

Contracts — four words, four different promises

def clipped(scores: list[f64], cap: f64) -> list[f64] !{}:
    require len(scores) > 0
    ensure len(result) == len(scores)
    out = [s if s < cap else cap for s in scores]
    ensure len(out) == len(scores)
    return out

struct Reading:
    celsius: f64 sem "Sensor temperature"
    invariant celsius >= -273.15

Clause	Checked	On failure	Use for
require	At the call boundary, before the body runs. Boundary-only — it cannot appear mid-body	Blames the caller; typed ContractViolation	Preconditions on inputs
ensure	In signature position, over result after the body; mid-body, a sound assertion over locals	Blames the callee; the failed value cannot flow onward	Postconditions and mid-body proofs
invariant	On a struct, at every construction boundary	Construction fails, typed	Datatype invariants that must always hold
check	Evaluated, never blocks — graded evidence carried with the value	Nothing fails; the Sim verdict feeds assure, monitors, and repair	Soft properties; check semantics("…") for NL predicates

The mnemonic: require guards the door, ensure signs the receipt, invariant lives with the data, check takes notes.

Two ensure-position forms are interpreted by the toolchain rather than evaluated as expressions. ensure semantics("…", x, alpha=…) is the calibrated semantic postcondition (hard — fails as a ContractViolation carrying the judge’s evidence). ensure total is a signature-position totality claim: for every argument satisfying the require clauses, the body terminates and yields a value of the return type. It is for exact-arithmetic kernels — arbitrary-precision int/bool/str and exact collections, an explicit !{} row, no floats, no while, no recursion — with //, %, and indexing licensed by require facts. sema check verifies the claim and module load re-verifies it, both fail-closed: an unprovable claim is a loud error, never a silent acceptance. A verified claim is statically discharged — total is not a runtime value.

def mean_floor(xs: list[int]) -> int !{}:
    require len(xs) > 0      # domain refinement — licenses // len(xs)
    ensure total             # verified claim, statically discharged
    return sum(xs) // len(xs)

def main() -> int !{}:
    return mean_floor([3, 4, 8])   # 5

Generative clauses — inside simulate def / agent

simulate def tag(note: str) -> str by writer:
    sem "A one-word topic tag for the note"
    use template terse()
    budget tokens=32, time="1s"
    repair retries=2, patch=fields
    ensure len(result) >= 1
    check semantics("tag names the dominant topic of the note")

Clause	Does
sem "…"	The behavior specification the model implements — compiled prompt material, not a comment
by <model>	Binds the site to a declared model (header position)
budget k=v, …	Hard resource bounds: tokens, time, model_calls, deadline, …
use template t(…) / use context C / use protocol P / use tools [f, g]	Attach a prompt builder, stateful context, session type, or tool set
repair retries=N, patch=fields	The decode-and-repair ladder: feed typed defects back instead of resampling blind

Robustness

def robust(x: int) -> int !{code.patch}:
    supervise quick_cycle:
        restart limit=2
        fallback 0
        heal budget=1:
            require x > 0
            rollout shadow -> canary -> full
        return x * 2
    return 0

def parsed(raw: str) -> int !{}:
    expect value = int(raw):
        return value
    except ValueError as error:
        return -1

Construct	Does
supervise <scope>:	A named recovery scope around the work; the triage ladder is language semantics
restart limit=N	Clean-state retry first — the cheapest honest recovery. window="…" is accepted and journaled but not yet enforced; sema check warns
fallback <expr>	Contract-declared degraded mode when restarts are exhausted — evaluated and journaled, its value is discarded, and execution continues after the block
heal budget=N:	Model-synthesized patch as the last rung. budget=N is enforced: at most N gauntlet attempts per scope entry (non-positive or non-integer budgets are a typed error). window=/scope= are journaled but not yet enforced — sema check warns. Gates are ordinary boolean require expressions
rollout a -> b -> c	Journal-recorded deployment stages of an accepted patch — meaningful only inside heal: (sema check warns elsewhere)
expect …: / except E as x:	Typed failure handling — consume a ContractViolation, SemanticsViolation, BudgetExceeded without a bare try
scope:	A structured nursery: every spawned child must finish inside it

lane is a worker-profile clause (worker Pool: lane best_effort in the top-level table), not supervise vocabulary. Neither lane nor enter has any semantics inside a def body — they used to be silently accepted, and sema check now flags both as unrecognized statements.

Flow

def refine(query: str) -> str !{}:
    mut state = query
    mut confidence = 0.0
    loop until confidence >= 0.9 max_iters 8:
        state = state + "."
        confidence = confidence + 0.2
    return state

def pick_pair() -> int !{}:
    solve:
        var x in range(1, 10)
        var y in range(1, 10)
        constraint x + y == 10
        constraint x < y
    return x * y

def fan_out_pair(article: str) -> list[str] !{agent.spawn}:
    scope:
        a = spawn slug(article)
        b = spawn slug(article + "!")
    return [a.join()?, b.join()?]

def vetted(feedback: str) -> str !{}:
    note = validate f"Feedback: {feedback}":
        check len(value) > 0
    return note

def metered() -> int !{model.invoke}:
    mut calls = 0
    with meter as u:
        tag("solar output rose")
        calls = u.total_calls
    return calls

Construct	Does
loop until <cond> max_iters N:	A convergence loop with an explicit bound — no unbounded agent loops
parallel [f(x) for x in xs]	Structured fan-out, fail-fast, ordered merge; variants: parallel xs map x => x * 2 by Pool ordered, unordered, limit, on_error collect
spawn f(…)	One structured child task; returns a Task[T] handle — consume with .join()?, stop with .cancel(). Needs !{agent.spawn}
solve: with var x in <domain> / constraint <expr>	Native finite-domain constraint search; solve all: enumerates into solutions
validate <expr>:	Gate a value through inline checks; the checked value is value
breakpoint when <cond>	Inert marker unless a debug session attaches — zero effect-row impact
emit Spike(value=v)	Publish a typed event to the journaled bus (effect event.emit)
yield <expr>	Produce the next stream element (only in stream def)
with meter as u: / with budget(calls=1) as b: / with policy(P):	Scoped observation, scoped hard cap, scoped authority shrink
inject T	Resolve a dependency from the active container (entrypoint decorated @App)

Suite-body directives

policy

policy Scratch:
    allow:
        fs.read("config/**")
        clock
    forbid cap:
        code.exec, proc.spawn
        net.connect except "metrics.internal:443"
    examples:
        deny:
            code.exec("rm -rf /")
        allow:
            read_config("config/app.yaml")
    justification "Scratch data must never become execution authority."
    budget model_calls <= 100

Directive	Does
allow	Grant effects, inline (allow clock) or block form with path/endpoint scopes
forbid cap:	Deny capabilities; except "…" carves out named endpoints
examples: with allow: / deny:	Executable documentation of intent — concrete calls that must (not) pass
justification "…"	The human reason, attached to every denial
budget <dim> <= <lit>	A policy-level resource ceiling

monitor

monitor tag_drift on tag:
    capture note, result
    baseline from assure
    test conformal_martingale(alpha=0.01)
    on drifted:
        alert("tag distribution drifted")
    on undecided:
        pass

Directive	Does
on <fn>	(header) which function’s call stream to watch
capture a, b, result.path	Which inputs/outputs feed the statistic
baseline from assure / baseline "calsets/…@v2"	Where the reference distribution comes from
test conformal_martingale(alpha=…)	The drift statistic and its confidence level
on drifted: / on undecided:	Deterministic reactions — emit an event, alert, degrade

bridge

bridge python.isolated title_glue:
    deps "python>=3.12,<3.13"
    expose def normalize_title(raw: str) -> str !{ffi.call}:
        sem "Normalize title whitespace"
        ensure len(result) > 0
    begin python
        def normalize_title(raw):
            return " ".join(raw.split())
    end python

Directive	Does
expose def …	The only callable surface — full Sema types, effects, contracts at the membrane
begin <lang> … end <lang>	Inline foreign source (alternative: from "path" in the header)
deps "…"	Foreign dependency pins
symbol "…"	Foreign symbol name mapping — c.abi bridges only (the runtime rejects it elsewhere)
link "…" / checksum	Prebuilt-artifact binding for c.abi, SHA-256 verified (§5.10)

container

container QuickApp:
    args QuickCli
    config QuickConfig
    bind QuickRuntime lifetime scoped(run)
    expose app_entry

Directive	Does
args A / config C	Attach the typed CLI and config tree
bind T [named "…"] [lifetime …] [= provider(…)]	One binding per (type, qualifier); ambiguity is a compile error
expose f	Which entrypoints this container serves (@QuickApp def app_entry…)

template

template quick_system(domain: str) -> Prompt[str]:
    role system:
        text f"You are a precise assistant for {domain}."

Directive	Does
role <name>:	A typed role block (system, developer, user, assistant, tool, data)
text <expr>	A line of prompt content; f-strings, if/for/match allowed around it

Common confusions

• require vs check — require is a hard gate at the call boundary: fail and the call never runs. check never blocks anything; it records graded evidence. If a violation must stop the program, it is not a check.
• ensure vs test — ensure lives in the function and guards every call at runtime. test lives outside and proves behavior at assure time. ensure is a seatbelt; test is the crash test.
• policy vs the effect row — !{fs.read} declares what a function can do; policy decides what is allowed. Rows are facts, policies are law: the same code can be legal under one policy and denied under another.
• agent vs circuit vs service — an agent is one model actor with a mission and budget. A circuit is deterministic code that orchestrates agents under a shared budget. A service is not generative at all — it is a typed interface to another process. Model work goes in agents; control flow in circuits; process boundaries behind services.
• template vs context — a template is a pure, stateless prompt builder. A context is a state machine over prompt slots with typed transitions. One render vs a conversation.
• struct vs config — both are typed records, but config adds ordered sources (files, env, CLI), provenance, and redaction. Data your program computes is a struct; data your deployment supplies is a config.
• def vs provide — provide is a def with a lifetime, registered for injection. If callers should say inject T rather than call you, you are a provide.
• monitor vs collector — a monitor answers “has this distribution shifted?” and can demote guarantees when unwatched. A collector just records typed telemetry via the |> tap. Monitors have verdicts; collectors have retention.
• event/subscriber vs calling a function — emit decouples in time and authority: delivery is queued, journaled, and policy-checked. If the reaction must happen before the next line runs, call the function.
• native import vs ported def vs bridge — native import binds a living ecosystem library; ported def translates a small algorithm into Sema (differential-tested against its source, then it is ordinary Sema); bridge is the general membrane when you author the foreign side yourself.

Next

• Cheat Sheet — the whole surface at a glance.
• Architecture & Best Practices — how these forms compose into a program.
• Construct catalog — the full specification per construct.