# Verification and assure > Verification is default-on (testable is retired). sema assure bronze|silver|gold — ensure property fuzzing, counterexamples, mutation testing, and test blocks. Sema treats verification as the *default*, not an opt-in. Weak or absent tests systematically launder wrong model-written code as correct, and an opt-in flag recreates exactly that failure mode — so Sema retired it. **Every function is verified by default; the depth is a dial.** This page covers the `assure` grades, `ensure` property fuzzing with counterexamples, mutation testing, and `test` blocks. ## Default-on verification The old `testable` keyword (an opt-in *gate*) is **retired**. There is nothing to turn on. Instead you choose a grade, and you can override it per function or, rarely, opt a scratch function out explicitly: ```sema assure silver # module-level grade: bronze | silver | gold @assure(gold) # per-function override def reconcile(ledger: Ledger) -> Ledger: ... @no_verify("scratch") # explicit, greppable, release-build-rejected opt-out def sketch(): ... ``` `@no_verify` is loud, greppable, and **rejected in release builds** — you cannot ship unverified code by omission, only by a conspicuous, reviewable annotation. ## The grades Verification runs a layered engine (deterministic checks → deterministic-adversarial properties/fuzzing/mutation → statistical verifiers → background adversarial). The three grades expose it as a dial: | Grade | What it runs | |---|---| | **bronze** | deterministic checks + authored `test` blocks (L0 + L1.1) | | **silver** | bronze + `ensure` property fuzzing (concolic falsification) | | **gold** | silver + a mutation-adequacy threshold + SMT proof of selected properties | :::caution[silver+ requires an explicit effect row] Effect-row **inference** is a `bronze` ergonomic. At `silver` and above, every declared function must state its `!{...}` row explicitly (`sema check` errors otherwise), so the published surface — the verification cache key and the caller contract — states the row, and a later `code.exec` shows up as a *signature diff*, not a silent change. `simulate`/`by` defs, `ported` defs, and `provide` are exempt because their row is derived. And `!{*}` (all-effects top) is warned at `bronze`, errored at `silver`+. ::: ## Verdicts are three-state Verification does not answer yes/no. It answers in three states: - **red** — a replayable counterexample with blame. - **amber** — *inadequate evidence*, a first-class compiler output. A green verdict is impossible on a weak suite by construction, so "we couldn't confirm this" is a real, honest answer rather than a false green. - **green** — counterexample-free *at a stated mutation score*. ## `ensure` property fuzzing and counterexamples Every function with an `ensure` postcondition is **fuzzed**: `sema assure` generates inputs from the parameter types (`int`/`float`/`bool`/`str`/`list[int]`), calls the function many times, and reports any violated `ensure` **with the concrete counterexample**. Self-referential algebraic properties work naturally: ```sema def add(a: int, b: int) -> int: ensure add(a, b) == add(b, a) # commutativity, fuzzed at silver return a + b ``` This works because contracts are enforced only at the *outermost* call: a function invoked *inside* a contract's evaluation runs its body but skips its own contracts (a `contract_depth` guard), so properties neither recurse nor re-check. Structural laws attach to types too — every decode-target type carries `law roundtrip: parse[T](serialize(v)) == Ok(v)`, discharged by this same property engine (see [/neurosymbolic/schemas/](/neurosymbolic/schemas/)). ## Mutation testing at `gold` `gold` adds a **mutation-adequacy gate**. The program is systematically mutated (binary operators flipped, int/bool literals nudged), and the tests plus properties are re-run against each mutant. A mutant that still passes everything **survived** — it exposes a gap in your checks. The score is *killed / total*, gated at **≥50%** for gold. This is the mechanism that makes a green verdict trustworthy: a stub or a weak contract can't kill spec-relevant mutants, so it can't earn green. Properties kill far more mutants than unit tests, which is why property-first verification is the default posture. :::note[Semantic properties over deterministic code become mutants] A `semantics("concern", …)` declaration guarding **deterministic** code does not compile to a runtime judge call — it compiles into targeted mutants plus killing tests, a permanent deterministic artifact. So a natural-language property becomes part of the mutation-adequacy gate. See [/neurosymbolic/contracts/](/neurosymbolic/contracts/). ::: ## `test` blocks — the author's voice Retiring the opt-in gate did not remove authored tests. `test` declares a named, deterministic verification entry point — the human-authored leg of the engine, alongside ghostwritten properties and trait laws: ```sema test "reconcile matches identical bank lines exactly": lines = [bank_line("acme", 120_00), bank_line("acme", 120_00)] ledger = [entry("acme", 120_00)] result = reconcile(lines, ledger)? ensure len(result.matched) == 1 # statement-position ensure is the assertion form ensure result.unmatched == [] check semantics("the match decision is explainable from amounts alone", result) ``` A `test` body is ordinary code. Its assertions are **statement-position `ensure`** (sound, blamed) and **`check`** (graded evidence) — there is no separate assertion vocabulary, so test expectations are the same contract machinery the rest of the language verifies (see [/neurosymbolic/contracts/](/neurosymbolic/contracts/)). A `?` in a test body fails the test with the propagated typed error as its evidence. Tests are **module-private**, excluded from release codegen and the public signature, and compiled only under verification profiles. A test whose effect row includes `model.invoke` **replays from the content-addressed cache** and never blocks a build on model availability — a cold cache is an authoring event, not a build step. Authored tests feed the **same mutation-adequacy gate** as synthesized ones — a test that kills no mutants and adds no coverage is flagged by the degenerate-body lint, so hand-written suites cannot launder a green verdict. :::tip[Counterexamples become regressions] The flow runs backward too: a red verdict's replayable counterexample can be materialized as a `test` declaration with `sema assure --materialize`, turning every falsification into a permanent regression. (Materialization is the remaining piece of the engine.) ::: ## Completeness — no silent stubs Completeness checking is folded in. Typed holes (`todo`) are first-class and tracked; **release builds reject reachable holes**. Degenerate bodies — constant-return, parameter-ignoring, catch-and-swallow — are decidable lints. Semantic completeness *is* mutation adequacy: a stub can't kill spec-relevant mutants. Honesty is cheaper than faking, by construction — this is the same ethos as the no-silent-no-op guard in [`sema check`](/start/toolchain/). ## Running it ```bash # module-level grade is honored; override with --grade sema assure examples/finops-ledger sema assure examples/finops-ledger --grade gold ``` Grades gate the exit code: `bronze` needs tests to pass; `silver` adds properties; `gold` adds the mutation threshold. Verification is **incremental** — a body edit that preserves the contract never invalidates callers' memos, which is what makes default-on affordable. ## Failure modes - **All-`Option` schema / weak contract** → amber, or a survived mutant at `gold`; `sema doctor` flags all-optional decode targets. - **A `test` that asserts nothing meaningful** → flagged by the degenerate-body lint; it cannot produce green. - **`silver`+ with an inferred effect row** → `sema check` error; state the row. - **Reachable `todo` in a release build** → rejected. ## How it is checked - `sema check` enforces the explicit-effect-row rule at `silver`+, the `!{*}` policy, and the reachable-hole/degenerate-body lints. - `sema assure [bronze|silver|gold]` runs the layered engine — `test` blocks, `ensure` fuzzing with counterexamples, and (at `gold`) mutation adequacy — replaying model calls from cache. - The full command surface lives in the [toolchain guide](/start/toolchain/) and the [CLI reference](/reference/cli/). ## Where to go next - **The toolchain and the edit → check → assure workflow:** [/start/toolchain/](/start/toolchain/). - **The complete command reference:** [/reference/cli/](/reference/cli/). - **The contracts this engine verifies:** [/neurosymbolic/contracts/](/neurosymbolic/contracts/).