Verification and assure

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:

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

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:

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/).

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.

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/.

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:

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/). 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.

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.

Running it

# 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 <project> [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 and the CLI reference.

Where to go next

• The toolchain and the edit → check → assure workflow: /start/toolchain/.
• The complete command reference: /reference/cli/.
• The contracts this engine verifies: /neurosymbolic/contracts/.