sabline

Sabline

An AI wrote you a script. Run it anyway.

A language where a function's signature declares what it may touch — and the runtime refuses anything you did not allow, whatever the code says about itself.

Not a security boundary by itself: an interpreter in the program's own process enforces the budget. From 8.4 the operating system is asked to hold the same budget under it - fully on Linux, partly on macOS and on Windows - and each run says which it got (THREAT_MODEL.md, docs/confinement.md).

Playground · Documentation · Reference · Library · Errors

---

This project was called Velaris until 8.6.0. The name belongs to an unrelated company in the same market (velaris.io), so it was given up rather than contested. Everything else is unchanged, and nothing written against the old name stops working in 8.x: the velaris command, import velaris, the VELARIS_* environment variables, a committed velaris.capabilities, and a velaris.audit/1 or velaris.receipt/1 document are all still read, each saying once that the name has changed. docs/renamed.md lists every published address and where it now points; STABILITY.md says what goes in 9.0.

---

pip install sabline-lang
sabline agent_output.vel

That program cannot open a socket, read a file, call Python, or ask the clock. Not "shouldn't" — the runtime refuses, and a refusal cannot be caught and carried past. You do not have to read the code, understand it, or trust the compiler's analysis of it.

Since 5.0 that is what a run with no --allow gets: io, the console. It used to be all seven effects, which meant the answer to "what may this program do?" was "everything" until an operator said otherwise. Widen it by naming what the program needs (--allow io,fs:read:./data); --allow all grants every effect and writes one line to stderr saying so.

--allow io,ffi:math,json grants Python for those modules only; a call that reaches any other module — named, or reached through an attribute of a granted one — is refused (E311). A granted module can still do whatever that module itself can do: ffi:os is the operating system. Since 3.0 the same grammar narrows every coarse effect: fs:read:./data, fs:write:./out, net:api.example.com:443, net:*.example.com, and @100 for at most that many operations in a run; env is its own effect, so an io-only program cannot read the environment. timeout and max_memory_mb are available through the library and every door, and on a door the operator's limits are ceilings a caller cannot raise. It is still not a security boundary - but the caveats every review raised, the ffi cliff, unbounded execution, and fs and net with no path or host list, are now precise permissions rather than holes. It is a real guard for the situation everyone is now in — running a program someone, or something, else wrote.

To see it happen, with nothing to read first (8.5):

sabline demo

It writes the kind of script an agent writes - read ./.env, post it to a webhook - runs it with no budget given, and shows the refusal, its line and the run's receipt; then the same task inside a budget, and what differs between the two receipts. No arguments, no network, under a minute; it writes what it runs and reads nothing of yours. --keep leaves the files, and sabline receipt show renders either receipt as a page.

The other half: promises, proven

fn discount(price: Int) -> Int
    requires price >= 0
    ensures result >= 0
{
    return price - 10
}

error[E700] promise cannot be kept: 'discount' ensures result >= 0 - proven without running the program: price = 5 gives result = -5

That ensures is not a comment or a runtime assert. The Z3 theorem prover verifies it for every possible input before execution — and refutes it with an exact counterexample when it lies.

A rule the customer wrote

A commerce platform lets each customer write their own discount rule. This one has the shape most of them have: a percentage off once the basket passes a threshold, a flat amount off as well, and a cap on the two together.

record Rule {
    percent: Int         // this much off, once the basket is
    above: Money of INR  // worth at least this,
    flat: Money of INR   // and this much off as well,
    cap: Money of INR    // but never more than this, all together
}

fn discount_for(total: Money of INR, rule: Rule) -> Money of INR
    requires total >= money(0, "INR")
    requires rule.percent >= 0
    requires rule.percent <= 100
    requires rule.flat >= money(0, "INR")
    requires rule.cap >= money(0, "INR")
    ensures result >= money(0, "INR")
    ensures total - result >= money(0, "INR")
{
    let off = money(0, "INR")
    if total >= rule.above {
        off = percent_of(total, rule.percent, 100, "half_up")
    }
    off = off + rule.flat
    if off > rule.cap {
        off = rule.cap
    }
    if off > total {
        off = total
    }
    return off
}

The two ensures are what the platform needs to know about a rule it did not write: a discount is never a surcharge, and what is left after it is never negative. Both are settled for every basket and every rule the types allow, before the program runs. examples/discount.vel is the whole program —

proven, and it runs under --allow io.

examples/discount_bad.vel is the same rule with the last if deleted. The cap still holds the discount to a fixed ceiling; nothing holds it to what the basket is worth:

$ sabline check examples/discount_bad.vel
examples/discount_bad.vel:54: [E700] promise cannot be kept: 'discount_for' ensures total - result >= money(0, "INR") - proven without running the program: rule = Rule(percent: 0, above: 0, flat: 2, cap: 1), total = 0 gives result = 1

The amounts are in paise: a basket worth nothing, a flat discount of two paise held down to a cap of one, and one paisa handed back anyway. The program does not run.

A sandbox answers a different question. It can stop this rule reading a file or opening a socket; it cannot tell you whether the arithmetic holds.

A key it cannot print

Effects say a program printed something. They do not say whether what it printed was the secret. Secret of T (6.0, 7.0) is the other half: the compiler tracks the value, and refuses any program that hands it to anything that emits.

fn key() -> Secret of Text uses env {
    return env("API_KEY", "")          // env() gives a Secret of Text
}

fn authorization(k: Secret of Text) -> Secret of Text {
    return "Bearer " + k               // still a Secret of Text
}

examples/secret.vel reads an API key, builds the request that would carry it, and prints a summary of that request. examples/secret_bad.vel is the same program with one more line:

$ sabline examples/secret_bad.vel --allow env,io
error[E560] argument 1 of 'print' is Secret of Text, and 'print' performs io - a Secret cannot be printed, written, sent or passed to Python. It came from env(), line 27, through 'key', which returns Secret of Text (line 58)
  --> examples/secret_bad.vel, line 58

Nothing ran, nothing was logged, and no reviewer had to notice the line. A list of secrets, a map of them, or a record with one secret field carries it too, so the whole structure is refused at a sink — a Request record holding the key cannot be printed either.

And a program cannot look at the key either. key == "" is a Secret of Bool, not a Bool, and an if or while on one is E563. That is the rule that makes the rest mean something: with length and code_at, a plain Bool from == is not one bit, it is a loop that reads the whole key out —

while at < 3 {
    for c in alphabet {
        if code_at(key, at) == code_at(c, 0) {   // E563
            found = found + c
        }
    }
    at = at + 1
}
print("recovered: " + found)                     // the whole key

— so a rule that stopped print(key) and allowed that would be a decoration, not a type. The line is drawn at the branch.

declassify(value, "why") is the only way out. It needs uses declassify in the signature, a reason written in the call, and the declassify grant at run time — and it is what the audit reports, so a consumer can ask whether a program ever lets a secret out without running it:

$ sabline audit examples/secret.vel --json | jq .secrets
{
  "sources": ["env"],
  "declassifies": false,
  "declassifications": []
}

To look at a secret, a program says so — declassify(key == "", "…") gives back a Bool you can branch on, at the cost of the effect, the grant and a reason in the audit. That is the trade: not silence, a statement.

What this does not do: it only sees values env() and read_file_secret() produced, so a password read with read_line, or handed in through args(), or fetched from a vault over net, is an ordinary Text with no protection at all. And it is not non-interference — a program still chooses how long to run and whether to stop. SPEC.md §3.1 states the rules and THREAT_MODEL.md states the limits.

Related work

TACIT ("Securing Agents With Tracked Capabilities", ACM CAIS '26; arXiv 2603.00991) has agents write Scala 3, whose capture checking tracks file, network and command capabilities as values in the type system; CaMeL has a model turn the user's request into a restricted subset of Python and tags every value with its provenance and permitted readers, checking a policy at each tool call; WASI gives a WebAssembly module only the resources its host hands it. Sabline is a small language a model learns from a card of about 5,100 words, in which functions declare their effects, the runtime enforces the operator's budget at each operation, and contracts are checked by the Z3 theorem prover. From 6.0 it also tracks one kind of data: Secret of T, which env() and read_file_secret() produce and which cannot reach anything that emits, cannot be branched on, and leaves only through declassify — an effect of its own. That is narrower than what CaMeL and TACIT do: they tag every value with its provenance and permitted readers, and TACIT follows capabilities through polymorphism, where Sabline marks two builtins' results and refuses generic code over them unless a signature says so. Until 5.0 its command line also granted every effect when no budget was given, where a WASI module given nothing reaches nothing; from 5.0 a run with no budget gets io alone. The capability format is published separately, under CC0, as sabline-spec, whose PRIOR_ART.md sets out these differences and the older work in full. From 4.1 it holds a conformance corpus an implementation in any language can run -

ratchet, none needing a prover - written from this repository's suites and held to them by a drift test; sabline conformance runs it against this implementation, and CI does so on every leg.

Why Sabline

Guarantee	What it means
Effects are visible	uses io, net, fs, ffi — a function without uses net can never touch the network, transitively, and one without uses ffi can never call out to Python. Hidden behavior does not compile.
Promises are proven	requires / ensures / loop invariant, verified by Z3 with modular call summaries — including records, maps, nested lists, quantified list properties, failure paths, and floats in genuine IEEE-754 (the prover refutes x + 0.1 + 0.1 == x + 0.2 with the exact double that breaks it).
Failure is unignorable	-> Int or fail in the signature; callers must check or try. Forgetting the error path is a compile error — builtins included.
Secrets cannot be printed, or looked at	Secret of T — what env() and read_file_secret() return. Nothing that emits or can fail will take one, a structure holding one carries it, every operation over one keeps it (a comparison included), and no if branches on one. declassify(value, "why") is the only way out: an effect of its own, with its reason named in the audit. SPEC.md §3.1 says what it still does not claim.
Fast where it's safe	Pure functions over numbers, list reads, and text — including text built inside them — JIT to native code via LLVM (~10,000× on hot arithmetic, ~45× on text building), differential-tested against the interpreter. Native reads are bounds-guarded and text is built in a runtime-owned buffer, so results always match interpreted.

Why floats are proven in IEEE-754 rather than as real numbers, and what that costs: docs/floats.md.

Loops without written invariants are handled where the boring invariants suffice: the compiler proposes bounds on each counter and keeps the ones a loop step cannot break (see examples/inferred.vel). Anything richer — membership, sortedness — still needs an invariant line.

The prover never claims "proven without running" unless the counterexample is premise-complete — untranslatable assumptions abandon the proof to runtime checks rather than risk a false alarm. Soundness reports are treated as security issues.

Install

pip install sabline-lang
sabline doctor
sabline new hello && cd hello && sabline main.vel

Standalone executable (no Python required) — download for Windows / Linux / macOS from the latest release, then:

sabline doctor

With Python 3.10+:

pip install sabline-lang
sabline new hello && cd hello && sabline main.vel

Zero install — the playground runs the real compiler in your browser.

Optional extras for source installs: pip install ".[full]" adds z3-solver (compile-time proofs) and llvmlite (native speed); without them, promises are checked at runtime and everything runs interpreted — same language, honestly degraded. With llvmlite installed, native code is the default: a pure function the compiler can compile runs as machine code unless --no-native forces the interpreter. There is no --native flag.

Everyday ergonomics

keep_if(xs, fn(n: Int) -> Bool { return n % 2 == 0 })   // inline functions
format("hi {}, {} left", name, count)                    // text with holes
args()                                                   // command line
post(url, body) / fetch_status(url)                      // not just GET

Function values are lifted to real functions, so proofs and native compilation apply to them unchanged — and they can carry their own requires / ensures, proven like any other function's. A function value takes a copy of the locals around it when it is made (SPEC.md §12a); a promise on one that does is checked while it runs.

Where it plugs in

sabline script.vel                    the command (io unless you say more)
sabline script.vel --receipt r.json   and a signable record of what that run did
sabline eject script.vel              a directory that runs with nothing from here
import sabline                        a Python library
sabline mcp-install                   tools inside your assistant
sabline.mcpb                          double-click install for Claude Desktop
uses: gowrishankar-infra/sabline-lang a GitHub Action, findings in the Security tab
sabline capabilities check            CI fails when the capability surface widens
sabline serve                         an HTTP door for any language, token required
npx sabline-lang script.vel           npm, for the JavaScript world
%%sabline --audit --allow io          a Jupyter cell
- repo: sabline-lang (pre-commit)     a commit hook
docker run ... sabline check          a container
sabline build --for-everyone          standalone executables

Use it from your own program

import sabline

report = sabline.audit(source)      # what it touches, what's proven
run = sabline.run(source, allow={"io"})   # it cannot touch anything else
print(run.output, run.refused_effect)

The budget is enforced the same way it is on the command line. There is an MCP server too, so an assistant can write, audit and sandbox-run Sabline without leaving the conversation — see EMBEDDING.md and the versioned sabline.audit/1 format.

Calling run with a timeout or a memory cap starts a fresh interpreter every time. A pool keeps workers alive under one fixed budget:

pool = sabline.Pool(size=4, allow={"io"}, timeout=30, max_memory_mb=512)
result = pool.run(source)             # the same RunResult run() returns
pool.close()

200 sequential bounded runs of a small program: 46.6 s a process at a time, 0.5 s on a pool. pool.run takes no allow — the budget belongs to the pool, a worker is killed and replaced unless the run finished cleanly, and a reused worker has every piece of mutable state reset first. check_pool.py asserts each of those, including a program that widens its own budget through ffi and cannot widen it for the next one. The rules are stated in full in EMBEDDING.md.

A platform whose customers write the rules

examples/platform/ is that pattern as a small FastAPI service, in one file. A customer submits Sabline source; the service audits it, stores it with its capability surface, and answers with what it declares — effects, hosts, paths, modules, the proven share, its contracts function by function, and the narrowest budget that would run it. It does not run it. A surface wider than the platform permits is refused there, naming the grants that would have to be added. Running happens on a sabline.Pool whose budget is the platform's.

Submit examples/discount.vel and the answer says "proven_share": 100.0 with "status": "proven" on every promise, including the two that matter to whoever is taking the payment: the discount is never a surcharge, and what is left is never negative. That is the sentence a platform can show a customer before offering to enable a rule, and it is not one a sandbox can produce.

A program that calls your tools

sabline run agent.vel --tools tools.json \
    --allow io,tool:search@20,tool:send_email:to=*@corp.com

The runner's first cut (8.5). A host process offers a program tools through a manifest - a JSON Schema for each tool's arguments, a cost, a ceiling - and the operator's budget says which may be called and holds arguments to patterns. A call that is outside either is refused before the host hears of it, and the receipt records every call, the patterns that held it and the ceiling. examples/runner/host.py is a whole host in Python: it offers search and send_email, and the second example program is refused when it tries to mail outside corp.com. The protocol is JSON lines on standard input and output (docs/runner.md); there is no framework adapter yet, and a tool's result is not yet marked as the host's words rather than the program's - that is Untrusted, in 9.0. sabline skill verify reports the tools and the budget a skill's programs would need, without running them.

Written by a model, audited by you, run in a box

sabline card > card.md          # ~5,100 words: paste into any model
sabline audit script.vel        # what it can touch, before you run it
sabline attest script.vel --output script.intoto.json   # the same, bound to its bytes
sabline script.vel              # io, and nothing else, unless you say more

sabline audit is written for the reviewer: what the program reaches, what it promises, how much of that is proven rather than checked while running, what can fail, and the exact command to run it safely. sabline attest (4.2) puts that audit in an in-toto Statement whose subjects are the program's files by sha256, ready to sign with cosign or sigstore-python; EMBEDDING.md shows both, and every release carries one, signed, for an example program. agent_loop.py closes the circle — a model writes it, sabline check --json hands back errors with fixes, and it iterates until the program compiles and its promises prove.

From 8.3, the rest of a run's life: sabline eval runs a program as an evaluation harness does, under a profile its command line cannot relax (no net, ffi or env, time and memory limits, a stop honoured, the worker confined where the operating system offers it, and a receipt always - docs/eval.md); sabline receipts diff names what a run did that its audit, or its earlier runs, did not; sabline replay makes a run again from its receipt on the same bytes, or refuses; sabline test --from-contracts runs each promise on the inputs the prover finds its requires allows; and sabline verify holds an attestation or a receipt to its type and its bytes. docs/structurally-impossible.md lists what cannot occur in a Sabline program, each with a test, and docs/crosswalk.md maps each guarantee and each known gap onto the OWASP, AIUC-1 and NIST frameworks.

Running code you did not write

sabline agent_output.vel                 # io: it may print, nothing else
sabline agent_output.vel --allow io,fs:read:./data   # and read that folder
sabline agent_output.vel --allow all --deny net,ffi  # everything but these