Changelog: 8.x: 8.6 to 8.5
Every release of this major version, newest first, as CHANGELOG.md records it.
8.6 - The name #
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 <owner>.github.io/<repo>, 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, examples/types_bad.vel - each prints the reference: line every error and refusal has carried since 8.0, and it now names sabline.dev where it named velaris-lang.dev. Nothing else in any of their outputs differs: same exit code, same error codes, same message text, same fixes. The old address redirects, so the line printed by 8.0 to 8.5 still reaches the card.
differential: examples/edges.vel - its own output shouts the project's name and encodes it: first, shouted: VELARIS is now SABLINE, and base64: dmVsYXJpcw== is the base64 of sabline. The program is a text-and-encoder exercise; the name is its input.
differential: examples/text_tools.vel - the same: the program's heading reads Sabline edge and property tests, and a shouted name in its output is SABLINE.
differential: examples/tools.vel - its usage line says try: sabline examples/tools.vel alpha beta where it said velaris.
differential: examples/trace_demo.vel - the prover's timeout note names SABLINE_PROOF_TIMEOUT where it named VELARIS_PROOF_TIMEOUT; both are read (STABILITY.md), and the note gives the name to write now.
differential: examples/native_build.vel - it reports [sabline] where it reported [velaris].
differential: examples/sandbox.vel - it tries to read the compiler's own launcher by name and is refused: cannot read file 'sabline.py' where the file was velaris.py. The refusal is the point of the program and is unchanged.
What is renamed #
- The packages. PyPI and npm
velaris-langbecomesabline-lang; the MCP registry serverio.github.gowrishankar-infra/velarisbecomes.../sabline; the VS Code extensiongowrishankar-infra.velarisbecomesgowrishankar-infra.sabline. - The repositories, renamed in place with
gh repo rename, so GitHub redirects every old URL - the web page,git clone, and a workflow that saysuses: gowrishankar-infra/velaris-lang@<commit>:velaris-lang,velaris-spec,velaris-kitandvelaris-canaryaresabline-lang,sabline-spec,sabline-kitandsabline-canary. - The domain. sabline.dev.
security@sabline.devis the security contact;security@velaris-lang.devstill reaches the maintainer. - The source, by
scripts/rename.py, which is committed: 7,393 occurrences in 293 files, as one case-preserving substitution with two lists beside it - the strings in which the old name is the fact being recorded, and the files that record rather than describe. The script run with no arguments is the drift test, andcheck_rename.pyruns it on every leg of CI beside a case for each of the nine aliases.
What is not renamed #
.vel, the file extension. It is name-neutral, and changing it would break every program that exists.- The eight published advisories, their text and their GHSA ids. An
advisory records what was wrong with a release that was called Velaris,
and its affected package really is
velaris-langon PyPI. - This changelog before this entry, and STABILITY.md's record of earlier releases. They say what happened.
- The documentation of 8.3, 8.4 and 8.5, at
/8.3/,/8.4/and/8.5/, left as those releases published it, at the address it was published at. Every link in it redirects. - Anything already published. Nothing on PyPI, npm, the MCP registry,
the Marketplace or the GitHub releases was deleted, yanked or moved. An
install pinned to
velaris-lang==8.5.0resolves to the same file, with the same digest and the same signature, for the reason 3.4 was not retagged and 6.0.0 was yanked rather than deleted. The old names get one last release that depends on the new one and prints the notice, and the npm one is marked deprecated. - Git history. Every file was moved with
git mv.
The new things this release does have #
docs/renamed.md, at sabline.dev/renamed.html: every published address, where it now points, and what was deliberately not renamed.sabline/naming.py, where every old name that is still accepted is decided - the environment, the document schemas, the file names, and the one-line notice each alias prints. One place to read, and one place to delete in 9.0.- A conformance case compares
safe_commandby its grants, not as a whole string (sabline-spec 8.3, 0.14.0). What that section defines is the grant list; what comes before--allowis the producer's own command name. Comparing the string had required every implementation to be called what the reference was called, so 27 L1 cases read as a changed verdict across the rename while nothing about the grants had moved. A corpus published for an implementation in any language must not ask it to be named a particular thing. check_rename.py, which runs every promise above: the command, the import, the submodule import, the warning,VelarisError, both spellings of six schemas, avelaris.capabilitiesofvelaris.capabilities/1checked by the ratchet, and a Statement of each earlier predicate type verified - and refuses one of a type Sabline does not define.
8.5 - Taste #
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,listwithnextLinkpaging (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'sSecret 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 exactlymanagement.azure.com:443.stdlib/k8s.vel: the API server over REST with aSecrettoken;in_cluster()reads the service-account file withread_file_secret;list(withmetadata.continue),read,watch_once, andpods,pod,services,deployments,deployment,configmaps,events,nodes,namespaces. It reads; what changes the cluster iswrite_create,write_patch,write_deleteandwrite_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 toapi.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 onnow(). 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) -> Textandhmac_sha256_chain(key, messages). The result is not a Secret, so the call needs thedeclassifyeffect and grant, the audit lists it undersecretswith the reasonhmac 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 thedeclassifygrant can MAC under a weak key it derived from a strong one - which is no more thandeclassifyalready 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 makeneta seconddeclassifythat no audit names. stdlib/rest.velis what the four needed thathttp.vellacked: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 andhttp.velis untouched: the first draft added these tohttp.vel, and a program that importshttp.velwithout a name and defines its ownitemsthen 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.velandgithub.velimport nothing, because an audit reads every function a program loads andhttp.vel's take any URL. - Each has an example under
examples/ops/-azure_groups.vel(resource groups and tag drift),k8s_pods.vel,github_issues.vel,aws_buckets.vel- a line on the Library page, and a test incheck_batteries.py, which runs on every leg against a stand-in server in the suite's own process: the request goes to the real host's name over TLS, under the real host's grant, and only where that name connects to is changed (tests/standin/, a certificate nothing else trusts).
The ffi count over examples/ (velaris stats --ffi examples): at 8.4.0,
106 programs, 8 of which call Python; at 8.5.0, 112 programs, 8 of which
call Python. The six new programs - the four under examples/ops/ and the
two under examples/runner/ - call none, and the audit of each shows no
ffi effect and no module. The eight are the ones that were there:
database.vel, edges.vel, ffi.vel, json_ffi.vel, report_fixes.vel,
sandbox.vel, stdlib_tools.vel and stress.vel, which exist to show
ffi, db.vel and dates.vel; none of them was rewritten.
Viewers #
velaris receipt show <file> and velaris audit <file> --html write a page:
what was read, written and fetched - by grant, with counts - which secrets
were declassified and why, what was refused and where, the confinement
level, the wall time, the subjects. Plain HTML with the documentation site's
stylesheet inside it; no script, nothing fetched, every value escaped;
--text for the terminal, with control characters written as escapes. The
same input gives the same bytes on every system (tests/viewers/).
To say which host, a receipt had to know, and a receipt holds no value the
program handled. So grants_used counts what each grant let through, by
the grant's own text - net:management.azure.com:443 three times - which is
the operator's and not the program's.
The runner, first cut #
velaris run program.vel --tools manifest.json. The manifest
(velaris.tools/1) declares tools by name, a JSON Schema for each one's
arguments, which results are secret, a cost, and a ceiling in calls and in
the host's own cost unit. The budget grants them as it grants anything:
tool, tool:search@20, tool:send_email:to=*@corp.com. A call goes
through a door to the host - JSON lines on standard input and output now; an
HTTP door later - pauses the run, and resumes with the result, which is a
Secret of Text when the manifest says so. Untrusted arrives in 9.0, and
the documents say so where it matters. Receipts record every call site, the
patterns that held its arguments and the ceiling; the audit lists tool
like any effect, and the tools a program names. examples/runner/ is a host
in Python offering search and send_email, and a program that is refused
(E321) when it mails outside the allowed domain, before the host hears of
it. velaris skill verify <dir> reads a skill's programs and manifest and
reports the tools and the budget it would need. There is no framework
adapter; docs/runner.md is the whole protocol, and who trusts whom.
The adversarial pass #
Kept as tests, so that each stays tried.
- An argument that escapes its constraint (
check_runner.py, fourteen ways againstto=*@corp.com). The first matcher was a glob, and a glob star matcheseve@evil.example, ann@corp.com. The rule that shipped: a pattern is matched against the whole value, nothing is trimmed or folded, and*never stands for the literal that follows it in the pattern, a separator (, ; < > " ' \), white space, a control or format character, or across..; a list matches when every item does; a held argument that is left out is refused, since the host's default is not the operator's pattern; and an argument the schema does not name is refused, since what nobody described nobody constrained. - A ceiling exceeded: five of them -
tool:NAME@N,tool@N, the manifest's calls, its cost, and a cost the host reports mid-run. - A host that lies: another call's id, a Bool for an id, a line that is
not JSON, a result and an error, neither, a negative cost to win budget
back, a cost that is not a number, NaN, a closed door, silence. Each is
E324 and the program does not go on. A reply's other fields change
nothing: a result is a
Textand never a grant. - A result that steers a host or a path: it cannot leave the budget (the
suite has a tool return a URL outside
net:, which is E314), and inside the budget it can. That is the 9.0Untrustedcase and is written down as open in THREAT_MODEL.md, not fixed. hmac_sha256: a key that reaches output other than as a MAC (check_digests.py). Sixteen routes - printed, logged, written, as a URL, as a tool's arguments, encoded first, through a list, a map,format,json_of, a loop overchars, as the message of another MAC - none compiles. One thing was changed for it: a call site that signs under many keys names sixteen fingerprints in a receipt and then saysmany, so a loop over keys derived from a secret cannot use the receipt as a channel. The limit above - a weak key derived from a strong one - is stated, not closed.velaris demoturned on a real.env(check_demo.py): run from a directory holding a.envwith a value only the suite knows, with seven argument forms, a proxy in the environment and the temporary directory pointed at the victim's. The value appears nowhere, nothing connects anywhere, and the directory is as it was.- A receipt somebody else wrote, shown as a page: markup in any value is text, and an escape sequence is written out, not sent to the terminal.
Known open #
- A tool's result is not marked as the host's words (
Untrusted, 9.0). - The pattern rule is conservative:
*@corp.comdoes not matchAnn@Corp.com, and/data/*.txtdoes not match/data/a.b.txt. k8s.velverifies TLS against the machine's trust store; a cluster with its own CA needsSSL_CERT_FILEset where the run starts. There is no switch that turns verification off, and no way yet to name a CA per run.aws.velandk8s.veltake their host from the caller, so an audit says "a host built while running" for them and the operator names the grant.call_retryingdoes not pause between attempts.- A named import still renames a library's parameters that share a name
with one of its functions;
http.velavoids the names. 9.0. - S3 and STS answer in XML, and
aws.velreads values out by tag. embedding.htmlandthreat-model.htmlare within a few hundred bytes of the site's 100,000-byte page budget. The runner's protocol and the viewers moved todocs/runner.mdfor that reason; the next addition to either document has to move text out as well.
Housekeeping #
build_docs.pyhashes and copies line-feed bytes (lf_bytes): the digest on the receipt page,site.css,site.js,llms.txtand the playground are the same bytes from a Windows checkout and from a runner, so the release's own rebuild ofdocs/no longer touches that page.velaris/site.cssis the site's stylesheet inside the package, for the viewers;check_viewers.pyholds it tosite/site.css.- velaris-spec 0.13.0: the
tooleffect and its grants (sections 3.1, 4.1 and 5.6), the URL-prefix rule (9.3), receiptgrants_used,tool_calls,tool_ceilingandkey_fingerprint(8.7), the audit'stoolsand the hmac declassification (8.6), andvelaris.tools/1(8.10, provisional). - velaris-kit, a
template repository: the Azure script, a committed
velaris.capabilities, the Action in a workflow, and an emptyFRICTION.md.
Measured #
Measured by perf_gates.py --against v8.4.0 on Windows 11 (10.0.26200,
AMD64, 16 CPUs), Python 3.13.13, z3-solver 5.1.0 and llvmlite 0.49.0: medians
of 5 runs after one warm-up. The machine was not idle: 17% busy when it
began, and this release's other suites ran beside the later measurements, so
every figure here is higher than 8.4.0's table for that reason and not for a
change in the code it measures. The comparison against v8.4.0 runs both
versions in alternation under the same load, and is the figure to read; the
release workflow repeats it on a runner that does nothing else, and fails
the release past +25%.
| Measure | 8.5.0 |
|---|---|
Cold start, velaris --version | 257 ms |
Cold start, velaris check of a one-line file | 531 ms |
| Check, per 1,000 lines (a 1,013- and a 10,013-line program) | 1.11 s and 1.33 s; 0.07 s and 0.07 s without proofs |
| Proof time per example with contracts, p50 / p95 | 23 ms / 488 ms, over 56 files |
Native code on examples/bench.vel: compile, and llvmlite's import | 90 ms, and 78 ms; burn compiled |
examples/bench.vel, native / --no-native | 6.76 s / 16.46 s, 2.44 times faster, 9.71 s saved |
--lite build | there is none |
| Pool worker's memory, after 1 run and after 1,000 more | 26.6 MB, 27.6 MB |
z3 or llvmlite imported by velaris --version, or by check of a program with no promise | neither |
| Importing z3 when a command needs it | +170 ms at cold start |
| Importing llvmlite when a command needs it | +173 ms at cold start |
Pure numeric against v8.4.0, native (bench.vel and an integer loop) | 6.76 s against 6.75 s, +0.2% (the gate allows +25%) |
| Pure numeric against v8.4.0, interpreted | 20.01 s against 18.64 s, +7.3%, measured under the load described above |
velaris demo, start to finish | about 1 s: two runs of the command line and nothing else |
check_differential.py against v8.4.0: none of the 97 examples' outputs
differs, velaris-spec's 456 conformance cases give the same verdicts, and
the quick benchmark's 15 programs the same verdicts.