Sabline

Sabline

Run code an AI wrote without handing it everything you can reach.

Each function declares what it may touch. You grant the run one folder, one host or a number of calls, and the runtime refuses anything else the moment it's tried.

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 · Guides · Reference · Paper

Formerly Velaris - why the name changed

Who it is for. The person about to run a program a model wrote - on a laptop, in CI, behind an MCP server - who wants what it can touch bounded by what they said, not by what the program says about itself. It bounds programs written in Sabline, not a Python or shell script the same model might write instead.

See it refuse, in one command - no arguments, no network, under a minute. 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 and the run's receipt; then the same task inside a budget:

pip install sabline-lang

sabline demo

error[E310] 'read_file' needs the 'fs' effect, which this run does not allow (it allows: io)

exit 1. receipt: refused; E310 (fs) at line 6; grants used: none 3 setting(s); the report is in out/report.txt

It writes what it runs and reads nothing of yours; --keep leaves the files, and sabline receipt show renders either receipt as a page.

---

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.

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 — five of the five functions that make a promise 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 prov