Policies

A policy is Sema’s native governance construct: an analyzable, compile-checked decision layer that grants and confines the capabilities code may exercise. Where effect rows state what a function wants to do, a policy states what the surrounding scope will permit — and it does so in the type system, so denial is a compile error or a typed value, not a runtime surprise.

Policies key on typed effects, never command strings. Every string-matching gate in a conventional harness (“block rm -rf”, “deny URLs matching this regex”) is respellable and bypassable; a policy on code.exec or net.connect("host") is not.

Why policies are in the language

In a typical LLM harness the safety rules — “never open a socket”, “don’t run shell”, “only this endpoint” — live in review comments, a linter, or a runtime sandbox. They are outside the code’s type, reimplemented per tool, and bypassable by construction. Prompt injection is especially corrosive here: an untrusted model output that reaches a shell is a breach, and the language cannot see it coming.

Sema makes the rules first-class. A policy is (a) an effect/capability restriction checked by the type system — code under a policy cannot reach a forbidden capability by reachability, including through closures (capture checking) — and (b) a Cedar-shaped, total, non-Turing-complete, analyzable decision layer for runtime grants (forbid overrides permit). Prompt injection stops being a breach and becomes “a denied request with an audit trail.”

Syntax

A policy declares allow: and forbid cap: rules, embedded examples: that are verified at load, and a mandatory justification surfaced in every denial:

policy NoExecFromGen:
    allow:
        fs.read("data/**")
    forbid cap:
        code.exec, proc.spawn
        net.connect except "api.internal:443"
    examples:
        deny:
            os.exec(generated_cmd)      # verified as code.exec at compile time
        allow:
            fetch("https://api.internal:443/v1")
    justification "generated artifacts must never gain execution authority"

The block forms (allow: / forbid cap: / examples: on their own indented lines) are the idiomatic spelling and what the corpus uses. They are pure sugar: allow: followed by effect-list rows expands to one allow rule per row, forbid cap: expands to forbid cap ... rules, and examples: expands to example allow: / example deny: cases. Commas separate items inside one row; new rows keep diagnostics local. The inline form (allow eff, eff) stays legal and is the canonical AST the formatter prints.

Attaching a policy: three scopes

A policy takes effect where it is attached. There are three code-level attachment sites (plus the manifest root, sema.toml [policy] root):

Declaration (a decorator). @PolicyName on a def or simulate def confines that declaration:

@NoExecFromGen
simulate def draft_migration(req: Request) -> MigrationPlan by models.writer: ...

Block (with policy(...)). A lexical scope confined for its dynamic extent:

with policy(NoExecFromGen):
    run_pipeline(inputs)

Module (@Policy or policy attach). A module-level attachment confines every declaration in the module.

Rules reference effect instances

Rules match parameterized effects, so a policy can be precise about endpoints and paths rather than all-or-nothing:

allow:
    net.connect("api.internal:443")
    fs.read("data/**")
forbid cap:
    net.connect except "api.internal:443"

An except list takes instances of the row’s effects; a bare string abbreviates an instance of the row’s single effect (net.connect except "api.internal:443"). Two qualifiers keep the layer Cedar-shaped — total, terminating, analyzable — while adding expressiveness:

• where <attr-expr> restricts a rule by decidable attributes of the request: the trust label of the flowing data (label(data)), the model tier/role, or effect instance parameters. No recursion, no user-function calls.
• budget <dimension> <= <literal> bounds a canonical resource dimension per policy scope; exceeding it is an ordinary typed denial, not a crash. (For ambient spend tracking see Budgets & Metering.)

examples: are verified, not decorative

This is the property that makes a policy trustworthy. At load, each direct-effect example is checked against the policy itself: an allow: example must be admitted and a deny: example must be denied, or loading fails with a policy example claims … error. A policy that claims to forbid code.exec but whose deny: code.exec(...) example would actually be admitted will not load.

From the verified finops-ledger corpus (policies.sema):

policy RegulatedExport:
    allow:
        fs.write("out/regulatory/**")
        net.connect("regulator-gateway.internal:443")
        model.invoke, model.embed
    forbid cap:
        code.exec, proc.spawn, package.install
    examples:
        allow:
            submit_report("https://regulator-gateway.internal:443/drafts")
        deny:
            submit_report("https://unknown.example/upload")
            code.exec(SuspiciousActivityDraft.summary)
    justification "Regulatory exports use one approved endpoint and cannot execute report content."

Note

Function-call examples whose callee has not yet had its effects inferred — e.g. allow: write_book(...) — are skipped pending effect inference on the callee, not silently passed. Direct-effect examples (code.exec(...), fetch(...), db.read(sql"...")) are the ones checked at load.

Composition: attachment only shrinks authority

Policies attach at four levels — manifest/package root, module, declaration, and block — and composition across all of them is lattice meet. Nesting a scope, or adding a decorator inside a module policy, can only shrink authority; it can never widen it. This is what makes a policy prelude safe: an outer permissive default plus an inner tight scope yields the tight scope’s authority.

The crisis-logistics corpus uses several stacked policies for one service — CrisisService for the pipeline, PublicComms for the publishing path, and ResponderMobile for field devices — each forbidding code.exec/proc.spawn so no untrusted report body can ever gain execution authority:

policy PublicComms:
    allow:
        fs.write("out/public/**")
        model.invoke, model.embed
        observe.record
        event.emit(IncidentQuarantined)
    forbid cap:
        net.connect except "public-alerts.internal:443"
        code.exec, proc.spawn
    examples:
        deny:
            publish(PublicBriefing.headline, destination="unknown-host:443")
        allow:
            publish(PublicBriefing.headline, destination="public-alerts.internal:443")
    justification "Public briefings can be published only through the approved alerting channel."

Note the event.emit(IncidentQuarantined) grant: a policy confines events per event type, just like network endpoints.

Dynamic semantics: denials are typed values

Enforcement is live. check_effects denies a function whose declared effect row is forbidden by an active policy, and net.connect operations are checked against endpoint allow/forbid scopes at the effect boundary. A denial is a typed Denied value carrying the policy name, the rule, and the justification — catchable with except Denied:

with policy(RegulatedExport):
    expect result = submit(draft):
        confirm(result)
    except Denied as d:
        log.warn("export denied", policy=d.policy, why=d.justification)

Two further guarantees:

• proc.spawn propagates the policy envelope into children — a spawned process inherits the confinement, closing the “shell out and escape the sandbox” hole.
• Code running under a policy cannot modify that policy. policy.change is a distinguished, human-approved transaction; a healer or a simulate output can never widen its own authority.

Failure modes

• A function reaches a forbidden capability → compile error by reachability (including through closures), or a typed Denied at the effect boundary.
• An examples: claim is wrong → the policy fails to load with policy example claims …; you cannot ship a policy that lies about its own effect.
• An over-broad prelude → approval fatigue. Mitigate with a standard policy prelude carrying per-capability defaults and tight inner scopes.
• FFI opacity → foreign code can hide effects; the kernel-sandbox backstop (Landlock/Seatbelt/Wasm) is the last line, documented in the governance spec.

How it’s checked

• sema check <project> verifies every policy’s examples: at load and enforces effect-row denial against active policies.
• sema assure <project> --grade silver requires explicit rows, which makes policy reachability precise.
• Denials are journaled with policy, rule, and justification, so an injection attempt leaves an audit trail rather than a breach.

See also

• Effects & Capabilities — the rows a policy confines.
• Provenance & Trust — the where label(data) refinement and the endorsement doors.
• Supervise & Heal — how a healer runs under a patch-scoped envelope with zero endorsement power.
• Construct Catalog — the full policy grammar.