Verification in Verum

Verum connects executable programs, contracts and explicit proofs. The verification interface must make each result inspectable: the checked statement, its assumptions, the deciding mechanism and any unfinished work. Different routes currently provide different kinds of evidence. Start with the kernel boundaries when a result will authorize another system's decisions.

This page is the deep architectural entry point. It explains what problem verification solves in Verum, how the compiler encodes that problem, and where each feature lives in the pipeline. The subsections that follow it are each a close-up of one layer; read this page first, then navigate into the layer you need.

Who should read this page

Anyone designing proofs, extending the solver, writing a framework axiom, or auditing the trusted computing base. If you only want to add a requires/ensures clause and move on, start at Contracts instead.

---

1. The core thesis

The design goal is a language where a program's contracts, implementation and proof obligations remain connected through compilation. Refinements express admissible values, theorem declarations express formal claims, and verification strategies choose how to investigate those claims.

The connection has several independent obligations: translating the source statement faithfully, obtaining a valid derivation, checking its assumptions, and preserving runtime behavior during compilation. Sharing an AST or an obligation hash helps track those obligations; it does not prove all of them.

Verum exposes concrete mechanisms for this work: a minimal proof-term checker, solver integration, framework-citation inventories, comparison checkers and compiler-attestation records. Their evidence should compose without being conflated. The knowledge-system profile makes that discipline explicit for Noesis and other theory-management systems.

---

2. The two-layer dispatch model

Every proof obligation flows through two independent layers. The first picks what kind of guarantee you want; the second picks which engine delivers it. Confusing these layers is the single most common source of misdirected bug reports — most "my proof is slow" or "my proof doesn't run" issues are mismatches between intent and engine.

Layer 1 — VerificationLevel

Three-valued enum defined in verum_verification::level:

Level	Intent	Pipeline effect
Runtime	Check on execution; no proof required.	Compile refinement checks into bytecode guards. No SMT invocation.
Static	Prove at compile time; fail build if the proof fails.	Invoke SMT; report failures through the diagnostic pipeline.
Proof	Prove at compile time AND emit a certificate.	Invoke SMT, replay through the trusted kernel, write the certificate to disk.

Level selection is per-declaration, per-file, or per-project. The compiler defaults to Static for code with refinements and Runtime otherwise; overrides live in verum.toml (project), @verify(level = …) (declaration), or --mode (CLI).

Layer 2 — VerifyStrategy

Seven-valued enum defined in verum_smt::verify_strategy:

Strategy	Operational meaning
Runtime	Skip the solver entirely; compile to an assertion.
Static	Single solver call; fastest. Used for simple LIA / bitvector obligations.
Formal	Single solver with rich tactics; default for anything non-trivial.
Fast	Low timeout (3s default). Use for CI checkpoints.
Thorough	Long timeout (300s), portfolio race, full reflection unfolding.
Certified	Portfolio + cross-validation + kernel replay; the most expensive strategy.
Synthesize	Treat the ensures as a specification; synthesize the body via SyGuS.

A single VerificationLevel admits many VerifyStrategy choices. Proof-level verification requires Formal, Thorough, or Certified. Static level admits all except Runtime.

Valid combinations

Level \ Strategy  Runtime  Static  Formal  Fast  Thorough  Certified  Synthesize
Runtime              OK       –       –      –       –          –           –
Static                –       OK      OK     OK      OK         –           OK
Proof                 –       –       OK     –       OK         OK          OK

Certified implies Proof (kernel replay is mandatory). Runtime level cannot escalate to compile-time strategies; you must change the level first. The compiler rejects invalid combinations at config parse time, never silently at solve time.

---

3. The verification pipeline, end-to-end

The compiler-facing SMT path organizes IR obligations into the stages below. It is separate from the minimal .vproof source bridge. A common goal data type does not establish that every source form has a faithful translation; see the source-to-goal boundary.

3.1 Obligation generation

The typed AST pass in verum_types emits IR-level proof obligations as it checks each declaration. Sources:

• Refinement types. Every Int { p }, List<T> { p }, or named refinement alias lowers to an obligation at each binding site: p must hold for every input, every assignment, and at every return.
• Function contracts. requires p becomes a hypothesis at the body entry; ensures q becomes the goal at body exit. Quantified clauses (forall i in 0..len(xs)) expand into a universally quantified formula.
• Loop specifications. invariant p must hold at every entry and exit of the loop body; decreases m must shrink on each iteration (a well-foundedness check).
• Theorem declarations. The IR path represents the stated proposition and its premises as obligations. This does not imply support in the minimal source bridge: from_theorem_decl refuses generic/value parameters and requires clauses rather than changing the formal goal.
• Algebraic data type encoding. Nullary and variant types emit structural axioms (disjointness, exhaustiveness) — see ADT encoding.

Each obligation carries its source span, provenance (RefinementCheck | EnsuresClause | RequiresClause | Subgoal | Frame), and hypothesis context into the next stage. No obligation is ever emitted without a real span — diagnostics always point at something the user wrote.

3.2 Translation

The verum_smt::translate module turns an IR obligation into an SMT-LIB formula. Key responsibilities:

• Theory selection. Int / Real / Bool / Bitvector / Array / String / Sequence — each term picks its native SMT sort.
• Uninterpreted symbols. A user-defined function that does not qualify for reflection becomes an uninterpreted function symbol; its arguments' shapes are preserved but its body is hidden from the solver.
• Refinement reflection. A pure, single-expression, parameterised function whose body is inside the translated fragment gets a defining axiom that constrains its symbol, so solvers can reason about its behaviour. See Refinement reflection.
• Variant encoding. ADTs use the disjointness/exhaustiveness scheme described in ADT encoding. The translator maintains a registry of variant tags per type so that patterns like x is Cons(_, _) become sound axioms.
• Quantifier trigger selection. forall / exists clauses get triggers chosen by matching term shapes; manual triggers via @trigger(pattern) are respected.
• Pending-axiom channel. Length additivity for concat, identity for empty collections, array read-through (arr.update(i, v).at(i) == v), and similar generic algebraic laws are emitted lazily only when the obligation references them.

3.3 Strategy dispatch

The capability router in verum_smt::capability_router classifies the SMT formula by which theories and quantifier patterns it touches, then consults the VerifyStrategy to choose a backend:

Classification        → Preferred backend    → Fallback
--------------------    --------------------   --------------
LIA-only                primary adapter
Nonlinear arith         primary adapter (NLA tactic)       fallback adapter (farkas)
Strings                 primary adapter (seq theory)
FMF/quantifiers         primary adapter (fmf_enum)       fallback adapter (mbqi)
Arrays only             primary adapter
Bitvector-heavy         primary adapter                    (no symmetric BV on the fallback)
Nonlinear + quantifier  primary adapter (portfolio)      fallback adapter (rlimit pass)

See SMT routing for the full table. The router is transparent to the user — you request a strategy, not a solver. Changing the backend set (e.g., when the in-house Verum SMT lands) doesn't require a single user-code change.

3.4 Solve / prove

Each strategy translates to a concrete solver invocation:

• Static / Formal: single (check-sat) call with a timeout.
• Thorough: a portfolio race — multiple solver workers launched in parallel, first to return unsat wins; on disagreement the result is logged as Split and escalated.
• Certified: portfolio + proof-term extraction from the winning backend + kernel replay + certificate write.
• Synthesize: SyGuS-style function synthesis from the ensures clause; returns a candidate body + a certificate of its correctness.

Every call writes telemetry (theory taxonomy, backend, outcome, time) to the session statistics cache; see verum smt-stats.

3.5 Kernel replay

There are two different certificate routes.

• A closed .vproof carries a term and claimed type for the minimal Π/Σ/identity-type checker. verum check-proof rechecks that judgment.
• SmtCertificate carries a solver envelope, backend, rule tag and obligation hash. The current replay_smt_cert validates those fields and creates a solver-attributed axiom witness. The replay_smt_cert_with_obligation variant additionally checks the consuming goal's expected hash.

Hash association prevents exchanging artifacts between named obligations. It does not prove a solver trace sound. This SMT route retains trust in the solver and translation until the actual inference steps are reconstructed and checked. Neither a strategy named Certified nor a successful audit renames that evidence into a minimal proof-term derivation.

See kernel trust boundaries for the implemented checks and proof-term rules for the separate minimal calculus.

---

4. Where each feature lives in the stack

• Refinement types & reflected predicates → encoded as axioms in the translator; invisible to the kernel (they constrain uninterpreted symbols, not core terms).
• theorem/lemma declarations → elaboration and obligation generation. Supported proof-term exports are checked against their formal claimed type; unsupported exports and source-to-goal correspondence remain explicit. The minimal AST converters refuse parameterized or premise-bearing theorems, function contracts and refinement types; explicit formal goals and the compiler's SMT obligations remain distinct interfaces.
• @framework(id, "citation") → framework attribution in the broader registry. The framework audit inventories those declarations, not every component of the execution or translation trust boundary.
• Cubical / HoTT → constructors and checking rules in the broader CoreTerm infrastructure. They are outside the minimal .vproof calculus; code-generation preservation is a separate obligation.
• SMT certificates → trust-tagged; replay reconstructs a CoreTerm::Axiom with the backend+rule as framework tag.

---

5. Kinds of obligation, kinds of proof

Not every guarantee looks the same. Verum supports four distinct obligation families, each with its own natural proof technique:

5.1 First-order propositional

n > 0 && n < 100, xs.len() > 0, !(a && !a). Pure Boolean / LIA / arithmetic. Every solver handles it; usually sub-millisecond.

5.2 Refinement + reflection

safe_index(xs, i) requires i < len(xs). The predicate references user functions (e.g., len). If the function reflects, the solver reasons symbolically; otherwise it becomes an opaque UF.

5.3 Inductive / structural

length(append(xs, ys)) == length(xs) + length(ys). Needs induction over xs. Verum offers three mechanisms:

• proof by induction(xs) — the tactic generates cases and base.
• Quantifier axioms from reflected predicates — works for simple laws when the solver's quantifier handling cooperates. Note that reflection is non-recursive today, so a self-calling predicate does not become an axiom.
• Manual structured proof (have chain + ind tactic) for cases the solver can't close directly.

5.4 Equational / cubical

transport(ua(e), x) == e.forward(x), Path<A>(a, a) = a = a. HoTT paths, univalence, Glue types. Not discharged by SMT; the kernel has native rules (Refl, HComp, Transp, Glue). See Cubical & HoTT.

5.5 Framework-axiom conditional

Arnold stability proof depends on Lurie higher-topos foundations. The axiom is not checked — it is explicitly trusted with a citation. verum audit lists every framework axiom in the dependency cone, so the trust boundary is enumerable and auditable.

---

6. The tactic DSL

A proof { … } block is a small program that produces a kernel term incrementally. The grammar recognises 22 built-in tactic forms (full reference in Proofs):

Decision procedures: auto, smt, omega, ring, field, simp, blast, decide.

Structural: assumption, intro, split, left, right, exists, witness, case, induction.

Cubical / HoTT: refl, transport, path, glue, hcomp.

Combinators: try, first, repeat, then, all, fail, orelse, ;, |.

Scaffolding: have, show, suffices, let, obtain, calc, using, apply, rewrite.

Escape hatches: admit (assume goal, marked in certificate), sorry (assume goal). A --strict-admits flag that would fail the build on either is described in places but is not accepted by the shipped CLI; verum audit --framework-axioms is the enumeration that does run today.

The tactic DSL is itself verifiable — tactics written with @tactic meta fn are stage-1 meta-programs that quote goal structure and emit CoreTerm values. See Tactic DSL for authoring custom tactics.

---

7. Framework-axiom stratification

Real-world theorems depend on external mathematical frameworks: a quantum field theory proof rests on measure theory; a statistical proof rests on Kolmogorov's axioms; a category theory result may cite Lurie's HTT. Verum makes this dependency explicit and enumerable:

@framework("baez_dolan", "Higher-Dimensional Algebra: An Octonionic
Hopf Algebra, §4.2")
public axiom baez_dolan_3brane_mass_unit(...): ...;

Running verum audit --framework-axioms lists every framework axiom reachable from a module's public API, with citations. The --format json output is machine-parseable for CI enforcement (e.g., "PR is forbidden if it adds a new framework dependency").

Eleven framework families ship with the stdlib (71 axioms total): lurie_htt, schreiber_dcct, connes_reconstruction, petz_classification, arnold_catastrophe, baez_dolan, diakrisis, diakrisis_acts, diakrisis_biadjunction, diakrisis_extensions, diakrisis_stack_model. See Framework axioms for the full inventory and for authoring new ones.

---

8. Gradual migration strategy

A realistic project does not start fully verified. Verum's gradient lets you climb:

1. Prototype — no annotations. Everything is Runtime-level; check and run work with zero SMT calls.
2. Add refinements — Int { > 0 } on a key parameter. Default escalates to Static level with Formal strategy; failing proofs surface as build errors. Sampling via @verify(level = Runtime) lets you defer individual failures.
3. Add contracts — requires / ensures on function signatures. Proof obligations expand; a helper predicate reflects automatically if it is pure and single-expression. Reflection is cheap.
4. Write theorems — theorem sort_is_stable { proof by … }. Now you're writing proofs, not just annotations.
5. Certify — @verify(strategy = Certified) on the theorems that matter most. Certificates land in target/proofs/ and survive in CI artifact storage.
6. Export — verum export-proofs --to lean for inspection and supported target translations. Inspect statement correspondence, placeholders and the receiving checker's outcome before claiming a cross-tool proof.

See CLI workflow for the complete command set; see Proof corpora for how large-scale corpora are structured on Verum.

---

9. What verification does NOT do

Honesty is part of the design. The compiler does not:

• Eliminate every bug. Verification proves the properties you write down. Correctness of the specification itself is outside the system.
• Eliminate the solver from the TCB by default. Formal and Thorough strategies trust the SMT result. Only Certified strategy replays through the kernel. Choose accordingly.
• Handle unbounded concurrent non-determinism. Async reasoning is sequential (happens-before + well-founded scheduling); arbitrary preemption is not a first-class verification target. Use @lock_ordering to prove deadlock freedom for specific structures.
• Replace testing. Proofs cover the abstract machine; testing covers the concrete one (float precision, OS quirks, ABI edges). Run both.
• Replace review. A @framework axiom is as trustworthy as its citation. If the citation is wrong, the proof is vacuous. Framework axioms must be reviewed by the maintainer.

---

10. Reading sequence

If you're new to Verum verification and want the full picture, read the subsections in this order:

1. Contracts — the annotation language.
2. Refinement reflection — how refinement types extend with user-defined logic.
3. ADT encoding — how sum types are axiomatised.
4. SMT routing — how obligations reach a solver.
5. Solver tuning — every config knob the solver subsystem exposes, with copy-paste recipes for common workflows (latency-sensitive, CI, debugging, research).
6. Proofs — the tactic DSL.
7. Tactic DSL — authoring custom tactics.
8. Trusted kernel — the LCF core.
9. Counterexamples — what the solver returns when proof fails.
10. Proof export — envelope format, cross-tool import.
11. Cubical & HoTT — equational reasoning beyond SMT.
12. Framework axioms — stratified trust.
13. Gradual verification — the strategy spectrum (full reference).
14. CLI workflow — end-to-end command use.
15. Proof corpora — how large-scale proof corpora are structured on Verum.
16. Proof-honesty audit — verum audit --proof-honesty walker, classification semantics, audit-reports/proof-honesty.json schema, and the core.math.* carrier-protocol surface (DiakrisisPrimitive, DualLAbsCandidate, OpenQuestion, StrictInclusionWitness, ...).
17. Coord-consistency + framework-soundness audits — verum audit --coord-consistency (M4.B; supremum-of-cited-coords gate) and verum audit --framework-soundness (M4.A; corpus-side K-FwAx classifier). CI gates closing the kernel-time vs audit-time soundness-gap.
18. Operational coherence (VVA-6 stdlib preview) — core/verify/coherence.vr (M4.E): CoherenceCert carrier protocol + 3-way CoherenceVerdict sum + concrete IdentityCoherenceCert instance. The 12-variant VerificationLevel enum extension covering coherent_static / coherent_runtime / coherent strategies (ν = ω·2+3 / ω·2+4 / ω·2+5).

If you only have ten minutes, read Gradual verification and Trusted kernel. They together cover 80% of the design.

---

11. The multi-kernel discipline

Verum compares direct proof-term checking with a Normalisation-by-Evaluation implementation. Both consume the same certificate language and share syntax and universe-level representations. A third registry slot, KernelV0Kernel, invokes the direct checker before checking bootstrap manifest policy; it is not an independent third term-checking algorithm.

The in-process differential audit, mutation audit and Lean reference-checker audit exercise complementary failure modes. Positive controls establish supported cases; rejecting controls and an always-accept test double check that failures are observable. Agreement on these inputs is regression evidence, not a general soundness proof or a claim of unique technology.

See differential verification for the mechanisms and the Noesis profile for how to record their separate results.

---

12. Beyond the kernel — meta-soundness layers

Additional modules describe reflection, theory dependencies, separation logic and compiler preservation obligations. Their contribution must be read at the level they implement:

• Reflection and foundation inventories record declared metatheory requirements. A universe lift or a set-inclusion check on requirement labels is not a proof of a theory's own consistency.
• Separation reasoning has explicit heap assertions and bridge-fidelity classifications. Preservation through the selected bridge is part of the claim, not an implication of its name.
• Codegen attestation records proposed simulation invariants and their evidence status. A cited compiler theorem does not automatically verify Verum's lowering passes.
• The kernel_v0 corpus describes bootstrap judgments and manifests. The registry's Rust wrapper checks these declarations; it does not execute a self-hosted Verum checker.

These surfaces support an ambitious goal: inspectable dependencies from foundations through programs and operational behavior. Each added mechanism needs its own executable contract and evidence before downstream results can rely on it.

---

13. The full audit gate catalog

Every claim Verum makes is mechanically observable. As of the current revision, verum audit exposes 54 gates organised into nine bands (counted from verum audit --help: 60 flags, of which six — --backend --color --details --direct-only --format --strict — are output modifiers rather than gates). This page said "~49" and named 49; every one of those 49 exists, and five more were shipped without reaching the catalog.

Kernel-soundness band (12 gates): --kernel-rules · --kernel-recheck · --kernel-soundness · --external-prover-replay · --differential-lean-checker · --kernel-v0-roster · --kernel-intrinsics · --kernel-discharged-axioms · --differential-kernel · --differential-kernel-fuzz · --reflection-tower · --codegen-attestation.

ATS-V band (6 gates): --arch-discharges · --arch-coverage · --arch-corpus · --counterfactual · --adjunctions · --yoneda.

Framework + citation band (10 gates): --framework-axioms · --framework-conflicts · --framework-soundness · --foundation-profiles · --accessibility · --soundness-iou · --dependent-theorems <axiom> · --apply-graph · --bridge-discharge · --bridge-admits.

Hygiene + coherence band (8 gates): --hygiene · --hygiene-strict · --coord · --coord-consistency · --no-coord · --coherent · --epsilon · --proof-honesty.

Cross-format + export band (3 gates): --round-trip · --cross-format · --owl2-classify.

Roadmap + coverage band (6 gates): --htt-roadmap · --ar-roadmap · --manifest-coverage · --mls-coverage · --verify-ladder · --ladder-monotonicity.

Tooling band (3 gates): --proof-term-library · --signatures · --docker.

Precompiled-stdlib + registry band (5 gates): --stdlib-layers (layer classification over the embedded archive) · --proof-archive (decodes the archive's theorems table and re-resolves each) · --cross-format-roundtrip (per-theorem roundtrip over every @theorem / @lemma / @corollary) · --trust-extension-report (per-rule proved/admitted snapshot) · --attribute-registry (exports every attribute the compiler knows, with targets and arity).

Aggregator (1 gate): --bundle — emits a single L4 load-bearing verdict. It does NOT run every gate above, which this page previously claimed: its own help names the four load-bearing gates it executes in dependency order — --bridge-discharge, --kernel-discharged-axioms, --apply-graph and --cross-format-roundtrip — and aggregates their JSON into target/audit-reports/bundle.json. The last of those four is one of the five that were missing from this catalog, so the page omitted a gate the aggregator depends on.

See Soundness gates for the predicate-level formalisation and ATS-V → audit protocol for the band-by-band detail and JSON schemas.

---

Feature inventory

Every feature described across this verification section is part of the shipping release:

Verification core

• Two-layer dispatch — VerificationLevel × VerifyStrategy with machine-checked policy table (evaluate_attempt). Thirteen strategies in the gradual ladder.
• Refinement types + reflection — pure user predicates lifted into solver axioms, including projections over record fields and protocol methods.
• ADT encoding — native SMT datatypes per variant with cached sort reuse.
• Cubical / HoTT primitives — PathTy, HComp, Transp, Glue as first-class kernel rules with subterm validation.
• Tactic DSL — block-form combinators, Quote/Unquote/GoalIntro meta-programming, cog-level tactic-package registry (Project > ImportedCog > Stdlib shadowing), 56-tactic stdlib across 7 files.
• Counterexample lifecycle — extract → syntactic minimization (pure, always-on) → semantic minimization (delta-debugging, Thorough/Certified) → fix suggestions.
• Trigger diagnostics — W502 / W503 / W504 structural validation of every quantifier trigger.

Trust boundary

• Minimal certificate checker — closed Π/Σ/identity-type terms; its authority is separate from broader CoreTerm mechanisms.
• NbE comparison — an alternative algorithm with shared syntax and universe-level helpers.
• SMT attestation — envelope and obligation checks with explicit solver trust until complete derivation reconstruction is available.
• Foundation and reflection inventories — declared requirements and policy checks, distinct from consistency proofs.
• Separation logic and compiler attestation — explicit bridge and preservation obligations with their individual evidence status.
• kernel_v0 bootstrap corpus — Verum-side rule descriptions and a manifest-backed wrapper around the direct checker.

Outputs

• Proof export — target-specific declarations and supported body translations, with placeholders and statement-correspondence obligations retained; see Proof export.
• Program extraction — Curry-Howard lifting of constructive proofs into runnable code (Verum / OCaml / Lean / Coq) via @extract / @extract_witness / @extract_contract plus the realize="<fn>" directive for native-binding wrappers.

Observability

• Obligation-level profiling — --profile-obligation breakdown with per-obligation timings.
• Solver diagnostic side channels — --dump-smt / --solver-protocol / --lsp-mode threaded through every solver adapter.
• core.verify stdlib — user-facing surface mirroring the compiler's VerificationLevel / ProofAttempt / VerificationOutcome / certificate-envelope types.
• SmtCertificate envelope v1 — schema_version gate, verum_version + created_at + free-form metadata, machine-checked schema validation on replay.
• 16-gate audit catalog — every claim mechanically enumerable; bundle aggregator produces L4 load-bearing verdict.

See also

• Architecture → trusted kernel (hardware/ABI perspective on the same kernel)
• Architecture → SMT integration (integration points for replacing backends)
• Language → refinement types (surface syntax)
• Tooling → CLI (verum verify, verum audit, verum smt-stats, verum smt-info)