# Toolchain > A complete reference to the sema command — check, run, assure, doc, repl, parse, and the package and editor commands — with an example invocation for each. The `sema` command is the whole toolchain: static checking, execution, verification, documentation, inspection, package management, and editor integration. This page is a reference to every command, with an example invocation for each. Running `sema` with no arguments prints the command list: ``` usage: sema ``` Most commands take a **project directory** (the folder containing `src/`). `check` also accepts individual files. ## Summary | Command | What it does | |---|---| | `sema check ` | Static checks: parse, arity, struct fields, effect discipline, unrecognized-directive and policy-example warnings. Run after every edit. | | `sema run ` | Execute `main()`. `SEMA_STRICT=1` fails hard on degradations; `SEMA_VM=1` runs the bytecode VM. | | `sema circuit ` | Durable runs: `run` executes like `sema run`; the rest manage recorded runs under `.sema/runs/`. | | `sema debug ` | Localhost token-protected run-inspector web UI; `replay` verifies determinism against a recorded run. | | `sema assure [--grade bronze\|silver\|gold]` | The verification engine: runs `test` blocks, fuzzes `ensure` properties for counterexamples, and (at `gold`) mutation-tests. | | `sema doc [--out DIR] [--html] [--skills]` | Reflected documentation from signatures + docstrings. | | `sema repl [project]` | Interactive console. | | `sema parse [--ast]` | Parse and inspect the parse tree. | | `sema tokens ` | Dump the lexer's token stream. | | `sema infer …` | Run a real local model (requires the `real-model` build). | | `sema add / remove / list` | Package management (PyPI and native Sema packages). | | `sema lsp` / `sema dap` | The language server and debug adapter for editors. | :::note[Tests and formatting] There is no separate `sema test` command — **authored tests run through `sema assure`**, which executes every `test "…":` block as part of the verification engine (see below). Source formatting (`sema fmt`) is planned but not yet a standalone command; use `sema parse --ast` to inspect structure in the meantime. ::: ## `sema check` — static checks The fast, run-after-every-edit command. It parses the project and runs the static checks: parse errors, function arity, struct fields, the effect-row discipline, **unrecognized-directive warnings** (the guard against silent no-ops — a directive in a `def` body that no runtime handler recognizes is flagged, so a typo or a misplaced clause surfaces here rather than doing nothing at runtime), and **policy-example verification** (a policy whose declared `examples:` contradict its rules is an error). It does not execute your program. ```bash sema check myproject sema check src/main.sema src/domain.sema # or individual files ``` A clean run reports no diagnostics. ## `sema run` — execute Runs the project's `main()` on the tree-walking interpreter, the reference semantics. ```bash sema run myproject ``` Two environment variables change its behavior: - **`SEMA_STRICT=1`** turns recoverable degradations into hard, typed errors. Off, the runtime self-heals a mis-estimate or a failed step, logs it to the journal and to stderr (`[sema:warn] …`), and keeps going. On, each such degradation aborts loudly — use it when verifying, in tests, and in CI. ```bash SEMA_STRICT=1 sema run myproject ``` - **`SEMA_VM=1`** runs compilable function bodies on the opt-in **bytecode VM** instead of the tree-walker. The VM compiles a function only if every construct in its body is supported and otherwise falls back transparently to the tree-walker, and every value operation delegates to the same runtime helpers — so results are identical; it is a performance path, not a different language. ```bash SEMA_VM=1 sema run myproject ``` ## `sema assure` — verification The verification engine. Verification is default-on in Sema — there is no opt-in `testable` keyword — and `assure` is where the grades run. It executes three things, gated by grade: - **Tests.** Every `test "name":` block runs; a block that finishes without a contract violation or error passes. - **Properties.** Every function with an `ensure` postcondition is *fuzzed* — inputs are generated from the parameter types and the function is called many times; a violated `ensure` is reported with a concrete counterexample. - **Mutation adequacy** (grade `gold`). The program is systematically mutated and the tests and properties are re-run against each mutant; a mutant that still passes exposes a gap. The killed/total score is gated at ≥50% for a green verdict. Grades set the depth, selected with `--grade` (default `silver`): - **bronze** — tests must pass. - **silver** — tests plus fuzzed properties; requires explicit effect rows. - **gold** — adds the mutation-adequacy threshold. ```bash sema assure myproject --grade silver sema assure myproject --grade gold ``` The exit code reflects the verdict, so `assure` slots straight into CI. Output lists tests passed, properties held (with any falsifying counterexample), and, at `gold`, the mutation score. ## `sema doc` — reflected documentation Generates Markdown documentation by **reflecting over the program** and merging in the docstrings you write inline. A docstring is a triple-quoted string as the first statement of a module, `def`, `struct`, or `enum` — no per-line marker. Reflection contributes the always-accurate part (signatures, typed parameters, return types, effect rows, decorators, struct fields with their `sem` descriptors, enum variants); your docstring prose contributes Markdown, LaTeX (`$…$`), and `sema` code examples. ```bash sema doc myproject # print reflected Markdown sema doc myproject --out docs/ # write to a directory sema doc myproject --html # also render a self-contained HTML page sema doc myproject --skills # emit with skill frontmatter (loadable as model context) ``` `--html` produces a standalone page (rendered Markdown + KaTeX, no build step). `--skills` writes each module's doc with skill frontmatter, so generated docs load as model context via `skills.load` — code that documents itself to humans *and* to the models that read it. ## `sema repl` — interactive console An interactive session for evaluating expressions and inspecting definitions. Passing a project directory loads its modules first. ```bash sema repl # a bare session sema repl myproject # with the project's definitions in scope ``` ## `sema parse` and `sema tokens` — inspection Low-level tools for understanding how Sema reads your source. `sema parse --ast` prints the parse tree; without `--ast` it reports parse success or errors. `sema tokens` dumps the lexer's token stream. ```bash sema parse src/main.sema --ast sema tokens src/main.sema ``` ## `sema infer` — real model inference Runs a real local model directly (GGUF generation on GPU/CPU). It requires the `real-model` build (`cargo build --release --features real-model`); a default build prints how to enable it. ```bash sema infer --gguf model.gguf --tokenizer tokenizer.json --prompt "Hello" --max 64 ``` ## Package commands `sema add` installs both PyPI packages (into `.sema/venv`) and native Sema packages (from a path or `git+`), `sema remove` uninstalls, and `sema list` shows what is installed. See [Project Layout](/start/project-layout/) for details. ```bash sema add numpy sema add ./greetings sema list sema remove numpy ``` ## Editor integration - **`sema lsp`** runs the language server (LSP) that editors talk to for diagnostics, hovers, and completion. - **`sema dap`** runs the debug adapter over stdio, so any DAP-speaking editor can drive a Sema debug session. ```bash sema lsp sema dap ``` ## The verification loop For everyday work the loop is **edit → `sema check` → `SEMA_STRICT=1 sema run` → `sema assure`**. `check` catches static mistakes in milliseconds, strict `run` proves the program does not quietly degrade, and `assure` grades the contracts and properties. ## Next - [Verification](/neurosymbolic/verification/) — the full model behind `assure`: contracts, properties, mutation adequacy, and the guarantee lattice. - [CLI reference](/reference/cli/) — the generated, exhaustive command reference.