Threat model

What Velaris defends against when it runs a program somebody - or something - else wrote, what it does not, and what to do about the gap. Written for the person who has to decide whether agent-written code may run on a machine they are responsible for. Every claim here names the suite that tests it; the numbers come from benchmark/RESULTS.md, which one command regenerates.

What Velaris is for #

A model hands you a script. You want to run it without reading it line by line, and you want the things it can do to be bounded by what you said, not by what it says about itself. Velaris is a small language in which a function's signature declares the effects it may perform, the failures it may raise and the promises it keeps, and a runtime that refuses any effect outside the budget the operator set.

It is not a general sandbox. It bounds programs written in Velaris; it does nothing for a Python or shell script the same model might write instead.

The trust boundary #

The budget is enforced inside the interpreter loop at the moment an effect is attempted, and a refusal (E310, E311, E313, E314, E315) is not a failure the program can check; it stops the program. The one catchable case is a redirect to a host outside the grants: the program did not choose it, so the request fails and the program hears why. check_sandbox.py holds the escape attempts that established this, including a helper two layers down and a program that tries to catch the refusal and carry on.

What it defends against #

On the 76-program benchmark (66 dangerous, 10 harmless), Velaris caught 64 of the 66 - 52 before running and 12 while running - and flagged none of the 10. Under the same rules Deno caught 42 (8 before, 34 during) and plain Python 31 (all while running). The two misses are named below. Three of the 66 (category 12, 7.1) are dependency upgrades, and Velaris's catch before running there is velaris deps-diff, whose limits are also below. Three more (category 15, 8.3) import a library that does not exist where the program says it is, which velaris check refuses before anything runs; three (category 14, 8.3) are skill scripts whose helper reads a credential and posts it, which the audit shows reaching beyond what the skill needs.

What it explicitly does NOT defend against #

No longer here: the permissive default. Fixed in 5.0, 2026-09-12. Until 5.0 a run given no budget - velaris program.vel, or velaris.run(source) with no allow - got all seven effects, and this repository said so plainly: the README's related-work paragraph and the paper both conceded that Velaris's command line granted every effect when no budget was given, where a WASI module given nothing reaches nothing. That was true until 5.0. It is not true now. The default is io - the console, and nothing else - in the command line, the library, Pool and both doors, and --allow all is the one way to ask for what a run used to get, which writes a line to stderr when it is used. The old text is not deleted anywhere it appeared; it is dated.

Moved, not removed: secrets. Until 6.0 this section had nothing about the values a program handles, and the residual-risks table below said only "do not grant env to code you have not read." From 6.0 a value read by env() or read_file_secret() is a Secret of Text the compiler will not let reach anything that emits it, and from 7.0 it will not let a program branch on one either; that moves to What it defends against above. What stays here is everything those rules do not cover, and it is more than one line:

• Only values the type system can see. A secret that arrives any other way is an ordinary Text with no protection at all: read through read_line, passed in through args(), fetched from a vault over net, returned by a granted ffi module, or hard-coded in the source. Secret marks two builtins' results; it does not discover secrets. A program that reads a password from standard input can print it, and nothing here stops that.
• Non-interference. A comparison over a secret gives a Secret of Bool, nothing prints one and nothing branches on one (E560, E563), so a program cannot read a secret out a character at a time and then say what it read. That was possible in 6.0.0, for one day, and closing it is what 7.0 is - see the CHANGELOG. What remains unbounded is everything a program controls that is not a value: how long it runs, how much it allocates, whether it stops at all. This is not a non-interference result and must not be described as one.
• A promise, once per run. A requires, ensures or invariant may be a Secret of Bool, because a broken promise stops the run, cannot be caught and cannot accumulate - so it is a statement about a secret, not a branch on one. An operator who runs the same program many times can still learn one bit per run from whether it stopped. If that matters, do not grant env at all.
• Where a declassified value goes. declassify returns an ordinary value. After it, the type system has nothing more to say: the audit records that it happened and why, and whether the reason was true is a person's judgement.
• What a granted ffi module reads for itself. A Secret is a compile-time distinction with no runtime representation, so Python code inside a granted module reads the environment directly if it wants to. ffi:os is the environment, whatever the Velaris types say.

What follows is what is still not defended.

• Anything a granted ffi module can do. ffi:os is the whole operating system as the current user. The allow-list narrows which modules a call may reach; it does not narrow what a module does. Plain ffi grants every module. From 3.3 the reach check bounds a scoped grant to the module actually reached along the attribute chain, so a granted module is no longer a door into the other modules it imported; but within a granted module, that module's full behaviour is still granted. Where the owning module of an object reached along the chain cannot be determined, the call is refused rather than allowed - the bound errs toward refusing more, not less.

• Native code inside a granted module. A granted module may be, or may ship, a compiled extension (.so/.pyd/.dylib), which has no source to read and whose behaviour a budget does not constrain any more than it constrains Python. From 8.0 velaris audit reports this per granted module in ffi_native - "native" when it finds a compiled extension on disk (found without importing the module), "unknown" otherwise, and never "false", since a pure-Python module can import a native one without that being visible. The audit names the risk; it does not remove it. Grant native modules only when you would grant the machine.

• Side channels. Timing, CPU load, cache effects, the size or timing of console output. Nothing measures or bounds them.

• Resource use below the limits. A program may run for 29 of its 30 seconds and hold 511 of its 512 MB, every time it is called. The limits stop a runaway; they do not ration.

• Rate, and the meaning of a request. A count (@100) bounds how many operations a run makes, not how fast, how large, or whether a request is a GET or a POST. A plain net grant is any number of requests to any host; a plain fs grant is any path the OS user can reach. Narrow them.

• What a granted host does with a request. The grant names a host as written; where the name resolves is DNS's business, and what the host does with the data it receives is outside the model.

• Closed in 8.0.0: the connection endpoint when a proxy is set. Through 7.1.x the network client honoured an ambient HTTP_PROXY / HTTPS_PROXY: a net: grant checked the URL's host, but the socket then went to the proxy, which need not be a granted host, so an http:// request carried its payload to the proxy. The grant bounded the URL string, not the peer. From 8.0 guarded_opener builds the opener with ambient proxies disabled, and honours one only when the proxy's own host:port is itself inside the net budget; a proxy the budget does not cover is refused (E317, uncatchable), naming the proxy and the grant that would allow it. velaris add ignores ambient proxies too. The grant now bounds the socket's peer, not only the URL - this moves to What it defends against. What is still not bounded is what a granted proxy does with the request, like any granted host.

• What a granted path contains. A hard link inside a granted directory is that directory's content. A file system changed by another process between the check and the open is outside the model; a Velaris program has no threads, so it cannot race itself.

• Still within io: args() and read_line(). Command-line arguments and standard input are the console.

• Logic errors with no contract. A function that returns the wrong number and promises nothing is correct as far as the compiler knows. Benchmark row 04c (a loop that stops one item early) is this, and is a miss. The audit lists such functions under contract_coverage so the gap is visible; it does not close it.

• The meaning of text. A program that prints rm -rf build for its caller touches nothing (benchmark row 09c, a miss); a program that prints the same words in a warning is harmless (row 10d). No effect system can tell them apart, and Velaris does not try.

• Code not written in Velaris. A model asked for Velaris may hand back Python. The guard applies only to what the Velaris runtime runs.

• Memory caps on macOS. max_memory_mb uses the OS address-space limit (RLIMIT_AS) on POSIX and, since 3.1, a job object with JOB_OBJECT_LIMIT_PROCESS_MEMORY on Windows - where the child is created suspended, put in the job and only then resumed, so nothing runs outside the cap. It is enforced on Linux and on Windows. On macOS it is best-effort: the limit is set but not reliably honoured, and in the suite the runaway program reached the timeout instead. If the Windows job object cannot be made, the cap is recorded and not enforced rather than the run failing, which is what a Windows before 3.1 always did. velaris.memory_cap_is_enforced() answers for the machine you are on. The timeout is enforced on every platform.

• A pool worker's budget, once chosen. A Pool fixes its budget when it is made. That is the point - it is what lets a worker serve the next program safely - but it means a caller who wants a narrower budget for one program must make another pool, and a caller who hands the same pool to two tenants has given them the same budget. A worker is also a process that outlives one program: everything a granted ffi module could do to a fresh process, it can do to a worker, and the pool's promise is only that the next program does not inherit it. check_pool.py is the whole of that promise.

• The door's token, once it is out. The token is a password with no user behind it: whoever holds it has every grant the ceiling allows, and the door cannot tell holders apart or revoke one of them. From 8.1 it limits how often the token is used, all its holders together; one holder can spend that allowance for the rest. It is only as secret as the file or environment it came from. A program the ceiling allows to read the token file can read it, and one allowed net as well can send it away. The door speaks plain HTTP: on any address but loopback the token crosses the network in clear unless a TLS proxy sits in front. A made token printed to a stdout that something writes to a file is in that file.

• --no-auth. Any program on the machine, run by any user, can send the door programs. The checks that replace the token stop a web page in a browser, not a local process.

• The MCP server's caller. The ceiling bounds what velaris_run grants, not who calls it: the client decides that. A ceiling raised to ffi is ffi for whatever the model is told to do.

• What mcp-verify does not see. It compares what a server says about its tools with what was signed; it does not watch what the server does, and a server that returns the signed descriptions and behaves differently passes. It checks at the moment it runs. If both the velaris package and velaris_mcp.py in an installation were changed, the checker was changed too - verify the wheel (SECURITY.md), or run mcp-verify from a separately verified Velaris.

• What the capability ratchet does not see. It reads the program text. What a granted ffi module does once called is not in the text: ffi:os in the baseline is the operating system, and a program that newly calls os.system through it is inside the surface. A path or URL built while running is recorded as the unscoped grant, so it is caught, but only as "any path" or "any host". Paths are compared as text, never against the file system, so a symbolic link inside a recorded directory is that directory's content - the budget, which resolves every path, is what stops it at run time. A function is known by its file and name: one renamed while it gains an effect is a new function, held to its program's entry and the surface, not to what its old name declared. A file that does not compile adds nothing until it does, since it cannot run. The count bound is derived by fixed rules, and a loop whose number of turns is not written in the text has no bound. And the ratchet guards nothing if it is not required: a pull request that edits velaris.capabilities has accepted a widening, and the review of that edit is the control.

• What velaris deps-diff does not see. It sees declared surface, not behaviour. For a Velaris library that is the surface the ratchet derives from the text, with every limit of the ratchet above: what a granted ffi module does, a path or URL built while running seen only as "any path" or "any host", a function renamed while it gains an effect. For a package that is not Velaris it sees almost nothing. It reads the install-time scripts and the declared dependencies, says whether a script was added or changed - not what the script does - and reports the capability surface as unknown, with exit status 3, which is not a pass. It would not have caught postmark-mcp 1.0.16: by Koi Security's account that release changed only the code that sent the copy, which adds no install script and no dependency, so the report would have been "nothing gained that could be seen, surface unknown". Beyond that: it reads only the lockfile formats it names, and lists any other changed lockfile as not read; an entry resolved from git, a path, or a private registry or index is left out rather than compared with a public package of the same name; a dependency new in the upgrade has no earlier version and is listed, not examined; it compares at most 30 upgrades in one pull request and names the rest; it cannot read a version a registry has removed; it checks downloads against the digests the registry publishes, which a compromised registry would publish too; and in CI it informs and never fails the job, so what it finds is worth what the reading of its comment is.

• What an attestation does not say. velaris attest signs nothing: an unsigned Statement is a claim anyone could write, and a signed one says only that its signer ran this producer on those bytes and got this audit. It says no more than the audit - not that the program is safe, that the audit is right, or that any runtime will enforce its safe_command - and whatever the audit could not determine, it could not either.

• What a receipt does not say. A receipt (8.1) holds no value the program handled, and nothing more careful than that: it holds what the program did, and a program controls some of that without handing it a value - its exit status, the line at which it was refused or stopped, how many times it did something, how long it ran. After a declassify, a program can choose any of those from the declassified value. A declassification's reason is text the program's author wrote, and nothing checks it. Velaris signs no receipt, and a signed one says its signer ran this Velaris on these bytes and saw this run - as strong as the machine it ran on, with confinement: "none" saying the budget was the only boundary, and silent about any other run. A receipt marked complete: false lists what the killed worker reported, and counts at least that. A receipt written by --receipt is written when the run ends; a process killed from outside writes none.

• What ejecting does not keep. An ejected directory runs the Velaris it was ejected with, and no later fix reaches it. Its main.py checks the runtime and the program against their digests and cannot check itself: if anything but its owner could have written to the directory, compare it with SHA256SUMS before running. The proofs recorded in it are a record, not something the launcher trusts. Its refusal of a budget that writes where Python imports from is made where and when it is launched: a directory added to PYTHONPATH later is not known to it.

• A write grant to where Python imports from. A program allowed to write into a directory on some Python's import path - a PYTHONPATH entry, a site-packages, a user site - can leave a sitecustomize.py or a module there that the next Python process started with that path runs. That is not a Velaris effect, and a plain velaris program.vel --allow fs:write:... does not look for it; the ejected launcher refuses such a budget, and python -I ignores PYTHONPATH and the user site. Grant writes to directories that hold data, not code.

• What the invocation log does not hold. The program's source, output, stdin and arguments, and request headers, are not recorded; what a granted ffi module does inside Python shows only as ffi calls. A refusal names the path or host the program tried, which is the program's choice of text. A log written to stderr is kept only if whatever runs the door keeps stderr.

• A tampered compiler. Velaris is one Python file running in the same process as the untrusted program's interpreter. If the file, the package or the binary you run has been altered, nothing above holds. The release workflow signs every artifact and publishes an SBOM; SECURITY.md says how to verify a download. Verify it.

• The compiler as a target. Checking runs the parser, the type checker and the prover on untrusted source. The prover has a time budget per query; the other passes do not, and a hostile source can make a check slow or large. From 8.0 velaris check and audit, and from 8.1 the library's check, audit and attest, the doors' check and audit, and a bounded run's compile, stop at a ceiling (E613, E614); what stays inside the ceiling - 59 seconds of it, every time - is still spent. The language server has no ceiling: an editor that opens a file written to stall the prover waits for it, and so does a program that calls check(timeout=None).

• Compile-time reads. import "path" reads that file when compiling, before any budget applies - the budget governs what a program does when it runs. Until 8.1 this section said such a read "reads Velaris source, not data". It was wrong: nothing held the path to a .vel file, and an error inside a file that was not Velaris source quoted what it found, so a program sent to a door or a platform could read the first word of a file (advisory-import-read.md). From 8.1 that error shows nothing of the file, and the doors, and the library given import_root=, refuse an import outside the directory they serve (E515). Without an import root - the command line, and the library by default - an import still reads any .vel file the process can read, and the audit's fs_paths, net_hosts and ffi_modules include that file's literals. Give the library an import_root for source you were sent.

• The proof cache: removed in 8.2. Every proof is made in the process that reports on it or runs it, and no proof result is kept anywhere between runs, so there is nothing on disk to plant. The cache existed from 2.29 to 8.1.1 and held two holes: from 2.29 to 7.1.1 a ./.velaris/proofs.json shipped beside an untrusted program was believed (advisory-proof-cache.md), and from 7.1.2 to 8.1.0 an entry planted in the per-user directory was (advisory-proof-cache-2.md); in both a false ensures was reported proven and, compiled to native code, ran unchecked. check_adversarial.py's CACHE-1 to CACHE-10 plant both files and hold that nothing reads them.

• The prover's reach. Three benchmark rows (03d, 03f, 04e) are caught only while running: a division on the unguarded of two paths, a remainder inside a loop, a read at i + 1 in a loop over length(xs). The runtime check stopped each; the prover did not settle them beforehand. These are limits of the current prover, listed in RESULTS.md rather than worked around.

Known open #

The gaps this model does not close, kept as a table so the list is one place and stays current. None is a defect to be reported under SECURITY.md's challenge; each is a stated limit of what the effect budget is. A finding that a guarantee above is broken - a "proven" promise that breaks at run time, or an effect performed outside the budget - is a different thing, and SECURITY.md says how it is handled.

Residual risks, and what to do about each #

What "not a security boundary" means here #

The README says the effect budget is not a security boundary, and this document is the long form of that sentence. The budget is enforced by an interpreter written in Python, in a process that also holds the compiler, on a host that trusts that process. It is a strong guard against a program that does what it was not asked to - the situation you are in when a model hands you a script - and it is tested as such on every push. It is not a substitute for an OS-level sandbox, a network policy or a separate user account, and it should sit inside one of those when the stakes warrant it.