# Policies > Native capability governance in Sema — policy blocks with allow/forbid/examples verified at load, @Policy decorators, and authority-shrinking scopes. 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](/governance/effects/) 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: ```sema 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: ```sema @NoExecFromGen simulate def draft_migration(req: Request) -> MigrationPlan by models.writer: ... ``` **Block (`with policy(...)`).** A lexical scope confined for its dynamic extent: ```sema 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: ```sema 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 `** 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 <= `** 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](/governance/budget/).) ## `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`): ```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: ```sema 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](/governance/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](/governance/effects/) 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`: ```sema 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 ` verifies every policy's `examples:` at load and enforces effect-row denial against active policies. - `sema assure --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](/governance/effects/) — the rows a policy confines. - [Provenance & Trust](/governance/provenance/) — the `where label(data)` refinement and the endorsement doors. - [Supervise & Heal](/governance/supervise/) — how a healer runs under a patch-scoped envelope with zero endorsement power. - [Construct Catalog](/reference/language-spec/05-construct-catalog/) — the full `policy` grammar.