Changelog: 4.x: 4.2 to 4.0

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

4.2 - A producer for the capability predicate #

A minor version. 4.1 published an in-toto predicate type for the audit and wrote no Statements of it; velaris attest writes them, and the release workflow signs one. The author's name is corrected everywhere it appears.

velaris attest <path> [--output FILE] [--json] writes an in-toto Statement v1 of the predicate type https://gowrishankar-infra.github.io/velaris-lang/capability/v1 (velaris-spec 0.5, section 8.5). Its subjects are the audited file and every file it imports, each by the sha256 of its bytes - a standard library file named <stdlib>/NAME, since where it sits on disk is the machine's business. Its predicate is the published shape: producer (velaris-lang and this repository), specification (velaris-spec 0.5), auditedAt - from SOURCE_DATE_EPOCH when it is set, so one commit gives the same bytes twice - and audit, which is audit()'s own velaris.audit/1 document for those bytes, not a copy recomputed beside it: effects, fs_paths, net_hosts, ffi_modules, ffi_any, counts, proven_share, prover and velaris_version are the audit's. It sets no conformance claim, since it runs no corpus. A directory gives one Statement per .vel file, found as velaris capabilities finds them, one to a line (JSON Lines), because the predicate type holds one audit per Statement. A file that is not UTF-8, or that changes while it is being attested, is an error (exit 2), not a Statement. Without --output or --json it prints a summary: each file's digest, whether it compiles, its effects, and ffi_any when set. velaris.attest(path) in the library returns the Statements as a list; STABILITY.md adds it to the stable API.

When the audit cannot tell, the Statement says so. Two fields are added to velaris.audit/1, optional within version 1 (velaris-spec 8.2), so that an attestation can state what was not determined instead of leaving it out:

counts: for fs and net, the most operations one call to a function the file defines can perform, by velaris-spec 9.4's rules - the same code (_operation_bounds) the capability baseline uses. 0 for an effect none of them declares; null where the text fixes no bound, such as a loop over args(); and null as a whole when the file does not compile.
prover: whether a prover decided the promises' status. It is false without one, where no status is proven and a proven_share of 0 says nothing about what could be proven; and false when the file does not compile.

With the fields already there - ok false and its problems, ffi_any for a module named while running rather than a shorter module list, read_any, write_any and any for a path or URL built while running - the Statement carries whatever the audit could not determine as the audit states it. EMBEDDING.md's table of audit fields has both. load_program takes an optional list it appends each file it reads to, which is how attest names the imports it digests.

Signing is left to Sigstore's tools. Nothing here signs. EMBEDDING.md gives working commands for cosign 3 (cosign attest-blob --statement, keyless and with a key pair, and cosign verify-blob-attestation, which fails when the file is not the Statement's subject by digest) and for sigstore-python 4, whose command line attests only SLSA provenance, so the library's sign_dsse and verify_dsse are used. The cosign key-pair commands were run here against a Statement from this build with cosign v3.0.6, offline - a signing config naming no transparency log, and --insecure-ignore-tlog to verify: it signed, verified, and refused an edited effects.vel ("provided artifact digest does not match any digest in statement"). The sigstore-python snippet was run as far as the browser sign-in, which needs a person.

The release signs one. release.yml has a new job, attestation: it installs this commit with the prover, writes velaris attest examples/effects.vel with SOURCE_DATE_EPOCH at the commit's time, signs the Statement keylessly as a DSSE envelope with cosign and with sigstore-python, verifies both bundles against the workflow's own identity - cosign against the example's bytes, sigstore-python by comparing the signed Statement and the first subject's digest - and attaches velaris-attestation-X.Y.Z.intoto.json and the two .sigstore.json bundles to the release. The workflow can also be run by hand (workflow_dispatch); then only this job runs, signing and verifying under the branch's identity and publishing nothing, and the jobs that build and publish packages run only for a tag. SECURITY.md gives the command to verify the attestation.

Tests. check_library.py gains 12 checks on five programs in a scratch directory and a two-file program: a directory gives one Statement per .vel file; every digest is the sha256 of the file's bytes; each predicate's audit equals audit() of the same program, field for field; every Statement validates against in-toto's Statement v1 schema, the capability/v1 predicate schema this repository publishes, and velaris-spec's velaris.audit/1 schema; a module named while running is ffi_any, with an empty module list; a count the text fixes is its number and one it does not is null; a program that does not compile is ok false with its problem, counts null and prover false; prover matches whether a prover is installed; an imported file is the next subject, with its own digest; and the command line's --json is the library's Statement, its time fixed by SOURCE_DATE_EPOCH. in-toto publishes its Statement schema as prose and protobuf, not JSON Schema, so tests/in-toto-statement-v1.schema.json is written from its statement.md, resource_descriptor.md and digest_set.md at commit 2dcd055e, which the file names. CI checks out velaris-spec before the suites run, so check_library.py holds the audit to the spec's schema on every leg.

velaris-spec 0.5 records the producer in section 8.5 and the two fields in 8.2 and its audit schema; its examples/capability-statement.json is now what velaris attest examples/effects.vel writes at this tag, and REGISTRY_SUBMISSION.md names the producer, the command that fetches the signed Statement, and embeds that Statement. Still not submitted.

The author's name. The author is Palakurthi Gowri shankar: family name Palakurthi, given name Gowri shankar. CITATION.cff in both repositories now says family-names: Palakurthi and given-names: Gowri shankar, and both validate against the CFF 1.2.0 schema (with jsonschema and with cffconvert --validate). The full name replaces the earlier forms in LICENSE, the VS Code extension's LICENSE, README.md, SUPPORT.md, MAINTAINERS.md, PROVENANCE.md, pyproject.toml, the npm, MCP bundle and winget manifests, the LangChain integration's metadata, paper/velaris.md and paper/references.bib (as {Palakurthi, Gowri shankar}, the comma form: without the comma BibTeX would read shankar as a particle like "van"), and in velaris-spec's NOTICE, README.md and REGISTRY_SUBMISSION.md. In a reference list the family name leads - "Palakurthi, Gowri shankar" in full; abbreviated, BibTeX writes "Palakurthi, G. s." and cffconvert's APA-like form "Palakurthi G.s." - and a citation in the text is "(Palakurthi, 2026)". A CSL processor (citeproc-js) abbreviates only a capitalised given name, so its APA style writes "Palakurthi, G. shankar".

Provenance. Both PROVENANCE.md files record the second pair of Software Heritage saves, 2471049 and 2471050, taken after the 4.1.0 and 0.4 push, with their snapshots, beside the first pair.

Sources, named (CONTRIBUTING.md rule): the parts of this release were specified by the maintainer. The Statement follows in-toto's Statement v1 and ResourceDescriptor specifications, and its directory form the JSON Lines layout of in-toto's Bundle specification, at commit 2dcd055e; the signing commands follow cosign's and sigstore-python's own documentation and were checked against cosign v3.0.6 and sigstore-python 4.5.0.

Verified, on Windows 11 with Python 3.13, with the proof cache cleared first. With the prover (z3 5.1.0, llvmlite 0.49.0): run_tests.py 92/92, check_library.py 196 correct (one skipped: its symbolic-link case is POSIX only), check_sandbox.py 49 (its symbolic-link case skipped: this machine will not make a link), check_fallible.py 26, check_refusals.py 21, check_termination.py 44, check_pool.py 39, check_ratchet.py 114, none wrong; fuzz_native.py 30 agrees; benchmark/run.py --quick --check matches results.json; velaris test examples/std_test.vel 7/7, velaris examples/edges.vel 20/20, velaris fmt --check clean, velaris capabilities check . passes; velaris conformance reports L1, L2 and L3 conformant, 443 of the 444 cases run and the symbolic-link case skipped, and --level 1, --level 2 and --level 3 each report their level conformant; build_conformance.py --check matches velaris-spec's corpus. Without the prover, in a fresh virtual environment holding this tree and jsonschema and no z3 or llvmlite, all of the same pass, with check_library.py 193 correct (two skipped for needing the prover, one POSIX only) and check_refusals.py 11 with 10 skipped for needing the prover. With the prover and without it, velaris attest examples/effects.vel at a fixed SOURCE_DATE_EPOCH writes the same Statement except prover. The audits of the 107 .vel files directly in examples/ and stdlib/ (73 compile, with counts set and prover true; 34 do not, with counts null and prover false) validate against velaris-spec 0.5's audit schema through its tools/validate.py --audits, as does this repository's velaris.capabilities; its tools/validate.py (schemas, examples, the example Statement, the 444 cases) and tools/check_sync.py pass. Both CITATION.cff files validate against the CFF 1.2.0 schema. The release workflow's attestation job has not run before this commit's push, so whether it signs and verifies in GitHub's runners is for that run to say.

4.1 - Conformance you can run, provenance you can check #

A minor version. Conformance to the capability format stops being a sentence naming this repository's suites and becomes a corpus any implementation can run; velaris conformance runs it here, on every CI leg. The project gets citation files, an entry in an independent archive, and a predicate type whose URL resolves; and a preprint is drafted, for the maintainer to read. One defect, found by writing the corpus, is fixed.

4.0.1 was committed and pushed but never tagged, so it was never published; its fix to velaris review ships in 4.1.0.

The conformance corpus. velaris-spec 0.4 holds tests/: 444 JSON cases, each with an id, its level, a description, the input - budget text, Velaris source, a tree of files and a change to it - and the outcome an implementation must produce: the grants a budget parses to or its refusal, an audit's effect surface, a refusal and its code, a baseline, or a verdict with every widening and the rules it fails. 298 cases at L1, declaration (280 budgets, 18 audits); 37 at L2, enforcement (programs run under a budget, with a fixture of files and two local HTTP servers); 109 at L3, the ratchet (14 baselines to write, 51 changes to check, two sequences, the writer's guard, and 32 covering, 3 reduction and 6 operation-bound cases). velaris-spec's CONFORMANCE.md defines the levels and the behaviours each requires, and says plainly that no level requires a prover; tests/README.md is the runner contract. Five L3 cases are the ratchet's known limits from the 4.0 entry below, recorded with the outcome the check gives today - two widenings that pass, three non-widenings that fail - so that another implementation matches it rather than guessing.

The corpus is not written by hand. build_conformance.py transcribes it from tables in three suites, where the same entries are asserted against this implementation, and computes nothing itself; --check regenerates it and fails when it differs from what velaris-spec commits. For that, the suites became tables, and asserting them made them stricter:

check_sandbox.py holds each case as data, with placeholders for its paths and ports, and asserts the refusal code each must carry. Until 4.1 it accepted any of the five codes, so a runtime refusing a path outside its prefix with E310 rather than E313 would have passed. It runs its fixture in a temporary directory rather than in the repository, and its symbolic-link case wherever the system will make a link, not only on POSIX. Four cases are new, the four rules velaris-spec 0.3 listed as untested (its Q9): @0, a count spent by an operation that then fails, a URL with no scheme taken as HTTPS, and an existence check under a write-only grant. 34 escape attempts and 16 honest programs.
check_library.py gains BUDGETS, 55 budgets each held to what velaris-spec sections 4 and 5 say it means - the grants for 51, a refusal for 4 - including the spec's own examples and denials (until 4.1 the awkward ones were checked to round-trip, not for what they parse to); and AUDITS, 18 programs each held to the effect surface its audit must report, and to the schema. The malformed-budget list moved out of main() so the corpus can be written from it.
check_ratchet.py's scenarios became DERIVE, CHECKS, SEQUENCES, WRITE_GUARD, COVERING, REDUCE and BOUNDS. Each check now asserts the complete list of widenings, with the rules each fails, where most cases asserted one finding; each derivation asserts the whole baseline. New: 14 baselines written for trees; the writer refusing, unasked, to write a baseline for a tree that needs more; a new effect; a new program outside the surface (W1 alone); fs declared with no file named, which needs plain fs; another spelling of a path; a port under a portless grant; 9 covering and 2 reduction cases; and the five known limits. What only this implementation says, such as the call chain, velaris review, SARIF and warning text, is asserted after, on the same scenarios.

Thirteen scenarios are left out of the corpus, and tests/index.json says why each: six attempts to reach an ungranted Python module through a granted one, which depend on Python's object model; four honest programs that need a Python host; a run given no budget, which the format leaves to the implementation; and two about this command line's flags.

velaris conformance [--level 1|2|3] [--json] [--corpus DIR] runs the corpus against this implementation, through the doors another implementation would use: the budget parser, the audit, the command line under a budget, the baseline writer and the check. It finds the corpus beside the working directory or the installation, prints a line per level and a one-line verdict, and exits 1 if any case of a level asked for fails. --json is velaris.conformance/1, one result per case, the report shape tests/README.md gives any runner. --level N runs the cases a claim at level N needs: L1 and N. A case that needs a symbolic link is skipped where none can be made, and the verdict says so; without jsonschema the cases that validate a document against velaris-spec's schemas are skipped too, and the level is reported as not shown. It passes at all three levels. Run against a copy of the corpus with twelve expectations broken, covering all ten kinds of case, and one case given a kind no runner knows, it fails exactly those 13 cases and exits 1.

CI. Every one of the twelve legs checks out velaris-spec, runs the drift test and velaris conformance against its corpus. velaris-spec's own CI runs the drift test and this implementation's conformance against its corpus, beside its schema and sync checks.

Found by the corpus, and fixed. The audit of a program refused for naming something that is not an effect in a uses clause (uses io, teleport, E300) still listed that name in effects and in the function's effects, and wrote a safe_command that does not parse. velaris-spec had said since 0.2 that effects holds only the seven names and that safe_command always parses; 3.3 had fixed the compile check and not the document that reports it. From 4.1 audit leaves any name that is not an effect out of all three; the E300 still names it. This is not a breaking change under STABILITY.md: the fields' documented meaning is unchanged, and it is the implementation that now matches it; what changes is the content of a document whose ok is false, which velaris-spec says bounds nothing. HALL_OF_FAME.md credits the corpus. velaris-spec 0.4 corrects the sentences that had inferred from 3.3's rejection more than the implementation did.

Provenance. CITATION.cff in both repositories (CFF 1.2.0, checked against the format's schema), with the author, the repository, the version and its date, and a note that a preprint is forthcoming; both READMEs say "Cite this repository". Both repositories were submitted to Software Heritage through its save-code-now API, and PROVENANCE.md in each records the save requests' ids and dates beside the first commit of the effect system, the date velaris-spec 0.1 was tagged, and that velaris-lang is the reference implementation.

A resolvable predicate type. velaris-spec 0.4 section 8.5 defines an in-toto predicate type for velaris.audit/1 bound to the digests of the files audited, and its URL is on this repository's documentation site: https://gowrishankar-infra.github.io/velaris-lang/capability/v1, which build_docs.py now writes, with schema.json beside it, identical to velaris-spec's schemas/capability-predicate.v1.schema.json (velaris-spec's tools/check_sync.py fails if they differ). velaris.dev was not used: on 2026-09-11 it answered every path with a Vercel DEPLOYMENT_NOT_FOUND, and nothing here says who controls it. This implementation publishes the type and does not yet write Statements of it; velaris-spec's example was assembled from velaris audit --json and a file's digest. A pull request listing the type in in-toto's predicate registry is prepared in velaris-spec's REGISTRY_SUBMISSION.md, and not sent.

A preprint, drafted. paper/velaris.md and paper/references.bib: the problem, the design, the implementation, the evaluation, related work, limitations and a reproducibility section, with a table naming the file each number comes from. Not submitted anywhere.

Also corrected. The documentation site's benchmark table said "Velaris 3.1" and the README's did too, where benchmark/RESULTS.md said the table was produced by 3.0.0. The table was regenerated with 4.1.0: every verdict and every line of evidence is what 3.0.0 produced, and only the version line of RESULTS.md and results.json changed; the pages now say 4.1. EMBEDDING.md's table of audit fields lacked ffi_any, added in 4.0. velaris-spec's PRIOR_ART.md said this implementation emits no SARIF, untrue since 3.4.

Sources, named (CONTRIBUTING.md rule): the parts of this release were specified by the maintainer. The runner contract follows no published harness. in-toto's docs/new_predicate_guidelines.md and predicate template, read on 2026-09-11, shaped REGISTRY_SUBMISSION.md. Hills, Caspary and Cooper Stickland, "Distributed Attacks in Persistent-State AI Control" (arXiv:2607.02514), is cited by the paper and by velaris-spec's PRIOR_ART.md as the gradual-attack result the ratchet addresses; the record does not say it influenced the ratchet's design in 4.0, and this entry does not claim it did.

Verified, on Windows 11 with Python 3.13, with the proof cache cleared first. With the prover: run_tests.py 92/92, check_library.py 184 correct (one skipped: its symbolic-link case is POSIX only), check_sandbox.py 49 (its symbolic-link case skipped: this machine will not make a link), check_fallible.py 26, check_refusals.py 21, check_termination.py 44, check_pool.py 39, check_ratchet.py 114, none wrong; fuzz_native.py 30 agrees; benchmark/run.py --check over the whole table and --quick --check match results.json; velaris test examples/std_test.vel 7/7, velaris examples/edges.vel 20/20, velaris fmt --check clean, velaris capabilities check . passes; velaris conformance reports L1, L2 and L3 conformant, 443 of the 444 cases run and the symbolic-link case skipped; build_conformance.py --check matches velaris-spec's corpus. Without the prover, in a fresh virtual environment with jsonschema and no z3 or llvmlite, the same pass - the benchmark with --quick --check only - with check_library.py 181 correct (two skipped for needing the prover, one POSIX only), check_refusals.py 11 with 10 skipped for needing the prover, and velaris conformance again conformant at L1, L2 and L3. velaris-spec 0.4's tools/validate.py (schemas, examples, the example Statement, all 444 cases against the case schema) and tools/check_sync.py (the quoted sections, and the predicate schema against docs/capability/v1/schema.json) pass against this tree. The symbolic-link cases run where a link can be made - the Linux and macOS runners, and the Windows runners if they allow it - and whether they pass there is for this commit's CI to say.

4.0.1 - The review read the old files from the wrong place #

4.0.0's CI failed on its four Windows legs, in check_ratchet.py: the five checks that go through velaris review failed. The capability check - the gate - passed every one of its cases on all twelve legs.

The cause was in review. To find where the checked directory sits in the repository, it compared the working directory's path with the path git rev-parse --show-toplevel prints, as text. On the Windows runners the temporary directory is a short name (C:\Users\RUNNER~1\...) and git prints the long one, so the two did not match, and the files at the ref were materialised and read from a directory that was not the ref's place in the tree. The review then reported the surface as widened, or as unchanged, whatever the change was. review now asks git where it is (git rev-parse --show-prefix) and compares no paths. The same mismatch happens wherever the path to a checkout goes through a link or junction, on any system.

The 4.0.0 entry's "Verified" paragraph was true of the machine it names, from a path git spells the same way, and was not true of the Windows runners. check_ratchet.py gains a case that runs review from a junction (Windows) or a symbolic link (elsewhere) to a repository whose working tree needs more than its last commit, and requires the review to see it: the case fails against 4.0.0 and passes now. 63 checks.

Affected: velaris review, and the review section of the Action's pull-request comment, on a machine where the two paths differ. velaris capabilities init and check were not affected, and neither was anything else in 4.0.0. This repository's velaris.capabilities is recorded again under 4.0.1; only its velaris_version changed.

Verified, on Windows 11 with Python 3.13, with the proof cache cleared first; the new case fails against 4.0.0's velaris.py and passes against this one. With the prover: run_tests.py 92/92, check_library.py 165 correct (one skipped, POSIX only), check_sandbox.py 45, check_fallible.py 26, check_refusals.py 21, check_termination.py 44, check_pool.py 39, check_ratchet.py 63, none wrong; fuzz_native.py 30 agrees, benchmark --quick --check matches, velaris test examples/std_test.vel 7/7, velaris fmt --check clean, velaris capabilities check . passes. Without the prover, in a fresh virtual environment with no z3 or llvmlite: the same thirteen pass, check_library.py 162 correct (two skipped for the prover, one POSIX only) and check_refusals.py 11 with 10 skipped. Whether the Windows runners agree is for this commit's CI to say.

4.0 - The operator sets the limits, and the capability surface cannot widen quietly #

This is a major version. Two gaps 3.4 left open on the doors are closed, which changes what a door started without flags will grant; the project's stability policy is written down for the first time, with the record of the times it was broken; and a repository can now declare the capability surface its programs may have and have CI fail any change that widens it.

The operator sets the limits, not the caller. On the HTTP door and the MCP server a request's timeout and max_memory_mb were whatever the caller sent; the 30 seconds and 512 MB the doors have had since 2.59 were only the values used when a caller sent none. Before 4.0 a caller could exceed them, by asking. Both doors now take --max-timeout and --max-memory-mb, 30 seconds and 512 MB when the flags are absent. A request that names neither gets the ceiling; one that asks for less gets less; one that asks for more is refused the way an over-wide budget is - 403 from the HTTP door, isError from the MCP server - with the ceilings named in the body (max_timeout, max_memory_mb, beside max_allow), and logged with outcome ceiling. A value that is not a number above zero - text, true, zero, a negative, a fraction of a MB - is a bad request. A flag value that is not a limit stops the door at start. GET /health with the token reports all three ceilings. The rule lives in one place, velaris.run_limits, used by both doors.

The HTTP door's default ceiling is io. Without --max-allow, velaris serve granted every effect, ffi included, to anyone holding the token; the MCP server has defaulted to io since 3.4. The door now does too, and starting it wider takes naming the grants: --max-allow io,env,fs,net,clock,rand,ffi is what 3.4 granted by default. Its start-up lines say which ceiling is the default.

One more change came with the flag: velaris serve --max-memory-mb was accepted before, and - through the command line's process-wide --max-memory-mb - set an address-space cap on the door's own process on Linux and macOS, never documented. It is now the most each run may have, and the door's process is not capped.

STABILITY.md. What semantic versioning covers here - the language as SPEC.md states it, the error codes, velaris.audit/1, the library API, the budget grammar, the command line's commands and documented flags - and what it does not: internals, the proof cache, the wording of messages, which promises happen to prove, the formatter's style, anything marked provisional. The rules: breaking changes only in a major version, security fixes included; a deprecation announced in a minor version, warning for at least one more, removed no sooner than the next major; an error code never reused for another meaning, and a removed one kept listed as removed (REMOVED_ERRORS, and a section on the errors page - empty today). A stronger prover refusing a program its proof shows wrong is stated as the one exception, and why.

Its "Breaks we have made" section is longer than expected when it was begun. 2.0 and 3.0 broke in major versions, as promised. 3.4 shipped three breaking changes in a minor version and named them as such, and it should have been 4.0; it was not retagged because 3.4.0 was already published, and this policy exists so that it does not happen again. Reading every entry for STABILITY.md found more: 3.4 broke three further things it did not list (serve and the MCP server refusing an unknown argument, GET /health without the token no longer naming the ceiling); 3.3 shipped five breaking changes as fixes and named none; and eight earlier minor releases, 2.20 to 3.1, each broke something - 64-bit integers, the formatter's style, three builtins made fallible, the http module's call, audit().problems, the doors' 2.59 limits, args(), Windows memory caps. E610 was reused, in 2.59, for a meaning other than the one 1.4 gave it. All of it is listed there, and 2.0 is recorded as its entry and commit describe it: four builtins made fallible. README and CONTRIBUTING link it; SPEC.md section 15 points to it.

Also corrected: the 3.3 entry of this file lost its heading in the 3.4 release, so its text read as part of 3.4. The heading is restored.

The capability ratchet.

Text

velaris capabilities init [path]          # write velaris.capabilities
velaris capabilities check [path]         # exit 1 if the surface widened
velaris review --against <ref> [path]     # a pull request's delta, as facts

A change can add capability to a repository a little at a time - a helper that builds a URL, a function that reads a file, a call three levels down that sends one to the other - and no single diff looks alarming, which is how such a change passes a reviewer and a diff-based monitor. Capability is binary and cumulative, so the steps add up to exactly what one large step would have done; but only a comparison with a declared baseline sees the sum. This release makes that comparison, and makes it the only one the gate uses.

velaris capabilities init reads every .vel file under the path, except in .git and what git ignores, and writes velaris.capabilities (velaris.capabilities/1, velaris-spec 0.3 section 9): the repository's surface - every grant its programs need, in the budget grammar, and for fs and net the most operations one run can perform, or null where the text sets no bound - and for each program its own grants and counts and the effects each of its functions declares, or that it does not compile; with the Velaris version and the date. One grant per line and one function per line, so accepting a widening is a one-line diff. It refuses to replace an existing file without --force.
velaris capabilities check derives the same from the working tree and compares it with the file - never with the previous commit - and exits 1 when anything widened: a grant the surface does not cover (a new effect, a new module, a path outside every recorded one, so ./data widened to ./ fails; a host, so api.example.com made *.example.com fails; a scoped grant made unscoped); more fs or net operations in a run than recorded (10 raised to 1000 fails); a program the file records needing something its own entry does not give, even when another program already had it; and a function the file records gaining an effect, even when its program's grants and counts stay the same. Narrowing never fails and is reported. A new program is held to the surface alone. Each widening names what widened, the file, function, line and call that introduced it, the chain of calls from main that reaches it, and the edit to the file that would accept it. A baseline from another Velaris version is compared with a warning, not a failure. A baseline that is missing, is not /1, or does not read exits 2 and never passes. --json is velaris.capabilities-check/1; --sarif reports each widening as an error at its line, through the 3.4 SARIF code, with two new error rules, capability-widened and capability-effect-gained, and a note, capability-narrowed, on the errors page.
What a program needs is read from its text: the effect and type checks run and the prover does not, so the result is the same with and without z3. A path, URL or module is taken as named when it is a literal or a variable bound once to one; one built while running is recorded as the unscoped grant, which a scoped baseline does not cover. The operation bound comes from loops whose counter and limit the text fixes - for i in 0 to 10, a counter started by let, a list literal - multiplied through nesting and calls; a loop the text does not bound, and recursion, have none.
velaris review --against <ref> runs the derivation and the audit on the files at a git ref - read with git show <ref>:<path>, nothing checked out - and on the working tree, and reports whether the capability surface changed, the proven share before and after, functions that became fallible, hosts, paths and modules newly named, whether velaris.capabilities itself changed, and one word of risk computed from those facts alone: high when the surface widened, or the declared surface widened or was removed; medium when it did not but a program or function the ref had came to need more, or the proven share fell; low when nothing widened and the proven share did not fall. No count of changed lines enters it. It informs a reviewer; the gate is check, since a review against the commit before loses a widening the moment it is merged.
The GitHub Action has a capabilities input, check by default when velaris.capabilities exists and off otherwise - except that a pull request deleting the file fails, since that would turn the ratchet off; capabilities: off in the workflow is the visible way to do that. Its findings are uploaded to code scanning beside the check's when sarif is on. The pull-request comment from 2.63 now holds the ratchet's result, each widening with the edit to the baseline that would accept it, and the review delta against the pull request's base.
This repository commits its own velaris.capabilities, written by velaris capabilities init .: 172 programs, 22 of them examples and benchmark rows built to be refused, recorded as not compiling. CI runs velaris capabilities check . on every leg.
velaris.audit/1 gains ffi_any, added within version 1: true when some Python call names its module with a value built while running, which ffi_modules cannot list. The ratchet needs it - a computed module name must not slip past a baseline naming ffi:math
- and it closes velaris-spec's open question Q4. The audit also warns when it is true.

check_ratchet.py, 62 checks, proves the rules rather than asserting them, through the command line in scratch trees and real git histories. The gradual case: six commits, the first five adding pure helpers, a text constant holding a URL and a call to print, each passing against the baseline, and the sixth sending a summary to that URL through a helper three calls below main - which fails, naming net:collector.example.net as a new effect, lib/deliver.vel line 2 in send, and the chain main -> summary -> deliver -> send, while a review of each commit against the one before calls the first five low. Why the gate must be the baseline: a count widened and merged anyway keeps failing the check at every later commit, while a review against the previous commit reports nothing one commit later; and seven steps from 10 to 1000 are reported as 1000 against the declared 10, where the previous commit shows 640 to 1000. Widenings through an import (the surface unchanged, the program's entry not), through the standard library, through a path prefix, a count, a wildcard host, a URL, path and module built while running, a new module, a new direction, a hidden directory, and a program whose main is imported from outside the tree. An effect added to a function whose program's grants and counts stay exactly as they were, reported. And the changes that must pass: narrowing; reordering functions, imports, uses clauses and statements, renaming locals, reformatting and velaris fmt; a file with no effects; a new program inside the surface; a literal moved into a variable; a function renamed or moved to another file; a program that stops compiling. Declared prefixes, wildcards and ports; a baseline from an older and from a newer version (a warning that never hides a widening); init without --force; four baselines that cannot be read (exit 2); the JSON and the SARIF, which validates; 23 covering cases and 6 operation-bound cases. CI runs it on every leg.

What the ratchet cannot do, and the cases where one of the two rules was not achieved. A widening never passes and a non-widening change never fails, among the changes check_ratchet.py holds; beyond them, these are the known limits, each stated in THREAT_MODEL.md:

A widening that passes: a function renamed in the same change that gives it an effect is a new function, held to its program's entry and the surface but not to what its old name declared - so a pure helper renamed while it gains an effect its program already had is not reported as a function that gained one. What a granted ffi module does is outside the text. A symbolic link under a recorded directory is that directory's content.
A change that does not widen, reported as one: the bound on operations comes from fixed rules, so a loop bound moved behind a function call (for i in 0 to limit()) loses its bound and is reported as unbounded; a path or URL passed to a helper as a parameter is taken as unscoped, as it always is, even when every caller passes a literal; and a path written with \ is covered only by the same text.

What a 3.4 user has to change.

A client of velaris serve that relied on the door granting more than io without --max-allow must start the door with --max-allow naming what it needs.
A client of either door that sends a timeout over 30 seconds or a max_memory_mb over 512 must have the operator raise --max-timeout or --max-memory-mb, or ask for less.
A client that sends timeout or max_memory_mb as text ("30"), or 0 to mean the default, must send a number, or leave the field out.
An operator who passed --max-memory-mb to velaris serve to cap the door's own process gets a per-run ceiling instead; cap the door with the operating system (ulimit -v, a container limit) if that was the intent.

Additions, which break nothing: velaris capabilities, velaris review, the Action's capabilities input (off unless the file exists), ffi_any, and the new SARIF rules.

velaris-spec 0.3. Section 9 stops being provisional: velaris.capabilities/1 replaces the provisional /0, which no version of this compiler wrote. The spec states the document, the derivation from a program's text, the operation bound, the covering rule (a path holding \ now compared whole), and the comparison as five rules, W1 to W5, with a table of what widens for each kind of scope - effect, path, host, module, count, function - and the rule that a check compares with the baseline and with nothing else. Q4 is resolved by ffi_any. Its conformance section adds check_ratchet.py. It still quotes this repository's SPEC.md sections 6, 7 and 7.1 word for word - none of them changed - so its drift check passes; its CI now also validates this repository's velaris.capabilities against the /1 schema.

Sources, named (CONTRIBUTING.md rule): the four parts of this release were specified by the maintainer. No published work is on record as the source of the ratchet's design, so none is named. The CHANGELOG scan behind STABILITY.md's record was made in this release, and its findings were checked against the entries and against git history (E610's two meanings are in commits 616579f, 79808fc and b5a4582).

The MCP manifest changes, by design. velaris_run's description and the descriptions of its timeout and max_memory_mb inputs now name the ceilings, so the signed velaris-mcp-tools-4.0.0.json differs from 3.4.0's: velaris mcp-verify against a 3.4.0 manifest reports velaris_run as CHANGED, which is what it is for.

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 165 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, check_ratchet.py 62, none wrong; fuzz_native.py 30 agrees, benchmark/run.py --quick --check matches results.json, velaris test examples/std_test.vel 7/7, velaris fmt --check clean, and velaris capabilities check . passes on the clean tree. Without the prover, in a fresh virtual environment holding this tree, jsonschema and no z3 or llvmlite: the same thirteen pass, with check_library.py 162 correct (two skipped for needing the prover, one POSIX only) and check_refusals.py 11 with 10 skipped for needing the prover. Every workflow file and action.yml parse as YAML. The Action's new steps were run outside GitHub as far as they go: the ratchet step under Git Bash in four cases (no baseline, off; a baseline and nothing widened, pass; clock added, fail naming it; a pull request deleting the baseline, fail), and the comment's Python against real capabilities check --json and review --json output. velaris review --against HEAD over this repository took 45 s with the prover. velaris-spec 0.3's tools/check_sync.py passes against this tree, its tools/validate.py passes with --capabilities on this repository's velaris.capabilities, and the velaris.audit/1 documents 4.0.0 produces for all 109 files in examples/ and stdlib/ validate against its audit schema, ffi_any included.