Capabilities & Security

Information-flow labels

Capabilities answer may this program touch the network at all? Labels answer may this value leave? You mark a value as belonging to a principal, and the engine carries that mark through every operation — arithmetic, text, field reads, json_encode, hashes, and the branches taken because of it — and refuses to let it reach a public sink unless you say, in writing and on the record, why it may be published.

You want this when the operator runs the code but must not read the data: a confidential deployment (TEE/enclave), a multi-tenant service that must not cross tenants, anything where "we are careful" is not an acceptable answer.

Turning it on§

Off by default. synsema run app.syn behaves exactly as it always has, down to the step counter.

synsema run  --labels app.syn
synsema test --labels app.test.syn
synsema serve --labels app.syn
synsema serve --attested app.syn    # labels are ALWAYS on here

With labels off, private(…) raises the moment it is called — private: labels are off; run with --labels or serve --attested. Note called, not loaded: synsema check passes, and a private(…) inside a branch that never runs never fires. If the program must refuse to start without labels, call one at the top.

Inside a guest adapter (Vela) labels are always on too — see Vela.

The four builtins§

let balance be private(1200, "app")        -- this belongs to the principal "app"
let doubled be balance * 2                 -- private(app) — every operation propagates
print(label_of(doubled))                   -- [private(app)]  ← redacted, see below
print(is_private(doubled))                 -- private(app)  ← redacted too
let code be declassify("insufficient", "the outcome code is public on-chain")
print(code)                                -- insufficient

• private(value, "principal") — mark a value. The principal is a text literal written at the call: a computed principal is refused, because choosing the principal from private data would be a channel of its own. Over a list or map it makes a private copy, so a public alias someone already holds keeps seeing the public original (since engine v0.6.29 lists and maps are values everywhere, so this is the same copy-on-write every let gets).
• declassify(value, "reason") — publish it, on the record. The reason is mandatory and public. Every declassify is logged with its source line and listed by synsema code check --json before anything runs, which is what an auditor reads.
• declassify(value, "reason", [...]) — narrow instead of publishing. The third argument must be a subset of what the value is already private to, because declassify may only narrow. A value private to ["app", "bank"] can come out private to ["bank"] alone; asking a value private to "app" for ["bank"] is widening, and the engine refuses it by name (cannot widen a label — [bank] is not a subset of what this value is private to).
• label_of(v) → the principals, as a list of texts (["bank"]); is_private(v) → bool. Both answers are as private as what you asked about. If they came back public they would be an oracle: one bit per question, and the branch you take on the answer would be a public branch on private data. Use them to decide inside the program, not to report.

Narrowing, in one example:

let joint be private(private(500, "app"), "bank")   -- private to both
let only_bank be declassify(joint, "the bank settles it", ["bank"])
print(declassify(label_of(only_bank), "probe"))   -- ["bank"]

Compare the list, not its text: since engine v0.6.29 a text inside a list prints quoted, so text(label_of(only_bank)) is ["bank"], not [bank] — a test that compared against the old spelling now fails.

These names, plus print, are protected: a program cannot bind them to something callable. Redefining one would silently un-label its own sources and mislead the audit listing.

Called by their name, nowhere else (engine v0.6.46+, breaking)§

declassify and private can only be called by their name. Reading either one as a value is a load error — the program does not start, not even its first line:

let d be declassify                -- an alias
let xs be [declassify]             -- a list entry
let m be {"k": declassify}         -- a map entry
f(declassify, x)                   -- an argument
task g()
    give private                   -- a returned value
call(declassify, {"value": x})     -- also through call()
let m be {private: 1}              -- a BARE key evaluates the name, so this is one too

Runtime error: app.syn:1:10: 'declassify' is read as a value here (an alias, a list or map entry, an argument): it can only be called by its name, `declassify(…)`, so that every call is in the review (`synsema code check`)

Before v0.6.46 each of those forms published for real while synsema code check --json listed none of them, so the review missed the call. Now there is no declassify the inventory cannot see, and its declassify_static_only field is gone (a tool that read it must stop). Each entry is {file, line, column, reason, to, constant}, with to = null for the two-argument form and the target list for the narrowing form. A program that reads declassify as a value gives "ok": false, the load error in errors and an empty declassify list.

• Fix: call it by name, declassify(x, "why"). The pipe x |> declassify("why") is a call by name and still works.
• A map key spelled like one of them is written quoted: {"private": 1}. A bare key is evaluated (v0.6.45 printed {builtin:private: 1}).
• Binding the name to a value still loads (let private be 5, a parameter called private): there the name is that value.
• The error fires with or without --labels, in synsema run, synsema test (as a <setup> failure) and synsema code check. The plain parse check, synsema check, does not report it.

-- Doc example: information-flow labels. Runs under `synsema test --labels` ONLY —
-- with labels off `private(...)` is a load error, which is the point: a program that
-- needs the second wall says so, instead of silently running without it.
intent: "doc example: information-flow labels"
-- v0.6.46: whose private data this program may send to a model the HOST allows
-- (`--cap-set "llm=customers@<provider host>"`). It also covers calls with public data.
require llm("customers")

let BALANCE be private(1200, "app")

task doubled()
    -- Every operation carries the union of its operands' labels.
    give BALANCE * 2

task marking_a_list_copies_it()
    -- `private` over a container gives a PRIVATE COPY: the public alias keeps
    -- seeing the public original, so marking cannot retroactively hide what
    -- someone else already holds.
    let public_rows be [1, 2, 3]
    let secret_rows be private(public_rows, "app")
    give public_rows[0]

task parse_untrusted(payload)
    -- An error CAUSED by private data is not catchable (whether an operation
    -- failed is exactly the bit labels exist to hide), so `try`/`recover` is not
    -- the answer for input an enclave receives from anyone. The total variant is:
    -- no error, so no bit.
    let d be json_decode(payload, nothing)
    when d == nothing
        give "malformed"
    give "ok"

task published()
    -- The only way out is on the record: the reason is mandatory and public, and
    -- `synsema code check --json` lists every declassify before anything runs.
    give declassify(BALANCE > 0, "whether the account is open is public")

test "labels propagate through arithmetic"
    assert(is_private(doubled()))
    assert_eq(text(declassify(doubled(), "doc example")), "2400")

test "the answer about a private value is as private as the value"
    -- `is_private`/`label_of` are NOT public oracles: one bit per question would
    -- be a channel of its own.
    assert(is_private(is_private(BALANCE)))
    assert(is_private(label_of(BALANCE)))

test "marking a container copies it"
    assert_eq(marking_a_list_copies_it(), 1)

test "untrusted input is parsed without exceptions"
    assert_eq(parse_untrusted("{\"a\": 1}"), "ok")
    assert_eq(parse_untrusted("not json at all"), "malformed")

test "declassify is the only way out, and it is on the record"
    assert_eq(published(), true)

test "text() does not sanitise: it is still the value, and still private"
    -- The redaction happens at the SINK, not in the conversion. Passing a private value through
    -- `text()` does not make it safe to hand around.
    assert_eq(declassify(is_private(text(BALANCE)), "doc example"), true)
    assert_eq(declassify(text(BALANCE), "doc example"), "1200")

test "a private value inside a concatenation takes the WHOLE string with it"
    -- At a public sink the entire line is replaced by `private(app)` — the prefix goes too.
    let line be "balance: " + text(BALANCE)
    assert_eq(declassify(is_private(line), "doc example"), true)
    assert_eq(declassify(line, "doc example"), "balance: 1200")

test "the third argument of declassify narrows WITHIN the value's own principals"
    let joint be private(private(500, "app"), "bank")
    let only_bank be declassify(joint, "the bank settles it", ["bank"])
    -- label_of gives the principals as a list of texts (itself private, so declassify to compare)
    assert_eq(declassify(label_of(only_bank), "doc example"), ["bank"])
    -- and `text` of that list quotes each principal, like any text inside a list
    assert_eq(declassify(text(label_of(only_bank)), "doc example"), "[\"bank\"]")

-- v0.6.46: a map key spelled like a protected name is written quoted. A bare key evaluates the
-- name, and reading `private` or `declassify` as a value is a load error.
test "a key named like a protected builtin is quoted"
    let m be {"private": 1, "declassify": 2}
    assert_eq(m["private"] + m["declassify"], 3)

-- v0.6.46: `sandbox under` can delegate `declassify` for some principals to one block.
test "sandbox under delegates declassify for the principals it names"
    let r be 0
    sandbox under {"declassify": "app"}
        set r to declassify(BALANCE, "the balance is shown to its owner")
    assert_eq(r, 1200)

-- v0.6.46: what receipt() publishes after private data does not depend on it.
test "receipt(): steps is nothing, declassified[].from is the declared set"
    let pub be declassify(private(7, "bank"), "probe")
    let r be receipt().credentialSubject
    assert_eq(r.steps, nothing)
    let last be r.declassified[length(r.declassified) - 1]
    assert_eq(last.reason, "probe")
    assert_eq(last.from, ["app", "bank"])   -- every principal the program declares, not the value's own
    assert_eq(last.to, [])

test "a declassify inside a private branch is left out of the receipt"
    let before be length(receipt().credentialSubject.declassified)
    let shown be private(0, "app")
    when BALANCE > 1000
        set shown to declassify(BALANCE, "inside a private branch")
    assert_eq(length(receipt().credentialSubject.declassified), before)

-- v0.6.46: `require llm("P")` also covers the calls with public data (it used to break them).
test "require llm(principal) still allows calls with public data"
    when not llm_available()
        assert(starts_with(reason about "the weather", "[reasoning about"))

-- v0.6.55: a mask keeps the label and never branches; an array is private as a whole.
let SCORES be private(array([1, 5, 2, 8]), "app")

task index_one()
    give 1

test "masks over a private array give private results, without a cut (engine v0.6.55+)"
    let m be SCORES > 2
    assert(is_private(sum(m)))
    assert_eq(declassify(sum(m), "doc example"), 2)
    assert_eq(to_list(declassify(where(SCORES, m), "doc example")), [5, 8])
    assert_eq(to_list(declassify(apply(SCORES, (v) => v * 10), "doc example")), [10, 50, 20, 80])

test "a private array takes private values; an index that runs code cannot write inside a list (engine v0.6.55+)"
    let q be private(zeros(3), "app")
    set q[0] to private(5, "app")
    assert_eq(to_list(declassify(q, "doc example")), [5, 0, 0])
    let L be [zeros(3)]
    let said be ""
    try
        set L[0][index_one()] to 2
    recover e
        set said to e
    assert(contains(said, "an index that runs code writes into an array inside a list or map"))
    let i be index_one()
    set L[0][i] to 2
    assert_eq(to_list(L[0]), [0, 2, 0])

What a sink is§

Every operation carries the union of its operands' labels. A public sink is anywhere a value leaves the program's own memory: the HTTP response and every stream, the on-chain result of a guest, a file, an outbound request, another interpreter (parallel_map, run_program, cron, the bus, the swarm). A private value at a sink is a label_violation — the request fails, and the message names the path the value took, never the value.

Two that surprise people:

• Branching on a private value makes the branch private. Anything the branch does carries the label, because which branch ran is the secret. print/show/log inside a private branch are refused: stdout is public and the number of lines is not redacted, so one line per iteration spells the data out.
• Printing a private value is fine — it comes out as private(app). The redaction is the answer; the refusal is for the branch.
• text(v) does not sanitise. The redaction happens at the sink, nowhere else: text returns the real content, still private. is_private(text(v)) is true, and declassify(text(v), …) gives the value back in full — passing a value through text does not make it safe to hand around.
• A private value inside a concatenation takes the whole string with it. print("balance: " + text(v)) prints private(app), not balance: private(app): the prefix is part of a private text now, and the sink replaces the whole thing.
• A template writes a private value as its value, and the HTML carries its label (engine v0.6.50+). With <p>{c.name} {upper(c.name)}</p> and a private c, render gives <p>Ana ANA</p> with the label [private(customers)]: the sink (the response, print) redacts or refuses the whole page, never one hole. Up to v0.6.49 the call wrote the marker (<p>Ana private(customers)</p>) while the plain field wrote the value. A private value the template reads from elsewhere — written, or deciding a { when } — labels the HTML too.

Three that touch capabilities and the audit log (engine v0.6.45+):

• A require cannot depend on private data. A require inside a branch decided by a private value, or with a private scope (require net(private_host)), is a label_violation: `require net runs in a branch decided by a private value (or its scope is private); what is granted cannot depend on private data`. Declare capabilities at the top of the program. The same holds for a require inside a task — it is the tool's ceiling in call_tool — so a task whose require has a private scope, or that is defined in a private branch, is a label_violation`.
• What writes the audit log does not run in a private branch. sign and the signing builtins, spend, reveal and the wallet operations write an entry to their audit log, and whether that entry exists tells the operator which way the branch went. Called under a private branch they fail with label_violation and write nothing. Decide with a public value, or declassify the condition first — that leaves its own record:

require secret("API_KEY")
require reveal("API_KEY")
let key be secret("API_KEY", "demo")
let balance be private(1200, "app")
let big be declassify(balance > 1000, "whether the balance is over 1000 is public")
when big                                    -- a public branch: reveal may run here
    let plain be reveal(key)

• A capability check inside a private branch leaves no audit entry (in --audit and in @synsema/wasm): how many entries there were would tell which way the branch went, or how many times a private loop ran. Since engine v0.6.46 an LLM or judge operation in a private branch is refused before its capability check, so it no longer leaves a "granted llm" entry either.
• With an auditor (engine v0.6.46+) the host can let those operations run: synsema run --labels --auditor <X25519 public key> --receipt <path> app.syn runs a reveal, a sign or a wallet operation inside a private branch and puts its audit line into a sealed receipt only the auditor can open. Without --auditor they are refused as above. See Attestation.

declassify is a capability: the program declares it, the host bounds it (engine v0.6.46+, v0.6.49+)§

declassify is the one place private data leaves. Without a ceiling nothing changes: the runtime grants it, like unsafe in your own Rust crate — explicit, with its mandatory reason, and listed in full by synsema code check --json. Under a ceiling (engine v0.6.49+) it works like require net: the program publishes only the principals it declares with require declassify("<principal>"), and only those the host's ceiling allows too. Nothing is granted from the environment.

synsema run --labels --cap-set "stdout,declassify=customers" app.syn

require declassify("customers")                 -- under a ceiling, what the program publishes
let c be private(3, "customers")
sandbox under {"declassify": "customers"}       -- delegate it to this block only
    print(declassify(c, "the count is public"))

• What is checked is what the call removes. declassify(v, "why") removes every principal of v. The narrowing form removes the rest: under declassify=app, a value private to ["app", "bank"] can be narrowed to ["bank"]. A declassify of a value that is not private removes nothing and always passes.
• The require goes through the ceiling like any other. Under declassify=customers, a require declassify("billing") is refused, and so is a bare require declassify (wider than the ceiling, refused whole, as require net is under net=api.example.com). A bare one is allowed only by a bare ceiling (declassify or declassify=*), and it warns at start: `synsema: warning: bare require declassify permits publishing data private to ANY principal; scope it with require declassify("principal") (the principal the call removes)`.
• Where the line goes. In the program's preamble for the program's own code. An agent declares its own: the program's require does not reach it, so a declassify inside an agent needs require declassify("customers") in that agent's body (an agent spawned by another declares its own too), and a parallel_map inside the agent inherits the agent's. A trusted task declares it in its own body, bounded by --trusted-cap-set.
• Breaking (v0.6.46, then v0.6.49). Since v0.6.46 a program that declassifies with --labels under --cap-set, --sandbox or --deterministic needs declassify=<principal> in the --cap-set (--sandbox and --deterministic never grant it: switch to an explicit --cap-set such as --cap-set "stdout,time,declassify=app"). Since v0.6.49 it also needs require declassify("<principal>") in the program, the agent or the trusted task that declassifies; before, the ceiling alone decided.
• A refusal is a label_violation that try/recover cannot catch — whether it passes depends on the real label of the value, so a catchable refusal would be an oracle. Like every label violation it ends the run and withholds the buffered output. A refusal only happens under a ceiling, so the program sees the fixed text (What a cut shows, and to whom); the operator's detail (the sealed receipt with --auditor) says where the line goes:

app.syn:3:17: label_violation: declassify is not granted for what this value is private to (customers). With a ceiling the program declares what it publishes (`require declassify("<principal>")` in the program's preamble, or in the body of the agent that runs this code: an agent declares its own, also for its `parallel_map`) and the host's ceiling has to allow it too (`--cap-set declassify=<principal>`); inside a `sandbox` only a `sandbox under` that delegates `declassify` allows it

• The detail names the place that applies: inside an agent, that agent (… add require declassify("<principal>") to the body of agent Sub …); inside a trusted module, the exported task and --trusted-cap-set (Trusted modules).
• The set in parentheses is the program's declared set — every principal it marks anywhere — never the value's real label, which would tell which value it was. The [INF] declassify: … (from […] to […]) log line names the declared set too ([…] when the program declares no principal).
• Without --labels nothing is checked: private(…) raises (labels are off) and declassify is the identity.
• The Vela guest runs its app under stdout,declassify=app: its only principal is app, and the app declares require declassify("app") and publishes its outcome codes and withdrawal receipts itself (Vela).

What receipt() publishes after private data (engine v0.6.46+)§

With --labels, receipt() no longer carries what depended on a private value. Each was a leak with the program counter public and no label_violation:

• steps is nothing once a private value was seen (it was the raw count: a loop over a private n gave its size). Before the first private value it is the number.
• declassified[] lists {reason, from, to, line}, and from is the declared set, not the value's real label (["a", "b", "c"] even when the value was private to a and c only). A declassify inside a private branch is left out of the list, and its [INF] declassify line is not written: how many there were told which branch ran.
• inputs: a read inside a private branch (read_file, env, …) is refused as a sink (read_file called under private control flow …), so it never reaches the list.

read_line, flush and the order of the output (engine v0.6.46+)§

• The prompt of read_line(prompt) is a public sink, like print. A private prompt, or a prompt inside a private branch, is a label_violation, and each says which (engine v0.6.49+; before, both said "control flow"): `the read_line prompt is private (to a) and the prompt goes to stdout, which is public … and read_line prompt under private control flow (pc = [a]); stdout is public …. read_line()` without a prompt inside a private branch is allowed.
• With --labels, flush() and read_line do not write the pending output live. print already kept it until the end; now the prompts come out first and the printed lines at the end — print("one"), flush(), read_line("> ") shows > one. How many lines came out before a prompt could depend on a private branch. Without --labels nothing changes.

Private data to a model, tools a person wrote (engine v0.6.46+)§

Two ways private data can now do useful work without the program publishing it:

• A model the host chose. With require llm("customers") in the program and --cap-set "llm=customers@api.anthropic.com" in the host's ceiling, reason, generate, llm_step… may carry data private to customers to that provider, and the answer stays private. The rules are in LLM primitives; the judge has its own item, judge=customers@… (Judge).
• Trusted tools. Under a ceiling without declassify, code written by a model cannot publish anything private, but the host can give it tools a person wrote, whose own policy declassifies: synsema run --labels --cap-set stdout --trusted tools=./tools.syn app.syn, then use "trusted:tools" as t. See Modules § Trusted modules.

Arrays (engine v0.6.55+)§

Masks keep the label and never branch. A comparison over a private array gives a private mask, and sum(m), where(a, m), some(m), if_else(m, x, y) and apply give private results — no cut, because nothing ran under a private condition. That is why the mask is the native path for private data.

require declassify("x")
let p be private(array([1, 5, 2, 8]), "x")
let m be p > 2
print(declassify(sum(m), "x"))         -- 2
print(declassify(where(p, m), "x"))    -- [5, 8]

• An array is private as a whole, not element by element. Writing a private value into a public array stops the run: label_violation: cannot write a value private to x into the array 'pub' (public): an array is private as a whole, not element by element — bind it as private(…, "<principal>") first, or declassify the value. The check is against the variable the array is reached from, not the containers in between: set m.a[0] to v is checked against m. A private index into a public array is a violation too.
• Writing into an array inside a list or map takes indices that run no code: set L[0][f()] to 2 → label_violation: an index that runs code writes into an array inside a list or map — compute the index into a variable first.
• An error of set that depends on private data is not catchable — a private index out of range (set xs[secret]), the length of a private list or array walked with a public index, the shape or type of a private value. It stops the run with private(x) and the place, like the same error in a read. (Before v0.6.55 a try caught it, and its text showed the data.)
• A try whose body wrote into a private list, map or array runs its recover under that private context, as if it had read it (breaking). A recover that then assigns a public variable stops the run (cannot assign to 'fails' (public) under private control flow …): move the write out of the try, or make the counter private (let fails be private(0, "x")).
• When the statement touched private data, the errors of the write reach the operator as a diagnostic, and the program sees the fixed cut text (§ What a cut shows, and to whom).

Errors that cannot be caught§

An error born under a private branch, or caused by private data, is not catchable: try/recover re-propagates it and assert_error does not absorb it. Whether an operation failed is exactly the bit labels exist to hide — xs[private_index], 1 / (secret - i) — and a recover that swallowed it would let the loop before it leave the secret in a public variable.

So how do you validate untrusted input, which an enclave receives from anyone? Not by raising at all. The operations that parse external input have a total form that returns a fallback:

let d be json_decode(payload, nothing)              -- no error, so no bit
let n be number(field, nothing)
let clear be aes_gcm_decrypt(k, nonce, ct, aad, nothing)

Also decimal, float, toml_parse, abi_decode, bech32_decode, rlp_decode. The fallback is evaluated eagerly (an effect inside it fires on the happy path too) and it never swallows a label violation — that would be a try/recover in disguise.

What a cut shows, and to whom (engine v0.6.47+)§

A cut by the flow checker — any label_violation — used to tell the program where it fell: the builtin, the argument, the line. That was a channel of its own, because a private value can choose which of N sites fails, and in an agent loop the error goes back to the model. Now who runs the program decides what it sees:

In every case the output printed before the cut is replaced by one line:

private(labels): the run was stopped by the flow checker; its output is withheld because the NUMBER of lines before the stop depends on private data

and the fixed error is:

Runtime error: label_violation: the flow checker stopped the run (private to customers); what failed, where and how to fix it go to the operator, not to the program

The set in parentheses is the program's declared set, a constant of the program, never the label of the value that failed. Measured on v0.6.47 with the same program: synsema run --labels cut.syn prints cut.syn:4:10: label_violation: print called under private control flow (pc = [customers]) …, and synsema run --labels --cap-set stdout cut.syn prints the fixed error above. To debug a cut, run it yourself without a ceiling, read operator_detail in WebAssembly, or open the receipt as the auditor (Observability). The messages quoted on other pages (fetch(argument 0) is private to …, declassify is not granted …, reason would send data private to …) are that detail.

• A cut in an agent cuts the run it belongs to. Under run that is the whole program: it ends with the same fixed error (without a ceiling, the detail starts agent Leaky_0: …). Under serve --labels it is the request or tick that spawned the agent. From then on every sink of that run fails.
• Under serve --labels, each request, cron tick and socket handler is its own run. Its stdout and stderr are held and written when it ends, or replaced by the fixed line if it was cut; what agents print is not written. The server says so at startup: [serve] labels: request and cron output is logged when each one ends, and not at all if a label cut stopped it; agent output is not logged (which agent stopped would be the private data). For a live log while you develop, run without --labels. agents() and agent_stop see only the agents of the same run.
• Under serve --labels, a run's blackboard writes and signals land all at once or not at all. A run — the request, or the preamble, with every agent it spawned — is committed when all of it has ended without a cut, and undone if any part is cut, including what its agents wrote after the request answered. Measured: a route that does share "should be undone" as "b" and then hits a cut answers 500, and a later request's observe "b" gets nothing, while a clean route's share is kept. What other runs read while it was open, and signals already consumed, stay — like any effect before a cut.

What leaves the process§

A redacted error says private(app) and nothing else — no file:line:column. If the secret chooses which of N sites fails, the location is log₂(N) bits. The principals named are the ones the program declares, never the ones of that particular value: naming the value's own was a channel, since in a multi-tenant deployment the principal is the tenant.

The auditor still learns why (engine v0.6.50+). An error whose text was redacted because it touched private data — when c.name == "Ana" then 1 / 0 gives Runtime error: b.syn:3:16: private(customers) without a ceiling — puts its real text in the sealed receipt, which only the auditor opens, with or without a ceiling: synsema receipt open shows an entry {"sealed": true, "entry": {"kind": "label_violation", "detail": "b.syn:3:16: Division by zero"}}. With a ceiling the program still sees the same fixed text, and the operator detail (a log) stays redacted, with its location. See Observability.

A label violation also ends the whole synsema test --labels run, with one outcome naming the violation, rather than a ✗ on that block with the suite carrying on — eight blocks each probing one bit and the column of ✓/✗ spells the byte. An ordinary failure is still a per-block verdict.

Limits, stated§

• Termination is one bit per run, and a server run is one request. A run the checker stopped tells an observer that it stopped. Under serve the caller chooses how many runs to make, so it is one bit per request, without a ceiling: eight public requests recover a value by binary search. If a request's outcome must not depend on private data, do not let a private branch decide whether it fails.
• Progress. Effects performed before the stop did happen. The engine withholds buffered output and rolls back what the request wrote to the shared state_* store and, since v0.6.47 under serve --labels, to the blackboard and the signal queue — all live in its own memory — but a file or an outbound call it cannot undo.
• Timing and resource use are not modelled at all.
• Crossing into another interpreter refuses, deliberately: the channel does carry labels, but what a worker may do with a private value is not yet specified, and the alternative it replaced was worse (the worker got the value stripped and did the effect in the clear while the result came back labelled, so the leak looked tracked).

Next§

Labels keep the data in. Attestation is the other half: proving to a remote party which code is holding it.