Sabline 8.6.0

Changelog: 3.x

Every release of this major version, newest first, as CHANGELOG.md records it.

3.4 - The doors are locked, and the findings go where findings go #

velaris serve ran any program sent to it by anyone who could reach its port; binding to localhost and printing a warning was the whole of the control. The MCP server granted whatever budget its caller asked for, ffi included. Neither door recorded what it was asked to do, and nothing let a client operator tell whether the MCP server's tool descriptions were the ones that were released. This release adds the four controls, and SARIF output so findings reach code scanning.

  • Bearer authentication on the HTTP door. Every endpoint but GET /health needs Authorization: Bearer <token>. The token comes from --token-file <path>, else VELARIS_TOKEN, else the door makes one with secrets.token_urlsafe(32) and prints it once. It is never read from the command line: --token, in either spelling, is refused at start, and the refusal does not repeat the value. Tokens are compared with secrets.compare_digest over sha256 digests; a missing token, a wrong one, another scheme, a bare Bearer or the token in a query string all get the same 401 body and a bare WWW-Authenticate: Bearer challenge, on every path including unknown ones, so nothing is learned about the door without the token. The door removes VELARIS_TOKEN from its environment before any worker starts, so a program granted env cannot read it. GET /health no longer names the ceiling to a caller without the token.
  • --no-auth, for local development, is refused unless --host is 127.0.0.1 or localhost, and prints a warning on every start. In its place a request must name a loopback Host, carry no other Origin, and post as Content-Type: application/json, which keeps a web page in a browser on the same machine (a cross-site fetch, or a DNS-rebinding page) from sending the door programs. It does not stop another local program, and the warning says so. These three checks were not in the request for this release; without them --no-auth would have let any open web page run programs.
  • The door refuses arguments it does not know, so --max-alow io is an error instead of a door whose ceiling silently stayed at every effect. A non-local --host now also warns that the door speaks plain HTTP and the token crosses the network in clear without a TLS proxy in front. The Server header no longer carries the Python version.
  • A ceiling on the MCP server. --max-allow takes the grammar the HTTP door takes - effects, fs:read:/fs:write: paths, net: hosts and ports, ffi: modules, @N counts - and the same Budget.covers check. A velaris_run asking for more at any level is refused with isError and the body the HTTP door sends with its 403: what was not granted, and max_allow. Without the flag the ceiling is io, and velaris_run's description and the .mcpb manifest say so. A ceiling that does not parse, or an unknown argument, stops the server at start.
  • A signed manifest of the MCP tools. The release workflow asks the MCP server inside the wheel it publishes for its tools, writes velaris-mcp-tools-X.Y.Z.json (velaris.mcp-tools/1: each tool's name, the sha256 of its description, the sha256 of its input schema in canonical form), signs it with sigstore alongside the wheel, sdist and SBOM, checks the signed manifest against the server with velaris mcp-verify, and attaches both to the release. velaris mcp-verify <manifest> -- <server command> verifies the signature as this workflow at the manifest's tag, starts the server the way a client does, and reports every tool whose description or schema changed and every tool added or missing (exit 1), or why it could not check (exit 2). It lives in velaris.py, not in the server file it checks. velaris mcp-manifest makes a manifest for any server. EMBEDDING.md says how a client operator uses it and what it does not tell them.
  • Invocation logging on both doors. One JSON line per call, velaris.invocation/1: when the call arrived, the door, the endpoint or tool, the outcome, the duration, the budget granted, the effects performed, what was refused and by what, the caller's address (HTTP), and the sha256 of the source - never the source, the output, request headers, the path as sent, or the token, which is also struck out of any line it could appear in. To stderr, or appended to --log-file; --log minimal keeps six fields, and nothing turns the log off. "Effects performed" is new in the runtime: RunResult.effects_used counts, per effect, the builtin calls the budget let through; it comes back from the pool workers the doors use, and is None for a child that could not report it.
  • SARIF 2.1.0. velaris check --sarif, proofs --sarif and audit --sarif write one run whose driver is Velaris at this version, with a rule for every code in the compiler's error table and for each finding that is not an error, each rule linking to its row on the published errors page. Results carry the file, the line and the message. Errors are error; a promise left to runtime is a warning (an error under --strict); a function promising nothing about its data, a loop not shown to end and each effect a function may perform are note. The output is validated against the OASIS schema, vendored under tests/ and held to its digest, in check_library.py. The GitHub Action has a sarif input, true by default, that writes the file and uploads it with github/codeql-action/upload-sarif pinned to the v4.38.0 commit.
  • What SARIF output leaves out. A Velaris fix is a sentence; a SARIF fix must carry the exact bytes to change (artifactChanges is required by the schema). Rather than make up an edit to fill the slot, the suggestions go in each result's properties.fixes. Figures with no line - a proven share, an audit's safe_command - go in the run's property bag, the latter as each file's velaris.audit/1 document unchanged.
  • The error table. velaris.ERROR_TABLE holds all 62 codes the compiler, runtime and library can give, one line each; the published errors page and the SARIF rules are both built from it, and check_library.py reads velaris.py's syntax tree and fails if a code is given anywhere that is not in the table, or is in the table and given nowhere. The page used to be a scrape of VelarisError(...) calls and missed E610, E611 and E612, which are reported another way; it now lists all 62, with an anchor on each row.

What a 3.3 user has to change. README's stability rule is that breaking changes wait for a major version; these three ship in a minor version because each closes an open door, and they are listed here so nobody meets them by surprise:

  1. A client of velaris serve must send Authorization: Bearer <token>. Start the door with --token-file or VELARIS_TOKEN, or read the made token from its first lines of output.
  2. An MCP client that relied on velaris_run granting more than io must start the server with --max-allow, as EMBEDDING.md shows.
  3. A workflow using the Action needs permissions: security-events: write for the upload, and code scanning enabled on a private repository - or sarif: "false".

THREAT_MODEL.md did not, in fact, list the unauthenticated door anywhere, as a residual risk or otherwise; it now has the door and the MCP server's caller in the trust boundary, the four controls in what is defended, what they do not defend in the list of what is not, and residual risks for the token, the ceiling, the tool manifest and the log. COMPLIANCE.md maps the four controls to OWASP MCP Top 10 (v0.1, beta) items MCP01, MCP02, MCP03, MCP07 and MCP08.

Verified, on Windows 11 with Python 3.13, before tagging, with the proof cache cleared first. With the prover: run_tests.py 92/92, check_library.py 142 correct (one skipped: the symlink case is POSIX only), check_sandbox.py 45, check_fallible.py 26, check_refusals.py 21, check_termination.py 44, check_pool.py 39, none wrong; fuzz_native.py 30 agrees, benchmark --quick --check matches results.json, velaris test examples/std_test.vel 7/7, velaris fmt --check clean. Without the prover, in a fresh virtual environment holding this tree, jsonschema and no z3 or llvmlite: the same eleven pass, with check_library.py 139 correct (two skipped for needing the prover, one POSIX only; the SARIF output validates there too, and check --strict --sarif reports that it could not check rather than passing) and check_refusals.py 11 with 10 skipped for needing the prover. Every workflow file and action.yml parse as YAML. velaris-spec's tools/check_sync.py and tools/validate.py pass against this tree; SPEC.md §6, §7 and §7.1, the grant grammar and velaris.audit/1 are unchanged, so the spec stays at 0.2. The new release steps were run by hand as far as they go without GitHub's signing identity: the wheel was built, installed in a clean environment, mcp-manifest made the manifest from its server, and mcp-verify --skip-signature matched 4 of 4 tools; the signature check itself was run against the sigstore bundle this workflow made for the 3.3.0 SBOM, accepting it and refusing it for changed bytes and for the wrong tag.

3.3 - The capability check now means what the spec says #

(This heading was lost from this file in the 3.4 release and restored in 4.0; the text below it is unchanged.)

velaris-spec 0.1 was extracted from 3.1.1 and, in writing each rule down precisely, found five places where this compiler did not do what the format says. 3.2 recorded them and changed no compiler code. 3.3 fixes all five, and velaris-spec goes to 0.2 in step, resolving the open questions the fixes close.

  • ffi:M is bounded to the module a call actually reaches, not just the one it names. The function argument of py, py_int, py_float, py_json and py_new may be a dotted path of attributes, and a granted module's attributes include the modules it imported. So py("json", "codecs.encode", ...) ran codecs code under ffi:json, because json imports codecs into its namespace and the chain walked straight into it. The whole dotted path a call names is now checked: the attribute chain is resolved step by step, and whenever a step yields an object whose owning module (a module's own name, or an attribute's __module__) has a top-level package outside the grants, the call is refused with E311 naming the module actually reached. The same check applies to a method or field reached through a handle (py_do, py_field) and to a non-JSON result kept as a handle. Where the owning module of an object reached along the chain cannot be determined - a bare code object, a frame, a reflective handle - the call is refused rather than allowed: the bound errs toward refusing more. Inert data (numbers, text, bytes, lists, maps) is not code from any module and is not checked, so a legitimate deep attribute like json.decoder.JSONDecoder still works. This is a security fix; where the chain cannot be placed soundly it refuses, and THREAT_MODEL.md and the spec say what remains reachable: a granted module can still do whatever that module itself can do.

  • ffi grants are additive, like fs and net. SPEC.md 7.1 says grants are additive; the parser restricted ffi to the named modules when both ffi and ffi:M appeared, so ffi,ffi:math granted math alone. It now grants every module: a plain ffi means every module, and the wider grant wins in either order, matching the reference text and fs/net. (velaris-spec Q2.)

  • safe_command round-trips. It wrote an IPv6 host without brackets (net:::1, which parses as the host : at port 1) and could not express a path or host containing , or @. An escaping rule is defined in the spec (v0.2 §5.1, §5.2) and implemented on both sides: IPv6 hosts are bracketed (net:[::1], net:[::1]:443), and , @ [ ] % are percent-encoded inside a path or host component and decoded when the budget is parsed. parse_budget of an audit's safe_command now reproduces the exact budget for awkward paths and hosts. (velaris-spec Q5.)

  • The budget parser is strict. An unknown effect name in a uses clause is a compile error (E300) naming the seven real effects; uses io, teleport no longer compiles and no longer reaches velaris.audit/1. Every malformed budget is a clean budget error, not a traceback: a count is ASCII digits only, so fs@² is a budget error rather than an uncaught ValueError; ffi takes no count and ffi: needs a module; an unbracketed IPv6 address, a stray bracket, a doubled @ and a scope on an effect that takes none are each refused with a readable message. (velaris-spec Q1, Q6.)

  • The command line's audit --json emits velaris.audit/1. It printed an older, unversioned shape the schema rejected; it now calls the library's audit().as_dict(), the same document the library, the MCP server, the HTTP door, the npm package, the CrewAI tool and the Action all emit. Its safe_command for examples/json_ffi.vel now says ffi:math,io rather than ffi,io. (velaris-spec Q3.)

The README's claim about ffi:M is restored. In 3.2 the README's "grants Python for those modules only; any other is refused" was weakened to say what was and was not reachable, because the claim was false: a granted module was a door into the modules it imported. With the first fix above it is true again, and the strong wording is back.

velaris-spec 0.2. The spec is revised where the behaviour changed and bumped to 0.2 with a dated annotated tag. It resolves Q1 (unknown names in uses are rejected), Q2 (ffi is additive; the wider grant wins), Q3 (the command line emits velaris.audit/1), Q5 (safe_command and net_hosts bracket IPv6 and the escaping rule holds , and @), and Q6 (non-ASCII count digits, ffi:M@N and ffi: are budget errors); the escaping rule is added to §5.1 and §5.2. Its section 2 still quotes this repository's SPEC.md §6, §7 and §7.1 word for word - those sections did not change, since "grants are additive" is now true for ffi too - so tools/check_sync.py still passes.

Sources, named (CONTRIBUTING.md rule): every fix here comes from the velaris-spec 0.1 extraction of 3.1.1, recorded in that spec's section 11 as open questions Q1, Q2, Q3, Q5 and Q6. HALL_OF_FAME.md credits the extraction under the standing challenge.

Verified, on Windows 11 with Python 3.13, before tagging. With the prover: run_tests.py 92/92, check_library.py 82 correct, check_sandbox.py 45, check_pool.py 39, check_refusals.py 21, check_fallible.py 26, check_termination.py 44, none wrong. Without the prover, in a fresh virtual environment holding this tree and no z3 - the subset the conformance suite requires: check_termination.py 44, check_sandbox.py 45, check_refusals.py 11 with 10 skipped for needing the prover, check_fallible.py 26, check_library.py with the runtime fallback asserted where a proof was, none wrong. fuzz_native.py 30, benchmark --quick --check, velaris test examples/std_test.vel and velaris fmt --check all pass. velaris-spec tools/check_sync.py and tools/validate.py pass against this tree.

3.2 - The capability format, published as a spec #

Nothing in the compiler changed: velaris.py differs from 3.1.1 only in its version string.

velaris-spec 0.1. The capability format has a specification of its own now, in a separate repository, gowrishankar-infra/velaris-spec, tagged v0.1: the seven effects and what "transitive" means; the grant grammar - fs:read:path, net:host:port, net:*.domain, ffi:module, @N - as this compiler parses and enforces it, edge cases included; what a budget guarantees at runtime and what it does not; velaris.audit/1 field by field; and velaris.capabilities/0, a ratchet baseline for CI that this compiler does not read yet, marked provisional until it does. It is written so that the format can be implemented in another language without reading velaris.py, and where a rule could not be stated precisely it says so, as one of eleven open questions. Its section 2 quotes sections 6, 7 and 7.1 of this repository's SPEC.md word for word; tools/check_sync.py there, run weekly by its CI, fails if the two drift. The spec is CC0, so anyone may implement it; this implementation stays MIT.

Conformance is defined here, not there. ARCHITECTURE.md now names check_termination.py, check_sandbox.py, check_refusals.py, check_fallible.py and check_library.py as the conformance suite, and an implementation claiming velaris.capabilities compliance must pass the subset that does not require the prover. The spec's JSON Schema for velaris.audit/1 was held against the audit of every one of the 107 .vel files in examples/ and stdlib/, and all 107 validate.

What writing it down found. Stating each rule precisely enough for someone else to implement it turned up places where the compiler, its documentation and its own SPEC.md do not say the same thing. None is fixed here, because this release changes no compiler code; each is recorded in the spec as what the reference does, and listed there as an open question:

  • velaris audit on the command line is not velaris.audit/1. With --json it prints an older, unversioned summary - compiles for ok, errors for problems, functions as a count - and both its safe_command and the command it prints under HOW TO RUN IT SAFELY are built from the coarse effects alone: for examples/json_ffi.vel, which calls only math, it says --allow ffi,io where velaris.audit() says --allow ffi:math,io. The library, the MCP server, the HTTP door, the npm package, the CrewAI tool and the Action's PR comment are all built on velaris.audit/1; the command line is the exception. The schema rejects the command line's output, and the spec says so rather than bending the schema to fit.
  • Grants are not all additive. SPEC.md 7.1 says they are. For fs and net that holds; for ffi it does not: ffi,ffi:math grants math alone. The spec follows the parser, since that is the reading that refuses.
  • ffi:M checks the module name a call gives, not what is reachable through the module. The function argument of py may be a dotted path of attributes, and a granted module's attributes include the modules it imported. THREAT_MODEL.md already said the allow-list narrows which modules and not what a module does; the README said "any other is refused", and now says what is refused and what is not.
  • safe_command is wrong in three cases. It writes an IPv6 host without brackets (net:::1, which parses as the host : at port 1); it passes through a path containing , or @, which the grammar cannot hold; and it copies in any name a uses clause gives, because uses io, teleport compiles and teleport reaches the audit.
  • The budget parser reads a count with Python's isdigit, so fs@٣ is a count of 3 and fs@² stops the parser with an uncaught error instead of a budget error; and ffi:math@5 is accepted as a module literally named math@5.
  • Six rules the spec states have no case in any check_*.py suite: a dotted function path through a granted module, ffi together with ffi:M, a URL without a scheme taken as HTTPS, IPv6 grants, an existence check under a write-only grant, and @0 or a count spent by an operation that then fails. The spec lists them as its Q9; adding the cases is work for a release that may change behaviour if a case fails.

Related work, cited. The README has a Related work section after the opening, naming TACIT (ACM CAIS '26, arXiv 2603.00991), CaMeL and WASI, what each does, and what Velaris does differently, including what it does not do: it tracks no data flow, and its command line grants every effect when no budget is given. The spec's PRIOR_ART.md has the longer account, with object capabilities, in-toto and SLSA, SARIF, Deno's permissions and effect systems. The README's velaris card line said ~1,500 words, the size of the card in 2.41; it is 3,335 words by wc -w now, and the README says ~3,300 in both places.

Sources, named. CONTRIBUTING.md gains a rule: when a design decision comes from published work, name the source in the CHANGELOG entry for that release; say which person, model or bot found a review finding; and when the origin is not known, do not guess. Applied backwards where the record allows it. 2.41.1 (a Gemini model), 2.41.2 (a ChatGPT model), 2.42 and 2.44 to 2.47 (a Claude model) now say which model family found what, from the maintainer's account, since none of those entries recorded it at the time and HALL_OF_FAME.md had declined to guess; HALL_OF_FAME.md carries the same names now. 2.59 names CodeRabbit on crewAIInc/crewAI#7279, from the public pull request, which also dates its review 2026-09-05; HALL_OF_FAME.md had said 2026-09-10, and is corrected. Nothing else was attributed, because no other entry's provenance is on record.

This release's own sources, under the new rule: the schemas are JSON Schema draft 2020-12, the spec's requirement words are those of RFC 2119 and RFC 8174, and its license is Creative Commons CC0 1.0. The work in PRIOR_ART.md is related work, not a source - none of it is on record as the origin of a Velaris design decision, and the spec says so.

Verified, on Windows 11 with Python 3.13, before tagging. With the prover: run_tests.py 92/92, check_library.py 75 correct, check_sandbox.py 34, check_pool.py 39, check_refusals.py 21, check_fallible.py 26, check_termination.py 44, none wrong; the one skip in each of the first two is the symlink escape, which needs POSIX. Without the prover, in a fresh virtual environment holding this tree and no z3, as rule 7 asks - the subset the conformance suite requires: check_termination.py 44, check_sandbox.py 34, check_refusals.py 11 with 10 skipped for needing the prover, check_fallible.py 26, check_library.py 73 with the runtime fallback asserted where a proof was, none wrong. The reference implementation passes its own conformance subset.

3.1.1 - A pool test that passed for the wrong reason #

check_pool.py claimed to hold a program that reaches into the compiler through a granted ffi module, adds fs to the live budget, and is then unable to leave it added for the next program. It did not. The program named py("velaris", "EFFECT_BUDGET.add", ["fs"]), and a worker runs velaris.py as __main__ - so that name imported a second copy of the module and widened that copy's budget, never the one the interpreter was enforcing. The next program was refused fs because it had never been granted, not because anything was reset. The check passed, and would have passed just as well with reset_program_state deleted.

It now names __main__, which is the live module, and reads a file immediately afterwards so the suite can assert the widening really took hold before it asserts that the next program is refused. Two checks where there was one:

Sabline
ok  a program CAN widen its own budget through ffi - the cliff is
    real, and this is what the next check is against
ok  ...and it cannot widen it for the next program

The reset was correct the whole time - the counted-grant check (fs:read:<dir>@2, spent per program rather than per worker) was already exercising the same reinstall from a different angle, and it still passes. What was wrong was a test whose label was stronger than its body, which is worse than no test at all: it is the one thing that makes a suite untrustworthy about everything else in it. The 3.1 entry below says "the suite has one that does exactly this"; of 3.1.0 that sentence was false, and it is true from 3.1.1.

Also here: check_library.py's skip messages said "(needs the prover)" for skips that had nothing to do with the prover - the macOS memory cap and the POSIX-only symlink escape now say why they were actually skipped.

39 checks in check_pool.py, all passing with and without the prover. Nothing in velaris.py changed.

3.1 - A pool that keeps its budget, memory caps on Windows, and a lockfile #

velaris.Pool: bounded runs without a new interpreter every time. Every run with a timeout or a max_memory_mb started a Python process, about a tenth of a second before a line of Velaris was read. An agent platform calling run thousands of times an hour paid that every time.

Text
pool = velaris.Pool(size=4, allow={"io"}, timeout=30,
                    max_memory_mb=512)
result = pool.run(source)          # the same RunResult run() returns
pool.close()                       # also a context manager

Measured by check_pool.py on the machine this was written on, 200 sequential bounded runs of a small program: 46.56 s a process at a time, 0.48 s on a pool - 233 ms each against 2.4 ms each, 96.7x. The suite asserts at least 3x and prints both numbers, so the claim is re-measured wherever it runs rather than quoted from here.

The speed is why it exists. The isolation is why it can be used, and these are the rules, each one asserted in check_pool.py:

  • The budget is the pool's, not the program's. It is parsed once, when the pool is made, and installed by each worker at startup. pool.run takes no allow argument - there is nowhere for a caller or a program to ask for more, and a different budget means a different pool. The budget is re-asserted from the pool before every program, so an @N count is spent per program rather than shared across a worker's whole life. A program that reaches into the compiler through a granted ffi module and adds fs to the live budget - the suite has one that does exactly this - cannot leave it added for the next program.

  • A worker is used once unless the run was clean. Anything other than ok - a refused effect, a failure that escaped, a program that did not compile, the timeout, the memory cap - kills the worker and starts a fresh one. This is stricter than it has to be: a program that failed to compile never ran, so it left nothing behind, and retiring its worker costs a restart. It is stricter on purpose, because "only a clean run hands its worker back" is a rule a reader can check in one line of Pool.run, and the weaker version is a rule about which failures are harmless.

  • A reused worker starts empty. Before every program the child resets every module-level mutable there is. Searching for them was the work; the list, exhaustively, is PROGRAM_ARGS, EFFECT_BUDGET, FFI_MODULES, FS_GRANTS, NET_GRANTS, OP_LIMITS, OP_COUNTS, PY_OBJECTS (handles from py_new, closed by the program or not), PY_NEXT (so handle numbering starts again), TRACE, and _NATIVE_KEEPALIVE - which holds the JIT engines and, through them, the native text arena. There is no proof cache in memory to clear: check_proofs keeps its cache on disk and only when asked (use_cache=True), and the library never asks. Three things that belong to the process rather than the module are put back too, because a granted ffi module can change all three: the working directory, the environment, and the recursion limit the interpreter raises. They are named in MUTABLE_GLOBALS and reset_program_state, and check_pool.py parses velaris.py's own module-level assignments and fails if a mutable one appears in neither that list nor its list of constants - so the next person to add a global cannot forget. That is now rule 6 in ARCHITECTURE.md.

  • The parent owns the deadline. A worker that has not answered within timeout is killed by the parent, not asked to stop, and a replacement is started; the call returns E610.

  • A program cannot reach the pipe. The worker keeps private duplicates of its own file descriptors 0 and 1 for the protocol and points the program's at the null device. The suite has a program that runs echo through ffi:os straight at file descriptor 1; the shell's output goes nowhere and the next program still runs.

  • Closing kills every worker, including one still running a program. A pool collected without close() is closed by its finalizer, one that outlives the interpreter is closed at exit, and a worker whose pipe closes ends by itself. The suite checks all three against the operating system's own answer about the process ids, not the parent's bookkeeping.

velaris.PoolRegistry keeps one pool per distinct budget and makes each the first time that budget is asked for - what a server needs, since it learns the budget from the request. The MCP server and the HTTP door each keep one and close it on shutdown; a caller who varies the budget every time cannot make either hold processes without end, because the registry keeps at most eight pools and closes the least recently used. The CrewAI and LangChain tools stay on plain run: a crew's tool is not called often enough for a pool to pay for itself, and one process per call is easier for a reviewer to reason about.

Memory caps are enforced on Windows. Windows has no RLIMIT_AS. The equivalent is a job object with JOB_OBJECT_LIMIT_PROCESS_MEMORY, which has to exist before the child does: the child is created suspended, assigned to the job, and only then resumed, so no instruction of it runs outside the cap. An allocation past the cap fails and reaches a Python child as MemoryError, which is already what _run_bounded reads as E611. JOB_OBJECT_LIMIT_KILL_ON_JOB_CLOSE means closing the handle kills whatever is inside, which is also how a pool kills a Windows worker. It is ctypes; no new dependency. If any step fails - CreateJobObject, SetInformationJobObject, AssignProcessToJobObject - the cap is recorded and not enforced, which is exactly what Windows did before 3.1, rather than the run failing.

So the platform rule is now: enforced on Linux (RLIMIT_AS) and on Windows (a job object); best-effort on macOS, where the limit is set and not reliably honoured and the timeout is what stops a runaway. velaris.memory_cap_is_enforced() answers for the machine you are on, and check_library.py asks it rather than reading the platform name, so the assertion now runs on Windows as well as Linux and skips only where the mechanism genuinely does not hold. Every place that stated the old rule was rewritten: EMBEDDING.md, THREAT_MODEL.md, COMPLIANCE.md, SECURITY.md, the MCP tool description, run's docstring, benchmark/README.md and the header benchmark/run.py writes - the last of which now asks the compiler instead of guessing from sys.platform.

On POSIX the cap moved from a preexec_fn in the parent to --max-memory-mb on the child's own command line, which the child applies before it does anything else. preexec_fn is documented as unsafe when the parent has threads, and the HTTP door has had threads since 2.54 - a latent hazard, not an observed failure, and it is gone.

velaris.lock. velaris add already recorded a sha256 in velaris.toml. It now also writes velaris.lock: every vendored library with its source, its sha256 and the version of Velaris that added it, as JSON, sorted, one library per entry.

Text
velaris deps --verify      # do the files match the lock?
velaris add <url> --force  # replace a library with different bytes

velaris deps --verify (velaris verify is the older spelling of the same check) fails if a vendored file's hash differs from the lock or a locked library is not on disk, and says which. A project with no lock falls back to checking velaris.toml and says the lock is missing. velaris add refuses to overwrite a library that is already vendored when the incoming bytes differ, printing both digests; --force replaces it. A library that does not compile is still not accepted - and now the file it would have replaced is put back rather than deleted.

One thing changed underneath: a vendored library is written as the exact bytes that arrived, in binary, rather than decoded and rewritten as text. Before 3.1 the same library added on Windows and on Linux locked two different hashes, because the rewrite translated line endings - which makes a lockfile useless for the one thing it is for. The digest is now the digest of what the source published, and the same everywhere.

Fixed: an empty budget did not survive the trip to a child process. velaris.run(source, allow=set(), timeout=1) came back with E000 and "'''' is not an effect" instead of refusing io with E310. The parent spelled an empty budget as the two characters '', which a shell strips and subprocess does not. Budget.parse now reads '' and "" as an empty budget. Without a timeout the same call was always correct, which is why it went unnoticed.

Fixed: run left Python handles behind in a shared process. It restored the budget and the program's arguments afterwards and not PY_OBJECTS, so a framework calling run in a loop accumulated every handle every program opened and did not close. It now puts those back the same way, which is also what a pool worker does between programs.

The benchmark. Rerun in full on Windows 11 with Deno 2.9.6 and Python 3.13: identical verdicts to 3.0 on all 63 programs. Of the 56 dangerous programs Velaris caught 54 - 42 before running, 12 while running - and missed 2; Deno caught 32 (5 before, 27 during) and missed 24; plain Python caught 28 (all while running) and missed 28; none of the three flagged any of the 7 controls. The Windows job object changed no verdict: in category 8 the interpreter still reaches the 5-second deadline before 256 MB, and RESULTS.md says so rather than implying the cap did the work. THREAT_MODEL.md had been carrying the 2.62 figures (60 programs, 53 dangerous, 51 caught) and COMPLIANCE.md said 60 programs; both now match RESULTS.md, and the README and docs/index.html carry the table for the first time. Two other stale counts in the README went with them: check_sandbox.py is 24 escape attempts and 10 honest programs, not 11 attempts, and check_refusals.py is 21 wrong programs, not 20.

The published docs were three versions stale. docs/ had last been rebuilt at 2.60, so the reference page still said the effects were io, fs, net, clock, rand, ffi with no env, and the library page still showed env_tools.setting using io. Rebuilding for this release brought the site up to 3.1; the error-code count on the home page is now read from the generated page rather than typed by hand, where it had drifted from 49 to 59.

New suite. check_pool.py - 38 checks, run without the prover first, as ARCHITECTURE.md rule 7 requires. check_termination.py joined CI at the same time; it had existed since 2.62 and never been wired in.

3.0 - Budgets that name paths, hosts, counts, and secrets #

This is a major version because a program that compiled under 2.x can be refused by 3.0: env() is its own effect now, and a function that called it under uses io alone is refused at compile time with exactly "env() now needs 'uses env'" and the fix. The reason is the sentence THREAT_MODEL.md had to carry since 2.63 - an io-only budget could read and print every secret in the environment. It cannot now. io is the console: print, read_line, args. stdlib/env_tools.vel and the two examples that read the environment declare env.

The 2.60 module allow-list, extended to every coarse effect. The budget grammar (SPEC.md 7.1) narrows fs and net the way ffi:math narrows ffi:

Text
fs:read:./data  fs:write:./out       one direction, under a path
net:api.example.com:443              one host and port
net:*.example.com                    one label in place of the star
fs:read:./data@50  net:...@100       at most that many operations

Every path is resolved with realpath when the budget is parsed and again at every read_file, write_file and file_exists, then compared as a prefix, so .. and symlinks cannot reach past a grant (E313, naming the path). fetch, post, fetch_status and request check the URL's host and port before any connection (E314); a wildcard matches exactly one label and never the domain itself, and no wildcard may stand over an IP literal. A count is the smallest given for that effect and applies to the whole run (E315); a budget with no count is a budget on what, not on how much. Every one of these refusals is uncatchable, like E310 and E311. The one catchable case is a redirect whose target lies outside the net: grants: the program asked for one host and was sent to another, so the request fails with the target named and the program hears why.

The grammar travels unchanged through --allow, velaris.run(allow=), the bounded child (which receives the budget re-spelled with absolute paths), the MCP server, the HTTP door, the CrewAI and LangChain tools and the Jupyter magic. The door's --max-allow takes it too, and a caller may not ask for more than the server grants at any level - an effect, a module, a wider path prefix, a host the server does not name, a port, a larger count, or an unscoped fs or net against a scoped ceiling - and is told which. The audit reads the paths and hosts a program names in literals (fs_paths, net_hosts, added within velaris.audit/1) and its safe_command grants exactly those, falling back to fs:read or net where a value is built at runtime.

Stated as outside the rule rather than claimed: 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, and a Velaris program has no threads to race itself; where a granted host name resolves is DNS's business.

Tested. check_sandbox.py gained twelve cases: a read outside the prefix, a write with only read granted, a .. escape, a symlink escape (POSIX; skipped on Windows), a host not in the list, a wildcard that must not match its parent domain, a port not in the list, a redirect to an ungranted host against a local server, the count reached on fs and on net, env() with only io granted, and an honest program using exactly its grants that must run - plus a redirect to a granted host that must be followed. check_library.py has the same through velaris.run and through the HTTP door with a ceiling narrower than the request at each level. check_fallible.py has the redirect failure as a recipe. The benchmark gained category 11 - a read outside the granted directory, a request to an ungranted host, a secret read through env - run under the narrowest budget each task needs, with Deno given the matching --allow-read=<dir> and --allow-net=<host:port>; Velaris refuses all three (the path and the URL arrive on stdin, so the first two are refused while running, and the third is flagged before), Deno refuses all three at the call, and Python, with no budget, does all three. THREAT_MODEL.md moves "io includes env", "fs has no path list" and "net has no host list" from the non-defences to the defences, each with its suite.