`Verum.toml` — Manifest Reference

The canonical project manifest is Verum.toml. The CLI also reads the legacy verum.toml spelling, preferring the canonical file when both exist. Project scaffolding still writes the lowercase spelling. Keep one manifest per project.

This page describes the host CLI schema. The Verum-side core.cog.manifest API has a separate schema and is not the parser used by the host CLI.

Minimal example

[cog]
name    = "my-project"
version = "0.1.0"

[language]
profile = "application"

`[cog]` — package identity

[cog]
name        = "my-project"           # required
version     = "0.1.0"                # required
authors     = ["Alice <a@example.com>"]
description = "A short description"
license     = "MIT OR Apache-2.0"
homepage    = "https://example.com"
repository  = "https://github.com/me/my-project"
keywords    = ["web", "async"]
categories  = ["network"]

The [cog] section is for metadata only. edition, profile, rust-min, readme, documentation, and verification are not recognised fields — the corresponding concepts live in the sections below.

`[language]` — language profile

[language]
profile = "application"          # application | systems | research

Profile	Unsafe	Dependent types	Target audience
`application` (default)	—	opt-in	~80 % of users — no `unsafe`, refinements + runtime checks
`systems`	✓	✓	allocators, drivers, OS code
`research`	✓	✓ + required verification	proof-heavy code

`[dependencies]`, `[dev_dependencies]`, `[build_dependencies]`

[dependencies]
serde  = "1.4"
tokio  = { version = "2.0", features = ["rt"] }
mylib  = { path = "../mylib" }
data   = { git = "https://github.com/me/data", rev = "abc123" }

[dev_dependencies]
criterion = "0.5"

[build_dependencies]
codegen = "0.2"

Note the underscore spelling: dev_dependencies, not dev-dependencies.

Detailed dependency fields: version, path, git, branch, tag, rev, features, optional, and default-features (alias default_features). Unknown fields are rejected, including ipfs, registry, package, and workspace.

For source publication, every entry in [dependencies] needs an explicit valid version requirement. Detailed entries preserve the feature list and both Boolean options. Source fields (path, git, branch, tag, rev) are refused even when a version is present; publication does not rewrite them. An explicit "*" is accepted, while a missing version is an error. See Cog packages.

Version specifiers follow SemVer:

"1.4" — ^1.4 (>= 1.4.0, < 2.0.0).
"=1.4.2" — exactly 1.4.2.
"~1.4.2" — >= 1.4.2, < 1.5.0.
">=1.4, <2.0" — explicit range.

`[features]`

[features]
default = ["std", "tls"]
std     = []
tls     = ["openssl"]
gpu     = ["opencl"]

The CLI accepts verum build --features gpu and --all-features. Publication preserves feature declarations and dependency options. Consumer activation of optional dependencies, default features, and transitive feature unification is not yet fully integrated; declaring these fields does not establish that all dependency edges will be selected correctly.

`[build]` — basic build settings

[build]
target        = "native"             # or a target triple
opt_level     = 2                    # 0-3
incremental   = true
lto           = false                # bool here; use [lto] for strategies
codegen_units = 16
panic         = "unwind"             # unwind | abort

`[profile.dev]`, `[profile.release]`, `[profile.test]`, `[profile.bench]`

Per-profile overrides. Each profile carries:

[profile.release]
tier             = "1"               # "0" interpreter | "1" aot (aliases accepted)
verification     = "certified"       # see "verification levels" table below
opt_level        = 3
debug            = false
debug_assertions = false
overflow_checks  = false
lto              = true
incremental      = false
codegen_units    = 1
cbgr_checks      = "optimized"       # all | optimized | proven

tier accepts the strings "0", "interpreter", "interp" for interpreter mode and "1", "aot", "release", "native" for AOT.

Verification levels — fourteen-strategy ladder

The verification field of every profile (and default_strategy of [verify] below) accepts one of fifteen lowercase strings: the fourteen verification strategies admitted by the grammar plus the tooling-side-only none sentinel. Strategies are ordered on a strictly monotone ν-ordinal ladder so promotions are always checked in one direction (lax → strict).

Value	ν-ordinal	Strategy	When to pick
`none`	—	Unchecked (tooling-only sentinel — does not correspond to a `@verify(...)` attribute)	Never auto-selected; only by explicit override.
`runtime`	0	Runtime assertions; no formal proof	Default for the `application` profile.
`static`	1	Dataflow + CBGR	Trivially decidable refinements without SMT.
`fast`	2	Capability router with reduced timeout (≤ 100 ms / goal)	UNKNOWN-tolerant; iterative development.
`complexity_typed`	< ω (n)	Bounded-arithmetic verification (V₀ / V₁ / S¹₂ / V_NP / V_PH / IΔ₀); polynomial-time; CI ≤ 30 s	Crypto protocols, real-time, embedded.
`formal`	ω	Full SMT verification (default strategy)	Default `dev` for `research` profile.
`proof`	ω + 1	User tactic block + kernel re-check (dominates SMT; admits induction)	Theorems / foundational lemmas.
`thorough`	ω · 2	Portfolio race with extended timeout; mandatory `decreases` / `invariant` / `frame`	Catches missing specs.
`reliable`	ω · 2 + 1	`thorough` + cross-solver agreement: two adapters must both return UNSAT	UNKNOWN on disagreement.
`certified`	ω · 2 + 2	`reliable` + certificate materialisation + multi-format export	Default `release` for `research` profile; required for `.verum-cert` export (Coq / Lean / Dedukti / Metamath).
`coherent_static`	ω · 2 + 3	Weak operational coherence — α-cert + symbolic ε-claim; polynomial in `\|P\|·\|φ\|`; CI ≤ 60 s	Production fallback for coherence-required code.
`coherent_runtime`	ω · 2 + 4	Hybrid operational coherence — α-cert + runtime ε-monitor; trace-bounded; CI ≤ 5 min	Hybrid coherence; runtime monitoring acceptable.
`coherent`	ω · 2 + 5	Strict operational coherence — α/ε bidirectional check; single-exponential; CI ≤ 30 min	Critical-safety code requiring full operational coherence.
`synthesize`	≤ ω · 3 + 1	Inverse proof search (synthesis); holes filled by capability-router-dispatched SyGuS adapter	Cost is unbounded — opt-in only.
`assume`	—	No verification is performed — escape hatch off the ladder	Audit-tracked via `verum audit --assumptions`; use only when the obligation is established outside the verification pipeline.

Direction — @verify(proof) on a function compiling under @verify(runtime) is always accepted (lax → strict, monotone in ν-ordinal). The reverse requires re-proof and is rejected by the level-inference pass.

See Gradual verification for the full ν-coordinate ordering, capability-router dispatch table, and cost / completeness trade-off per strategy.

`[verify]` — formal verification

[verify]
# Base behaviour
default_strategy      = "formal"          # runtime | static | formal | fast |
                                          # thorough | certified | synthesize
solver_timeout_ms     = 10_000
enable_telemetry      = true              # write .verum/state/smt-stats.json
persist_stats         = true
fail_on_divergence    = true              # certified + cross-verifier divergence = build fail

# Budget / profiling knobs — see `docs/verification/performance.md` and
# `docs/verification/cli-workflow.md` for the workflow.
total_budget            = "120s"          # fail the build past this wall-clock
slow_threshold          = "5s"            # flag functions slower than this
profile_slow_functions  = true            # enable profiler when --profile given
profile_threshold       = "1s"            # only profile functions past this

# On-disk cache
cache_dir               = ".verum/verify-cache"
cache_max_size          = "500MB"
cache_ttl               = "30d"           # evict entries older than this

# Shared CI cache — S3 or Redis, reads + writes proofs across runs.
distributed_cache       = "s3://my-bucket/verify-cache"

# Per-module override: narrower scope than top-level [verify].
[verify.modules."crypto.signing"]
strategy                = "certified"
solver_timeout_ms       = 60_000

# Named profiles — selected via `verum verify --verify-profile <name>`.
# Inheritance: CLI flag > profile > [verify] > default.
[verify.profiles.release]
default_strategy        = "certified"
solver_timeout_ms       = 300_000
fail_on_divergence      = true

[verify.profiles.ci]
default_strategy        = "fast"
solver_timeout_ms       = 3_000
total_budget            = "60s"

Strategy-specific timeout multipliers: fast 0.3×, thorough 2×, certified 3×, synthesize 5×.

Precedence (highest → lowest):

CLI flag (--solver, --timeout, --budget, --distributed-cache, …).
Active [verify.profiles.<name>] if --verify-profile <name> is set.
Per-module override in [verify.modules."module.path"] (for functions that live in that module and its descendants).
Top-level [verify].
Built-in default.

Human-readable durations: s, m, h, d suffixes (or a bare integer = seconds).

`[verify.solver]` — solver tuning

Direct passthroughs to the backend configs (Z3Config, Cvc5Config) and the intermediate verifier configs — see Architecture → SMT integration → Configuration knobs for the full matrix and which solver-adapter parameter scope each setting reaches.

A misspelled key here is an ERROR, not a shrug

[verify.solver] and its sub-tables deserialize with deny_unknown_fields. Writing [verify.solver.sep-logic] (hyphen) or max_unfoldng_depth fails the manifest parse and names the offender, rather than being dropped.

Two consequences worth knowing:

A partial table is fine. Every field defaults, so [verify.solver.qe] simplify_level = 0 leaves the other six keys of that table — and the other nine tables — exactly as they were.
The values are read once, early. verum build and verum verify install this block before any verification work begins; the solver layer refuses a later install rather than let one component run on the manifest and another on the defaults.

[smt], [smt.fallback], [smt.portfolio] and [smt.validation] appear in verum_smt's own Rust doc-comments. They are NOT an alternative spelling for a project manifest: that loader (SmtConfig::from_toml_file) reads a standalone file and is called from one example programme. In a Verum.toml, [verify.solver.*] is the surface.

[verify.solver]
# Solver selection
backend                 = "auto"          # auto | auto | portfolio | capability_router

# Z3 context tuning — `verum_smt::z3_backend::Z3Config`
[verify.solver.z3]
enable_proofs           = true
minimize_cores          = true
enable_interpolation    = false
global_timeout_ms       = 30_000          # context-level cap (Config::set_timeout_msec)
memory_limit_mb         = 8_192           # process-wide (set_global_param)
enable_mbqi             = true
enable_patterns         = true
random_seed             = 42              # reproducibility (smt.random_seed)
auto_tactics            = true            # auto_config Config param

# cvc5 adapter tuning — `verum_smt::cvc5_backend::Cvc5Config`
# (this used to repeat the `[verify.solver.smt-backend]` header above,
#  which is a duplicate-key error: two backends with different fields
#  cannot share one table)
[verify.solver.cvc5]
logic                   = "ALL"           # ALL | QF_LIA | QF_LRA | QF_BV |
                                          # QF_NIA | QF_NRA | QF_AX |
                                          # QF_UFLIA | QF_AUFLIA
timeout_ms              = 30_000          # tlimit-per
incremental             = true
produce_models          = true
produce_proofs          = true
produce_unsat_cores     = true
preprocessing           = true            # preprocess-only=false
quantifier_mode         = "auto"          # none | ematching | cegqi | mbqi | auto
random_seed             = 42
verbosity               = 0               # 0–5, saturates at 5

# Quantifier elimination
[verify.solver.qe]
timeout_ms              = 5_000
simplify_level          = 2               # 0=skip | 1=simplify | 2=+propagate-values | 3=+ctx-simplify
use_qe_lite             = true
use_qe_sat              = true
use_model_projection    = true
use_skolemization       = true

# Interpolation
[verify.solver.interpolation]
algorithm               = "MBI"           # McMillan | Pudlak | Dual | Symmetric | MBI | PingPong | Pogo
strength                = "balanced"      # weakest | balanced | strongest
simplify                = true
timeout_ms              = 5_000
quantifier_elimination  = true            # if false, project_onto_shared returns input verbatim
max_projection_vars     = 100             # MBI bails when elimination set exceeds this

# Static verification (bounds elimination)
[verify.solver.static]
timeout_ms              = 30_000          # global
constraint_timeout_ms   = 100             # per-constraint
enable_proofs           = true
enable_unsat_cores      = true
minimize_cores          = true
enable_caching          = true
max_cache_size          = 10_000
auto_tactics            = true
memory_limit_mb         = 4_096

# Bisimulation
[verify.solver.bisimulation]
max_depth               = 100
timeout_ms              = 30_000
generate_counterexamples = true
infinite_strategy       = "bounded_unfolding"  # coinduction | up_to | bounded_unfolding

# Separation logic
[verify.solver.sep_logic]
entailment_timeout_ms   = 5_000
max_unfolding_depth     = 10
enable_frame_inference  = true            # set false to skip residual computation (~30% encoder reduction)

# Unsat-core extraction
[verify.solver.unsat_core]
minimize                = true
quick_extraction        = false
max_iterations          = 100
timeout_ms              = 10_000
proof_based             = false

# Optimizer (MaxSAT, Pareto)
[verify.solver.optimizer]
incremental             = true            # if false, push/pop are no-ops
max_solutions           = 100             # Pareto-front cap; the field is
                                          # `Maybe<usize>`, so a negative
                                          # sentinel cannot parse — omit the
                                          # key for the default, which is 100
                                          # (`unwrap_or(100)`), NOT unbounded
timeout_ms              = 30_000
enable_cores            = true
method                  = "lexicographic" # lexicographic | pareto | independent | box

# Parallel portfolio
[verify.solver.parallel]
num_workers             = 8
timeout_ms              = 30_000
enable_sharing          = true            # broader gate over enable_lemma_exchange
enable_lemma_exchange   = true            # effective only when enable_sharing is also true
race_mode               = true
lemma_exchange_interval_ms = 500
max_lemmas_per_exchange = 10
enable_cube_and_conquer = false
cubes_per_worker        = 4

# Verification cache (cross-build SMT result reuse)
[verify.solver.cache]
max_size                = 2_000           # entries
max_size_bytes          = "500MB"
ttl                     = "30d"
statistics_driven       = true            # cache only expensive queries
min_decisions_to_cache  = 1_000
min_conflicts_to_cache  = 100
min_solve_time_ms       = 100

Solver parameter-scope discipline

Each tunable in this section is wired to a specific scope inside the SMT layer (process-global, per-context, or per-query). The mapping is not interchangeable — assigning a parameter at the wrong scope can silently no-op. The verifier picks the correct scope per key, and the operator's manual at Verification → Solver tuning → Parameter-scope discipline documents every knob the manifest exposes.

Recap: how the manifest reaches the solver

The full chain when you set a value in verum.toml:

Verum.toml [verify.solver.<sub>]
    ↓ (VerifyConfig.solver — verum_cli::config)
verum_smt::config::install(…)   ← once, before any verification work
    ↓ (verum_smt::config::effective)
Subsystem constructors (QuantifierEliminator::new, StaticVerifier,
                        SeparationLogic::new, SepLogicEncoder::new)
    ↓ (consulted by the verifier method)
Backend config (verum_smt::z3_backend::Z3Config,
                verum_smt::cvc5_backend::Cvc5Config)
    ↓ (per-call wiring on each fresh solver)
Adapter Params / SMT-LIB options

Default::default() is deliberately NOT rerouted through the installed configuration — only the new() constructors consult it. A test or a caller that asks for the literal defaults still gets them, whatever a manifest elsewhere says.

An earlier revision of this page claimed every field in the chain had been audited for "set but never read". That audit measured the arrows below the first one and not the first one itself, which was the arrow that did not exist.

`[workspace]`

[workspace]
members = ["core", "api", "cli"]
exclude = ["vendor/*"]

`[registry]`

[registry]
index = "https://registry.example.com"

Supply your registry's base URL without /api/v1; package commands append the API path. publish, search, and install read this setting from the active manifest. Set it explicitly because projectless and manifest-backed defaults differ. An invalid manifest is reported instead of selecting a fallback registry. See Cog packages for the publication workflow and its limits.

Language-feature sections

Nine orthogonal sections each gate a subsystem. Every field defaults to a sensible value; include only the ones you want to change.

`[types]`

[types]
dependent              = true
refinement             = true
cubical                = true
higher_kinded          = true
universe_polymorphism  = false       # opt-in; rare & costly
coinductive            = true
quotient               = true
instance_search        = true
coherence_check_depth  = 16

`[runtime]`

[runtime]
cbgr_mode            = "mixed"       # managed | checked | unsafe | mixed
async_scheduler      = "work_stealing"  # single_threaded | multi_threaded | work_stealing
async_worker_threads = 0             # 0 = logical CPU count
futures              = true
nurseries            = true
task_stack_size      = 0             # 0 = OS default
heap_policy          = "adaptive"    # aggressive | conservative | adaptive
panic                = "unwind"      # unwind | abort

`[codegen]`

[codegen]
tier                    = "aot"      # interpret | aot | check
mlir_gpu                = false      # MLIR path for @device(GPU) code
gpu_backend             = "auto"     # auto | metal | cuda | rocm | vulkan
monomorphization_cache  = true
proof_erasure           = true
debug_info              = "line"     # none | line | full
tail_call_optimization  = true
vectorize               = true
inline_depth            = 3

`[meta]`

[meta]
compile_time_functions  = true
quote_syntax            = true
macro_recursion_limit   = 128
reflection              = true
derive                  = true
max_stage_level         = 2          # 0=runtime, 1=meta fn, 2+=multi-stage

`[protocols]`

[protocols]
coherence                 = "strict"       # strict | lenient | unchecked
resolution_strategy       = "most_specific" # most_specific | first_declared | error
blanket_impls             = true
higher_kinded_protocols   = true
associated_types          = true
generic_associated_types  = true

`[context]`

[context]
enabled              = true
unresolved_policy    = "error"       # error | warn | allow
negative_constraints = true
propagation_depth    = 32

`[safety]`

[safety]
unsafe_allowed       = true
ffi                  = true
ffi_boundary         = "strict"      # strict | lenient
capability_required  = false
mls_level            = "public"      # public | secret | top_secret
forbid_stdlib_extern = false

`[test]`

[test]
differential     = false             # VBC vs LLVM AOT must agree
property_testing = true
proptest_cases   = 256
fuzzing          = false
timeout_secs     = 60
parallel         = true
coverage         = false
deny_warnings    = false

`[debug]`

Debug Adapter Protocol (DAP) configuration for IDE integration.

[debug]
dap_enabled        = true
step_granularity   = "statement"     # statement | line | instruction
inspect_depth      = 8
port               = 0              # 0 = auto-pick; used when --transport socket
show_erased_proofs = false

verum dap refuses to start when dap_enabled = false.

`[linker]` — native linking

Full linker control (parsed by verum_compiler):

[linker]
output            = "executable"     # executable | shared | static | object
lto               = "thin"           # none | thin | full
use_lld           = true             # default true on Linux, false elsewhere
pic               = true
strip             = false
strip_debug_only  = false
debug_info        = true
static_link       = false
entry_point       = "main"
target            = "native"
library_paths     = ["/usr/local/lib"]
libraries         = ["ssl", "crypto"]
exports           = ["verum_init"]
extra_flags       = ["-Wl,--gc-sections"]

[linker.linux]
library_paths     = ["/opt/local/lib"]
libraries         = ["dl"]

[linker.macos]
extra_flags       = ["-framework", "CoreFoundation"]

[linker.windows]
libraries         = ["kernel32", "user32"]

Profile-scoped overrides:

[profile.release.linker]
lto               = "full"
strip             = true

`[llvm]`, `[optimization]`, `[lto]`, `[pgo]`, `[cross_compile]`

LLVM backend fine-tuning. These sections let you control the native code generator beyond what [build] exposes.

[llvm]
target_triple    = "x86_64-unknown-linux-gnu"   # override `[build].target` for LLVM
target_cpu       = "native"                     # "native" | "generic" | "znver3" | …
target_features  = "+avx2,+fma"                 # comma-separated, `+`/`-` prefixed

[optimization]
level    = 3           # 0–3, orthogonal to `[build].opt_level` when you need
size_opt = false       # to diverge from the CLI's debug/release mapping
inline   = true

[lto]
enabled = true
mode    = "thin"       # "thin" (fast, moderate wins) | "full" (slow, maximum wins)

[pgo]
enabled      = true
profile_path = "target/pgo/default.profdata"

[cross_compile]
target  = "aarch64-apple-darwin"
sysroot = "/opt/xcode-sdks/MacOSX.sdk"
linker  = "clang"

[cross_compile] is parsed and validated, but nothing yet wires target / sysroot / linker into the toolchain invocation — setting it is observed (a build emits a debug-log line noting the values) and otherwise has no effect. The active cross-compile path is [llvm].target_triple or the --target CLI flag; sysroot and linker have no working manifest equivalent yet — pass them to your system linker the way you would for any other cross-compiled toolchain (see Installation → Cross-compiling Verum programs).

CLI equivalents (build-time):

TOML field	CLI flag
`[build].target`, `[llvm].target_triple`	`--target TRIPLE`
`[optimization].level`, `[build].opt_level`	`--release` (= 3)
`[lto].enabled` + `[lto].mode`	`--lto thin\|full`
`[build].incremental`	`--timings` triggers report when enabled
static linking	`--static-link`
stripping	`--strip` / `--strip-debug`
emit artefacts	`--emit-asm`, `--emit-llvm`, `--emit-bc`, `--emit-types`, `--emit-vbc`

CLI flags always override the manifest for the current build; verum.toml values describe the project baseline. [cross_compile] is the exception — per the note above, it doesn't reach the build at all yet.

`[lint]` — linter policy

The [lint] section drives verum lint. It supports per-rule severity, profiles, per-file overrides, named architecture layers, naming-convention enforcement, plus refinement / capability / context / CBGR-tier / verification policies that are unique to Verum.

[lint]
extends  = "recommended"          # minimal | recommended | strict | relaxed
disabled = []
denied   = ["deprecated-syntax"]

[lint.severity]
unused-import     = "warn"
deprecated-syntax = "error"

[lint.rules.large-copy]
size-threshold-bytes = 256
exempt-types         = ["UserId", "Hash"]

[lint.per_file_overrides]
"tests/**" = { allow = ["unused-result", "todo-in-code"] }

[lint.architecture.layers]
core   = { allow_imports = ["core", "std"] }
domain = { allow_imports = ["core", "std", "domain"] }

[lint.refinement_policy]
public_api_must_refine_int   = true
require_verify_on_refined_fn = true

[lint.context_policy.modules]
"core.*" = { forbid = ["Database", "Logger", "Clock"] }

Full schema, every knob, every preset and the precedence stack: Reference → Lint configuration.

`[profile]` — per-build-kind compilation settings

Four sub-tables, one per build kind: [profile.dev], [profile.release], [profile.test], [profile.bench]. Each carries the same ten keys.

[profile.release]
tier              = "1"          # "0" (interpreter) | "1" (AOT)
verification      = "static"     # none | runtime | static | fast
opt_level         = 3            # 0..3
debug             = false
debug_assertions  = false
overflow_checks   = false
lto               = true
incremental       = false
codegen_units     = 1            # omit for the compiler's choice
cbgr_checks       = "optimized"  # all | optimized | proven | audit-points

tier is written as the string "0" or "1"; "interpreter", "interp", "aot", "release" and "native" are accepted aliases. verification is lowercase; cbgr_checks is kebab-case, matching the three-tier reference model — optimized lets escape analysis elide what it can prove, proven checks only what it could not, and audit-points restricts checks to boundary points.

Every key is optional and every sub-table is optional: an absent [profile.release] gets the compiler's defaults, which are what verum build --release uses today.

`[lsp]`

[lsp]
enable_cost_hints = true             # show CBGR tier / refinement costs inline
validation_mode   = "incremental"    # incremental | batch
auto_import       = true
format_on_save    = false

`Verum.lock`

Generated automatically. Pins exact versions of all transitive dependencies. Commit for binary projects; optional for libraries.

CLI overrides (`-Z`)

Any manifest value can be overridden at the command line without editing the file:

verum build -Z codegen.tier=interpret -Z safety.unsafe_allowed=false
verum run --no-cubical -Z runtime.cbgr_mode=unsafe
verum test -Z test.parallel=false -Z test.timeout_secs=120

Precedence (low → high):

Built-in defaults
verum.toml values
High-level CLI flags (--tier, --no-cubical, --cbgr, --gpu)
-Z KEY=VALUE overrides

Invalid keys produce a descriptive error listing all valid prefixes. Typos trigger "did you mean" suggestions via edit distance.

Inspecting & validating

verum config show              # human-readable resolved feature set
verum config show --json       # machine-readable JSON
verum config validate          # exit 0 on valid, non-zero with diagnostics

verum config show displays every flag's effective value after all overrides are applied, so you can verify that your -Z flags and verum.toml produce the expected configuration.

Minimal example​

[cog] — package identity​

[language] — language profile​

[dependencies], [dev_dependencies], [build_dependencies]​

[features]​

[build] — basic build settings​

[profile.dev], [profile.release], [profile.test], [profile.bench]​

Verification levels — fourteen-strategy ladder​

[verify] — formal verification​

[verify.solver] — solver tuning​

Recap: how the manifest reaches the solver​

[workspace]​

[registry]​

Language-feature sections​

[types]​

[runtime]​

[codegen]​

[meta]​

[protocols]​

[context]​

[safety]​

[test]​

[debug]​

[linker] — native linking​

[llvm], [optimization], [lto], [pgo], [cross_compile]​

[lint] — linter policy​

[profile] — per-build-kind compilation settings​

[lsp]​

Verum.lock​

CLI overrides (-Z)​

Inspecting & validating​

See also​