Contracts

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.

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.

Statement-position contracts

Contract clauses may also appear inside a body. A mid-body ensure <expr> 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/.

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:

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

• 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/).
• Soft semantic assertion — statement-position check semantics(...). It never blocks; its Sim evidence is journaled and feeds assure, monitors, and repair context.

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

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

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 <project> [silver|gold] fuzzes ensure postconditions and reports counterexamples; check evidence feeds amber verdicts; gold mutation-tests to catch weak contracts. See /neurosymbolic/verification/.
• At runtime, a failed hard contract is a typed ContractViolation — handle it with expect …/except, described in /language/error-handling/.

Where to go next

• How contracts are verified — grades, fuzzing, mutation: /neurosymbolic/verification/.
• The typed-failure model behind ContractViolation: /language/error-handling/.
• The calibrated Sim that semantic contracts return: /neurosymbolic/similarity/.