---
name: sema-language
description: "Use when reading, writing, reviewing, or running Sema code (.sema files) or working on the Sema compiler/toolchain under sema/. Sema is Cortex's AI-native, neurosymbolic programming language (Rust reference implementation, Python-shaped syntax). Covers the toolchain (sema check/run/assure/doc/circuit/debug/repl + cargo for the compiler), the core + neurosymbolic constructs, durable circuits and the run debugger, the no-silent-mock model contract, the equation/scientific surface, the mandatory edit→check→assure workflow, and the no-silent-no-ops ethos. Trigger phrases: sema, .sema file, sema check, sema assure, sema circuit, sema debug, simulate def, semantic.*, policy, loop until, with meter, equation, deterministic engine, neurosymbolic, write this in Sema, the language, LANGUAGE.md."
---

# Sema Language

Sema is Cortex's **AI-native, neurosymbolic programming language** — a first-class
Cortex language on par with Python and TypeScript. It has a real Rust reference
implementation (interpreter + opt-in bytecode VM) in the `sema/` submodule. Syntax
is Python-shaped (indentation, `def`, `struct`), but the semantics are new: models,
contracts, effects, and semantics are language constructs, not library calls.

Treat this skill as the operational guide. The **normative reference** is
`sema/docs/LANGUAGE.md` (sections are cited as §N below; the newest-first D-numbered
decision log is at its end). Runtime design is `sema/docs/RUNTIME.md`; the scientific
release matrix is `sema/docs/SCIENTIFIC-COMPUTING.md`; debugging is
`sema/docs/DEBUGGING.md`; the release contract is `sema/docs/PRODUCTION-READINESS.md`.

## Where things live

- `sema/crates/` — the compiler/runtime (Rust). `sema-core` (lexer/parser/AST),
  `sema-runtime` (tree-walker + VM + prelude + stdlib injection + `check`),
  `sema-cli`, `sema-lsp`, `sema-math` (equations/CAS/SMT), `sema-model` (candle
  backends, `--features real-model`), `sema-py`/`sema-node` (bindings).
- `sema/stdlib/sema/*.sema` — the **standard library written in Sema**, embedded in
  the compiler, importable as `from std.<module> import …`: `agent_loop`, `agents`,
  `belief`, `cache`, `circuits`, `collections`, `completion`, `document`,
  `provenance`, `usage`, `web`.
- `sema/examples/<project>/src/*.sema` — the worked corpus (each is a runnable project).
- `sema/grammar/` — `sema.ebnf` (must stay in sync with LANGUAGE.md §6, checked by
  `grammar/check-drift.sh`) and `tree-sitter-sema/`.
- `sema/impl/` — the machine-validated truth ledgers: `STATUS.md` (dated milestone
  log), `conformance.json`, `scientific-conformance.json`, `advertised-profile-*.json`
  (validators: `scripts/validate_conformance.py`, `scripts/validate_scientific_conformance.py`).
- `sema/debug-ui/` — the TypeScript debugger web UI served by `sema debug`.
- `sema/docs-site/` — the doc website; `npm run generate` regenerates the reference
  mirror from LANGUAGE.md + the reflected APIs and publishes this skill.

## The toolchain (this is how you verify Sema)

A Sema **project** is a directory with `sema.toml` + `src/*.sema` (entry: `main.sema`'s
`main()`). Run from `sema/` (the CLI is `./target/release/sema` after a build). The
real subcommands are `tokens parse check run circuit debug infer doc assure repl dap
add remove list lsp` (there is **no** `fmt` and **no** `test` subcommand):

- `sema run <project> [--posture <id>] [--policy-snapshot <f>] [--policy-endpoint <s>]`
  — execute `main()`. `SEMA_STRICT=1` turns recoverable degradations into hard
  errors — use it when verifying. `SEMA_VM=1` opts into the bytecode VM.
- `sema check <project | files...>` — static checks: parse, arity, struct fields,
  effect-row discipline, **unrecognized-directive warnings** (the silent-no-op
  guard, §3.6), and **policy-example verification** (§5.8 — a contradictory
  `examples:` block fails check with the same message `run` fails with at load).
  Run this after every `.sema` edit; warnings alone exit 0 but fix them anyway.
- `sema assure <project> [--grade bronze|silver|gold]` — the verification engine
  (§5.7); default `silver`. Runs the `test "…":` blocks, fuzzes `ensure` properties
  (counterexamples), and at `gold` mutation-tests. `silver`+ requires explicit
  effect rows. (Tests run inside `assure`; there is no separate `sema test`.)
- `sema circuit run|resume|list|show|cancel` — durable circuits (§5.54): `run`
  executes like `sema run`; the others manage recorded runs under
  `<project>/.sema/runs/<run-id>/` (resume continues from the durable journal).
- `sema debug serve <run-dir|project> [--latest] [--port N]` / `sema debug run
  <project> [--port N]` / `sema debug replay <project> --against <run-dir>` — the
  localhost token-protected run inspector (typed `sema.observation/v1` graph +
  timeline over the chained journal; DEBUGGING.md). `replay` verifies determinism
  against a recorded run (exit 0 match / 1 diverge).
- `sema doc <project> [--out DIR] [--html] [--skills]` — reflected documentation
  (docstrings + signatures), default out `<project>/docs/api`. Drives the docs site.
- `sema parse <files...> [--ast]` / `sema tokens <files...> [--quiet]` — inspect the
  parse tree / token stream of **files** (not a project dir).
- `sema infer --gguf <path> --tokenizer <path> [--prompt S] [--max N] [--temp T]`
  — real local GGUF text generation (requires a `--features real-model` build; it
  is **not** a type-inference command).
- `sema add <pkg==ver | local-path>` / `sema remove` / `sema list` — the package
  manager (§5.45/§5.46). `sema repl [project]` — interactive console (`:doc NAME`,
  `:trace`); `sema dap` / `sema lsp` — debug-adapter / language-server entry points.

**Compiler work (editing `sema/crates/` or `sema/grammar/`)** is verified with the
Rust toolchain, not the Sema CLI:

- `cargo build -q` (expect **0 warnings**) and `cargo build -q --features real-model`.
- `cargo test -q` (all suites green; never accept `0 passed; … filtered out` as evidence).
- `./grammar/check-drift.sh` (grammar EBNF ↔ LANGUAGE.md §6 must stay in sync).
- `python3 scripts/validate_conformance.py` + `…_scientific_conformance.py` after any
  ledger/anchor-relevant change (anchors are content markers — renaming a test
  invalidates its anchor).
- After adding a language keyword: update the lexer/parser, `exec_stmt`/dispatch,
  the typechecker + `assure` walkers, the tree-sitter grammar, the LSP keyword list,
  and the VS Code extension (`sema/editors/vscode`).

## The model contract (no silent mocks — 2026-07-13)

Model-backed operations (`generate`/`chat`/streams, agent tool-loops, `code.gen`,
heal suggestions, `simulate def`, semantic judging incl. `judge=`) resolve through a
`@provides(...)` provider, a configured real model (`sema.toml [models]` +
`--features real-model`), or fail **loud with a typed error** —
`ModelUnavailable` / `SimulationUnavailable` / `SemanticJudgeUnavailable` (multimodal
compose: `SttError`/`VisionError`). The built-in **deterministic engine** runs ONLY
under an explicit opt-in: `[engine] deterministic = true` in `sema.toml` or
`SEMA_DETERMINISTIC=1` — an intentional hermetic "mock run" for tests, **never** a
fallback for a configured-but-failed backend. The built-in hash embedder remains a
real (grounded, deterministic) unconfigured default for embeddings (D61).

Env vars the runtime honors (all fail-closed on bad values): `SEMA_STRICT`,
`SEMA_VM`, `SEMA_DETERMINISTIC`, `SEMA_DEBUG_SOURCE` (opt-in immutable source
capture), `SEMA_HEAL_LIVE` (heal apply authority), `SEMA_NODE`/`SEMA_PYTHON` (bridge
binaries), `SEMA_LEAN_BINARY`+`SEMA_LEAN_SHA256`, `SEMA_Z3`; governance:
`SEMA_POSTURE`/`SEMA_POLICY_SNAPSHOT`/`SEMA_POLICY_ENDPOINT`; CLI styling:
`NO_COLOR`/`SEMA_NO_COLOR` > `SEMA_FORCE_STYLE=1` > TTY detection.

## Cortex governance (posture-gated runs)

In a Cortex runtime, `sema run` is **policy-governed**: the harness seeds a sealed,
program-immutable root policy before `main()` runs, so a program can only *shrink*
authority, never widen past the Cortex posture. Design + acceptance:
`agent-harness/sema-governance-integration.md` and `agent-harness/acceptance-tests.md`
→ "Sema Governance Validation".

- **Flags / env.** `sema run <proj> --posture <id> [--policy-snapshot <file>]
  [--policy-endpoint <sock>]`, or the launcher-set env vars above. Unset ⇒ ungoverned
  (unchanged dev behavior). Implementation:
  `sema/crates/sema-runtime/src/governor.rs` + `sandbox.rs`.
- **Built-in postures.** `sema-sandbox` (least authority — pure compute + workspace
  `fs.read`; no net/exec/ffi/write) is the default; `sema-agent` (workspace fs r/w +
  db, approval-gated net/ffi/model, no raw exec); `admin` (unrestricted, but the
  danger floor + command denylist still apply). These mirror the `sema.effect.*`
  capabilities + postures in `control/plane/src/server/services/policies.ts`.
- **What a governed run enforces.** Each effect is checked against the posture's
  allow-set (`Denied: policy cortex:<posture> denies effect <e> …`), plus: `!{*}`
  refused under any restricting posture; `net.connect` endpoint scoping;
  approval-required effects fail closed when headless; a posture command denylist on
  `proc`/`code.exec`; a bounded taint watermark (model/net/ffi output can't reach an
  exec sink); and, when exec *is* granted, an OS sandbox (macOS `sandbox-exec` /
  Linux `bwrap`) confines the child. Missing/stale snapshot ⇒ deny-all.
- **A `Denied` under governance is expected, not a bug.** Do **not** route around it by
  widening the program's own `policy`/effect row — you cannot widen past the sealed
  root. Use a more capable operator-assigned posture, or narrow the code's effects.
- **Verify governance** with `make sema-govern-audit` (runtime gauntlet
  `sema/crates/sema-cli/tests/governance.rs` + control-plane `test/sema-policy.test.mjs`
  + `tests/test_sema_govern.py`); it is wired into `make agentic-security-test`.

## Writing Sema — the constructs you will use

Core (Python-shaped): `def f(x: T) -> R !{effects}:`, `mut`, `struct`, `enum`,
`trait`/`impl`, `match`/`case`, `for`/`while`, `with`, `expect`/`except`, lambdas
(`lambda x: e` / `x => e`), generics `[T]`, `list`/`dict`/`tuple`, and
Python-shaped strings (§5.13/D126): `"…"`/`'…'` interchangeable, Python escape
set (`\xHH`/`\uXXXX`/`\UXXXXXXXX`, unknown escapes are loud errors), raw
`r"…"`, f/`rf`/`fr` templates with `{expr:spec}` interpolation, raw `re"…"`
regex literals (`\d+` needs no double escaping), typed `sql"…"` templates, and
always-raw triple-quoted bodies (intentional Python divergence — docstrings
and prompts keep backslashes verbatim).
**No classes/inheritance** — traits + ADTs only.

Neurosymbolic + governance (what makes Sema Sema):

- **Effects** `!{fs.read, model.invoke, net.connect}` — typed capability rows on
  every function; the deterministic core is `!{}` (§3.6). The row vocabulary is
  **open**: declare custom capabilities (`!{mysql.query}`) as markers on wrapper
  modules — the checker enforces caller containment and policies allow/forbid
  them by path (§3.6 "Custom capabilities"; full built-in catalog: docs-site
  `/reference/effects-catalog/`). Calling an unknown op on a known namespace
  errors; `sema check` flags near-miss typos of built-in namespaces/ops
  (`fss.read`, `fs.raed`) while genuinely distinct custom names pass.
- **`simulate def … by <model>:`** — a model implements the body; `sem "…"`
  descriptors (triple-quoted for multi-line), `budget tokens=…, time=…`,
  `ensure`/`check semantics(…)` contracts, `use template/context/protocol` (§5.5).
- **Semantic verbs** `semantic.filter/rank/map/classify/extract/summarize/`
  `translate/cluster/dedup/…` and the `~=` calibrated-similarity operator (§5.30/§5.1).
- **Contracts** `require`/`ensure`/`invariant` (hard, raise `ContractViolation`) and
  `check` / `check semantics(…, alpha=…)` (soft, monitored) (§5.4). Two ensure
  forms are INTERPRETED, not evaluated: `ensure semantics(...)` and
  `ensure total` (D129).
- **Certified totality** — `ensure total` in the signature preamble claims
  "terminates + yields a value on every input satisfying the `require`
  clauses" (§3.6). Verified by `sema check` AND at load, fail-closed (bad
  claim = load error; REPL/live-patch claims = typed error; a hot-swap drops
  the module's verified status). v1 fragment = EXACT arithmetic only:
  exact-typed signatures (`int`/`bool`/`str`/exact collections; NO floats),
  explicit `!{}`, no `while`, no recursion, finite iterables, `/` never;
  `//`/`%`/`**`/indexing discharge against `require` facts over
  never-reassigned names (`require len(xs) > 0` licenses `// len(xs)`).
  Callees: sibling total defs, exact-fragment equations (no CAS), whitelist
  (`len/abs/range/sum/bool/str/repr`, 2-arg `min`/`max`). `sema doc` renders
  a **Total** badge only after re-verification.
- **`policy`** — capability governance with `allow:`/`forbid:`/`examples:` +
  justification; examples are verified by `sema check` AND at load (§5.8);
  `@Policy` decorators and `with policy(...)` scopes compose by lattice meet.
- **`agent` / `circuit`** — native agents and durable circuits (§5.54): derived
  authority, memoized `WorkTree` work, isolated parallel fan-out/merge, durable
  runs under `.sema/runs/` (resume/inspect via `sema circuit` + `sema debug`).
- **`supervise`/`heal`** (§5.11) — restart-first robustness: `restart limit=N`
  (enforced; `window=` recorded-only, check-warned), `heal budget=N:` (enforced,
  fail-closed) with real `require` gate predicates journaled per attempt,
  `rollout a -> b -> c` (journal-recorded stages, only meaningful inside
  `heal:`), then `fallback <expr>` (value journaled + discarded — the scope
  recovers). Patch application is governed by `[heal] apply` / `SEMA_HEAL_LIVE`
  (staged default / live hot-swap / persistent ledger). `lane`/`enter` are NOT
  supervise clauses (check flags them; `lane` belongs to `worker` profiles).
  Breakpoints fire inside supervise bodies every attempt; config-clause lines
  and heal bodies are honestly unverifiable.
- **Equations** — `equation name(...):` native mathematical formalism (§5.28,
  §5.31–§5.32): exact `QQ`/BigInt, symbolic CAS (`cancel`/`integrate`/`limit`/
  `series`), dense/sparse/complex linalg (`svd`/`solve`/`lstsq`/`pinv`/`cond`),
  statistics/Normal, number theory, interpolation, tensors (f64/bool/complex),
  `solve` constraint solving (§5.51), Z3-backed SMT, bounded Lean adapter. Status
  per public spelling lives in the scientific ledger — most rows are *partial*;
  check `sema/docs/SCIENTIFIC-COMPUTING.md` before claiming coverage.
- **`loop … until <cond> [max_iters N]:`** — bounded do-until agent loop (in §5.29,
  Ergonomics); the functional form is `std.agent_loop.loop_until`.
- **`with meter as u:` / `with budget(tokens=…, calls=…) as b:`** — ambient usage
  metering + hard spend caps (§3.6); no `(result, usage)` tuples.
- **`monitor`** (conformal-martingale drift + `on drifted:`, §5.9), **`protocol`**
  (session-type transitions, §5.12), **`collector`**/`|>` tap (retention + export,
  §5.16), **`trace`** (self-repair packets, §5.48), **`test`/`assure`**
  (verification, §5.7).
- **Decorators** — any function is a decorator (`@name`); `call(fn, args)` proceeds
  (§5.53). **Capability providers** `@provides("embed"|"generate"|"db"|…)` swap a
  backend in Sema (§5.52). `@inject(...)` native DI (D82).
- **Native modules** (import explicitly, §5.35): `math`, `lean`, `io`, `http`
  (`http.serve(port, handler, host?)`, §5.34), `latex` (`latex.render` /
  `latex.of` — console math rendering), plus `python`/`js`/`c.abi` bridges (§5.10).
- **Standard library**: `from std.belief import Belief`, `from std.cache import
  memoize`, `from std.document import Report, render`, `from std.agent_loop import
  loop_until`, `from std.web import router, get, serve`, `std.agents`,
  `std.circuits`, `std.completion`, `std.usage`, `std.provenance`, `std.collections`.

## Structuring a Sema project (quick-reference pages: docs-site `/quick/*`)

The docs site ships three orientation pages — `/quick/cheat-sheet/` (one-page
syntax + toolchain), `/quick/declarations/` (every top-level form and body
keyword contrasted: when to use `def` vs `simulate def` vs `provide`, `struct`
vs `config`, `agent` vs `circuit` vs `service`, `require` vs `ensure` vs
`check`, …), and `/quick/architecture/` (best practices). The load-bearing
rules:

- **Layout**: `sema.toml` + `src/` (module id = file stem, globally unique;
  discovery is recursive) + sibling `tests/` (discovered ONLY by
  `check`/`assure`, never plain `run`) + generated `docs/api` + `.sema/`
  runtime state (never committed).
- **One concern per module**: domain types (+`sem`+invariants) in
  `domain.sema`; policies with their helper defs and tests in `policies.sema`;
  effectful adapters (`storage.sema`, `ingest.sema`) at the edges; a thin
  `main.sema`. Naming: modules snake_case, types/traits/policies/agents
  PascalCase, functions/fields snake_case, test names are sentences.
- **Effect discipline is the architecture**: keep the core `!{}`-pure, push
  effects to edge modules, declare rows explicitly (silver+ requires it), and
  treat `!{*}` as a spike-only escape hatch.
- **Contracts placement**: `require` at public boundaries, `invariant` on
  domain structs, `ensure` on results, soft `check semantics(…)` at model
  boundaries; unit `test "…":` blocks next to the unit, cross-module and
  fuzz-facing properties in `assurance.sema`/`tests/`.
- **Model work**: every `simulate def` carries `sem` + `budget` + `ensure`;
  prompts live in `template`/`context` suites (triple-quoted raw bodies), not
  inline strings; SQL goes through typed `sql"…"` templates.

## Mandatory workflow

1. **Before writing**, skim the relevant `sema/docs/LANGUAGE.md` § and a matching
   `sema/examples/*` project — the syntax is new; do not guess it.
2. **Edit** `.sema` files. Prefer the stdlib and the neurosymbolic constructs over
   hand-rolled loops (e.g. `semantic.dedup`, `loop until`, `with meter`).
3. **`sema check <project>`** — must be clean (fix every warning; an unrecognized
   directive means a typo/misplaced clause that does nothing at runtime).
4. **`SEMA_STRICT=1 sema run <project>`** and **`sema assure <project> --grade silver`**.
5. For **compiler** changes: `cargo build -q` (0 warnings), `cargo test -q` (green),
   `./grammar/check-drift.sh`, the ledger validators, and update `impl/STATUS.md`.
6. For **LANGUAGE.md** changes: prove every new snippet in a scratch project
   (`sema check` + `SEMA_STRICT=1 sema run`), keep §6 in sync with the EBNF, and
   re-run `cd docs-site && npm run generate`.

## Ethos (enforced by the sema-quality rule)

- **No silent no-ops.** Syntax that parses must have an effect or fail loudly. If a
  construct can't be implemented, make it error or document it — never let it
  silently do nothing. `sema check` flags unrecognized directives for this reason.
- **Never fake.** Don't stub a feature to look done. An absent/failed model backend
  fails typed — deterministic output only by explicit opt-in. Real models run via
  `--features real-model` (download outside the sandbox with the sandbox disabled).
- **Keep it compact + honest.** Use the new constructs to shrink code; state what is
  verified vs partial (the ledgers in `sema/impl/` are the truth, not prose). Update
  `impl/STATUS.md` and the LANGUAGE decision log (D-numbers) for language changes;
  keep the grammar and tree-sitter/LSP/VS-Code surfaces in sync.