Tooling | Verum

📄️CLI

The verum binary is self-contained: compiler, interpreter, linker,

verum build runs the full compilation pipeline (see

A cog is Verum's unit of distribution — a self-describing archive

Verum's testing surface is built into the verum binary. There is no

Verum ships with first-class property-based testing. Mark a function

Language Server Protocol 3.17 — diagnostics, completion, hover, refinement counter-examples, CBGR hints.

Verum Language Support for Visual Studio Code — syntax, LSP, inlay hints, debugger, profile dashboard.

The interactive terminal-UI for exploring a Verum project — discover, invoke, verify, profile.

Interactive REPL backed by the VBC interpreter — bind values, define functions, verify, inspect bytecode.

How the Verum toolchain captures panics and fatal signals, and how to inspect the structured crash reports it produces.

This page is the complete reference for Verum's tactic system —

verum proof-draft is the IDE / REPL / CI surface for Verum's

When the kernel rejects a term or the type-checker fails on an

For corpora with hundreds of theorems (a typical research corpus

A Verum corpus IS a formal proof AND a paper draft. Pre-this-tool

verum foreign-import is the inverse of cross-format export.

Verum is the first proof assistant where LLM assistance is

verum proof-repl is a non-interactive batch driver for the

verum benchmark is the head-to-head comparison surface for

Verum joins the small group of proof assistants (alongside Coq's

Verum's package manager is to verified mathematics what Cargo is

Verum is foundation-neutral: classical logic, cubical type theory,