v9.0.0-alpha.4

9.0.0-alpha.3 published its crate and made no GitHub release. The two
hard things worked: release.yml dispatched publish-crate.yml, waited
for the run with gh run watch --exit-status, and sabline-rt
9.0.0-alpha.3 went to crates.io through OIDC with no stored credential.
Then the release job fell over on one line:

Post https://uploads.github.com/.../assets: read assets/rt: is a
directory

The crate job gave upload-artifact two paths, so the artifact kept
the directories they had in common - rt/target/package/... - and the
release step globbed assets/*, handing gh a directory. gh refuses
one, and then deletes the release it had just created, so there is no
GitHub release under v9.0.0-alpha.3 although the tag and the crate
stand.

Two fixes, and the second is the one that matters:

• the step names files rather than globbing a tree (find assets -type f), so a directory can never reach gh whatever the artifact's shape,
  and it attaches what an existing release lacks rather than doing
  nothing - the same shape the ordinary release's job has always had;
• the artifact is one flat directory, so assets/ holds the two files
  and nothing else.

The part worth keeping

Three releases were spent on three defects, and all three were in
workflow code I had verified by reading it. A skip that travels past a
job which rescued itself; a registry that refuses a token minted under
workflow_run; a glob that hands a directory to a command that refuses
one. Every one of them takes seconds to see in a run and is invisible on
the page.

This project already knew that. check_release.py has run the
Marketplace job's and the pin-moving job's own steps, in bash, against
stand-ins since 8.2.1 and 8.4 - because both had failed in ways reading
did not catch. The jobs added for 9.0 did not get the same treatment.

They do now. run_prerelease_github_job lays the assets out from the
crate job's own upload-artifact path, so the fixture tests the
artifact this repository actually produces rather than one chosen to
pass, and runs the release job's real steps against a gh that refuses a
directory exactly as the real one does. Run against the job as
9.0.0-alpha.3 shipped it, the fixture fails with gh refused a directory; against the fix it passes. Writing it found two more things a
reading had not: the notes step needs the checkout's CHANGELOG, and the
"nothing else moved" step needs the registry to say the crate is there.

check_release.py: 175 passed, 0 broken.

compatibility: a pre-release publishes the sabline-rt crate and a GitHub
release marked pre-release and nothing else, so nothing a user of 8.6.0
has is touched - not PyPI, not npm, not the VS Code Marketplace, not the
MCP registry, not the Action pins, and not any "latest" anywhere.

v9.0.0-alpha.1, v9.0.0-alpha.2 and v9.0.0-alpha.3 stay where they
are, neither moved nor deleted nor retagged. alpha.1's crate is on
crates.io because a person put it there, which is how a crate's first
version always gets there; alpha.3's is there because the workflow put it
there, which is how every one after it will. None of the three has a
GitHub release, and the entries below say why each.

---

Made by release.yml after every leg of the tests passed on 5c4af91. Nobody tagged it by hand (RELEASING.md).

v9.0.0-alpha.4 is an annotated tag and is not signed: the workflow holds no signing key, and a keyless signature made in Actions (gitsign) is one GitHub does not show as verified. Every file below is signed with sigstore as release.yml@refs/heads/main, and its certificate names this commit; SECURITY.md says how to check one.

Full Changelog: v9.0.0-alpha.3...v9.0.0-alpha.4

v8.6.0

The project is renamed. Velaris is Sabline from this release. Nothing
else changed: not the language, not the budget grammar, not an error code,
not a guarantee, not a line of the threat model. 8.6.0 renames, and does
nothing else.

Why. The name Velaris belongs to an unrelated company in the same
market - velaris.io, which sells an agent product with an MCP server. Two
things with one name in one market is a problem for whoever meets the
second one, and they were there first. The name was given up rather than
contested. There is no dispute, and nothing was asked of anyone.

What a user of 8.5 has to change: nothing, until 9.0. A rename that
stopped a command, an import, an environment variable or a committed file
from working would be a break, and a break ships only in a major version
(STABILITY.md rule 1). So every name that worked in 8.5 works in 8.6, each
saying once on stderr that it has changed, and each is removed no sooner
than 9.0 (rule 2). The nine are listed under Deprecations in force in
STABILITY.md, and docs/renamed.md is the whole table:
velaris the command, import velaris, velaris.VelarisError,
velaris_mcp, velaris_mcp_install, velaris_magic, VELARIS_*,
velaris.capabilities / velaris.toml / velaris.lock, and every
velaris.* document schema. Each is an alias and not a copy - velaris
is the sabline module object, VelarisError is SablineError - so
there is no second implementation that can drift.

compatibility: the velaris command is kept as a second entry point on the same main(), on PyPI and on npm, so every command line, script, CI step and Dockerfile that runs velaris runs, with one line on stderr saying the name has changed. No flag, command name or exit code changed; the command line STABILITY.md covers is sabline's, and it is velaris's.
compatibility: import velaris gives back the sabline module itself, so the six library names STABILITY.md covers - velaris.check, velaris.audit, velaris.run, velaris.Pool, velaris.card, velaris.attest - are the same functions, returning the same CheckResult, AuditResult, RunResult and Problem objects. velaris.VelarisError is SablineError, the same class rather than a subclass, so except and isinstance answer as they did. A DeprecationWarning is raised as well as the line on stderr, so -W error finds it.
compatibility: Sabline writes sabline.audit/1, sabline.receipt/1, sabline.capabilities/1 and every other sabline.* schema where 8.5 wrote velaris.*, and reads both spellings of each as the same format at the same version. One document is the exception, and is still written under the old name: sabline-spec's conformance corpus, tests/index.json, whose format is velaris.conformance-corpus/1. The corpus is published for an implementation in any language to run, and every implementation that exists is a released version of this one - each reads that field strictly and none can be changed - so a corpus under the new name would stop velaris conformance for everyone who has not upgraded. The three schema files beside it keep their names for the same reason: v8.5.0 opens schemas/velaris.audit.1.schema.json and velaris.capabilities.1.schema.json by name, so renaming them was the same break by another route. 8.6 reads the corpus format under either name and looks for the sabline.* schema filename before falling back, so it is ready for the move before the move happens; the name moves no sooner than sabline-spec 0.15.0. check_differential.py found both halves of this, by failing to run the corpus under v8.5.0. That is an addition to what a reader accepts, which the velaris.audit/1 clause allows within version 1; nothing a consumer could rely on disappeared. A tool outside Sabline that matched the schema string exactly must accept both - the Kyverno policy in policies/ shows how, with AnyIn.
compatibility: a committed velaris.capabilities still holds the capability ratchet, read when there is no sabline.capabilities beside it, so a repository that upgrades needs no commit to keep its baseline working; the same rule covers velaris.toml and velaris.lock. Sabline writes only the sabline.* name.
compatibility: a VELARIS_* environment variable is read where the SABLINE_* name of that variable is unset. Both set to different text is refused rather than guessed, because a guess at SABLINE_TOKEN decides who may reach a door; both set to the same text is one name written twice, and is fine. A message about such a variable names the spelling the operator wrote: VELARIS_PROOF_TIMEOUT=x is complained about as VELARIS_PROOF_TIMEOUT, not as the new name, which would send somebody to look at a variable they never set.
compatibility: sabline attest writes the predicate type https://sabline.dev/capability/v1, and a receipt names https://sabline.dev/receipt/v1, where 8.3 to 8.5 named both at velaris-lang.dev and 4.2 to 8.2.1 at the project's GitHub Pages address. All three spellings are read as the same type by sabline verify, sabline receipts diff, sabline replay and the OPA policy, so every attestation and receipt ever signed still verifies; nothing is removed from that list, a name only ever joins it. A verifier outside Sabline that pins one type name - cosign's --type, the Kyverno policy - takes the name the Statement carries.
compatibility: the documentation site is sabline.dev, and velaris-lang.dev redirects to it path for path, so the reference: line every error and refusal printed by 8.3 through 8.5 still leads to the card. Error codes, messages and the errors page's anchors are unchanged. One address could NOT be kept: a GitHub Pages site is served at .github.io/, so renaming the repository moved it, and https://gowrishankar-infra.github.io/velaris-lang/... - the reference: line of 8.0 through 8.2.1 - answers 404. Serving it again would need a repository called velaris-lang, and creating one would end GitHub's redirect from every old repository URL, uses: gowrishankar-infra/velaris-lang@<commit> among them; those are worth more than one address. It does not touch the predicate type named there, which is a name and not a page: every Statement signed by 4.2 to 8.2.1 still verifies. docs/renamed.md says all of this.
compatibility: no error code was added, removed or changed in meaning; no flag was removed; no default changed. The release gate reads the compiler's source at v8.5.0 under the name it had then (release_checks.py, RENAMED_IN_8_6), so the package moving from velaris/ to sabline/ is not read as every code, flag and default being added at once - which is what it looked like before that was taught to it.
compatibility: the VS Code extension is republished under a new id, gowrishankar-infra.sabline, because a Marketplace id cannot be renamed. The old id gets a final version whose README says where it went. This one is a real break for anyone who had the extension installed: they must install the new one. It could not be avoided, and it is the only thing in this release that a user must do something about.
compatibility: GET /health on the HTTP door names the version under both sabline and velaris. The endpoint is documented (EMBEDDING.md) and is not provisional, and what reads it is a monitoring script doing jq .velaris, which would have begun reading null rather than failing. velaris goes in 9.0. sabline deps-diff finds a dependency's lockfile under either sabline.lock or velaris.lock, since a dependency locked by an earlier release has the old name.
compatibility: two fields of documents STABILITY.md marks PROVISIONAL are renamed rather than added to, which is what provisional is for, and each is named here as that clause requires: sabline.deps-diff/1's velaris_files is sabline_files, and the ready line of sabline.tools-door/1 names the version under sabline where 8.5 wrote velaris. Both are one release old, both are read by a host written against 8.5, and both are declared rather than doubled, because a provisional format that is never allowed to change is not provisional.
api: velaris_version is added beside sabline_version in every sabline.audit/1 and sabline.capabilities/1 document, in what the MCP server's audit returns, and as a property of AuditResult; velaris is added beside sabline in what GET /health, GET /health without a token and GET / answer - the same value under both names, because a required field of a version-1 document may not disappear and STABILITY.md covers the fields of what a call returns; velaris.VelarisError is added to the library's names, as an alias of SablineError; CAPABILITY_PREDICATE_TYPE and RECEIPT_PREDICATE_TYPE name sabline.dev, and each of CAPABILITY_PREDICATE_TYPES and RECEIPT_PREDICATE_TYPES gains a third spelling. No name was removed, no signature changed, and no return type changed.
differential: examples/avg_bad.vel, examples/builtin_unhandled.vel, examples/callsite_bad.vel, examples/caught.vel, examples/conj_bad.vel, examples/contract_broken.vel, examples/contract_impure.vel, examples/discount_bad.vel, examples/div_bad.vel, examples/fail_proof_bad.vel, examples/failing_bad.vel, examples/ffi.vel, examples/floats_bad.vel, examples/fp_proof_bad.vel, examples/funcs_bad.vel, examples/generics_bad.vel, examples/grid_bad.vel, examples/import_bad.vel, examples/lambda_contract_bad.vel, examples/list_mixed.vel, examples/list_oob.vel, examples/list_proof_bad.vel, examples/loop_bad.vel, examples/loop_proof_bad.vel, examples/many_errors.vel, examples/map_bad.vel, examples/maps_bad.vel, examples/ns_bad.vel, examples/offbyone_bad.vel, examples/proof_catch.vel, examples/qlist_bad.vel, examples/rec_proof_bad.vel, examples/records_bad.vel, examples/secret_bad.vel, examples/sneaky.vel, examples/std_bad.vel, ...

v8.5.0

A minor version, additive throughout: what it is like to use. One command
that shows a refusal and a run inside a budget with nothing to read first;
four libraries, written in Velaris, so that an operations script against
Azure, Kubernetes, GitHub or AWS calls no Python; a receipt and an audit as
a page a person can read; and the first cut of the runner, in which a host
process offers a program tools and the budget holds their arguments.

No program that compiles and runs under 8.4.0 inside its budget is refused
by 8.5.0. Every new builtin gives way to a function of the program's own
name (SPEC.md 10.1); uses tool did not compile and a tool grant did not
parse until now; with no --tools there is no tool to reach.
check_differential.py holds the examples, velaris-spec's corpus and the
quick benchmark to 8.4.0's outputs.

compatibility: sha256, hex_encode, hex_decode, base64_encode, base64_decode and url_encode are new pure builtins, and each gives way to a function of that name in the program (they are in NEW_BUILTINS, SPEC.md 10.1), so a program that defined its own sha256 under 8.4 still calls its own; a program that called an undefined one did not compile (E200).
compatibility: hmac_sha256 and hmac_sha256_chain are new builtins that give way to the program's own function in the same way; they need the declassify effect, which no program can come to need without calling them, and the E560, E561 and E609 they can give are given only to a program that calls them, which under 8.4 was E200.
compatibility: tool is a ninth effect. uses tool was E300 under 8.4 and --allow tool a budget error, so no program or command line that worked changes meaning; --allow all now grants nine effects and says so in the line it has always written to standard error, and a program run under it that does not call tool runs as before; velaris.ALL_EFFECTS is one longer.
compatibility: tool and tool_secret are new builtins that give way to the program's own function; E320, E321, E322, E323 and E324 are given only to a call of one of them, which no program that compiled under 8.4 makes, and the last four only under velaris run --tools.
compatibility: velaris demo, velaris receipt show (and velaris receipts show, the same page), velaris skill verify, velaris audit --html [-o FILE] and velaris run --tools MANIFEST [--tool-timeout S] are new; a file named demo, receipt or skill in the working directory is now run with velaris run demo, as a file named audit or check always had to be.
compatibility: velaris.receipt/1 gains grants_used in every receipt, tool_calls and tool_ceiling in the receipt of a run given --tools, and key_fingerprint on the declassification an hmac call records - all within version 1, where fields may be added (velaris-spec 8.7, 0.13.0); velaris replay and receipts diff compare what they compared, and a receipt written by 8.4 is read, shown and verified as before.
compatibility: velaris.audit/1 gains tools within version 1, and secrets.declassifications gains an entry, with a builtin key, for each hmac call; effects may hold tool.
compatibility: the audit and the capability ratchet now name the host of a URL that only begins fixed - "https://api.example.com/" + path, or format("https://api.example.com/{}", id) - when the fixed part holds the / that ends the host, where 8.4 said "a host built while running". net_hosts, safe_command and a derived baseline are narrower for such a program, never wider: the ratchet passes a narrowing against an 8.4 baseline, and the run-time check of net: grants is unchanged. velaris-spec 9.3 states the rule (0.13.0).
compatibility: inside a library imported with a name, a call to a builtin older than 4.3 reaches the builtin, as it does in a flat import and as SPEC.md 10 says a named import behaves; until now a library's own get took a get(list, i) written inside it, a for loop's included. Only the shipped library may define such a name (E204) - http.vel has a get - and no shipped library made such a call, so no program's meaning changes.
compatibility: stdlib/http.vel is byte for byte what it was in 8.4.0. What the batteries needed beside it - retries within a bound, JSON bodies, headers from a map - is in a new file, stdlib/rest.vel, because a function added to http.vel would stop a program that imports http.vel without a name and has a function of that name itself (E513), and items and succeeded are names a program has; azure.vel, github.vel, k8s.vel, aws.vel and rest.vel are new files that no 8.4 program imports.
compatibility: host_refusal takes an optional count and the run state gains TOOL_GRANTS, TOOL_LIMITS, TOOL_COUNTS, GRANT_USES and TOOL_SESSION, none of which STABILITY.md covers and each of which has the value a run without tools had before.
api: AuditResult gains the tools slot; velaris.ALL_EFFECTS gains tool; the run state gains TOOL_GRANTS, TOOL_LIMITS, TOOL_COUNTS, GRANT_USES and TOOL_SESSION; host_refusal(url) becomes host_refusal(url, count=False); the command line gains demo, receipt, skill, audit --html and run --tools/--tool-timeout; receipts from every door gain grants_used, and audits tools.

velaris demo

One command, no arguments, no network, about a second. It makes a directory,
writes into it a .env whose one value is made up, a script of the kind an
agent writes - read ./.env, post it to a webhook - and the same task
rewritten to stay inside a budget. It runs the first with no budget given
and shows the refusal, the exact line, the reason and the receipt; runs the
second under io,fs:read:settings.txt,fs:write:out and shows it succeed,
with its receipt; and prints what differs between the two receipts. --keep
leaves the files. The documentation's first page now opens with it.
check_demo.py runs it on every leg: under a minute, under a screen, exit
0, nothing left behind.

Batteries, written in Velaris

• stdlib/azure.vel: Azure Resource Manager over REST - read,
  put_resource, patch_resource, delete_resource, list with
  nextLink paging (a link that leaves the host is not followed), a 429 or
  a 5xx asked again within a bound, and ARM's {"error": {"code", "message"}} as the failure's words. The bearer token is the caller's
  Secret of Text; nothing in the library signs in. Every request is
  written "https://management.azure.com:443/" + path, so the audit of a
  program that uses it names exactly management.azure.com:443.
• stdlib/k8s.vel: the API server over REST with a Secret token;
  in_cluster() reads the service-account file with read_file_secret;
  list (with metadata.continue), read, watch_once, and pods,
  pod, services, deployments, deployment, configmaps, events,
  nodes, namespaces. It reads; what changes the cluster is
  write_create, write_patch, write_delete and write_scale, and the
  suite fails if a function that sends a changing method is named otherwise.
  It has no function for reading a Secret resource, on purpose.
• stdlib/github.vel: repos, issues, pulls, check runs, releases and
  contents; Link-header paging held to api.github.com; the rate limit
  in every reply (remaining, reset) and, when it is reached, a failure
  that says when it resets and is not asked again.
• stdlib/aws.vel: Signature Version 4 in Velaris, to S3 (list
  buckets, list objects with continuation, get, put, delete) and STS
  (GetCallerIdentity), with a session token when there is one. The date
  is whole-number arithmetic on now(). It reproduces the signature AWS
  publishes for its own test request, and the stand-in checks each
  signature the way AWS does, from the request as it arrived.
• hmac_sha256(key: Secret of Text, message: Text) -> Text and
  hmac_sha256_chain(key, messages). The result is not a Secret, so the
  call needs the declassify effect and grant, the audit lists it under
  secrets with the reason hmac signature, and the receipt records it
  with the key's fingerprint. The chain exists because SigV4's derived keys
  are credentials themselves: with it they are never values of the program.
  THREAT_MODEL.md has a new section saying why a MAC does not give the key
  away, what somebody holding one can do (replay it while it is valid), and
  the limit: a program with the declassify grant can MAC under a weak key
  it derived from a strong one - which is no more than declassify already
  let it do, and should be read in an audit as what it is.
• sha256, hex_encode, hex_decode, base64_encode, base64_decode,
  url_encode: pure, over UTF-8; the decoders fail on what is not the
  encoding or not text.
• Bearer tokens leave through declassify, once, where the header is
  built, with a reason that names the host. 8.5 adds no builtin that sends a
  Secret: one that did would make net a second declassify that no audit
  names.
• stdlib/rest.vel is what the four needed that http.vel lacked:
  call_retrying (a bound of ten, no pause - a program has no clock unless
  granted one), call_json, header_map, header_of, items,
  succeeded, worth_retrying, after_prefix, no_leading_slash. It is
  a new file and http.vel is untouched: the first draft added these to
  http.vel, and a program that imports http.vel without a name and
  defines its own items then stopped compiling (E513). A minor version
  does not do that, so they moved.
• The audit names the host of a URL that begins fixed (above), which is
  what lets a library written against one host audit as that host.
  azure.vel and github.vel import nothing, because an audit reads every
  function a program loads and http.vel's take any URL.
• Each has an example under examples/ops/ - azure_groups.vel
  (resour...

v8.4.0

A minor version, and the last before 9.0. Until now the budget was enforced
by the interpreter alone, in the process that runs the program, and
THREAT_MODEL.md said so under "No OS confinement". From 8.4 the process that
runs a program also asks the operating system to hold the same budget, before
the program's first statement runs, so that a fault in Velaris itself - in the
interpreter, a builtin, the budget's own checks - is a crash inside a box and
not an escape. On Linux that is Landlock and seccomp-bpf, and a run under the
default budget is fully held. On macOS and on Windows it is partial, and
every run says which it got and why. Beside it: the release workflow now
moves its own Action pins, so main does not go red after a release.

Nothing that compiles and runs under 8.3.1 inside its budget is refused: what
the system is asked to refuse is what the budget already refused, and
--no-confine restores 8.3.1 exactly.

compatibility: confinement is on by default for a run in a process of its own - the command line, run(timeout=...), Pool, both doors, velaris eval and velaris replay - and asks the operating system to refuse only what the run's budget already refuses, so a program that stays inside its budget runs as it did under 8.3.1, with the same output and exit status; a granted ffi module widens what is asked to what that module needs, and a module the table does not name, ffi:os, ffi:subprocess and plain ffi widen it to nothing enforced rather than risk refusing what worked. --no-confine on the command line, on velaris serve and on the MCP server, and confine=False in the library, do not ask, and say so on stderr. Against v8.3.1 no example's output and no conformance verdict changes.
compatibility: E319 is given only under the fault-injection hook (VELARIS_FAULT_INJECT, new in 8.4), when the operating system refuses an effect the runtime itself attempted; no program and no run of 8.3.1 or earlier can meet it.
compatibility: --confine was never a documented flag: 8.3's velaris eval passed it to the pool worker it started, with the directories the worker might write. From 8.4 every pool worker derives its OS policy from its own budget, and the worker's flags are --confine-at, --confine-temp and --no-confine; nothing a person or a script typed is removed.
compatibility: velaris doctor prints one more line, the confinement level a run under --allow io gets on this machine, and a why: line under it when the level is not full; its exit status and every other line are as they were.
compatibility: velaris.audit/1 gains confinement within version 1 - the level and reason on Linux, macOS and Windows for a run under safe_command, and the granted modules that widen the OS policy - derived from the budget alone, so an audit is still the same bytes on every system; the command line's audit prints a CONFINEMENT ON THIS MACHINE section after the lines it printed before.
compatibility: a receipt's run_parameters.confinement, which 8.3 wrote as "none" for every run but velaris eval's and as the name of a mechanism (landlock-net, landlock, job-one-process, sandbox-exec) there, is now the level - full, partial or none - with confinement_reason, confinement_layers (where the mechanism names now are) and os_policy_sha256 added beside it, all within velaris.receipt/1; a receipt written before 8.4 still verifies, and velaris replay and velaris receipts diff compare the level only between receipts that have the new fields.
compatibility: velaris eval refuses to run (exit 2, before the program is sent to the worker) where the operating system holds none of the budget; 8.3 ran such a program under the budget alone and wrote "confinement": "none". On Linux 5.13 and later, on macOS while it honours sandbox profiles, and on Windows, the level is full or partial and eval runs as before. velaris eval is documented as provisional.
api: run(), Pool() and PoolRegistry() take confine=True; AuditResult gains the confinement slot; the run state gains CONFINE, CONFINEMENT, WORKER_CONFINEMENT, BEFORE_FIRST_STATEMENT and PROGRAM_FILES; velaris serve and the MCP server take --no-confine; the audit and the receipt the HTTP door and the MCP server return carry the new fields. Nothing is removed and no default argument changes.

The release workflow moves its own pins

README.md and EMBEDDING.md pin the Action by commit, and run_tests.py fails
unless that commit is the one the newest tag names. A release commit cannot
name its own hash, so from the moment a release was tagged main's first test
step failed until somebody pushed the pin move - twenty of twenty-one jobs,
after 8.3.1.

• release.yml's move_pins job runs once the tag exists, whatever the
  publishes after it did. It checks out main, runs release_checks.py move-pins vX.Y.Z --commit <sha> - the pins in both documents, the
  version: example beside them, the pre-commit rev: - rebuilds the pages,
  fails if anything outside README.md, EMBEDDING.md and docs/ changed, commits
  Move the Action pins to vX.Y.Z, asks the gate about that commit and pushes
  only when the gate says it is not a release, and does it again on top of
  main if main moved. A push made with GITHUB_TOKEN starts no workflow, so it
  then starts tests on main by name; test.yml takes workflow_dispatch
  for that, and the release run that follows those tests stops at its gate,
  which takes only a push's tests.
• check_release.py runs the job's own steps in bash on a throwaway copy
  of this repository with a simulated tag, and holds the result to be that
  commit and nothing else: one commit past the tagged one, five lines in the
  two documents, pages under docs/, no tag made or moved, the tests started
  once; nothing pushed when it is run again; the pins moved on top of a commit
  that landed meanwhile; and a red job, with main where it was, when the tag
  does not name the released commit.

The operating system holds the budget

velaris/confine.py's os_policy(budget) is the one derivation: budget in, OS
policy out, reading nothing of the machine. THREAT_MODEL.md's new section,
What the operating system enforces, prints the module's table - every
budget item, and what each system enforces for it - and check_confine.py
fails when the document and the module differ by a word.

• Linux: Landlock and seccomp-bpf. Landlock holds reads to the fs:read
  grants and what the interpreter itself reads - Python's installation and
  import path, the package and the standard library, shared libraries, the
  devices and /proc entries Python asks for, time zone data, the program's
  own files, and the resolver's files and the TLS roots under a net grant
  only - and writes to the fs:write grants and a private temporary
  directory. seccomp-bpf answers EPERM to every socket call when no net is
  granted; to execve, execveat, fork, vfork and a clone without CLONE_THREAD,
  and ENOSYS to clone3; and always to ptrace, mount and its newer calls,
  pivot_root, chroot, unshare, setns, kernel modules, kexec, bpf,
  perf_event_open, process_vm_readv and writev, keyrings, io_uring,
  userfaultfd, open_by_handle_at, setting the clock, and a signal to any
  process but this one. The filter is installed on every thread; Landlock,
  which holds one thread, is applied to the main thread as well on Python
  3.10, where a run is on a thread of its own, and a thread it could not
  reach makes the level partial and is named.
• macOS: a sandbox profile, derived from the same policy and applied with
  sandbox_init, the call sandbox-exec makes: writes, the network and
  fork/exec held, reads refused under the home directory and /Volumes. Apple
  has deprecated both, and THREAT_MODEL.md says so.
• Windows: a job object holding one process, the clipboard and the
  desktop; every privilege removed from the token but
  SeChangeNotifyPrivilege; and the low integrity level for a budget that
  grants no write, under which the kernel refuses a write to anything of the
  user's. Reads and the network are not held: that needs an AppContainer,
  which a running process cannot enter and which a python.exe from
  python.org, the Store or a virtual environment cannot start in, since it
  could not read its own installation there.
• A granted ffi module widens the policy to what that module needs,
  named per module in FFI_WIDENS and in THREAT_MODEL.md: nothing, any path,
  any host, or - for ffi:os, ffi:subprocess, plain ffi and any module
  the table does not name - nothing enforced. The audit's
  confinement.widened_by says which.
• The level a run reports - full, partial or none - is what was applied
  and held, with the reason: in the receipt, in the audit, in velaris doctor. velaris receipts diff names a run whose level no earlier run of
  the same program had, and says when it is weaker. velaris eval requires
  full or partial.
• When it is applied. A single run - the command line, run(timeout=...),
  velaris replay - reads, proves and compiles its program first, from
  wherever its imports are, and is confined at the program's first statement.
  A pool worker is confined when it starts, before it is sent anything; it
  holds reads only when the pool has an import_root, as both doors' pools
  do, and says partial otherwise. A receipt and --record-responses are
  opened before the run and written after it, since a confined process cannot
  open them then.

The honesty test

check_confine.py, on every leg. A fault-injection hook
(VELARIS_FAULT_INJECT) makes the runtime itself, from Python and not from
Velaris, read a file, write one, connect, start a process and - except on
Windows, which has no signal to send - send a signal outside the budget.
Under confinement, what that system's row says is held is
refused by the ke...

v8.3.1

A patch release that adds no code. 8.3 moved the documentation to
velaris-lang.dev; this builds it into a site rather than a handful of pages.
build_docs.py writes every document - README, SPEC, TUTORIAL, EMBEDDING,
STABILITY, SECURITY, THREAT_MODEL, the CHANGELOG, the error pages, the two
predicate types, docs/eval.md, docs/crosswalk.md,
docs/structurally-impossible.md and llms.txt - through one generator,
with one stylesheet and one script, into three trees: the top of the site,
latest/, and 8.3/. A version directory the build does not write is left
alone, so an address published under an earlier one keeps working. Every
copy's canonical link names the page at the top.

Nothing in the package changed but its version: no error code, flag, default,
output or verdict moves, and a program that compiled under 8.3.0 compiles the
same way.

• The renderer is docs_markdown.py, beside the generator: headings with
  anchors, tables, callouts (> [!NOTE], > [!REFUSES], > [!KNOWN-OPEN],
  and the **Note.** lead-ins the documents already used), and Velaris code
  highlighted from velaris.lexer's own MASTER_RE and KEYWORDS, so the
  site cannot colour a keyword the compiler does not have.
• A search index of every heading of every page, fetched only when the
  search box is given focus. A theme toggle follows the system until a reader
  chooses, and the choice survives a reload.
• check_site.py builds the whole site into a scratch directory and
  holds it there: version directories kept and latest/ rebuilt, no raw
  Markdown in page text, a strict HTML parse, every relative link and anchor
  resolving, one stylesheet and one script per page under a
  Content-Security-Policy, no request to another host, pages within their
  byte budget, the search index complete, llms.txt byte for byte in every
  tree, and the contrast ratios recomputed from the stylesheet's own tokens.
  With Chrome it also drives the pages: every one fits 360px, no console
  error, the copy buttons, the menu, the search (E700 reaches
  errors.html#E700), and the theme toggle. --no-chrome prints those as
  skipped, which is how test.yml runs it; site.yml runs it with
  --require-chrome and then Lighthouse, asserting 95 in performance,
  accessibility and best practices, and a transfer budget per page.
• TUTORIAL.md's code blocks now run under check_docs.py, as every
  other document's already did.
• check_docs.py also admits the generated pages that hold the changelog's
  own history, and the search index built from them, as the only files
  besides those it already lists that may name the site's earlier address.

Known open

• The playground is over the page budget (about 1 MB: it carries the
  compiler) and loads Pyodide from a CDN, so it keeps its own layout, lives
  only at the top of the site, and check_site.py lists it as an exception
  rather than holding it to the rules.
• The build does not remove a stale generated file at the top of the
  site: it rebuilds latest/ and its own version directory, and a page
  renamed in a later release would leave its old file behind until it is
  deleted by hand.

---

Made by release.yml after every leg of the tests passed on d457f50. Nobody tagged it by hand (RELEASING.md).

v8.3.1 is an annotated tag and is not signed: the workflow holds no signing key, and a keyless signature made in Actions (gitsign) is one GitHub does not show as verified. Every file below is signed with sigstore as release.yml@refs/heads/main, and its certificate names this commit; SECURITY.md says how to check one.

Full Changelog: v8.3.0...v8.3.1

v8.3.0

A minor version. A receipt has said, since 8.1, what one run did; 8.3 adds
what can be done with one - a profile for running code in an evaluation
harness that always leaves a receipt, a comparison of a receipt with its
program's audit and with earlier runs, a replay of a run from its receipt, and
a verifier for attestations and receipts. Beside them: promises exercised on
the inputs the prover finds, a page of what cannot occur in a Velaris program
with a test for each, RFC 4180 quoting in csv.vel, log lines a value cannot
forge, two benchmark categories, a workflow-permissions ratchet for the
Action, and a crosswalk onto four agent-security frameworks. The project's
documentation moved to velaris-lang.dev, and every name of it moved with it.
A test written for a surviving mutant found a fault in the prover, which
reported proven a promise past a comparison of two maps or lists; it is
fixed, and has an advisory.

compatibility: E615 is given only under velaris eval, new in 8.3, to a run that was asked to stop from outside; no run of 8.2.1 or earlier can meet it.
compatibility: E616 is given only under velaris replay --responses, new in 8.3, to a call a recording of tool responses does not hold in that place; no earlier run can meet it.
compatibility: check, proofs, explain, audit, attest and the library no longer report a promise proven when its proof passes through == or != on two maps, two lists other than List of Int, a map and put of it, or two records holding a Float field: until 8.3 each such comparison was a constant to the prover, and a promise past it could be reported proven and then break when the program ran (Goal A, advisory-prover-compare.md). Such a promise is now checked while the program runs, as every unproven promise is, so the count of proven promises a report, an audit or an attestation gives can fall. Two records with a List of Int field now compare as two such lists do, so a false promise past that comparison, reported proven until 8.3, can be refused with E700. Against v8.2.1 no example's output and no conformance verdict changes.
compatibility: every compiler error's and refusal's reference: line, the reference field of --json output and of SARIF, and each SARIF rule's helpUri name https://velaris-lang.dev/llms.txt and https://velaris-lang.dev/errors.html, where they named the same pages at the project's GitHub Pages address, which now redirects there. Only that text changes; no code, message, exit status or verdict does, and a reader following the earlier address reaches the same page.
compatibility: velaris attest writes the predicate type https://velaris-lang.dev/capability/v1, and a receipt names https://velaris-lang.dev/receipt/v1, where 4.2 to 8.2.1 named both at the project's GitHub Pages address (https://gowrishankar-infra.github.io/velaris-lang/...). velaris verify, velaris receipts diff, velaris replay and the OPA policy read each earlier name as the same type, so every attestation and receipt signed until now still verifies with Velaris; a verifier outside Velaris that pins one type name - cosign's --type, the Kyverno policy - takes the name the Statement carries. velaris.dev was never this project's domain: it is registered to someone else, 4.1 chose not to use it, no Velaris ever wrote a type under it, and velaris verify refuses a Statement naming one as it refuses every type Velaris does not define. The types now name a domain the project controls. A Statement's specification and a receipt's say velaris-spec 0.11.0, the version that records the new names.
compatibility: velaris verify given a file checks it as an attestation or a receipt (exit 0 verified, 1 refused or naming other bytes, 2 not checked); with no file it is the older spelling of velaris deps --verify, as before. Until 8.3 a file given to velaris verify was ignored and the vendored libraries were checked.
compatibility: log, every function of stdlib/log.vel, and velaris trace write a line feed, a carriage return, an escape, a NUL, every other C0 and C1 control character but tab, DEL, U+2028 and U+2029 in a value as an escape (\n, \r, \xNN, \uNNNN), so each call writes one line. Output changes only for a logged or traced value holding one of those characters, which until 8.3 reached the error channel as it was and could end its line, begin another, or move a terminal's cursor over one; print is unchanged.
compatibility: stdlib/csv.vel quotes as RFC 4180 does. line_of changes its output only for a value holding a comma, a double quote, a carriage return or a line feed, which it now writes between double quotes with each double quote doubled: a value with a comma never came back from fields as one field, and one with a double quote, a carriage return or a line feed came back from fields but was split by rows_of and by any RFC 4180 reader. fields and column change only for a line with a field that begins with a double quote, now read as a quoted field; rows_of changes only for text in which a line feed falls inside such a field, which now stays in its row.
compatibility: a receipt may carry stop and run_parameters.profile, added within velaris.receipt/1 (velaris-spec 0.11.0, section 8.7); only a run of velaris eval writes them, and a reader ignores a field it does not know.
api: the command line gains velaris eval, velaris receipts diff, velaris replay, velaris permissions-ratchet, velaris test --from-contracts (with --count, --witness-seconds and --json), velaris verify <file> (with --root, --identity, --skip-signature and --json) and --record-responses on a run; the library gains SITE, CAPABILITY_PREDICATE_TYPES, RECEIPT_PREDICATE_TYPES, predicate_kind, the run-state names STOP_FILE and RESPONSES, and the permissions ratchet's read_workflow, permissions_compare, permissions_ratchet, permissions_lines, permissions_exit, permissions_main, WorkflowUnreadable, PERMISSION_SCOPES, PERMISSION_LEVELS and PERMISSIONS_RATCHET_SCHEMA; check_proofs gains witnesses_out and witness_count; CAPABILITY_PREDICATE_TYPE and RECEIPT_PREDICATE_TYPE are the velaris-lang.dev names; and the Action gains the permissions-ratchet input, off by default.
differential: 14a - a program of benchmark category 14, new in 8.3, so v8.2.1 has no verdict for it
differential: 15a - a program of benchmark category 15, new in 8.3, so v8.2.1 has no verdict for it

Against v8.2.1 (check_differential.py), velaris-spec's 456 conformance
cases give the same verdicts, and the quick benchmark differs only in the
two programs above. Of the 97 examples, 36 print something different, and
in every one the only line that differs is the reference: line of an
error, which names velaris-lang.dev (the compatibility line above): examples/avg_bad.vel, examples/builtin_unhandled.vel, examples/callsite_bad.vel, examples/caught.vel, examples/conj_bad.vel, examples/contract_broken.vel, examples/contract_impure.vel, examples/discount_bad.vel, examples/div_bad.vel, examples/fail_proof_bad.vel, examples/failing_bad.vel, examples/floats_bad.vel, examples/fp_proof_bad.vel, examples/funcs_bad.vel, examples/generics_bad.vel, examples/grid_bad.vel, examples/import_bad.vel, examples/lambda_contract_bad.vel, examples/list_mixed.vel, examples/list_oob.vel, examples/list_proof_bad.vel, examples/loop_bad.vel, examples/loop_proof_bad.vel, examples/many_errors.vel, examples/map_bad.vel, examples/maps_bad.vel, examples/ns_bad.vel, examples/offbyone_bad.vel, examples/proof_catch.vel, examples/qlist_bad.vel, examples/rec_proof_bad.vel, examples/records_bad.vel, examples/secret_bad.vel, examples/sneaky.vel, examples/std_bad.vel, examples/types_bad.vel.

A promise past a comparison was reported proven

A test written for a mutant the monthly run left alive found a Goal A break
in the prover as released, from 2.6 through 8.2.1
(advisory-prover-compare.md). == and != on
two values the prover holds as its own objects - two maps, two lists of
lists, two lists of Bool or of Text, a map and put of it - were Python's
comparison of those objects, a constant. So a branch taken when two maps are
equal looked unreachable, a promise past it was reported proven, and it broke
with E601 when the program ran. Two records compared field by field had the
same fault for a List of Int field; for a Float field, the prover's
equality and a run's disagree about NaN whichever rule the prover takes.
Those comparisons now leave the promise to runtime, as SPEC.md 9.4 says a
premise the prover cannot translate does, and a record's List of Int field
compares as two such lists do.

The interpreter checks every promise, proven or not, and no function that can
hold such a comparison is compiled to native code, so no run went unchecked.
What was false is the report: check, proofs, explain, the audit, an
attestation's count of proven promises, the library's proven, and the proof
of any function that relied on such a function's ensures.
check_prover_lies.py gains nine lies (COMPARED), check_mutant_kills.py
V6 holds the map case, and SECURITY.md lists the advisory; a CVE is requested
for it, as for every Goal A finding.

The documentation moved to velaris-lang.dev

The project holds velaris-lang.dev, and GitHub Pages serves this repository's
docs/ there; the earlier address redirects. Every link that names the
project's home moved: README, SPEC, TUTORIAL, LLM.md (and so llms.txt),
EMBEDDING, SECURITY, STABILITY, docs, CITATION.cff, pyproject.toml's
Homepage and Documentation, the npm package, the VS Code extension, the MCP
bundle and registry manifest, the Homebrew and winget manifests, and the
release workflow. The two predicate types moved too, as the compatibility
lines above say, and velaris/predicates.py holds...

v8.2.1

A patch release with no features. Under 8.2.0, printing one kind of
counterexample ended in a Python traceback instead of its error, and the
release workflow's Marketplace job ended green having published nothing.
Two gaps are closed with them: velaris capabilities check gets the check
ceiling, and the perf gate no longer accepts fewer than three runs a side.

compatibility: velaris capabilities check runs under the ceiling check and audit have had since 8.0 - 60 seconds and 2048 MB, raised with --check-timeout and --check-memory-mb, removed with --no-check-ceiling - and a check past it stops with E613 or E614 and exit 2. A tree whose check takes longer than 60 seconds needs --check-timeout; this repository's takes 0 to 3 seconds on each CI leg. No program that compiled under 8.2.0 is refused, and no report, audit or proof changes.
api: against 8.2.0 the command line moved in one place: velaris capabilities takes --check-timeout and --check-memory-mb, as check and audit do.

What was wrong

A counterexample that could not name a value ended in a traceback.
When the prover finds that a call can break its callee's requires
(E701), the message gives each argument's value in the counterexample. An
argument the prover does not translate - in the program found, put(...)
of a map - has no value in the model, and printing it asked Z3 to evaluate
nothing: check, proofs, audit and the library's check() each ended
in AttributeError: 'NoneType' object has no attribute 'as_ast' instead of
E701. The verdict was reached before the printing, and nothing reported
proven depends on it. Such a value is now shown as <unknown>:

[E701] this call can break a promise: 'f0' requires false, but 'caller' can call it with p0 = <unknown> - proven without running the program

In that program proofs reports abs_of proven and f0 and caller
checked at runtime. fuzz_parsers.py 30 found it under seeds 493132804
and 769080785, on test.yml's macOS legs for f64552f, which is why no
release followed that commit; both seeds reproduce it at 8.2.0 on Python
3.13 and 3.10. The printing dates from 0.13. Which releases could reach it
was not traced.

• check_hostile.py holds the program as found (section 1c: check,
  proofs, audit and velaris.check()).
• fuzz_parsers.py runs FIXED_SEEDS after its own seed whenever it is
  given a number of iterations and no --seed, with Python's hash seed
  fixed as --seed fixes it, so every leg runs the two seeds. Run against
  8.2.0's prover, it reports the AttributeError under each of them.

The Marketplace job ended green having published nothing. The release
workflow's vscode job had run with continue-on-error since 2.22, and
its publish step exited 0 after three Marketplace timeouts. 8.2.0's release
run (34923131050) reported the job a success with NOT PUBLISHED in its
summary, and the extension 8.2.0 did not reach the Marketplace in that run.
Because the job had succeeded, gh run rerun --failed had nothing to
re-run.

The job now has no continue-on-error. A timeout is retried up to five
times, 30, 60, 120, 240 and 480 seconds apart; a failure that is not an
outage (no token, a token or a manifest the Marketplace refuses) is not
retried. Whatever the publish step did, the job's last step runs
release_checks.py published vscode <version> --require --timeout 900,
which asks the Marketplace until it lists the version and exits 1 if it
does not, so the job is red whenever the extension is not listed at its
end. The jobs after it run either way, as before. check_release.py runs
the job's steps in bash with stand-ins for vsce, npm and sleep -
every attempt timing out, timeouts that clear, a version listed after a
timeout, a refused token, no token, a version already listed - and runs a
failed Marketplace publish, and its re-run, through the job-by-job
simulation.

Also

• velaris capabilities check stops at the check ceiling. It compiled
  every program under the directory in its own process with no ceiling, so
  a program built to stall the type checker held it, and the Action's
  ratchet step, until the job's own timeout; 8.2 listed this as known
  open. check_ratchet.py adds a map literal nested 22 deep to a tree and
  holds the check to E613 after --check-timeout 2 and after
  --check-timeout 5. THREAT_MODEL.md's known-open table no longer lists
  it. velaris review has the same gap and stays listed; the Action runs it
  in its pull-request comment step.
• The perf gate compares medians of three runs. release.yml's perf
  job already ran perf_gates.py --runs 3, and each side's figure was the
  median of its three runs, taken in turns (8.2.0's job logged "round 3 of
  3 done"). What changes is that --against refuses fewer than three runs,
  so no gate compares one run with one run. The limit is still 25%.
  check_release.py holds the gate to one slow or one fast run on either
  side.

velaris-spec is unchanged.

---

Made by release.yml after every leg of the tests passed on 1109058. Nobody tagged it by hand (RELEASING.md).

v8.2.1 is an annotated tag and is not signed: the workflow holds no signing key, and a keyless signature made in Actions (gitsign) is one GitHub does not show as verified. Every file below is signed with sigstore as release.yml@refs/heads/main, and its certificate names this commit; SECURITY.md says how to check one.

Full Changelog: v8.2.0...v8.2.1

v8.2.0

A minor version with no language features. It is about what holds Velaris
to what it says: tests, gates, and the work of keeping them running. Along
the way the new suites found holes, and they are fixed here: three with an
advisory, and several more named below.

compatibility: the proof cache is removed. Velaris keeps no proofs between runs, and every promise is proven in the process that reports on it or runs it, as 8.1.1 already required. --no-cache is accepted everywhere it was and does nothing, with one notice on stderr, and velaris clean does nothing and exits 0. Both are removed in 9.0 (STABILITY.md, "Deprecations in force"). No program, budget or report changes.
compatibility: on a run, -- ends Velaris's own flags, and every word after it is the program's args(). A flag written after -- used to apply to the run: -- --allow all granted every effect (advisory-cli-double-dash.md). args() no longer holds the -- itself. A flag written before --, or with no -- at all, is read as before.
compatibility: a local or parameter named like a builtin, or like one of the program's functions, no longer hides a call to that name from the effect check (E300) or the Secret check (E560). The runtime always called the builtin or the function, so each such program already did what the checks now say.
compatibility: unary minus of the smallest whole number, and that number divided by -1, stop with E407, as every other arithmetic past 64 bits did (advisory-int-negation.md). to_int, json_int and py_int fail on a number outside the range, round of a value with no whole number in range stops with E407, and native code refuses an argument outside the range with E407.
compatibility: blocks nested more than 4,000 deep, else if chains included, are refused with E102. Past some thousands they ended in a Python traceback; 3,000 deep runs on every leg.
compatibility: velaris check and the library give a main marked or fail E524, as a run always did; they gave E523. E523 is now only fail in a function that does not declare or fail. The descriptions of E102, E542 and E609 in the error table say what the compiler gives them for.
compatibility: read_file of a path holding a NUL character fails with a reason the program can handle, write_file of one stops with E608, and file_exists of one is false. Each was a Python traceback.
api: tests/api/golden.json is new in 8.2 and records the library, the command line, both doors, the MCP tools and the Action, with signatures written without their annotations; against 8.1.1 the surface moved in two places, both text: velaris check --help lists --json, and the velaris_card tool's description says about 4,600 words.

What was wrong

Unary minus was not range-checked (Goal A; advisory-int-negation.md;
2.14 through 8.1.1). -n of the smallest whole number was 2^63 in the
interpreter and wrapped back to itself in native code, and the smallest
number divided by -1 was unchecked in the interpreter. A function proven to
return result > 0 from -n for n < 0 ran as native code and returned a
negative number, exit 0. Found by the corpus of false promises
(check_prover_lies.py), which this release extends.

Words after -- were Velaris's flags (Goal C;
advisory-cli-double-dash.md; 5.0.0 through 8.1.1). Every flag read in
the command line scanned the whole command line, and the first occurrence
won. A wrapper that passed someone else's words after --, with no
--allow of its own, handed them the budget. Found by
check_self_budget.py.

A program given to the library as text imported from the temp directory
(Goal C; advisory-source-temp-import.md; 2.52 through 8.1.1). The text
was written to a file directly in the system temp directory, and its
imports resolved beside that file first. A std.vel another local user
planted in /tmp ran instead of the standard library's, under the
caller's budget, and the audit reported it. Found by check_self_budget.py.

A local named like a builtin hid a call from the checks (Goal B). The
effect check skipped every call to a local's name (1.6 through 8.1.1), so
let print = 0 let a pure function print, and let shout = 0 let it call
a function with effects. From 7.0.0 the Secret check did too: a Secret
reached print, and velaris audit said no secret left the program. The
budget still held - the run had been granted io. Found by the stage unit
tests.

The standalone executables could not check (8.0.0 through 8.1.1). The
check ceiling runs a check in a child process, and the executable started
velaris.py for it, which it does not hold: every velaris check and
velaris audit failed with E001. The release workflow's smoke test ran
--version, doctor and a program, and not a check. Found by the new
canary on its first run. 8.2 starts the executable itself, and the smoke
test and the nightly install test run check.

Tracebacks, and a hang. check_hostile.py found five:

• a value nested some thousands deep, printed, compared, encoded or
  formatted, ended in a Python RecursionError (now E609);
• blocks nested past some thousands deep did the same in every command
  (now E102, above);
• a NUL in a path reached open (above);
• printing a character a cp1252 console cannot show ended the run with a
  UnicodeEncodeError; standard output now writes an escape for it, as
  standard error always did;
• native compilation emitted the left side of every + twice, so a sum of
  n terms emitted 2^n trees and a 20-term sum never finished compiling.

proofs and audit --sarif left out any path holding ".velaris" (Goal
B; 2.33 through 8.1.1). The test was a substring, meant for the old
project-local cache folder, so cfg.velaris.d/ was skipped too. Both now
read a directory as capabilities check does: every directory but .git.

The standing adversarial pass, run against the split and the gate,
found six more, all fixed before release.

• The new gate counted a compatibility: line in a code block, in an HTML
  comment, with nothing after the colon, or saying TODO. A line now counts
  only as prose that says something.
• It saw only a code written in the literal ERROR_TABLE; a code added by a
  subscript, by update() or in a sub-package went past it. Any text in the
  source that is one code now counts.
• It compared defaults as text, so a default read from another constant,
  a variable of the run state such as EFFECT_BUDGET, and a parameter that
  lost its default went past it. Each is now seen; a default computed in a
  function body still is not.
• A VERSION holding line breaks could write step outputs of its own (in
  the gate since 7.2). A VERSION that is not X.Y.Z now writes none, and
  no output may hold a line break.
• A module that is not UTF-8 or does not parse made the gate stop with a
  traceback; it fails closed as before, now in one line.
• The split made a write to a run-state name silent (Goal C, 8.2 before
  release). velaris.IMPORT_ROOT = root set the global the runtime read
  while Velaris was one file; in the package it set an attribute nothing
  read, and imports stopped being confined. A write to such a name now
  reaches velaris.state (check_adversarial.py SPLIT-1 and SPLIT-2). No
  release had this.

Smaller. velaris check and a run gave main ... or fail two codes
(above). The loader left each file it read open until the garbage collector
closed it. On Linux, check_adversarial.py stopped with a TypeError when a
child it timed out had printed something. examples/bench.vel said both its
functions run as machine code; fib is recursive, which native code
refuses, so only burn does, and the comment now says so. The documents said things the
code did not; check_docs.py found them, and each is corrected: README's
benchmark and proven-share figures and its card length, SPEC.md's escapes,
import cycles, what the prover models of Money, and its lists of fallible
builtins, LLM.md's rules 2 and 7 and its E523, E524 and E542 rows, and the
paper's benchmark and conformance figures, which are now generated from
benchmark/results.json and velaris-spec's index.

The proof cache is gone

8.1.1 stopped believing the cache; 8.2 removes it. There is no cache
directory, no VELARIS_CACHE_DIR, no loader and no saver. CACHE-1 to
CACHE-10 in check_adversarial.py now plant what used to work - 8.1.1's
file, under the key 8.1.1 computed, where 8.1.1 looked - and hold that
nothing reads it. THREAT_MODEL.md's cache rows say "removed in 8.2".

The release gate

• A minor or patch release says what it changes that STABILITY.md
  covers. The gate compares the previous tag with this commit: an error
  code added anywhere in the compiler's source, a flag the command line or
  the MCP server no longer knows, a default that is not what it was - a
  named default, a variable of the run state, or a parameter default of
  the library, read through any constant it names. Any one of them in a
  minor or patch release needs a compatibility: line in the entry, and the
  refusal names what it found. A moved tests/api/golden.json needs an
  api: line in any release. RELEASING.md step 7 and STABILITY.md rule 5.
• RELEASE_PAUSED, a variable of the release environment, stops the
  tag and every publish while the tests and builds still run.
• Held to the previous release. Before tagging, perf fails the release
  if pure-numeric time, native or interpreted, is more than 25% slower than
  the previous tag's (perf_gates.py), and differential fails it if the
  examples, the conformance corpus or the quick benchmark print anything
  the entry does not name (check_differential.py).
• check_release.py runs release.yml job by job against a stand-in for
  PyPI, npm, the Marketplace, GitHub and the MCP registry: a publish that
  fails midway, the re-run that finishes it with every publish made exactly
  ...

v8.1.1

A patch release with one fix. Compatibility: a patch under STABILITY.md
rule 1, because it refuses no program that legitimately worked. A false
promise that a planted cache entry let through now fails - before the run
with the prover (E700), while running without it (E601) - where it used to
pass without a word. A user with no planted entry sees one difference, in
time: a second velaris check of an unchanged program takes about as long
as the first.

What was wrong (Goal A; advisory-proof-cache-2.md; 7.1.2 through
8.1.0). 7.1.2 moved the proof cache out of the program's directory into a
per-user one, and bound each file to the source's path, its bytes and the
compiler version. What an entry said was still believed. A remembered
"proven" was reported as proven by check, proofs, audit and explain
without running Z3, and it made the function eligible for native code,
which has no runtime promise check. Everything a cache file's name and an
entry's key are made from is public, so a process running as the same
user, or anything that set XDG_CACHE_HOME or LOCALAPPDATA for the
process running velaris, could write an entry under the real proof_key. A false
ensures was then reported proven, and a run compiled the function to
native code and returned the wrong result with exit code 0. Run with
--no-native, the interpreter's own check still stopped it (E601). Two
independent external assessments of 8.0.0 reported it. The cause was the
design, not the file's location: a cached "proven" was allowed to switch off
a runtime check.

What changes.

1. Nothing in the cache is believed. Every function is proved in the
   process that reports on it or runs it. Only a proof made in that process
   marks a promise "proven" in check, proofs, audit, explain,
   attest and the library, and only such a function is compiled to native
   code. A contract not proven in that process keeps its runtime requires
   and ensures checks, interpreted or native.

2. A remembered promise is proved again, under a short budget. Of the
   two ways to keep the cache honest - prove a remembered promise again, or
   report it as "cached, unverified" - this release proves it again. The
   short budget is one second plus three times what the proof took when it
   was remembered. A proof that has not settled by then is proved under the
   usual budget, so a check finds what --no-cache finds, and an entry can
   change how long a check takes but not what it reports. The cost is time:
   Z3 keeps nothing that makes a second proof cheaper than the first.
   Measured on the machine this was built on (Windows 11, Python 3.13,
   z3-solver 5.1.0), each second run against 8.1.0's:

   Second run of	8.1.0	8.1.1	8.1.1, --no-cache
   velaris check examples/fp_proof_bad.vel (a float refutation)	1.0 s	21.5 s	21.9 s
   velaris proofs examples	7.5 s	11 to 14 s	12 s
   velaris check examples/discount.vel	1.1 s	1.7 s

   That cost was accepted because the other way adds a third status to
   check, proofs, audit, explain, SARIF and velaris.audit/1, and
   every second check of a program would have reported less than its
   first.

3. No cache where nobody vouches for the directory. The Action runs
   check, proofs and review with --no-cache, since a runner's cache
   directory can be restored from another workflow's run, and velaris review now accepts the flag. The HTTP door, the MCP server and the
   library have never read the cache; from this release the language
   server's code lenses do not read it either. agent_loop.py passes
   --no-cache too.

4. A cache file is written whole, and an odd one is ignored. A save
   writes a temporary file, flushes it to disk and renames it into place.
   On POSIX the rename is flushed as well, and the velaris and proofs
   directories are made 0700; one an earlier Velaris made wider is narrowed.
   A file is ignored whole if any of these holds:

   • it is not whole JSON;
   • it names another schema, path, content or version;
   • it holds a malformed entry;
   • it is a link or not a regular file;
   • on POSIX, another user owns it or can write to it.

   A relative XDG_CACHE_HOME or LOCALAPPDATA is now ignored, as the XDG
   specification says, so the cache is no longer placed under the directory
   velaris runs in.

5. THREAT_MODEL.md's known-open table gains a row: the user running
   velaris is trusted; anything running as that user is that user - the
   cache, the receipts, everything. SECURITY.md lists the advisory as
   resolved, and HALL_OF_FAME.md credits the two assessments.

check_adversarial.py (CACHE-3 to CACHE-10) now covers the outside
reproduction and the cases around it:

• The reproduction: the real proof_key, with the cache moved through
  XDG_CACHE_HOME and LOCALAPPDATA, in a file this release's loader
  accepts. With the prover, E700 under check, proofs, audit,
  explain, a run and a run with --no-native. Without it, E601 on both
  runs and nothing reported proven.
• A lie no prover refutes: a planted entry for a loop whose false
  promise the prover cannot settle stops at E601 on both run paths.
• Files and settings: torn and foreign files, the directories' modes,
  links, and a relative redirect.
• Doors: the library, the language server and the Action.

The cache's format and location stay outside what STABILITY.md covers. The
file format is unchanged apart from a seconds field in each entry.
velaris-spec is unchanged.

---

Made by release.yml after every leg of the tests passed on 56afc32. Nobody tagged it by hand (RELEASING.md).

v8.1.1 is an annotated tag and is not signed: the workflow holds no signing key, and a keyless signature made in Actions (gitsign) is one GitHub does not show as verified. Every file below is signed with sigstore as release.yml@refs/heads/main, and its certificate names this commit; SECURITY.md says how to check one.

Full Changelog: v8.1.0...v8.1.1

v8.1.0

A minor version. A program, a budget or a command line written for 8.0
means the same under 8.1, except for what "What 8.1 refuses that 8.0 did
not" names below: on the two doors, an import from outside the directory
they serve, and in the library, a check or audit past the ceiling the
command line has had since 8.0. The adversarial pass run against this
release found two holes, and both are fixed here, each with an advisory
draft.

Check and audit have a ceiling in the library and the doors. 8.0 put
velaris check and velaris audit under a time and memory ceiling on the
command line. velaris.check(), velaris.audit() and velaris.attest()
now run under the same one: 60 seconds and 2048 MB, raised with timeout=
and max_memory_mb=, and None for both checks in the calling process as
before. Source written to stall the prover or to bloat the checker comes
back as a problem - E613 past the clock, E614 past the memory cap -
and an audit that is stopped says ok: false with nothing determined.
velaris.Pool gains check() and audit(), which keep their worker
between calls. The HTTP door and the MCP server check and audit on their own
workers under --check-timeout and --check-memory-mb, and the command
line gains --check-memory-mb beside --check-timeout. The command line's
memory cap did not hold in 8.0 except on Windows: on Linux and macOS the
child it checked in was started without it, so an audit that 8.0 said was
held to 2048 MB used what it liked until the clock stopped it. It is set
now - on Linux, and on macOS as far as the system honours a cap, as for a
run - and check_library.py's Linux legs are what found it. Setting it
showed a second thing: under a cap, CPython on Linux reports running out
about half the time as SystemError: error return without exception set
rather than MemoryError, which the command line and velaris.Pool read
as a crash (E000). Both now read it as running out: E614 for a check or
an audit, E611 for a run. run(timeout=...)
now compiles inside its child, under the deadline: until 8.1 it compiled
first in the caller's process with no limit, so a program crafted to stall
the prover held run(source, timeout=5) for as long as it liked. A bounded
run is now a pool of one worker, and reports effects_used where it
reported None. A library check() or audit() costs a child process's
start - a third of a second on the machine this was built on - where it cost
nothing; timeout=None, max_memory_mb=None avoids that for source you wrote
yourself.

Receipts. velaris.receipt/1 records one run: the program and its
imports by sha256 - the subjects velaris attest writes for the same bytes,
so an attestation and a receipt of one program are its before and its
after - the budget, every refusal (code, effect, line), every
declassification with its reason, the run's parameters (seed, frozen clock,
timeout, memory cap, and confinement: "none"), the exit status and
outcome, and the wall time. It is an in-toto Statement of a new predicate
type, https://gowrishankar-infra.github.io/velaris-lang/receipt/v1, signed
as an attestation is signed. velaris program.vel --receipt FILE writes
one, run() and Pool.run() return one as RunResult.receipt, and the
doors return one when a request says "receipt": true. A run stopped by its
time or memory limit still has one, marked complete: false, holding what
the worker reported before it was killed. A receipt holds no value the
program handled: a refusal is recorded without the path or host it named, a
declassification without its value, and no output, input, argument or
message is kept. The release workflow signs the receipt of one run of
examples/effects.vel with cosign and with sigstore-python and verifies
both, so a release holds 27 files. velaris-spec 0.10.0 section 8.7 defines
the format.

What a policy can ask. policies/opa/capability.rego refuses an in-toto
capability attestation - what velaris attest writes - whose effects are
outside an allowed set or whose net hosts are outside an allow-list, and one
whose program did not compile or whose host is built while it runs, since
neither can be held to a list. capability_test.rego holds a pass, a fail
and the edges. policies/kyverno/require-capability-attestation.yaml
refuses a Pod whose image lacks a capability attestation, using Kyverno's
image verification with a keyless attestor. check_policies.py runs opa test, and opa eval against Statements velaris attest writes, and skips
them with a notice where OPA is not installed; CI installs OPA 1.20.2.
EMBEDDING.md has the example.

velaris eject. velaris eject program.vel writes a directory that
runs, and builds into one executable with PyInstaller, with nothing from
this project installed: the program and what it imports, a copy of the
runtime and of the standard library files it uses, main.py with the budget
fixed at eject time, a requirements.txt pinning the prover and the native
compiler to the versions installed, proofs.json recording what was proven,
SHA256SUMS, and a README saying what holds once ejected and what does not.
The copied runtime enforces the budget whatever the program says. main.py
refuses --allow; refuses a program that differs from eject time unless
given --changed-ok, and a runtime that differs whatever it is given; and
refuses a budget that would let the program write into its own directory or
where Python imports from (sys.path, PYTHONPATH, the site directories),
and a --receipt inside its directory. The last two came from the
adversarial pass: a program granted a write to a PYTHONPATH directory
left a sitecustomize.py that the next Python started there ran, and
--changed-ok ran a runtime that had been edited. The proofs are a record
that nothing trusts when the
program runs; main.py --prove runs them again. check_eject.py ejects
examples/discount.vel, runs it from a fresh virtual environment with no
packages, then changes it to reach the network and sees E310.

The doors.

• velaris serve --rate-limit N answers at most N requests a minute - 600
  unless told otherwise - per token, and per address for requests without
  it, so a caller guessing tokens is limited and cannot spend the holder's
  allowance. Past it the answer is 429 with Retry-After, logged
  rate_limited.
• --bind names the address (--host still does). A door bound anywhere
  but loopback says so on stderr before it listens.
• The token comparison was confirmed rather than assumed:
  secrets.compare_digest over two sha256 digests, whatever length was
  sent. It is one function now, which a test watches.
• EMBEDDING.md says what can connect to the MCP server and the language
  server, and that neither runs a program to answer a hover, a format, a
  check or an audit; a test sends both a program that writes a file, and no
  file is written.

What 8.1 refuses that 8.0 did not.

1. On the HTTP door and the MCP server, an import from outside the
   directory they serve - --root, the directory they were started in
   unless it names another - or of a file there that is not .vel, is
   refused with E515 before the file is opened. A program sent as text
   is compiled as a file in that directory, so its relative imports resolve
   there. Until 8.1 such a program could import any file the door's user
   could read, and the compiler's error quoted what it found
   (advisory-import-read.md). A door serving programs that import files
   elsewhere needs --root naming their directory. The library is
   unchanged unless import_root= is given. By the reading STABILITY.md
   applied to 3.4, a door that refuses what it accepted is a break; this
   one is made in a minor version, and STABILITY.md records it as such and
   says why.
2. In the library, a check() or audit() past 60 seconds or 2048 MB
   is stopped (E613, E614) where 8.0 waited for it. The command line has
   stopped it at the clock since 8.0, and on Linux now stops it at the
   memory cap too, which 8.0 named and did not set there.

Two holes, fixed.

• A false promise could come back proven (Goal A;
  advisory-prover-names.md; 0.9 through 8.0.0). The prover gave the values
  it made up Z3 names a program could also write: __g_result_1 for the
  result of a call to g, xs__n for the length of a list xs. A
  parameter with such a name was the same Z3 value, so a parameter named
  __g_result_1 turned g's promise about its result into an assumption
  about the parameter, and a false ensures was reported proven - and,
  compiled to native code, never checked when it ran. The prover's own names
  now begin with ! or contain #, which no identifier can. It was found
  checking this release's item 6: the prover builds every query from the
  syntax tree and parses none from text, so an identifier spelled like
  SMT-LIB is an identifier - but a name the prover spelled for itself could
  be written by a program.
• An import could read a file and quote it (Goal C;
  advisory-import-read.md; 0.16 through 8.0.0). An imported file that is
  not Velaris source gave an error naming its first token - import "/home/me/.env" answered found 'API_KEY' - through the library and both
  doors. That error now names the file and nothing in it, everywhere, and
  the doors hold imports to their root. THREAT_MODEL.md said an import
  "reads Velaris source, not data"; that was wrong, and it now says what an
  import reads.

Smaller things.

• VELARIS_CACHE_DIR names the directory the proof cache goes under
  (<dir>/velaris/proofs); velaris clean still deletes only that
  velaris directory. A cache file is written beside itself and renamed
  over the old one, so two checks of one file at once each read a whole
  entry. audit() no longer writes the cache, which README.md already said
  the library never did.
• refused_effect and...