Changelog: 7.x
Every release of this major version, newest first, as CHANGELOG.md records it.
7.2 - Releases that tag themselves #
No change to the language, the library, the error codes or the command
line, except one mcp-verify default that follows from how releases are
now signed.
A release is made by the workflow, not by a tag. release.yml no
longer runs when a tag is pushed. It runs when the tests complete on a
push to main with every leg passed, and a gate - release_checks.py gate - decides whether that commit is a release: VERSION must be newer
than every tag, CHANGELOG.md must have an entry heading for exactly that
version, and the six version files must agree. Otherwise the run says
why in one line and ends green without doing anything, so an ordinary
push to main stays ordinary. A release must also be the very commit the
tests passed on; if main moved while they ran, the gate refuses.
Everything is built, signed and verified before the commit is tagged,
and then published in order, each step skipping what is already there:
PyPI and npm by OIDC trusted publishing, with no token stored for
either; the VS Code Marketplace, as before; the GitHub release; the MCP
registry, logged in by GitHub OIDC, with server.json listing both
packages; and the attestation. Last, PyPI, npm, the registry and the
GitHub release must all report the version, or the run fails and names
the one that does not. RELEASING.md is the procedure,
what a person still does - publishing an advisory, yanking - and the rule
that nobody tags by hand. check_release.py holds the gate to fixtures
(a docs-only commit, a version bump without a CHANGELOG entry, a correct
bump, and what else it refuses), and the release runs it before gating.
test.yml is unchanged.
The tag is annotated, not signed. This repository has no tag-signing setup - no earlier tag is signed - the workflow holds no signing key and should not, and a keyless gitsign signature is one GitHub does not show as verified. The release notes say so. What is signed is every artefact, as before.
Signed as main. A workflow_run runs on main, so from 7.2.0 the
sigstore certificates name release.yml@refs/heads/main instead of
release.yml@refs/tags/vX.Y.Z; they also record the commit and the
workflow_run trigger, and SECURITY.md shows how to check both.
velaris mcp-verify now expects the main identity for a manifest of
7.2.0 or later and the tag's for an earlier one; a Velaris older than
7.2.0 checking a 7.2.0 manifest needs --identity.
An advisory file becomes a draft request, never an advisory. When a
release adds an advisory-*.md, the workflow writes the request for a
draft repository security advisory and prints the two gh commands
that create it and request its CVE. It cannot run them - GITHUB_TOKEN
cannot be given the repository-security-advisories permission - and it
never publishes an advisory.
README said the proof cache lived in ./.velaris/. That stopped
being true in 7.1.2, and it described the very behaviour the proof-cache
advisory is about. "Remembered proofs" now says where the cache is, how
it is keyed, that a ./.velaris/ is ignored, and what --no-cache and
velaris clean do; STABILITY.md's mention is corrected as well.
7.1.2 - The proof cache could be lied to #
An adversarial pass against 7.1.1 found four things. One is a soundness hole and the reason for this release; three are hardening.
The proof cache could be lied to (soundness; SECURITY.md challenge #1;
2.29 through 7.1.1). A second velaris check need not re-run the prover
because proof results are cached on disk. Until now that cache was
./.velaris/proofs.json, read from the directory the compiler ran in -
the directory that holds the program. A "proven": true entry was trusted
without re-proving, and the cache key is a SHA-256 of public, deterministic
inputs (the version, the function's text and contract, its callees'
contracts, the records). So a ./.velaris/ shipped alongside an untrusted
program - inside a project directory or a tarball - could forge an entry
that made a false ensures be reported "proven" by check, proofs,
audit, explain and the library; and because a "proven" pure-integer
function is compiled to native code, which carries no runtime promise
check, the false promise was also unenforced when the program ran - it
finished with the wrong result and exit code 0. SPEC.md §9.2 says "proven
means established by Z3 before the program runs"; a poisoned cache made
that a lie.
The fix: the program's directory is never trusted for the cache. It moves
to a per-user directory (%LOCALAPPDATA%\velaris on Windows,
$XDG_CACHE_HOME/velaris or ~/.cache/velaris elsewhere), and each entry
is bound to, and re-verified against, the source's absolute path, a hash of
its exact bytes, and the compiler version - so a transplanted or hand-edited
entry is re-proved, not trusted. A ./.velaris/ present in a project is
ignored; velaris audit prints ignored: ./.velaris/. If no per-user cache
can be written, the run proceeds without one. A poisoned ./.velaris/ is
therefore never read: the first run on a malicious program refutes the false
promise (E700 with the prover, or the runtime check E601 without it). See
advisory-proof-cache.md and THREAT_MODEL.md.
Native recursion is bounded like interpreted recursion (hardening). A
runaway recursive function compiled to native code looped unbounded, because
the interpreter's E609 "recursion that never stops" guard had no equivalent
in native code; the same function run --no-native reported E609 promptly.
A directly or mutually recursive function is now left interpreted so the
guard applies, and the interpreter runs a program on a thread with a large
stack so the guard fires cleanly - as E609, within a few seconds - rather
than overflowing the C stack, which on CPython 3.10 for Windows could
crash the process before the guard was reached.
A giant expression is a clean error (hardening). A single expression chaining thousands of operators, or nesting thousands of brackets, built a tree deep enough to overflow a later pass with a Python traceback. The parser now stops such an expression with E102, and the compile pipeline lifts Python's recursion limit so ordinary deep trees still walk.
read_file has a size ceiling (hardening). read_file and
read_file_secret read a whole file into memory at once. They now refuse a
file larger than 64 MiB with E316, raised for a run with --max-read <MB>.
fetch and post already capped their reads; this brings the disk to
parity.
The adversarial pass also confirmed, and this release keeps as regression
cases (check_adversarial.py), that secrets reach no sink, the sandbox
paths hold on Windows, the ffi reach check refuses foreign modules,
shadowed builtins never win, bidi and zero-width characters outside a
string are refused, velaris trace redacts, and the pool leaks nothing
between runs. One finding is left open on purpose: a net: grant does not
bound the socket peer when an ambient HTTP_PROXY is set, because closing
it refuses traffic that reaches a proxy today and STABILITY.md rule 1 makes
that a major - it is fixed in 8.0.0 and listed in THREAT_MODEL.md until then.
7.1.1 - 7.1.0 did not import on Python 3.10 or 3.11 #
7.1.0, published earlier today, declares requires-python >= 3.10 and
does not import on Python 3.10 or 3.11. velaris.py held an f-string
with a backslash inside a replacement field - re.split(r'[\s=]', ...),
in the lockfile reader added for deps-diff - which is a syntax error
before Python 3.12, so every command, every library call and the MCP
server fail at import there. CI caught it on all six Python 3.10 legs.
The release had been verified locally before tagging, but only under
Python 3.13, and a scan written to look for exactly this construct had
a quoting mistake and checked nothing. The expression is now computed
before the f-string, and every Python file in the repository compiles
under Python 3.10.
The second defect was in deps-diff's pull-request comment. To keep an
@name taken from a lockfile from mentioning anyone, 7.1.0 put a
zero-width space after the @ - the character itself. A console that is
not UTF-8, such as the cp1252 of a Windows runner, cannot encode it, so
velaris deps-diff --markdown failed at the first @ in a report, and
check_deps.py failed on both Windows Python 3.12 legs. The comment now
carries the same character as an HTML entity, ​, so the text is
ASCII and GitHub still renders no mention. A comment posted with
--comment was not affected: its body goes to the API as JSON, with
anything outside ASCII escaped.
Nothing else changed. A 7.1.0 user on Python 3.12 or later has nothing to change; on 3.10 or 3.11, 7.1.0 cannot have run, and 7.1.1 is the version to install.
Verified before pushing. Every Python file in the repository
compiles under Python 3.10.20, and under that interpreter, with
.[test] installed and no prover, the whole list the 7.1 entry names
passes with none wrong: run_tests.py 97/97, check_sandbox.py 57,
check_secret.py 78, check_pool.py 39, check_ratchet.py 114,
check_deps.py 54, check_fallible.py 29, check_refusals.py 15 with
10 skipped for needing the prover, check_library.py,
check_money.py, check_platform.py, check_termination.py,
fuzz_native.py 30, conformance at L1, L2 and L3, the 456-case drift
test, benchmark/run.py --quick --check, velaris capabilities check .,
the formatter, and the docs and playground builds. Under Python 3.13
with the console forced to cp1252 (PYTHONIOENCODING=cp1252),
check_deps.py passes 54/54, and 7.1.0's escaping raises
UnicodeEncodeError where 7.1.1's prints. Neither fix is on a path
the benchmark takes; a full run at 7.1.1 wrote every verdict and every
line of evidence 7.1.0's had, and benchmark/RESULTS.md and
results.json differ only in the version they record. The paper's
benchmark figures and its reproducibility section now name 7.1.1, the
release to check them out at, rather than 7.1.0.
7.1 - What an upgrade gained #
A dependency can change what it can do between two versions while its name, its publisher and its declared dependencies stay the same. Koi Security's report on the npm package postmark-mcp describes versions 1.0.0 to 1.0.15 working as an email tool, and 1.0.16 adding a blind copy of every outgoing message to an outside address and nothing else. A signature from the same publisher verifies 1.0.16 as readily as 1.0.15, and an SBOM lists the same dependencies for both. What changed was what the package could do. This release compares that where it can be compared, and says plainly where it cannot - which, for a package that is not Velaris, is nearly everywhere.
velaris deps-diff <package> <old> <new> reads two versions of one
dependency - pypi:NAME, npm:NAME, git:URL or a path to a git
repository (versions are tags, branches or commits), or dir:PATH (one
subdirectory per version) - and reports what the newer one gained.
- A Velaris library. Each version's capability surface is derived
from its
.velfiles ascapabilities initderives a tree's, and the newer is held to the older bycapabilities check's rules, W1 to W5, with the older standing as the baseline. What it reports gained is what the check reports widened: a new effect; a host, path or Python module inside an effect the older version already had; morefsornetoperations in a run; a function that declares an effect it did not. Each finding names the file, line, function and call that introduced it and the chain of calls that reaches it, in the check's own shape less the edit tovelaris.capabilities, since there is no such file to edit. A version that narrows, or that only moves text around - functions reordered, locals renamed, a literal moved into a variable - reports nothing gained. - Any other package. What the registry and the package's archive
declare is read, and nothing more: the install-time scripts npm runs
(
preinstall,install,postinstall, andnode-gyp rebuildfor a package with abinding.gypand neither of the first two), what pip runs when it builds a source distribution (setup.py, the build backend and what that requires), a.pthfile with animportline, which Python runs at every start; and the declared dependencies - npm's dependencies, optional and peer dependencies, PyPI'sRequires-Dist. A script added or changed is reported, including a changed file behind an unchanged command. When a registry's manifest and thepackage.jsonin the tarball disagree, the scripts of both are reported, each marked with where it was read, because which one npm runs has differed between npm versions and depends on whether it installs from a lockfile; a disagreement about dependencies is named, and the manifest's, from which npm resolves a fresh install, are the ones compared. What a script does is not derived. Nor is what the package's code can do: no effect, host or path is read off Python or JavaScript, and the report says the capability surface is unknown. A package holding both Velaris and other code gets the.velsurface and a statement that the rest is not in it. - Exit codes. 0 when both surfaces were derived and nothing was
gained; 1 when something was gained - a widening, or an install
script added or changed; 3 when nothing visible was gained and the
surface was not derived, so that "this could not be seen" is never a
0; 2 when a version cannot be read - one that does not exist (the
message lists what does), an unpublished npm package, a download
whose digest is not the one the registry lists, an archive past
64 MB.
--jsonisvelaris.deps-diff/1;--sarifreports each finding under six new rules on the errors page:dependency-capability-widened,dependency-effect-gainedanddependency-install-scriptas errors, anddependency-surface-unknown,dependency-addedanddependency-narrowedas notes. A bare package name is refused, so an npm package is never read from PyPI, or the reverse, by accident.
Lockfiles, and the Action. velaris deps-diff --against REF [path]
finds the lockfiles changed since REF - package-lock.json,
npm-shrinkwrap.json, requirements*.txt pins, Pipfile.lock,
poetry.lock, uv.lock, pdm.lock and velaris.lock - and compares
every upgraded dependency, up to 30 (--max), placing each finding on
the line of the lockfile that pins the new version. A library
velaris.lock vendors is compared file against file: the file at REF
against the file in the tree. A lockfile it recognises and does not
read (yarn.lock, pnpm-lock.yaml, Cargo.lock and others) is listed
as changed and not read. An entry resolved from git, a path, a link, or
a registry or index other than the one deps-diff reads is listed and
not read, because the public package of the same name is a different
package; so is every pin of a requirements*.txt that sets
--index-url or --extra-index-url. A dependency new in the lockfile
is listed as added, with nothing to compare it with. --comment --pr N puts the
report in one pull-request comment, found again by its own marker and
edited in place on later runs, and edits it to say so once no lockfile
changes any more; --from FILE renders a saved --json result, so the
registries are read once. The GitHub Action's new deps-diff input,
off by default, does all of that on a pull request and uploads the
SARIF when sarif is on. It never fails the job: for most packages the
answer is "unknown", and a gate on that would stop nothing it could
name. A package name, version or script from a pull request's lockfile
reaches the comment inside a code span, or with HTML and mentions
escaped, and a velaris.lock entry naming a file outside the
repository is not read.
The npm wrapper's table of subcommands names deps-diff as new in
7.1.0, so npx velaris-lang deps-diff against an older compiler says
which version it needs instead of the old compiler taking deps-diff
for a file name; check_library.py, which holds that table to the
compiler's own dispatch, found it missing before this release.
What it does not see, as THREAT_MODEL.md now says: declared
surface, not behaviour. For a Velaris library the ratchet's own limits
apply. For anything else it sees almost nothing, and postmark-mcp is
the example: by Koi Security's account 1.0.16 changed only the code
that sent the copy, which adds no install script and no dependency, so
deps-diff would have reported nothing gained and the surface unknown
- exit 3, not a finding. It would not have caught that case and does
not claim to. npm has since unpublished every version of the package,
and asked about it today
deps-diffreports that the versions cannot be read.
The benchmark: category 12, indirect authority. Three programs
whose calling code is the same file before and after an upgrade, and
whose dependency's declared budget widened between the two versions -
12a, a formatting library that declared nothing and starts posting
each line to a second host; 12b, a mail library that already reached
the mail service and starts sending a copy to a second host; 12c, a
settings library that read a file and starts writing one - and a
control, 12d, whose dependency narrows. Each caller already declares
the effect its dependency comes to use, so it compiles against both
versions and the compiler has nothing to refuse; the Velaris static
step is velaris deps-diff on the two versions, and it flags the three
before running and not the control. Deno stops all three while
running, each time with the dependency swallowing the denial and the
program exiting 0; Python misses all three. The harness gained what
that needed and nothing tuned per program: a program may import one
dependency at two versions; the DANGER marker is in the new version,
and the caller and the old version must carry none; placeholders are
filled in all three source files, with / in paths; and two
observations were added - a request that reached the second listener,
told apart from the caller's own request to the granted one, and a file
the dependency wrote. The table is now 67 programs, 59 dangerous and 8
controls: Velaris 45 caught before running, 12 while running, 2
missed; Deno 5, 30, 24; Python 0, 28, 31; no false positives anywhere.
No existing verdict moved: the 63 earlier rows have the verdict and
the evidence they had in 7.0.0's results.json, and the verdict they
had at 4.1.0. The benchmark README's table, the README's, and the
paper's section 4.1, Table 1, abstract and conclusion carry the new
figures; the rest of the paper stays pinned to 4.2.1, and its
reproducibility section says which figures come from 7.1.0.
Also fixed in the harness: benchmark/run.py --check on a full run
compared verdicts with results.json after the run had rewritten that
file, so it could not fail. It now compares before writing. The quick
run CI makes was never affected, since it writes nothing.
The README's CI section pinned gowrishankar-infra/velaris-lang@v5.0.1
and version: "5.0.1", two majors late, and EMBEDDING.md pinned the
same Action. All three now say 7.1.0, and run_tests.py's version
check fails when an Action pin or a version: in either file is not
the compiler's VERSION, so the pin moves with each release or the
suite stops.
check_deps.py, 54 checks, runs on every CI leg and reaches no
network: it serves PyPI, npm and the GitHub API on 127.0.0.1. A library
gaining net, a host inside net, a count, a Python module (read from git
tags) and a function's effect; one narrowing and one rewritten without
changing its surface, neither flagged; a version, a tag and a release
that do not exist, an unpublished package, a digest that does not
match, a package named without its registry; a JavaScript package
whose new source reaches the network, reported as unknown with no host
read off it; install scripts added and changed, a changed file behind
the same command, a registry manifest that hides the tarball's script,
a Python package gaining setup.py and an importing .pth; a package
holding Velaris and JavaScript; a tarball whose paths climb out, are
absolute or name a drive; the lockfile mode, with an unread lockfile
listed, a vendored library compared, a velaris.lock entry naming a
file outside the repository refused, and its plain-text report; the
lockfile formats read directly - a v1 package-lock.json whose entries
from git and from a private registry are left out, a Pipfile.lock
with an entry from another index and two packages pinning one version,
poetry.lock and uv.lock entries not from PyPI, requirements*.txt
with extras, markers, hashes and ===, and one that sets another index
- and how an upgrade is paired with the version it replaced; a hostile package name and error text rendered with no HTML, mention or broken code span; the SARIF of both modes, validated; the pull-request comment posted once and edited on the second run, edited again when no lockfile changes, and never posted for a pull request that changed none; and the four programs of category 12, each asserted directly with its unchanged caller compiling against both versions.
velaris.capabilities is recorded again at 7.1.0: 190 programs, the
new ones being category 12's callers (which do not compile outside the
harness, since their dependency is placed beside them only there) and
its eight dependency versions. The surface is unchanged. velaris-spec
needs no change: SPEC.md sections 6, 7 and 7.1, the budget grammar and
the formats it specifies are untouched, and the comparison deps-diff
makes is its section 9.5. The two JSON documents deps-diff writes are
marked provisional in STABILITY.md.
Verified, on Windows 11 with Python 3.13, in two fresh virtual
environments holding this tree - one with .[full,test] (z3 5.1.0,
llvmlite 0.49.0), one with .[test] and neither - rather than in this
machine's global Python, which holds an older Velaris. With the prover:
run_tests.py 97/97, check_library.py 240 correct,
check_fallible.py 29, check_money.py 81, check_sandbox.py 57,
check_secret.py 78, check_pool.py 39, check_platform.py 15,
check_termination.py 44, check_ratchet.py 114, check_deps.py 54,
check_refusals.py 25, none wrong; fuzz_native.py 30 agrees;
velaris conformance passes at L1 (307 cases), L2 (39, and one not run
because this system would not make a symbolic link) and L3 (109);
build_conformance.py --check matches velaris-spec's 456 cases;
benchmark/run.py --quick --check matches results.json; velaris test examples/std_test.vel 7/7; examples/edges.vel 20 passed;
velaris fmt --check is clean; velaris capabilities check . passes;
the playground and the docs build. Without the prover the same list
passes, with check_library.py 229 correct, check_platform.py 14 and
check_refusals.py 15 with 10 skipped for needing the prover, the
other counts as above, and the quick benchmark naming 03a and 04a as
caught while running, as it does whenever the prover is absent. Eleven
consecutive full benchmark runs with Deno 2.9.6 - the last after the
final change to velaris.py - wrote byte-identical RESULTS.md and
results.json. velaris-spec's tools/check_sync.py passes against this
tree, and its tools/validate.py --capabilities accepts the
re-recorded velaris.capabilities. The arXiv package was regenerated
with pandoc 3.11 and builds to 12 pages. Verifying found three defects
in this release's own work, each fixed before tagging: inserting
section 20 had deleted the line def card(), which check_library.py
caught; two new module-level tables were not registered with
check_pool.py's reset scan; and the npm wrapper's table lacked
deps-diff.
Sources, named (CONTRIBUTING.md rule). The test category 12 is
built on was proposed by Ali Khater (dev.to alikhatersaibreakroom) in
a comment of 12 September 2026 on the dev.to post about this benchmark,
https://dev.to/alikhatersaibreakroom/comment/3elgc: "A next test I would
love to see is indirect authority: a safe-looking function calling a
dependency whose declared effect budget changes between versions." The
postmark-mcp case is from Koi Security, "First Malicious MCP in the
Wild: The Postmark Backdoor That's Stealing Your Emails" (Idan
Dardikman, 25 September 2025), read through the Internet Archive's copy
of that date because the original address now redirects elsewhere; its
indicators name 1.0.16 and later as malicious. npm's registry record
lists thirteen version numbers before 1.0.16 (1.0.4 to 1.0.6 were never
published) and every version unpublished on 25 September 2025. That a
registry's manifest and a tarball's package.json are published
separately and never checked against each other is from Darcy Clarke,
"The massive bug at the heart of the npm ecosystem" (vlt blog, 27 June
2023). npm maintainers have described which copy npm reads in two
contradicting comments on npm/cli issue 5234, and Arborist's source
shows the answer changed between npm releases; that is why deps-diff
reports both copies rather than choosing one. npm's default
node-gyp rebuild install script for a package with a binding.gyp
is from npm's scripts documentation. The design of the command - the ratchet's comparison with the older version
as the baseline, exit 3 for a surface not derived, the comment - was
specified by the maintainer.
7.0 - A secret you cannot look at #
6.0, published this morning, shipped Secret of T with a hole in it,
and this release closes it. The hole was in a decision 6.0 made
deliberately and argued for in writing, which is the kind worth
describing rather than quietly fixing.
What 6.0 got wrong. It let a comparison over a secret give an
ordinary Bool. The argument was that a comparison is one bit, that
if key == "" has to be writable, and that refusing print(k == "")
while allowing if k == "" { print("empty") } would stop nothing.
Every step of that is true of one comparison. It is false of a loop:
let at = 0
while at < 3 {
for c in alphabet {
if code_at(key, at) == code_at(c, 0) {
found = found + c
}
}
at = at + 1
}
print("recovered: " + found)That program compiled under 6.0 and printed the key. A comparison is
not a one-bit channel; with length and code_at it is a
character-by-character oracle. A type that stopped print(key) and
allowed the loop above is not information-flow control, it is a
decoration — and shipping a decoration under that name is worse than
shipping nothing, because somebody relies on it.
What 7.0 does. The rule loses its exception and gains a second half:
- Every pure operation over a secret gives a secret, a comparison
included.
key == ""is aSecret of Bool. So arelength(key) < 10andcontains(key, "a"). Nothing prints one — it is a Secret, so E560 already covers it. What a container is, as against what it holds, is not:lengthof a list of secrets is an ordinaryIntandhas(m, key)an ordinaryBool, because a program cannot have made a list's length depend on a secret without branching on one. So a program can still walk a list of secrets. - Nothing branches on one. An
iforwhilewhose condition carries a secret is E563, naming where the secret came from. The loop above is refused at the branch, before the print. - A promise is not a branch.
requires length(key) > 0is still allowed: a broken promise stops the run, cannot be caught and cannot accumulate, so it tells a reader one bit per run rather than reading a secret out in a loop, and its message already redacts the values whose type is secret.
To look at a secret, a program says so:
let empty = declassify(key == "",
"whether a key is set at all is not the key")
if empty { ... }which needs uses declassify, the operator's grant, and a reason the
audit records. That is the trade the language now offers: not silence,
a statement.
A third rule, and the second hole. Looking for the first hole turned up two more routes, both the same shape - a value derived from a secret coming back as an ordinary one.
A generic body is checked once, with its type variables standing for
nothing in particular, so inside fn contains_item(xs: List of T, item: T) -> Bool the comparison get(xs, i) == item is a plain Bool;
there is no secret in sight. Bind T to one at the call site and
contains_item([guess], key) hands the caller an ordinary Bool about
the key. 6.0 refused only effectful generics, on the reasoning that a
pure one can reach no sink - which was wrong, because it does not have
to reach a sink, it only has to hand the value back. No type variable
is now bound to a type that carries a secret (E560), pure or not. The
way to write a generic over secrets is to say so:
fn pass(s: Secret of T) -> Secret of T for any T.
And the second hole. A failure's reason is Text the
program can print, and the runtime writes it out of the values it was
given — to_int quotes the text it could not read. So
check to_int(key) { fail w { print(w) } } printed the key under 6.0.
No builtin that can fail now takes an argument carrying a Secret
(E560): to_int, parse_money, json_get, pop, slice, set_at
and the _or_fail family. get on a map is the exception that proves
the rule — its reason names the key, and a key is Text or Int.
The whole sink check now lives in one place in the type checker, so a
builtin added later cannot acquire a route quietly.
What a 6.0 user has to change #
6.0 was published for one day. If you wrote anything against it:
if key == ""and any other branch on a value derived from a secret — E563. Declassify the answer with a reason, or decide without looking.to_int(key),parse_money(key, ...),json_get(key, ...)and any other fallible builtin given a secret — E560. Declassify first.stdlib/env_tools.vel'snumber_settingnow declassifies before it looks, rather than after; its signature is unchanged.
This is a major version because it refuses programs that compiled under 6.0, and STABILITY.md rule 1 says that ships in a major version even when — especially when — it is a security fix. STABILITY.md records 6.0.0 as a release that stood for one day.
The record #
One new code, E563. check_secret.py grows from 58 checks to 76:
every fallible builtin refused, the comparison rules in both
directions, the branch refused in if and in while, the extraction
loop refused at the branch and the same program accepted with
declassify and recorded in the audit, contains_item, index_of and
first each refused a secret, and the Secret of T signature that is
the way to write a generic over one. check_refusals.py gains E563.
velaris-spec goes to 0.8.0: no rule of the format changes, and section
8.6 narrows what it claimed. The corpus is 456 cases.
The benchmark is unchanged: 42 caught before running, 12 during, 2 missed, 0 false positives.