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] [--skip-verify]

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.

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 E0312
verum info [--features] [--llvm] [--all]
verum smt-info [--json]                # verification backends
verum smt-stats [--json] [--reset]     # last-session routing telemetry

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.