# Contracts > Hard contracts (require / ensure / invariant) raise ContractViolation; soft contracts (check, check semantics) are monitored and never block. Where each runs. Contracts are how Sema makes a boundary — a function call, a `simulate` output, an FFI edge — into something that *holds*. Two families do two different jobs, and the distinction is the whole point: - **Hard contracts** — `require`, `ensure`, `invariant` — are **sound checks that block**. A failure raises a typed `ContractViolation` and the offending value cannot flow onward. - **Soft contracts** — `check`, `check semantics(...)` — are **monitored, graded, and never block**. Their `Sim` evidence travels with the value and feeds verification and monitors. Getting the choice right is what separates a guarantee from a note. ## Contracts are part of the public signature Signature-position contract clauses are part of the function's **public interface** — they are the cache key of Sema's incremental-verification economy, so a later `ensure` change is a signature diff, not a silent shift. ```sema def normalize(scores: list[f32]) -> list[f32]: require len(scores) > 0 ensure all(0.0 <= s <= 1.0 for s in result) # fatal, sound check check semantics("result preserves ranking order") # graded, carried as Sim metadata ... struct Account: balance: Money sem "Current settled account balance" invariant balance.minor_units >= 0 ``` - **`require`** — a precondition on the arguments; **boundary-only** (it appears in the signature, before the body). - **`ensure`** — a postcondition. In signature position, `result` names the return value. - **`invariant`** — a struct-level property that must hold for every value of the type; it is re-checked on every mutation. - **`check`** — graded, non-blocking; its result rides along as `Sim` metadata. ## Hard contracts — `require` / `ensure` / `invariant` Hard contracts are **sound**. Over SMT-decidable refinements they are discharged statically where possible; the residue becomes runtime checks **with blame**. When a hard contract fails at runtime it produces a typed `ContractViolation` value, and — this is the inversion of the "forward-runs-anyway" behavior of earlier neurosymbolic tools — **the raw result cannot flow onward**. A `ContractViolation` is not an exception you might swallow; it is a typed value that carries: - the failing field path (for boundary/field contracts) or the failed clause, - the enclosing struct descriptor and the callable descriptor, - the policy envelope, the raw and normalized values, and the blame party, - the stack trace. Every boundary is a **monitored contract boundary with party labels**, so blame provably lands on the *violator* — the caller for a broken `require`, the callee for a broken `ensure`. Blame routes the error message, the self-healing target, and cache invalidation. :::note[Statement-position contracts] Contract clauses may also appear **inside a body**. A mid-body `ensure ` is a sound checked assertion over locals — it participates in verification as a proof obligation and carries blame like any boundary check, but it is not part of the public signature (only signature-position clauses are cache keys). `require` is boundary-only. Statement-position `ensure`/`check` are also the assertion vocabulary inside `test` blocks — see [/neurosymbolic/verification/](/neurosymbolic/verification/). ::: ### There is no `assert` The Python `assert` is a **reserved, rejected token** with a machine-applicable fix-it to `ensure`/`check`. Python's `assert` strips under optimization and unwinds the stack, so a partly-compatible alias would train authors — and models emitting Sema — into the wrong semantics. The compiler teaches the right spelling instead: an `assert` in Sema source is a check-time error pointing you at `ensure` (sound, blocking) or `check` (graded, non-blocking). ## Soft contracts — `check` and `check semantics(...)` Soft contracts **never block**. A `check` clause's `Sim` result travels with the value as metadata; a `check semantics(...)` clause runs a calibrated verifier and journals graded evidence. That evidence: - feeds `sema assure` verdicts (it can push a verdict to *amber* — inadequate evidence), - feeds `monitor` channels for drift detection, - becomes repair context inside a `simulate def` / decode loop (the R3 stage), and - is recorded to the event log for the semantic debugger. Use `check semantics(...)` when meaning is the property and you want it *observed and verified* but not enforced as a blocking gate. This corpus example layers two soft semantic checks over a generated `Book`, against two different `verifier`-role judges: ```sema check semantics( "every substantive claim from paper is present in result with appropriate citation", paper, result, judge=claim_judge, alpha=0.01, ) check semantics( "result preserves the book's existing unrelated claims and remains coherent", book, paper, result, judge=coherence_judge, alpha=0.01, ) ``` ## Semantic assertions — the hard/soft split for meaning The statement-position forms generalize to **graded predicates**, and this is where the hard/soft distinction becomes load-bearing. Both build on the calibrated `Sim` of [/neurosymbolic/similarity/](/neurosymbolic/similarity/). - **Hard semantic assertion** — `ensure semantics("...", x, alpha=0.02)` (or any calibrated coercion in `ensure` position, e.g. `ensure draft ~= reference`). Legal **only under a calibrated judge** — an uncalibrated judge here is a compile error, not a silent downgrade. It fails as a `ContractViolation` carrying the judge's evidence, and the downstream region types `statistical(α)`. Every hard semantic assertion on a path joins the same **union-bound α accounting** as branch guards, and each is a calibrated decision site, so the monitor-or-decay rule applies exactly as at branches (see [/governance/monitor/](/governance/monitor/)). - **Soft semantic assertion** — statement-position `check semantics(...)`. It never blocks; its `Sim` evidence is journaled and feeds `assure`, monitors, and repair context. :::caution[A hard semantic `ensure` spends α] Because a calibrated `ensure semantics(...)` types the region `statistical(α)`, it consumes part of the site's α budget under the union bound — chaining several on one path can push the summed α past the declared budget, which is a compile error. A soft `check semantics(...)` spends nothing: it observes without guaranteeing. ::: ## Interpreted clauses — `ensure total` Two `ensure`-position forms are **interpreted by the toolchain** rather than evaluated as ordinary expressions: `ensure semantics(...)` above, and `ensure total` — a signature-position **totality claim** over the `require`-refined domain: for every argument satisfying the `require` clauses, evaluation terminates and produces a value of the return type. `require` clauses are domain refinements here, not exceptions. The claim is verified statically by `sema check` **and again at module registration** before any def can run — an unprovable claim is a loud error, never a silent acceptance. A verified clause is statically discharged: it never evaluates at runtime (`total` is not a value). Body-position `ensure total` is rejected, and a binding named `total` anywhere in scope makes the claim ambiguous — a loud error. The verified fragment is **exact arithmetic** — arbitrary-precision `int`, `bool`, `str`, exact collections and recursively-exact structs/enums, an explicit `!{}` row; no floats, no `while`, no recursion — with partiality discharged by `require` facts: `require len(xs) > 0` licenses `// len(xs)`, index-bound facts license `xs[i]`, `require k in d` licenses `d[k]`. ```sema def mean_floor(xs: list[int]) -> int !{}: require len(xs) > 0 # domain refinement — licenses // len(xs) ensure total # verified claim, statically discharged return sum(xs) // len(xs) def main() -> int !{}: return mean_floor([3, 4, 8]) # 5 ``` What `total` does **not** claim, stated exactly: - **`ResourceLimit` and memory exhaustion** are operational faults outside the semantic claim — the same status they hold in every proof assistant's extracted code. - **`ensure` postconditions** on a total def remain runtime-checked — a failure reports a bug; it is not admitted partiality. - **Dynamic type errors** inside bodies are the static type checker's dimension, progressively closed as it grows. ## Where each contract runs | Clause | Kind | Position | On failure | Guarantee | |---|---|---|---|---| | `require` | hard | signature (boundary) | `ContractViolation`, blames caller | `proved`/`checked` | | `ensure` | hard | signature or statement | `ContractViolation`, blames callee | `proved`/`checked` | | `invariant` | hard | struct, re-checked on mutation | `ContractViolation` | `proved`/`checked` | | `ensure semantics(...)` | hard | signature or statement | `ContractViolation` + evidence | `statistical(α)` | | `ensure total` | interpreted | signature only | `sema check` / load **error** if unprovable; never evaluated at runtime | `proved` | | `check` | soft | signature or statement | never blocks; `Sim` metadata | graded | | `check semantics(...)` | soft | signature or statement | never blocks; journaled evidence | graded | ## Over deterministic code, `semantics` becomes tests When a `semantics(...)` property guards **deterministic** code, the compiler does not insert a runtime judge call — it compiles the property into **targeted mutants plus killing tests**, a permanent deterministic artifact that `sema assure` runs. So a semantic contract over pure code costs nothing at runtime and everything at verification time. Full detail: [/neurosymbolic/verification/](/neurosymbolic/verification/). ## Failure modes - **Contract-passing garbage (a weak contract)** — mitigated by the mutation-adequacy gate in `sema assure gold`: a contract that kills no mutants is flagged. - **Brittle SMT proofs** — SMT is reserved for the runtime core; user code gets a gradual fallback (checked at runtime with blame) rather than a fragile proof. - **An uncalibrated `ensure semantics(...)`** — compile error, never a silent best-effort downgrade. ## How it is checked - `sema check` validates contract clauses, rejects `assert` with a fix-it, and errors on an uncalibrated hard semantic assertion or an α-budget overrun. - `sema assure [silver|gold]` fuzzes `ensure` postconditions and reports counterexamples; `check` evidence feeds amber verdicts; `gold` mutation-tests to catch weak contracts. See [/neurosymbolic/verification/](/neurosymbolic/verification/). - At runtime, a failed hard contract is a typed `ContractViolation` — handle it with `expect …/except`, described in [/language/error-handling/](/language/error-handling/). ## Where to go next - **How contracts are verified — grades, fuzzing, mutation:** [/neurosymbolic/verification/](/neurosymbolic/verification/). - **The typed-failure model behind `ContractViolation`:** [/language/error-handling/](/language/error-handling/). - **The calibrated `Sim` that semantic contracts return:** [/neurosymbolic/similarity/](/neurosymbolic/similarity/).