verum — Command-line interface

The verum binary is self-contained: compiler, interpreter, linker, package manager, LSP server, and formatter in one executable. It exposes the following subcommands.

Project lifecycle

verum new <name>                     # create a new project
verum init [path]                    # initialise an existing directory
verum deps add <pkg> [--version X] [--dev] [--build]
verum deps remove <pkg> [--dev] [--build]
verum deps update [<pkg>]
verum deps list [--tree]

Build, run, test

verum build [--release] [--target TRIPLE] [--lto thin|full] [--timings]
verum run [--interp | --aot] [-- args...]
verum check [PATH] [--workspace] [--parse-only]
verum test  [--filter STR] [--exact] [--skip PAT] [--include-ignored] \
            [--ignored] [--list] [--interp | --aot] \
            [--format pretty|terse|json|junit|tap|sarif] \
            [--test-threads N] [--nocapture] [--coverage]
verum bench [--filter STR] [--interp | --aot] \
            [--warm-up-time SECS] [--measurement-time SECS] \
            [--min-samples N] [--max-samples N] [--sample-size N] \
            [--save-baseline NAME | --baseline NAME] \
            [--noise-threshold PCT] [--format table|json|csv|markdown]
verum watch [<command>] [--clear]

verum run is interpreter-first. Add --aot for LLVM native execution when latency matters (LLVM warmup adds ~200 ms).

Script invocation

Verum has a third execution mode reserved for single-file scripts with a #! shebang line. Bare verum file.vr (no run subcommand) and ./file.vr direct exec both route into script mode, where top-level statements are accepted without an enclosing fn main():

$ cat hello.vr
#!/usr/bin/env verum
print("hello");
$ ./hello.vr        # OS-level shebang exec (chmod +x first)
$ verum hello.vr    # bare invocation, no `run`

A .vr file lacking the shebang must use the explicit verum run form — the bare shorthand surfaces an actionable advisory that points back at verum run. Full contract, exit-code propagation, and roadmap live in Getting Started → Script mode.

Permission flags

verum run and the bare script invocation accept three permission CLI flags that augment frontmatter declarations:

verum --allow=<scope>[=<target>]   # add a single grant
verum --allow-all                   # universal grant set
verum --deny-all                    # empty grant set (drops every grant)

--allow is repeatable: --allow=net=api.example.com:443 --allow=fs:read=./data installs both. --allow-all and --deny-all are mutually exclusive and override repeated --allow flags.

Either flag installs a permission policy even if the script's frontmatter is silent — opt-in to sandboxing without editing the source. The resolved policy mixes into the script's VBC and AOT cache keys, so two runs with different policies never share a cached binary. The interpreter and AOT-compiled binary enforce the resolved policy identically: every gated FFI call (open, connect, socket, _exit, …) lands in the same (scope, target_id) decision table whether the script is running under Tier 0 or as a native executable. Full mechanism, diagnostics, exit-code contract (143 = capability denied, 1 = logic), and the wire-format scope-tag mapping live in Getting Started → Script mode → Sandboxing scripts with permissions.

verum test and verum bench form the developer-facing testing surface — property-based testing with integrated shrinking, parametrised tests, deterministic seed replay, CI output formats (JUnit / TAP / SARIF), and Criterion-style time-budget benchmarks. Full guide in Tooling → Testing; PBT deep dive in Tooling → Property testing.

Architecture queries & tier identity

verum arch query --at FILE [--json]   # what may this code do?
verum diff-tiers FILE [--json]        # do both tiers agree about it?

verum arch query answers the machine-facing question of ATS-V-2's inference-first discipline: the module's inferred capability surface (row-solved and transitive — a helper's Network reaches the module surface through the call graph, and mounted callees resolve across module boundaries), the @arch_module pin if one is declared, and the two-direction judgment between them — escalations (code exceeds the pin) and dead rights (pinned, never exercised). Per-function summaries carry their open row variables (named capability-bearing parameters), and unresolved local calls are surfaced, never guessed. --json emits the append-only machine schema that coding agents consume in the ask → patch → diff cycle; every atom carries its provenance (computed, or the citation source for extern pins and protocol @max_shape declarations).

verum diff-tiers is the tier-identity judge: it runs the same program under Tier 0 (interpreter) and Tier 1 (AOT) as isolated subprocesses, compares program output and exit codes, and refuses to call different answers anything but a defect — verdict identical or DIVERGENT with the first diverging output line, exit code 3 on divergence so CI fails by default. One bytecode with two executions is the language's core promise; this command makes the promise continuously checkable rather than point-fixed.

Binary shape manifests

verum inspect BINARY [--json]         # what does this binary claim to do?

Every AOT binary embeds a shape manifest: a magic-tagged JSON block carrying the schema version, the building toolchain, and the program's capability surface (pinned and inferred) as the compiler judged it. verum inspect reads it back without the compiler — from any Verum binary, anywhere — so a deployed artifact can answer "what may you do?" years after its build. A non-Verum binary is refused with a diagnosis (exit 1), never guessed at.

Notebook replay

verum playbook --replay BOOK.vrbook           # bit-for-bit replay verdict
verum playbook --freeze REPORT.md BOOK.vrbook # replay + frozen snapshot report

.vrbook v2 notebooks carry a content-address chain over their code cells. --replay recomputes the chain from the sources (an out-of-step hand edit is refused before execution, exit 2), re-runs every cell from scratch, and compares recorded outputs bit-for-bit — the first divergence names its cell and address (exit 3). --freeze additionally writes the frozen report: sources, chain addresses, and the outputs that actually happened on that run. See Playground for the notebook itself.

Verification & analysis

verum verify [FILE] --mode <runtime|static|formal|fast|thorough|certified|synthesize> \
                    --solver <auto|portfolio|capability> \
                    --timeout 120 [--cache] [--function NAME] [--diff GIT_REF] \
                    [--verify-profile NAME] [--smt-proof-preference auto] \
                    [--profile] [--profile-obligation] [--budget DURATION] \
                    [--export PATH] [--distributed-cache URL] \
                    [--closure-cache] [--closure-cache-root PATH] \
                    [--ladder] [--ladder-format plain|json] \
                    [--dump-smt DIR] [--check-smt-formula FILE] \
                    [--solver-protocol] [--show-cost] [--compare-modes] \
                    [--interactive] [--interactive-tactic] [--lsp-mode]
verum analyze [--escape] [--context] [--refinement] [--all]
verum audit [--details] [--direct-only] [--framework-axioms] \
             [--kernel-rules] [--epsilon] [--coord] [--no-coord] \
             [--hygiene] [--hygiene-strict] [--owl2-classify] \
             [--framework-conflicts] [--accessibility] \
             [--round-trip] [--coherent] [--proof-honesty] \
             [--framework-soundness] [--coord-consistency] \
             [--format plain|json]
verum lint [--fix] [--deny-warnings] [--profile NAME] [--explain RULE] \
            [--list-rules] [--validate-config] [--since GIT_REF] \
            [--severity error|warn|info|hint] \
            [--format pretty|json|sarif|github-actions|tap]
verum fmt [--check]

verum lint runs two cooperating engines: a fast text-scan path (20 rules — Rust-isms, missing context decls, CBGR hot paths, …) and an AST-driven path (refinement-type and other Verum-unique rules whose evidence is structural). See Reference → Lint rules for every rule shipped today, Architecture → Lint engine for the design, and Cookbook → Linter recipes for pre-commit / CI / migration recipes.

Verification modes map to strategies documented in Verification → gradual verification.

Audit subcommands

verum audit is the project-wide trust-boundary tool. As of the current revision it exposes ~48 gates organised in eight bands plus the --bundle aggregator. Each gate emits both human-readable and structured JSON output (under audit-reports/*.json); the JSON is schema_version-pinned for archival use. For the predicate-level formalisation see Verification → soundness gates; for the workflow see ATS-V → audit protocol.

Kernel-soundness band (13 gates)

Flag	Verifies
--kernel-rules	The trusted-base inference rule list (one row per rule with citation)
--kernel-recheck	Re-checks every theorem in the project against the trusted base
--kernel-soundness	Per-rule discharge inventory + parallel Coq / Lean / Isabelle export
--trust-extension-report	Auditor-facing snapshot of the kernel-rule trust extension surface — every KernelRule partitioned into Proved / DischargedByFramework { lemma_path, framework, citation } / Admitted { reason } buckets. The current steady state is zero Admitted; an Admitted entry trips the gate. See framework axioms — IOU registry.
--external-prover-replay	Drives the kernel-soundness export through Lean 4 (lake build), Coq / Rocq (coqc), and Isabelle/HOL (isabelle build); reports per-backend clean / iou-only / hard-error / not-available. Three independent foundations agreeing. Backend filter via --backend lean,coq,isabelle,all; --strict requires all installed. See external-prover-verification.
--differential-lean-checker	Cert-by-cert agreement gate: a 24-cert battery (T-Univ / T-Var / identity at multiple universes / polymorphic identity / T-Pi-Form / T-App-Elim correct + mismatched / T-App on non-function / boundary-pin certs / nested binders / η-redex / negative shapes) is run through both the Rust kernel (Certificate::verify) and the Lean executable verum_replay_checker (built via lake build); per-cert verdicts must agree. Where --external-prover-replay checks meta-theory shape (the 38 K_*_sound theorem statements type-check across four foundations), --differential-lean-checker checks the operational kernel — same accept/reject judgements as a re-implementation. See differential-lean-checker.
--kernel-v0-roster	The kernel_v0 Verum-self-hosted manifest vs filesystem
--kernel-intrinsics	Kernel intrinsic registry — every kernel_* dispatch entry
--kernel-discharged-axioms	Axioms admitted under @kernel_discharge(...) markers
--differential-kernel	N-way agreement gate over the canonical 24-cert battery. Runs every cert through the default kernel registry — Slot A (bidirectional + WHNF), Slot B (Normalisation by Evaluation with closures + level-indexed quote), Slot C (manifest-driven meta-soundness verifier) — and asserts unanimous accept/reject. Complementary to --differential-lean-checker: that gate compares the trusted-base kernel against an independent Lean re-implementation cross-language; this gate compares three structurally-distinct algorithms within the same process on the same battery. See three-kernel-differential.
--differential-kernel-fuzz	Property-based mutation fuzz over the canonical-battery seed roster. Each iteration picks a seed, samples a mutation chain (length 1–3 from an 11-variant grammar — universe lifts, subterm swaps, binder-domain rewrites, app-injections, free-variable substitutions), applies it, and runs the mutant through the default kernel registry (Slot A / B / C). Disagreements are auto-shrunk to a minimal failing case via greedy 1-element-removal. The audit report carries per-mutation hit counts + per-seed hit counts + chain-length distribution so sampling bias is observable when the gate passes. See property-fuzz.
--reflection-tower	MSFS-grounded 4-stage meta-soundness
--codegen-attestation	Per-pass codegen kernel-discharge status

ATS-V (architectural-types) band (6 gates)

Flag	Verifies
--arch-discharges	The 40-pattern anti-pattern catalog (AP-001..AP-040)
--arch-coverage	Annotation density + missing-Shape report
--arch-corpus	Per-Lifecycle inventory of annotated cogs
--counterfactual	Non-destructive scenario battery over Shapes
--adjunctions	Architectural adjunction detection (4 canonical pairs)
--yoneda	Yoneda-equivalence checker per ATS-V spec §20.7

Framework + citation band (10 gates)

Flag	Verifies
--framework-axioms	every @framework(name, "citation") marker, grouped
--framework-conflicts	known-incompatible framework pairs
--framework-soundness	per-axiom K-FwAx classification (sound / trivial-placeholder)
--foundation-profiles	Foundation-by-cog inventory
--accessibility	enact / EpsilonOf without @accessibility(λ)
--soundness-iou	outstanding "admitted" lemmas + IOU manifest
--dependent-theorems <axiom>	apply-graph walker for downstream impact
--apply-graph	whole-corpus apply-graph
--bridge-discharge	Diakrisis-bridge @effect(...) marker discharge
--bridge-admits	bridge-marker admits + their citation IOUs

Hygiene + coherence band (8 gates)

Flag	Verifies
--hygiene	self-referential surface-form classification (factorisation report)
--hygiene-strict	reject raw self in free functions (CI gate)
--coord	per-theorem (Framework, ν, τ) MSFS coordinate
--coord-consistency	per-theorem supremum-of-cited-coords gate
--no-coord	cogs missing MSFS-coord declarations
--coherent	per-theorem @verify(coherent*) α-cert ⟺ ε-cert status
--epsilon	every @enact(epsilon = …) marker grouped by ε-primitive
--proof-honesty	per-theorem proof-body shape classification

Cross-format + export band (3 gates)

Flag	Verifies
--round-trip	per-theorem 108.T round-trip status (Decidable / SemiDecidable / Undecidable)
--cross-format	cross-format coverage matrix (Lean / Coq / Dedukti / Metamath / Isabelle)
--owl2-classify	OWL 2 subclass closure + cycle / disjointness violations

Roadmap + coverage band (6 gates)

Flag	Verifies
--htt-roadmap	Lurie HTT mechanisation roadmap status
--ar-roadmap	Arnold-Stability mechanisation roadmap status
--manifest-coverage	manifest-vs-filesystem coverage per kernel-component manifest
--mls-coverage	MSFS-corpus coverage classification
--verify-ladder	per-cog verification-strategy ladder enumeration
--ladder-monotonicity	the ν-ordinal monotonicity check on the verify ladder

Tooling band (3 gates)

Flag	Verifies
--proof-term-library	inventory of canonical proof-term examples
--signatures	cross-format-roundtrip signatures audit
--docker	container-image reproducibility check

Domain-specific dispatcher band

verum audit surfaces several focused dispatchers that route specific predicate shapes to specialised solvers. Each dispatcher reuses the existing capability-router infrastructure (no new FFI surface) and produces a structured outcome the audit gate maps onto a verdict.

Flag	Dispatcher	Routes
--count-o-dispatch	verum_smt::count_o_dispatch	OWL 2 count_o_unbounded predicates inside refinement-bounded contexts → SMT Finite Model Finding (see Verification → OWL 2 §5).

Aggregator (1 gate)

Flag	Verifies
--bundle	runs every gate above and emits a single L4 load-bearing verdict

--format plain (default) emits human-readable output. --format json emits a stable machine-parseable schema suitable for CI dashboards and audit-reports/*.json archival. Each subcommand may be passed solo (e.g. verum audit --framework-axioms) or via --bundle to run all of them.

Verification profiling & budgets

Flag	Purpose
--profile	Per-function timings, bottleneck categories, cache stats; printed at end of run.
--profile-obligation	Break each function's time into individual obligations (pre/postconditions, refinements, loop invariants). Implies --profile.
--budget DURATION	Project-wide wall-clock budget — 120s, 2m, 1h, or bare integer (seconds). Fails the build past the limit.
--export PATH	Write profile report as JSON to PATH. Implies --profile.
--distributed-cache URL	S3 / Redis shared proof cache (e.g. s3://bucket/verify-cache).
--verify-profile NAME	Apply [verify.profiles.<NAME>] from verum.toml. CLI flags still win over the profile.
--diff GIT_REF	Only verify functions whose source has changed since the ref (HEAD~1, origin/main, abc123).
--dump-smt DIR	Dump every SMT-LIB query to DIR/<function>-<idx>.smt2.
--check-smt-formula FILE	Dispatch a raw .smt2 file to the configured solver; prints sat/unsat/unknown. Ignores FILE argument.
--solver-protocol	Log every solver send/recv on stderr, prefixed [→] / [←].
--lsp-mode	Emit LSP Diagnostic JSON on stdout, one per line. Suppresses human output.
--interactive-tactic	Ltac2-style tactic REPL — prints the goal, accepts tactics one line at a time.
--smt-proof-preference BACKEND	Which backend exports proof traces for Certified strategy. Default smt-backend (ALETHE, more stable).
--closure-cache	Opt in to per-theorem closure-hash incremental verification. Theorem proofs whose fingerprint + Ok-verdict are cached are skipped without invoking the SMT/kernel re-check. See Tooling → Incremental cache.
--closure-cache-root PATH	Override the cache root (default <input.parent>/target/.verum_cache/closure-hashes/). Implies --closure-cache. Standard CI use is to point this at a shared NFS path.
--ladder	Route every @verify(strategy) annotation through the typed 13-strategy ladder dispatcher. Emits per-theorem verdicts (Closed / Open / DispatchPending / Timeout) plus a totals summary. Non-zero exit on Open / Timeout (real failures); DispatchPending is advisory. See Verification → CLI workflow → Ladder.
--ladder-format plain|json	Output format for --ladder. JSON suitable for CI / IDE consumption.

Manifest equivalents in [verify]: total_budget, slow_threshold, distributed_cache, cache_dir, cache_max_size, cache_ttl, profile_slow_functions, profile_threshold, profiles.<name>.*. CLI flags always override the manifest.

Tactic catalogue

verum tactic list    [--category identity|composition|control|focus|forward] [--format plain|json]
verum tactic explain <name> [--format plain|json]
verum tactic laws    [--format plain|json]

Surfaces the canonical 15-combinator catalogue + 12 algebraic laws. Used by IDE completion, the docs generator, and CI shape-pinning. Full guide in Tooling → Tactic catalogue.

Proof drafting

verum proof-draft --theorem <T> --goal <G> \
                  [--lemma name:::signature[:::lineage]]… \
                  [--max <N>] [--format plain|json]

Ranked next-step tactic suggestions for a focused proof state. Drives LSP / REPL hover panels. Full guide in Tooling → Proof drafting.

Proof repair

verum proof-repair --kind <K> [--field key=value]… \
                   [--max <N>] [--format plain|json]

Where <K> is one of: refine-depth, positivity, universe, fwax-not-prop, adjunction, type-mismatch, unbound-name, apply-mismatch, tactic-open.

Structured repair-suggestion engine for typed proof / kernel failures. Full guide in Tooling → Proof repair.

Closure-hash incremental cache

verum cache-closure stat   [--root <P>] [--format plain|json]
verum cache-closure list   [--root <P>] [--format plain|json]
verum cache-closure get    <theorem> [--root <P>] [--format plain|json]
verum cache-closure clear  [--root <P>] [--format plain|json]
verum cache-closure decide <theorem> --signature <s> --body <s> \
                           [--cite <c>]… [--kernel-version <v>] \
                           [--root <P>] [--format plain|json]

Inspector / control surface for the per-theorem closure-hash cache (target/.verum_cache/closure-hashes/). The verum verify --closure-cache flag is the production reader/writer; this subcommand is for ad-hoc inspection + CI scripts. Full guide in Tooling → Incremental cache.

Foreign-system theorem import

verum foreign-import --from <coq|lean4|mizar|isabelle> <FILE> \
                     [--out <PATH>] [--format skeleton|json|summary]

Reads a Coq / Lean4 / Mizar / Isabelle source file and emits a Verum .vr skeleton with one @axiom-bodied declaration per imported theorem, attributed back to the source via @framework(<system>, "<source>:<line>"). The inverse of verum export. Full guide in Tooling → Foreign-system import.

LLM tactic protocol

verum llm-tactic propose --theorem <T> --goal <G> [--lemma ...]
                         [--hyp ...] [--history ...] [--model <ID>]
                         [--hint <TEXT>] [--persist] [--audit <PATH>]
                         [--format plain|json]
verum llm-tactic audit-trail [--audit <PATH>] [--format plain|json]
verum llm-tactic models [--format plain|json]

LCF-style fail-closed LLM proof proposer. An LLM may propose tactic sequences for a focused goal but the kernel re-checks every step before committing — any rejection discards the proposal. Every invocation is captured in an append-only audit trail keyed by model id + prompt hash + completion hash so the proof is reproducible from the log. Full guide in Tooling → LLM tactic protocol.

Proof REPL

verum proof-repl batch --theorem <T> --goal <G> [--lemma ...]
                       [--commands <FILE>] [--cmd <LINE>]…
                       [--format plain|json]
verum proof-repl tree  --theorem <T> --goal <G> [--lemma ...]
                       [--apply <STEP>]…

Non-interactive batch driver for the proof REPL state machine. Apply tactics, navigate with undo / redo, request hints, and emit the proof tree as Graphviz DOT — all from the shell, with full kernel-grade feedback on every step. Non-zero exit on any kernel rejection (CI-friendly). Full guide in Tooling → Proof REPL.

Cog distribution registry

verum cog-registry publish    --manifest <FILE> [--root <DIR>] [--registry-id <ID>] [--output ...]
verum cog-registry lookup     --name <N> --version <V> [--root <DIR>] [--registry-id <ID>] [--output ...]
verum cog-registry search     [--name SUB] [--paper-doi DOI] [--framework TAG] [--theorem NAME]
                              [--require-attestation KIND] [--root <DIR>] [--registry-id <ID>] [--output ...]
verum cog-registry verify     --name <N> --version <V> [--root <DIR>] [--registry-id <ID>] [--output ...]
verum cog-registry consensus  --name <N> --version <V> --mirror <DIR> [--mirror <DIR>]… [--output ...]
verum cog-registry seed-demo  [--output ...]

Verified-mathematics package distribution. Per-cog reproducibility hash chain (sources + build env + output) plus typed attestations (verified_ci / honesty / coord / cross_format / framework_soundness). Immutable releases — republishing a version with different content is a hard failure. Multi-mirror consensus check via cog-registry consensus. Full guide in Tooling → Cog distribution registry.

SMT certificate replay

verum cert-replay replay      --backend <B> [--cert FILE | --format F --theory T --conclusion C --body B]
                              [--output plain|json|markdown]
verum cert-replay cross-check [--backend <B>]… [--cert FILE | --format F …]
                              [--require-consensus] [--output ...]
verum cert-replay formats     [--output ...]
verum cert-replay backends    [--output ...]

Multi-backend SMT certificate cross-validation surface. The kernel-only structural check makes solvers external to the trusted computing base — a tampered cert is caught regardless of what external solvers claim. Multi-backend cross-check --require-consensus is the @verify(certified) semantics: every available backend must accept. Full guide in Tooling → SMT certificate replay.

Continuous benchmarking

verum benchmark run     --system <S> --suite-name <N> [--theorem <T>]…
                        [--format plain|json|markdown|csv]
verum benchmark compare [--system <S>]… --suite-name <N> [--theorem <T>]…
                        [--format plain|json|markdown|csv]
verum benchmark metrics [--format plain|json|markdown|csv]

Head-to-head comparison surface vs Coq / Lean4 / Isabelle / Agda across nine canonical metrics (kernel LOC, compilation speed, memory peak, cross-format export coverage, tactic-library coverage, trust diversification, LLM-tactic acceptance, etc.). Markdown output decorates the leader cell per metric with ⭐. Full guide in Tooling → Continuous benchmarking.

Auto-paper documentation

verum doc-render render     [--format md|markdown|tex|latex|html] \
                            [--out <PATH>] [--public]
verum doc-render graph      [--format dot|json] [--public]
verum doc-render check-refs [--format plain|json] [--public]

Walks every public @theorem / @lemma / @corollary / @axiom declaration and renders Markdown / LaTeX / HTML directly from the corpus. Eliminates the duplicate-source problem (paper.tex + verum-corpus): the corpus IS the paper draft. Full guide in Tooling → Auto-paper generator.

Profiling

verum profile [FILE] [--compilation] [--memory] [--cpu] [--cache] [--all] \
                     [--hot-threshold 5.0] [--sample-rate PERCENT] \
                     [--functions NAME1,NAME2] [--precision us|ns] \
                     [--output OUT] [--suggest]

--memory reports CBGR tier distribution (Tier 0 / 1 / 2 breakdown); --cpu shows runtime cost; --cache analyses cache behaviour; --compilation shows compiler-phase timings. --all expands to every slice and renders them in a single unified dashboard (spec §6) — one header, correlated sections, ranked hot-spots, actionable recommendations. --suggest emits optimisation hints.

CBGR sampling knobs

Flag	Purpose
--sample-rate PERCENT	Sampling rate for the CBGR profiler, 0.0–100.0. Smaller values reduce overhead; 1.0 is the safe default.
--functions a,b,c	Restrict the report to these exact function names. The filter is applied upstream, so every downstream section (hot-spots, breakdown, recommendations) sees the same population.
--precision us|ns	Timer granularity. us renders timings in milliseconds (default); ns uses the native Instant.now resolution and dynamically picks ns / µs / ms per magnitude so sub-microsecond costs stay legible.

Docs & diagnostics

verum doc [--open] [--document-private-items] [--format html|markdown|json]
verum explain <code> [--no-color]      # e.g. verum explain E400
verum info [--features] [--llvm] [--all]
verum smt-info [--json]                # verification backends
verum smt-stats [--json] [--reset]     # last-session routing telemetry

verum explain takes the code exactly as the diagnostic prints it — the E400 in error<E400>: type mismatch. The leading E is optional, so verum explain 400 works too. Codes fall into bands by what went wrong:

Band	Meaning	Example
E0xx	parse	E001 unexpected token
E1xx	name resolution	E100 undefined variable, E102 wrong arity
E2xx	modules	E201 circular import
E3xx	memory and lifetimes	E305 uninitialized value, E310 use after move
E4xx	types	E400 type mismatch, E404 missing protocol impl
E5xx	verification	E502 refinement predicate false
E6xx	contexts	E600 context not provided
E8xx	FFI	E800 foreign call convention
E9xx	internal	E900 internal compiler error

Some codes carry a worked example with causes and fixes; the rest show their one-line meaning and category.

One caveat worth knowing: a handful of codes are printed by the compiler with a meaning the registry does not share — E801 is printed for an undeclared context and registered as an FFI ABI mismatch, so explain answers about the second. Being tracked; if an explanation does not match the error you saw, trust the error.

Crash reports

The toolchain captures panics and fatal signals to structured reports under ~/.verum/crashes/. See Tooling → Crash diagnostics for the full workflow; the commands themselves are:

verum diagnose list [--limit N]
verum diagnose show [REPORT] [--json] [--scrub-paths]
verum diagnose bundle [-o OUT] [--recent N] [--scrub-paths]
verum diagnose submit [--repo owner/name] [--recent N] [--dry-run]
verum diagnose env [--json]
verum diagnose clean [--yes]

Interactive

verum repl [--preload FILE] [--skip-verify]
verum playbook [FILE] [--tier 0|1] [--vim] [--preload FILE] [--tutorial] \
                       [--profile] [--export OUT] [--no-color]
verum playbook-convert to-script <IN> [-o OUT] [--include-outputs]
verum playbook-convert from-script <IN> [-o OUT]

Packaging

verum package publish [--dry-run] [--allow-dirty]
verum package search <query> [--limit 10]
verum package install <name> [--version X]
verum tree [--duplicates] [--depth N]

Workspace

verum workspace list
verum workspace add <path>
verum workspace remove <name>
verum workspace exec -- <command> [args...]

Architectural type system (verum arch)

verum arch primitives [--format plain|json]
verum arch catalog    [--format plain|json]
verum arch rules      [--format plain|json]
verum arch graph      [--cog NAME] [--format dot|json]

These commands provide structured machine-readable surfaces for coding-agents alongside human-friendly CLI output (dual-audience design):

Subcommand	What it surfaces
primitives	The eight ATS-V primitives (Capability / Boundary / Lifecycle / Foundation / Tier / MsfsStratum / CveClosure / VerifyStrategy) with their canonical variant rosters.
catalog	The 40-pattern anti-pattern catalog (AP-001..AP-040). Same data as verum audit --arch-discharges, surfaced without running the gate.
rules	The kernel-rule discharge inventory — same data the audit's --kernel-rules band reports.
graph	Per-cog composes_with graph rendering (Graphviz DOT or JSON).

For the catalog itself see Architecture-as-Types → anti-pattern overview.

Cubical / HoTT primitives (verum cubical)

verum cubical primitives  [--format plain|json]
verum cubical rules       [--format plain|json]
verum cubical face <formula> [--output ...]

Inventory of the typed cubical / HoTT primitives (Path / Refl / J / Transp / Coe / Hcomp / Comp / Glue / Equiv / Univalence + 7 more), the computation-rule registry, and the face-formula validator. Architectural foundation for foundation-neutral cubical type theory in Verum. See Tooling → Cubical.

Knowledge-base import (verum import)

verum import --from owl2-fs <FILE> [--out PATH]

Inverse of verum export. Reads an external knowledge-base format and emits a .vr file with the corresponding typed attributes. Currently supports OWL 2 Functional-Style Syntax; round-trips with verum export --to owl2-fs.

For Coq / Lean4 / Mizar / Isabelle theorem import see verum foreign-import above.

Program extraction (verum extract)

verum extract [--target verum|ocaml|lean|coq] [--out DIR]

Walks the project for declarations marked with @extract / @extract_witness / @extract_contract, dispatches each to the program-extraction pipeline at the attribute's ExtractTarget, and emits per-target files at <output>/<decl>.{vr,ml,lean,v}. Default output dir is extracted/. See Verification → program extraction.

Proof-term verification

verum check-proof    [--cert FILE]
verum elaborate-proof <FILE> [--out DIR]

check-proof re-verifies a .vproof JSON certificate ({ term, claimed_type, metadata }) via the trusted-base kernel. Exits 0 iff the term has the claimed type. The kernel's thirteen rules (Π/Σ/Id with universe polymorphism) form the irreducible trusted base — every other discharge route reduces to a sequence of rule applications this command can re-check.

elaborate-proof walks every theorem / lemma / corollary in <FILE> and emits a <theorem-name>.vproof file per declaration into <output-dir> (default: <source-dir>/elaborated/). The output is consumable by check-proof.

Script-mode cache (verum cache)

verum cache path                 # show cache root
verum cache list                 # entries by hash
verum cache show <ENTRY>         # entry detail
verum cache gc [--budget BYTES]  # evict LRU until under budget
verum cache clear                # wipe everything

The script-mode VBC cache lives at ~/.verum/script-cache/. It is content-addressed by source + compiler version + flags, so a hit is always a valid reuse — there is no "stale cache" failure mode. gc evicts least-recently-accessed entries until under a budget; clear removes everything.

Health & diagnostics (verum doctor)

verum doctor [--json] [--strict]

Health-check survey of the Verum installation. Verifies the home directory is writable, surveys the script cache and content store, parses any verum.lock in the cwd, and probes the permission-grammar surface. --json emits NDJSON for scripting; --strict exits non-zero on warnings as well as failures.

For panic / fatal-signal crash reports see the verum diagnose family above.

VBC archive inspection (verum vbc-version)

verum vbc-version <FILE>

Inspect a VBC archive header (magic, version, sections, hashes). Used to debug compiler / interpreter version skew between a built artefact and the running toolchain.

Git hooks (verum hooks)

verum hooks install   [--force]
verum hooks uninstall
verum hooks list

Manages git hooks for the current project. The install subcommand wires verum lint --since HEAD --severity error + verum fmt --check into .git/hooks/pre-commit. Each generated hook carries a header marker so uninstall only touches files we wrote.

Shell completions (verum completions)

verum completions <bash|zsh|fish|powershell> > <DEST>

Emits a shell-completion script for the named shell. Drop into the shell's completion path (e.g. ~/.zsh/completions/_verum) to enable tab completion for every verum subcommand and flag.

Services

verum lsp --transport stdio|socket [--port N]
verum dap --transport stdio|socket [--port N]

Configuration

verum config show [--json] [-Z key=val] [--tier interpret|aot]
verum config validate [-Z key=val]    # typo-check verum.toml

verum export --to <dedukti|coq|lean|metamath> [-o PATH]
verum export-proofs --to <dedukti|coq|lean|metamath> [-o PATH]  # alias

verum clean [--all]
verum version [--verbose]

config show resolves verum.toml + CLI overrides and prints the effective configuration — the source of truth for "what's actually compiled". See Reference → verum.toml for the manifest schema.

verum export walks every theorem / lemma / axiom in the project and emits a statement-only certificate file; proofs are admitted. See Verification → proof export.

Global flags

--tier 0|1|2|3          # override execution tier
-Z <flag=value>         # unstable / experimental feature flag
-D <lint>               # deny lint
-W <lint>               # warn on lint
-A <lint>               # allow lint
-F <lint>               # forbid lint

-Z, -D/-W/-A/-F are accepted wherever a command compiles code (build, run, test, check, fmt, lint, doc, lsp, dap, playbook).

Environment variables

VERUM_HOME=~/.verum               # toolchain root
VERUM_LOG=debug                   # log level
VERUM_SMT_TELEMETRY=1             # emit SMT routing telemetry
VERUM_TARGET_DIR=target           # build-output directory
VERUM_TOKEN=...                   # registry token for package publish

Configuration files

• verum.toml — project manifest (see verum.toml).
• .verum/config.toml — user-level config.
• target/.verum-cache/ — build / VBC / proof cache.

See also

• Build system — how invocations feed the pipeline.
• Cog packages — verum package flows.
• Reference → CLI commands — full per-command reference with all flags.