Changelog: 8.x: 8.2.1 to 8.0

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

8.2.1 - Two things that should have been red #

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.

8.2 - Held to it #

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 once, a second run that publishes nothing, and a paused run that tags and publishes nothing. It holds 80 cases, the adversarial pass's among them.

One file became a package #

velaris.py is now velaris/, one module per stage in pipeline order, with run state in velaris/state.py (decisions/0001-split-the-file.md says why the single file aged out; ARCHITECTURE.md maps it). velaris.py remains as a launcher. import velaris and the command line are what they were: check_api.py records every public name and signature, every command's usage, both doors' request and response shapes, the MCP tools and the Action, and holds them to a golden. tests/unit/test_pipeline_order.py fails if a module imports one after it. The package and every script are typed: mypy --strict and ruff check report nothing over 182 files.

The test ladder #

check_adversarial.py gains N1 to N4, SHADOW-1 to SHADOW-5 and SPLIT-1 and SPLIT-2, 131 cases in all.

What runs, and where #

• test.yml is 18 legs: Linux, Windows and macOS x64 on Python 3.10 and 3.12, with and without z3 and llvmlite; Linux and macOS arm64 on 3.12; and Python 3.14 on Linux, run and reported and allowed to fail. Plus the suites twice at once, the cross-system comparison, and lint. CI installs z3-solver and llvmlite at the versions in requirements/ci.txt: llvmlite 0.49.0, and 0.45.1 on macOS x86_64, where llvmlite publishes no wheel of anything newer.
• nightly.yml installs every artefact built from main - wheel, sdist, MCP bundle, npm wrapper, standalone executables, Docker image, pre-commit hooks, the Action, the VS Code extension's language server.
• monthly.yml fuzzes for 20 minutes, mutates for 90, soaks the pool for 5,000 runs, asks every URL, compares against the previous release over the full benchmark, and runs native code and the parsers under AddressSanitizer and UndefinedBehaviorSanitizer.
• adversarial-models.yml, weekly, sends the standing adversarial prompt and one area of the compiler to Claude, Gemini and Grok, and skips any whose key is not set.
• Dependabot watches z3-solver, llvmlite and every action.
• velaris-canary, a public repository, checks the newest release every day from outside, as a user installs it, with the Action holding a committed velaris.capabilities.

Every scheduled job reports failures as issues - one per failed job, per surviving mutant, per adversarial finding - and nothing scheduled commits; MAINTENANCE.md is the long form, including the kill switch and the reference-runtime variable reserved for 9.0.

Measured #

Measured by perf_gates.py --against v8.1.1 on Windows 11 (AMD64, 16 CPUs, 4% busy when it began), Python 3.13.13, z3-solver 5.1.0.0 and llvmlite 0.49.0: medians of 5 runs after one warm-up. Wall-clock figures; another machine will differ.

check_differential.py against v8.1.1: the 97 examples, velaris-spec's 456 conformance cases and the 13 programs of the quick benchmark give the same output under 8.2.0 as under 8.1.1, so no difference needed naming.

velaris stats --ffi examples: 106 programs, 70 of which compile. 8 call Python, and all 8 name every module they call (a grant like ffi:math); none names a module while running. The modules named: builtins in 4 (native), datetime in 3, math in 3 (native), sqlite3 in 3, base64 in 1.

Proven share over examples/ and stdlib/: 70 of 99 promise-carrying functions (70.7%), generated into README and held by check_docs.py.

agent_loop.py --metric --offline, the ten tasks with recorded replies: 10 of 10 compile, each in its second round after the compiler named the first round's mistake, with the effects each task needs; 1 of 1 promise proven. No live model was run for this release.

Mutation, locally for 25 minutes on wrappers: 9 of 17 mutants killed (52.9%). The 8 survivors are in strip_secret, currency_clash and carries_secret.

Known open #

• A declared effect can move a promise from proven to checked at run time. A call the prover does not model (env, read_file, fetch, now, py, declassify, ...), and a let-bound call to a function that declares an effect, abandon the proof of the function they are in (SPEC.md 9.4). A limit of precision, not of soundness; found by check_properties.py, whose fifth property allows exactly that.
• The prover spends its whole budget on a loop invariant beside upper or lower in a function with nothing else to prove: 3 seconds a query where 0.02 would do.
• Deeply nested map and list literals are slow to type-check: 14 levels take about 27 seconds. A check or an audit stops at its ceiling with E613; a run has no such ceiling unless given --timeout.
• velaris capabilities check and velaris review have no check ceiling. They compile every program under the directory in this process, so a program built to exhaust the type checker - a map literal nested twenty deep - stalls them, and the Action's ratchet step, until the job's own timeout. A check and an audit have stopped at their ceiling since 8.0. Until the ratchet does too, give a job that runs it on other people's pull requests a timeout-minutes. This repository keeps the two programs that test the check's ceilings as text in tests/error_messages/golden.json, not as .vel files, so its own ratchet does not compile them.
• The standalone executables of 8.0.0 to 8.1.1 cannot check (above); there is no patch release for them. Use the wheel, or 8.2.

velaris-spec is unchanged: its tools/check_sync.py finds SPEC.md sections 6, 7 and 7.1 and both predicate schemas as it quotes them, and no document format changed.

8.1.1 - The proof cache can no longer lie #

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.

8.1 - Receipts, and what a policy can ask #

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 the doors' log name the refusals 7.1.2 and 8.0 added (E316, E317, E318), which a door logged as failed.
• Every suite writes to a temporary directory of its own and keeps its own proof cache (suite_dirs.py), so two runs from one checkout do not collide: until 8.1 run_tests.py wrote report.txt and ledger.txt into the checkout, check_library.py shared one door log, and seven suites wrote a scratch program beside the source. CI runs run_tests, check_library, check_adversarial and fuzz_native twice at once, in one job, to show it. build_docs.py and build_playground.py write each page beside itself and rename it.
• README.md and EMBEDDING.md pin the Action by commit, with its tag in a comment, and run_tests.py checks that the commit is the one the newest tag names. Pinned to a commit, the Action installs the version that commit's velaris.py names, as it installs a tag's.
• packaging/placeholders/ records the names beside velaris-lang. velaris is free on PyPI and on npm, and the packages that would hold it are ready, not published: publishing takes a registry account this repository keeps no credential for. velarislang and velaris_lang cannot be registered by anyone on either registry.
• examples/platform audits a submission under its own limit, 20 seconds and 1024 MB, and answers 422 when the audit does not finish.

New codes: E515, E613, E614. velaris-spec goes to 0.10.0.

8.0 - What the socket reaches, and other things the audit now says #

A major version. Two of its changes refuse programs that ran under 7.x, so by STABILITY.md rule 1 they ship in a major - and a major is where a user learns to read the CHANGELOG before upgrading. Four things break; the rest add.

The socket peer, not the URL string (the proxy hole; E317). Through 7.x a net: grant checked the URL's host, but an ambient HTTP_PROXY / HTTPS_PROXY in the environment then routed the request - its payload included - to a proxy that need not be a granted host. The grant bounded a string, not the peer. This was the open hole THREAT_MODEL.md carried and the adversarial pass against 7.1.1 found (advisory left for a major). guarded_opener now disables ambient proxies unless the proxy's own host:port is itself inside the net budget, in which case that one proxy is honoured; a proxy the budget does not cover is refused with E317, naming the proxy and the grant that would allow it, and the refusal cannot be caught. velaris add no longer defers to an ambient proxy either. With no proxy set, behaviour is identical to 7.2.0.

A function named like a built-in is refused (E204). Through 7.x a program that defined fn print, fn env, fn read_file and the like was silently shadowed - the built-in won and the function was never reached, a call that read as one thing and did another. It is now E204. The rule of SPEC.md 10.1 is unchanged: a built-in added in 4.3 or later (the Money and Secret builtins) still gives way to a program's own function of that name, so fn money and fn split in a namespaced library keep working; only the older built-ins, which a program could never actually shadow, are the error. The shipped standard library is exempt, since it is always imported under a name.

A credential file wants read_file_secret (E318). read_file on a documented credential location - ~/.aws/*, ~/.ssh/*, .env, ~/.config/gcloud/*, ~/.docker/config.json, ~/.kube/config, ~/.netrc, *.pem, *.key - is refused with E318 and pointed at read_file_secret, which returns a Secret the compiler will not let escape. And a credential location is never covered by a broad fs:read: grant that merely sits above it: an operator names it, or a path within it, explicitly. read_file_secret on an explicitly granted credential path is the sanctioned way and works.

velaris add refuses two redirects. It refuses a redirect from https to http (which would drop the encrypted connection) and a redirect to a host outside the URL's origin - the two ways a vendoring fetch could be steered to bytes other than the ones the URL named.

What a user of 7.x has to change (STABILITY.md rule 4):

1. Proxies. A program that reaches the network with an ambient HTTP_PROXY / HTTPS_PROXY set and a scoped net: grant that does not cover the proxy is refused (E317). Grant the proxy's host too (net:PROXYHOST:PORT), or run with no proxy set. velaris add ignores ambient proxies entirely now.
2. Built-in names. A function named like a built-in from before 4.3 (print, env, read_file, fetch, get, length, split, ...) is refused (E204). Rename it, or move it into a file imported under a name so it is reached as prefix.name.
3. Credential reads. read_file (or file_exists) on one of the documented credential locations above is refused (E318). Read a secret with read_file_secret and grant its exact path; a broad fs:read: grant no longer includes a credential file.
4. velaris add redirects. A source URL that redirects https→http, or to a host outside its origin, is refused. Vendor from a URL that does neither, or fetch and add the file from disk.

The rest, none of it breaking:

• The audit says whether a granted module is native. velaris.audit/1 gains ffi_native: per named Python module, "native" when a compiled extension (.so/.pyd/.dylib, or a built-in) is found on disk, and "unknown" otherwise - never "false", because a pure-Python module can import a native one without that being visible. It is found from files on disk without importing the module, so a module whose import would act does nothing. A new SARIF note ffi-native; a THREAT_MODEL.md paragraph.
• Secrets in code scanning. audit --sarif emits secret-source (note) for env / read_file_secret, and secret-declassified (warning) for each declassify - an error under --strict unless its reason is listed in --allow-declassify-reasons <file>. No rule-id clashes with deps-diff's.
• Errors that teach. Every compiler error and every runtime refusal now ends with one line, reference: <URL>, pointing at the card (llms.txt), served at the documentation site; --json and SARIF carry it as a field. velaris check reports every error in a file, recovering at statement boundaries; SPEC.md 14 says the first is authoritative, and it is the one a single-error run gives.
• --seed <n> and --freeze-time <iso8601> make a run's randomness and clock reproducible, recorded as the run's parameters (the doors log run_params). Neither is a grant: random() still needs rand and now() still needs clock, and the budget still refuses them.
• check and audit run under a time and memory ceiling (60 s, 2048 MB by default; --check-timeout raises the clock), so a crafted contract or expression cannot stall a platform that audits before running.
• The Action installs its own version. With no version: input, the Action installs the release matching the tag it was used at (@v8.0.0 installs 8.0.0), and the newest on PyPI only from a branch or a commit.
• New suites. check_metamorphic.py (an audit is unchanged by renaming, reordering, dead code, or splitting a program across files, and one added effect changes it in exactly one way) and check_prover_lies.py (a corpus of false promises that must never come back proven).
• A TrapDoor benchmark case (category 13): a program whose stated purpose is a security scan and whose behaviour is read-credentials-then- post, caught before running.

velaris-spec goes to 0.9.0 for the two added velaris.audit/1 fields.