Changelog: 2.x: 2.63.1 to 2.40.1

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

2.63.1 - The memory cap claim, narrowed to where it holds #

The tests workflow had failed on every macos-latest leg since 2.62, in check_library.py: "a memory cap STOPS a program that eats memory". The cap is RLIMIT_AS, and macOS treats that limit as best-effort - the doubling program ran to the 60 second timeout (E610) instead of being stopped at 150 MB (E611). Linux honours the limit; Windows has no equivalent and was already skipped. The CrewAI tool's test had been narrowed to Linux for the same reason.

The assertion now runs on Linux only, unchanged there; macOS prints a skip line saying why, Windows keeps its skip. Every place that stated the platform truth says the same thing now - EMBEDDING.md, THREAT_MODEL.md, COMPLIANCE.md, SECURITY.md, the MCP tool description, the run() docstring (a comment-only change, the only edit to the compiler), the benchmark README and the header the harness writes: enforced on Linux, best-effort on macOS, not applied on Windows; the timeout is enforced everywhere. Neither check_termination.py nor the benchmark harness asserts a memory-cap outcome, so nothing else needed narrowing.

2.63 - What a security reviewer looks for #

Nothing in the compiler changed. Six pieces for the person who has to decide whether agent-written Velaris may run on a machine they answer for.

THREAT_MODEL.md. The trust boundary (the operator sets the budget, the program is untrusted, the compiler and the granted ffi modules are trusted in full), what is defended against with the mechanism and the suite that tests each, and what is explicitly not: anything a granted module does, side channels, use below the limits, request volume within net, logic errors with no contract, the meaning of text, code not written in Velaris, the memory cap on Windows, a tampered compiler. Two items that were not in any list before: io includes env(), so an io-only program can read and print the environment; and fs has no path list. Each residual risk has a recommendation. The benchmark numbers are cited; the misses are named.

COMPLIANCE.md. One row per guarantee against the OWASP Top 10 for LLM Applications (2025) and NIST AI RMF functions - mechanism, framework item, suite, what it does not cover. Nearly every cell says "partially addresses", because that is the truth; the items Velaris does nothing for are listed by name.

Signed releases with an SBOM. release.yml now signs the wheel and sdist through sigstore, the three executables and velaris.mcpb through cosign, attaches the bundles, signatures and certificates, adds a CycloneDX SBOM and SHA256 checksums, builds the wheel twice under the same SOURCE_DATE_EPOCH and fails if they differ, and publishes to PyPI the same files it signed. Every third-party action is pinned to a commit with the tag beside it. SECURITY.md says how to verify a download, with the exact identity string. None of this could be exercised locally; the v2.63 tag is its first run, and the recap of this release names what to watch.

A standing challenge. SECURITY.md: make Velaris report "proven" for a promise that is false at runtime, or escape --allow io, and you are credited by name in the changelog and in HALL_OF_FAME.md, with the report treated as a security issue and fixed within a week. There is no money. HALL_OF_FAME.md opens with the three model-family reviews of August 2026 and the review bot of September; the changelog never recorded which family produced which review, and the file says so rather than guessing.

A card eval. evals/card_eval.py gives a model LLM.md and five fixed tasks - a CSV total, a grade filter with a proven contract, a sandboxed file read, a JSON path read, a stack calculator using pop and div_or_fail - and checks, audits and runs each answer under --allow io with a 10 s timeout, writing compiled-first-try, ran correctly and proven promises to evals/RESULTS.md. It skips with one line when no key is set, and was not run against any API for this release; the results file holds only the three August reviews, marked as reported rather than reproduced.

PR audit comments. The GitHub Action gains pr-comment: on a pull request it posts one comment with the audit of every changed .vel file - effects, modules, proven share, safe command, warnings - and edits that comment on later runs, found by a hidden marker. Plain curl against the REST API with the job's token; no third-party action. The comment builder was exercised locally against real files, including one that does not compile; the posting itself was not.

2.62 - Loops that provably end, and a corpus built to fool it #

The 2.61 benchmark named three programs Velaris could not catch. Two stay misses, by construction: an off-by-one that stops early instead of reading past the end (no contract, so nothing to refuse), and a program that prints rm -rf build for its caller (the only effect is io, and a harmless warning prints the same words). The third - a loop that ends, slowly - is now shown to end before the program runs.

Termination. Every loop gets one of two verdicts, by a syntactic rule that needs no solver and so answers the same with and without the prover. terminates is claimed for exactly one shape: the condition is, or has as an and conjunct, v < E, v <= E, v > E or v >= E, where E mentions nothing the body assigns and calls only pure functions, and every path through the body moves v by exactly one step toward E, with v assigned nowhere else. Everything else - a step of two, a step on one arm only, a counter reset on some path, a limit the body grows, a flag-only condition, an or - is unshown, whether or not it happens to end. A for loop goes through the same rule rather than being exempted: for i in 0 to length(xs) with a push inside does not end, and the rule says so. SPEC.md section 9.5 states it.

It surfaces in three places. velaris explain prints "loops: 2 terminate, 1 not shown" per function. velaris audit and velaris.audit() gain loops_unshown per function and a warning naming the functions, in schema velaris.audit/1 (added fields, not a change); they also gain contract_coverage, the functions that take or return a List, a Map or a record and promise nothing about it - a coverage note, not a defect. velaris check --strict refuses a loop whose end is not shown with E612; without --strict it is not an error, and the time limit in velaris.run remains the guard.

Stressed before trusted. check_termination.py holds 44 adversarial loops with their required verdicts: the wrong direction, a step of two, a step spelled 1 + i, a reset on one path, a limit the body changes, a limit changed only inside a nested if, length(xs) with a push inside, nested loops where only the inner qualifies, a flag alone, a flag with or, a float counter, the step inside a check on both arms and on one, a return with and without a step, recursion instead of a loop. The analysis was wrong twice on the first attempt, both times in the same direction - refusing a loop that ends: it counted the standard library's loops when a program imported it (a scoping error in the report, fixed by carrying the file), and it did not accept a text literal or a pure builtin such as split inside a limit, so for part in split(line, " ") was unshown and a control program in the benchmark was a false positive. Both are fixed in the analysis, not the tests. No existing example changed proof status (velaris proofs examples --json before and after, diffed). examples/termination.vel and examples/termination_bad.vel join the suite; the latter runs and is refused only by --strict.

The benchmark, doubled. Sixty programs now, thirty of them written against the tools: effects three helpers deep or inside a record, a division guarded on one path and not the other, an off-by-one only on empty input, an overflow inside a record field and inside a map, a failure ignored inside an inline function, a loop that ends only when input says so, growth by repeated text concatenation, subprocess reached through the JSON-shaped call and through a handle, and control programs that look suspicious - printing "rm -rf", reading their own arguments, importing math in a loop - and are harmless. Same three languages, same rules. On the machine that produced RESULTS.md (Windows, prover present, Deno 2.9.6): of 53 dangerous programs Velaris caught 51 - 41 before running, 10 while running - and missed the two above; Deno caught 29 (5 before, by its lint on a while (true)) and Python 28; no tool flagged any of the 7 control programs, the slow loop among them. Ten consecutive runs produce identical output. What the doubling found: the prover does not flag a division on an unguarded path when another path guards it, a remainder inside a loop, or a get(xs, i + 1) - all three are caught while running, not before, and the table says so.

args(). Under --allow io the program's args() used to contain --allow and io. It no longer contains --allow, --deny, --timeout or their values, from the command line or from velaris.run; check_sandbox.py has the case.

2.61 - A table anyone can rerun #

Every claim this project makes about catching what a model writes has been a claim. benchmark/ turns it into a table that one command regenerates: python benchmark/run.py. Thirty programs in ten categories - a file write hidden in a helper, a network call hidden in a helper, division by input, an off-by-one read, integer overflow, an ignored failure, an infinite loop, runaway memory, reaching subprocess or os.system, and three correct programs that must not be flagged - each written three times with the same behaviour, in Velaris, in JavaScript for Deno and in plain Python. The harness runs every program through check + audit + run under the budget the task needs (io, plus ffi:math for one control program, with timeout 5 and max_memory_mb 256), through deno run --no-prompt with no flags, and through a Python subprocess with the same timeout, and records caught-before-run, caught-during-run, missed, not-applicable, false-positive or tool-absent, with the evidence in the cell.

On the machine that produced the committed RESULTS.md (Windows, prover present, Deno 2.9.6): of 27 dangerous programs Velaris caught 24 - 15 before running and 9 while running - and missed 3; Deno caught 13 and Python 13; no tool flagged a control program. The three misses are in the corpus on purpose and are named in the results: an off-by-one that stops early instead of reading past the end (no contract, so nothing to refuse), a slow but finite loop (ends before the deadline), and a program that prints rm -rf build for its caller (the only effect is io). Deno's no-unreachable lint flags the three memory-growth programs before running, where Velaris only stops them while running; and on Windows it stops them with the timeout, not the memory cap, because the cap is not enforced there and the interpreter allocates slowly. Both are in the table.

Two things learned while building it. Under --allow, args() hands the budget words to the program as well (['--allow', 'io', ...]), so the corpus reads its input from stdin; that is a compiler bug to fix in its own release, not here. And a Deno permission denial is an ordinary exception, so a fetch inside try/catch exits 0 - the harness had to watch the socket rather than trust the exit status. A Velaris refusal cannot be caught by the program, which is the difference the benchmark exists to show.

benchmark/README.md has the rules and the exact commands so a stranger can rerun it and dispute a row. CI runs run.py --quick --check on the legs with the prover, with Deno absent there; a verdict that changes between compiler versions fails the build and names the row.

2.60 - The ffi cliff becomes a permission #

Every review of this project, from three model families and one automated reviewer, raised the same caveat: allow ffi grants everything Python can do. That was true, and it was the sentence a security reviewer would stop reading at.

The budget can now name modules. --allow io,ffi:math,json grants the ffi effect for those top-level packages only; anything else is refused with E311, and the message names the exact flag that would permit it. Plain ffi still grants every module, for programs whose author you trust. The library takes the same form: run(source, allow={"io", "ffi:math"}), and refused_effect reports "ffi:os" when that is what was reached for.

The audit reads the modules a program names in its py* calls and reports them as ffi_modules; its safe_command grants exactly those. A reviewer no longer has to choose between "no Python" and "all of Python".

Four ways around it were tried and refused, in check_sandbox.py: a module outside the list, a submodule path (os.path), the same module through py_json, and through a handle via py_new. All three FFI import sites go through one gate, and the bounded child process receives the same list. An allowed module still works.

2.59 - Time and memory limits, prompted by a review bot #

The CrewAI pull request's automated reviewer flagged what three human reviews had also noted and this project kept deferring: the effect budget bounds what a program may touch, but nothing bounded how long it could run or how much memory it could take. For an agent framework calling run in a loop, that is the first thing that goes wrong.

velaris.run(source, allow={"io"}, timeout=30, max_memory_mb=512). With either limit set the program runs in a separate, killable process. A program that never ends is stopped at the deadline (E610, timed_out=True); one that eats memory is stopped at the cap (E611, out_of_memory=True, caught in 0.4 seconds in the test). The effect budget still holds inside that child - verified - and an honest program is unaffected.

Memory caps use the OS address-space limit, so they apply on Linux and macOS; on Windows the timeout applies and the cap is recorded but not enforced, which the docs say plainly rather than implying otherwise.

The MCP server and the HTTP door now default to 30 seconds and 512 MB. The CrewAI tool does too, reports STOPPED with the limit it hit, and gained the assertion the reviewer asked for: a refused effect must not reach the program's own fail branch either.

Attribution, added in 3.2 from the public record: the reviewer was CodeRabbit (coderabbitai[bot]), on crewAIInc/crewAI#7279 at 2026-09-05 06:56 UTC, under the heading "Denial of Service (CWE-400): Uncontrolled Resource Consumption"; the fail-branch assertion answers a second finding in the same review.

2.58 - Ready to submit to the frameworks #

Three integrations in integrations/, each written to the target's own conventions and each with tests that assert the effect budget holds through the framework's tool interface - because a budget that leaks one layer up would be the worst kind of promise.

CrewAI (crewai/): VelarisAuditTool and VelarisRunTool(allow= ["io"]), five tests, a README, and the pull-request text ready to paste. crewai-tools accepts community tools; this goes first.

LangChain (langchain_velaris/): a partner package, langchain-velaris, since LangChain lists packages rather than merging tools. Verified through .invoke() that a program granted only io is refused fs.

MCP registry (mcp_registry/): the server.json for registry.modelcontextprotocol.io, which every MCP client reads. A form rather than a PR, and the highest reach of the three.

integrations/README.md says what to submit, where, in what order, and what makes a maintainer say yes: a test that runs in their CI, a description of the problem rather than the product, no marketing words, and fast replies to review.

2.57 - --strict, from a question on r/Compilers #

Someone asked whether users could choose between strict and flexible proof modes rather than having leniency imposed on them. They were right, and half the answer already existed - velaris proofs --min 80 holds a line across a project - but the compiler itself always accepted a promise that fell back to a runtime check.

velaris check program.vel --strict refuses when any promise could not be proven, and names them:

examples/wordcount.vel: 2 promise(s) could not be proven, and
--strict does not accept runtime checks:
  bar
      needs    biggest > 0
  report
      needs    top > 0

With no prover installed it refuses rather than pretending - a strict check that silently proves nothing would be the worst of both.

The default stays lenient because the solver is optional and strict-by-default would mean the language does not run for anyone who has not installed z3. That is an argument about the default, not a reason the flag should not exist.

2.56 - Seamless means tested, not claimed #

Three gaps between "the door exists" and "the door works".

The Jupyter magic was never installed. velaris_magic.py was not in the wheel, so %load_ext velaris_magic worked in the repository and failed for everyone who installed from PyPI. Found by checking from outside the repo rather than inside it - the difference between a door that opens and a door that appears to.

One shape for problems. audit() returned dicts while check() and run() returned objects, so callers - including this project's own Jupyter magic - had to handle both. Now everything returns Problem objects and as_dict() flattens them for JSON. The magic got simpler by six lines, which is what an API fix should look like.

The version guard covers every version. It watched velaris.py, pyproject.toml and the VS Code extension, but not the npm package or the .mcpb manifest - either could have shipped claiming a version the compiler never had. Both are guarded now.

check_library.py grew a section that asserts every door works after a real install: all four modules importable, both APIs reporting the same shape, the npm version following the compiler, the hooks present. 39 checks with the prover, 38 without, and rule 6 was followed - the no-prover run happened before this was written down.

2.55 - Four more doors #

Velaris was reachable from a terminal, Python, MCP, CI, Docker and HTTP. Four populations were still locked out.

npm. npx velaris-lang script.vel --allow io, plus a real library with TypeScript types: audit(source) and run(source, {allow: ["io"]}) from Node. Verified through Node that a program granted only io is still refused fs - the same guarantee, one process further away. The compiler stays a Python package; the wrapper says so plainly when it is missing instead of failing with a spawn error.

Jupyter. %%velaris --audit --allow io runs a cell in a box and prints what it can touch and how much is proven first. When an effect is refused it names the flag that would permit it. The natural home for the finance and measurement work where proven contracts earn their keep.

pre-commit. Three hooks - velaris-check, velaris-fmt, velaris-proofs - so a repository can require that its Velaris compiles, is formatted, and keeps its proven share above a threshold.

Homebrew and winget manifests in packaging/, both with tests that assert the effect budget still holds in a packaged build. They need a tap and a pull request respectively, which is paperwork rather than code, and the files say exactly what to do.

Building the Jupyter magic surfaced a wart in the library: audit() returns problems as dicts while run() returns them as objects. The magic handles both; the API should not need it, and that is worth straightening when the format version next moves.

2.54 - A door for languages that are not Python #

Velaris was reachable from a terminal, from Python, from an MCP client and from CI. Everything else - a Node service, a Go tool, a Rust agent, a shell script - was locked out.

velaris serve opens a local HTTP door with the same three calls: POST /check, POST /audit, POST /run, plus GET /card and GET /health. Same library underneath, so the same guarantees.

Two ceilings, both enforced. The allow in a request is the program's budget. --max-allow is the server's own limit - a caller asking for ffi on a server started with --max-allow io,fs gets 403 and is told what it does grant. Verified both ways in check_library.py, which now drives a real server on a real port.

It binds to localhost unless told otherwise, warns when it is not, and warns when ffi is grantable - because this endpoint runs programs and that should be said out loud rather than buried.

ARCHITECTURE.md gained a table of what each suite is for, and a sixth rule: run every new suite without the prover BEFORE wiring it into CI. That mistake has now been made three times; this release is the first where the rule was followed rather than learned again.

2.53.1 - The library suite knows what needs the prover #

Three of the 25 checks in check_library.py are about proofs - what was proven, a refuted promise, a 100% proven share - and the no-solver CI legs have no prover, so every minimal leg failed the moment the suite joined CI. The same mistake as 2.39.1, in a new suite.

They are now conditional, and without the prover the suite asserts the fallback instead: that a false promise breaks while running (E600 or E601) and that the audit reports nothing proven. That is a stronger test than skipping, because it checks the degraded path rather than ignoring it.

25 with the prover, 24 with the fallback. Both green.

2.53 - Setting it up should not be a chore #

The MCP server worked; getting it into an assistant meant finding a Python path and editing JSON. Two ways to skip that.

velaris mcp-install finds every MCP client on the machine - Claude Code, Cline, Cursor, Windsurf, Continue, Zed - and adds a velaris server to each, using the Python that is running it. It never disturbs what is already there: tested against a config holding another server with its own env block and an unrelated top-level key, both of which survived, and every file is backed up before writing. --list shows what it found without touching anything, --remove undoes it.

velaris.mcpb is the double-click bundle, 94 KB, with the compiler and standard library inside it - newer Claude Desktop builds only accept remote connectors in the add-connector dialog, so a local server has to arrive as a bundle. Verified by extracting it somewhere with no Velaris installed, driving it as a client would, and watching the sandbox still refuse fs to a program granted only io. It is built and attached to every release automatically.

The bundled server now finds the compiler whether it was pip-installed, vendored beside it, or sitting in the repo next door - a user's own install still wins.

2.52 - Velaris from inside other programs #

The effect budget is the idea most easily copied out of this project. The way to make copying pointless is to make importing cheaper - so Velaris is now a library, a documented format, and an MCP server, as well as a command.

The library. velaris.check(source), velaris.audit(source), velaris.run(source, allow={"io"}) and velaris.card(). run captures stdout and stderr, accepts stdin and args, reports which effect was refused, and restores the previous budget afterwards so a process can audit and run many programs. The guarantee is identical to the command line: a refused effect stops the program and cannot be caught by it.

A versioned format. audit().as_dict() is velaris.audit/1: effects, per-function contracts with proven-or-runtime status, the proven share, the safe command, and warnings - including that ffi cannot be contained by a budget. Documented field by field in EMBEDDING.md, with a stated compatibility rule. Formats outlive the tools that produce them.

An MCP server. velaris_mcp.py offers velaris_card, velaris_check, velaris_audit and velaris_run over the Model Context Protocol, so an assistant can write Velaris, check it, see what it touches and run it in a box without leaving the conversation. velaris_run defaults to allow: ["io"] - the least that is useful.

check_library.py proves the library and the server keep the same promises as the command: 25 checks, including that a program refused fs does not carry on, that budgets are restored between runs, and that a refusal through MCP is reported as such. In CI on every push.

2.51 - Smaller per-call costs, and an honest note about the ceiling #

Two more measured savings on the interpreted path, both verified against every suite and the fuzzer.

The evaluator and statement runner compared node types with isinstance, which walks a class hierarchy; the AST dataclasses have no subclasses, so 22 of those became pointer comparisons. And a function with no requires or ensures was copying its entire scope on every call to snapshot values for promises it does not have.

Interpreted record work is now 1073ms where it was 1314ms at the start of this run - about 18% - on top of startup halving in 2.48.

The honest ceiling: the remaining cost is the sheer number of evaluator calls, roughly 580,000 for that benchmark. Removing it needs the AST compiled to closures or bytecode, which is a rewrite of the execution core rather than an optimisation of it. Native compilation for records has the same character - it is the LLVM struct ABI work that already caused a Windows-only bug once. Both are worth doing and neither is worth starting at the end of a long session; they need a plan, a branch, and the fuzzer running between every step.

2.50 - Function values carry their surroundings #

Two reviewing models named the no-capture rule as a real expressiveness cost, and they were right: writing fn(n: Int) -> Bool { return n > limit } meant hand-writing a loop instead. Inline functions now capture by value.

The values are copied when the function value is made, so later assignment to those locals cannot change what the function sees - examples/lambda_capture.vel demonstrates a captured cutoff staying 2 after the local is set to 99. There are no reference cells, so a function value can never observe a change it was not handed.

What did not change, verified: a capturing inline function that tries to print is still rejected (E300 - effects cannot be smuggled past a signature); a false promise on one is still caught while running (E601); a name that exists nowhere is still E402. The prover treats captured values as unknown, which is the conservative direction.

examples/lambda_bad.vel was the test asserting capture is an error. It is now examples/lambda_capture.vel and asserts the opposite - the right way for a language to record a change of mind.

2.49 - The card's gaps were hiding three real bugs #

A model reviewed LLM.md without a compiler and reported five things the card never explained. Writing them down meant testing them first, and three turned out to be defects rather than omissions.

Deep recursion crashed. Past about 300 frames a program died with a Python RecursionError traceback. Velaris now stops at 2000 frames with E609 and says the recursion looks like it never ends - and Python's own ceiling is lifted so that ours is the one that fires.

write_file crashed on any OS failure. An unwritable path threw a raw traceback. It is now E608 with the reason from the operating system. It stays non-catchable by design - a program that cannot write where it was told to should stop - but it stops as a Velaris error.

A dead write_file branch sat unreachable in the interpreter, left from an earlier edit.

Two card claims were simply wrong. Recursion works, carries contracts, and is checked at call sites - the card never mentioned it, so a reviewing model refused to use it. And invariant works on for loops as well as while; the card documented only while. examples/recursion.vel proves three contracts across both.

Handle lifecycle, tested and written down: double close is a no-op, use after close fails catchably, handles copy by reference.

Full module signatures for http, db, dates, csv, log and env_tools - every parameter type, every return type, which functions can fail, which carry proven contracts. Guessing these was the commonest source of wasted attempts for a model with no compiler.

2.48 - Speed, without touching a single guarantee #

Three measured wins, none of which changes what the language promises.

Startup halved: 133ms to 67ms. Every run - including every hello world - was importing z3 (about 350ms of the cold cost) whether or not anything needed proving. The prover is now located rather than imported at startup, and check_proofs returns immediately when no function carries a contract, no division or list read creates an obligation, and no callee has a promise to satisfy. Programs that do need proofs pay exactly what they paid before; the counterexamples in avg_bad, offbyone_bad and conj_bad still appear.

Interpreted work is faster. sorted() was running on every single builtin call to check the effect budget - now precomputed once. length, get and push sat behind thirty string comparisons and two module imports - now first, with the bounds guard intact. The evaluator and statement runner dispatch the hottest node classes directly instead of walking an isinstance chain: 5.8 million isinstance calls became 3.8 million on a record-heavy benchmark, and that benchmark went from 1314ms to 1139ms.

Measured, not claimed: a 3-million-iteration loop on the native path runs in about 80ms against Python's 445ms for the same loop. The fuzzer confirms both engines still agree exactly on 30 random programs, and all 89 examples, 25 fallible builtins, 15 sandbox cases and both stress suites pass unchanged.

2.47 - The periphery round #

A third adversarial pass executed everything the card mentions - every builtin, all seven modules against live systems, every error code - and held the score at 88 while finding the roughness had moved from the core to the edges. All five findings, fixed:

Division joins the catchable family. A zero divisor from user input was the one remaining way to kill a checked program: E403 stops the process and no check sees it. div_or_fail and mod_or_fail fail the normal way, for exactly the input-driven case; plain / and % stay strict for divisors the code controls. The card says which to use when.

The http envelope is a record. call returned Text and get returned Text, so feeding a raw body to code_of compiled and died at runtime with a misleading JSON error. call now returns an Answer record (status, body, raw); code_of and body_of read fields and cannot fail; the wrong pairing is a type error. linkcheck got simpler for it. Writing this found a genuine language subtlety: a local named status shadowed the module's status function and produced a confusing E530 - renamed, and worth remembering.

log.die says what it does. fail_with logged and killed the process - correct behaviour, wrong name in a language where "fail" means catchable. die is the new name; fail_with remains as an alias so nothing breaks.

velaris check treats a library as a library. Requiring main at check time (v2.44) was too broad: velaris check stdlib/http.vel is a legitimate thing to do. A missing main is now only an error for the file being run - which the runtime already enforced.

The card grew the last empirical truths: E525 (binding a void-returning fallible call), sort_by keys are Int, the _or_fail guidance, the Answer record, and log.die's semantics.

Attribution, added in 3.2 from the maintainer's account: the third pass was by the Claude model whose review is 2.44.

2.46 - Contents, not just lengths #

Two additions, both from the adversarial rubric's remaining points.

map_to(xs, f) - projection that changes type, fn(T) -> R, so a record becomes one of its fields in one call instead of a hand-written loop. The generics system supported two type variables all along; nobody had written the function. Its ensures length(result) == length(xs) proves.

Quantified contents prove through loops. ensures all_of(result, is_positive) on a filtering loop was runtime-only; now the inference harvests each all_of predicate from the function's own ensures and tries "everything pushed so far satisfies it" as an invariant. Entry is vacuous, each push must satisfy it on its path, and the promise follows. The unguarded version correctly does NOT prove - the candidate is dropped when a step can break it - and the runtime check catches it with the actual offending list. Sound in both directions, and the suite's wall time did not move.

Attribution, added in 3.2 from the maintainer's account: the rubric is that of the Claude model's review in 2.44.

2.45 - The road from 84 #

Three of the four items that separate this language from the low 90s, by its own adversarial grading.

The v2.42 mistake cannot recur. check_fallible.py reads FALLIBLE_BUILTINS from the compiler itself, generates an ignore-the-failure program for every member, and asserts each is refused with E520 - then a caught-failure program for each, asserting the failure formats and never escapes as a traceback. 23 builtins, all enforced, in CI on every push. A fallible builtin added without enforcement now fails the build by construction.

The prover reads record fields through lists. A List of Row is modelled as one Int array per provable field, so get(rows, i).amount is a real array read: the off-by-one over a record list - the adversarial report's exact deferral - is refused before running (E705), and ensures result >= 0 on a total over record amounts is proven, which was flatly impossible before. Building this introduced a truthiness bug on a Z3 array (or on an array is not a None-check) that silently un-refuted a v2.38 regression test; the refusal harness caught it within the same session, which is the layered suites doing exactly their job.

The break question has an answer in writing. SPEC.md §13a: no break, because the prover's exit knowledge - "the condition is false" - is what pins counters at boundaries and proves loop promises; a break turns that into a disjunction over hidden paths and abandons most loop proofs. The supported idiom is the exit in the loop test (while i < n and not found), which the prover can see, and the card now teaches it with the reasoning. The decision names the condition under which it would be revisited.

The fourth item is not code: another adversarial round, finding less.

Attribution, added in 3.2 from the maintainer's account: the grading is the second pass of the Claude model's review in 2.44.

2.44 - Everything the adversarial report found #

A model ran 86 adversarial artifacts against 2.43 - one production program, 34 broken fragments, 52 single-point mutations - and scored the language 76/100 with a list of defects. All of them are fixed.

The soundness hole (critical). pop, slice and set_at were documented fallible but the checker never demanded handling, so a clean velaris check could be followed by a raw Python traceback at runtime. The list-operations type check returned before the fallibility check ran. They now require check or try like every other fallible call (E520).

The checker cannot crash. An unknown parameter type escaped as a Python traceback instead of E500, breaking --json consumers and any automated fix loop. Every checker pass now reports instead of raising.

main is validated at check time. No main at all (E400), a main with parameters (E401), and a main marked or fail (E523, new) are all compile-time findings now, not runtime surprises.

The typed FFI carries numbers. py_float("math", "sqrt", ["16"]) sent Python the string "16" and failed. Arguments that read as numbers are now passed as numbers, with an all-strings retry so functions genuinely wanting text still get it.

Conjunctions stop masking. requires divisor > 0 and length(items) > 0 over a record list dropped the WHOLE clause when one conjunct could not translate - the checkable divisor > 0 included. Conjunctions are now split and each part checked on its own, and record lists carry a modelled length even where their contents cannot be seen. The report's exact shape is rejected at the call site with a counterexample.

The card grew fifteen truths the reviewer had to discover by experiment: % exists, random(n) is 0..n-1, random(0) is E405, record fields go one per line, oversized literals are accepted but arithmetic is checked, unused effects are viral, time needs ffi and can fail, apply_to_each maps T to T only, the --allow/--deny budget flags, velaris proofs --detail, and codes E400 E405 E509 E513 E521 E523 E542 E602 E704 - plus the E506/E507 correction (E507 is about duplicate records, not empty maps).

Attribution, added in 3.2 from the maintainer's account: the reviewing model was a Claude model, and the same review's later passes are behind 2.45, 2.46 and 2.47.

2.43 - The prover crosses the loop boundary #

The sharpest finding in the last review was that the prover went blind the moment a loop touched a list: a promise like ensures length(result) == length(xs) - 1 would not prove even with a hand-written invariant, and the textbook off-by-one while i <= length(xs) { get(xs, i) } was caught only at runtime. Both are fixed.

Two invariants were missing. A counter walking toward a limit stops at the limit - without that, the state after a loop only says i >= limit, so "the loop ran exactly that many times" could never follow. And a list built one item per turn has exactly as many items as the counter has turns. Both are inferred automatically now; the promises in examples/loop_lists.vel prove with no invariant written at all. The proven share across the examples went from 60% to 64%.

The off-by-one is refused before running. Reporting a bug about a loop's index used to be unsound, because the index inside a loop stands for any state the invariants allow. The sound route is the loop's last real turn: a counter that starts inside the limit and steps by exactly one takes every value up to the largest the condition allows, so that turn genuinely happens and a read on it is a genuine read. examples/offbyone_bad.vel is rejected with the position and the length. Correct loops - i < length(xs), guarded reads, and counting backwards - are unaffected, which was checked before anything shipped.

2.42 - Findings from a model that installed it and tried to break it #

A third model read velaris card, installed the language, wrote a 30-function calculator that compiled and ran correctly first try, then spent its time attacking it. Nearly everything it reported was true.

Lists can shrink. pop, slice and set_at, all fallible, all returning new lists. A stack machine - the natural shape for a calculator - previously required rebuilding the whole list one element shorter for every pop. examples/stack.vel is that program.

Overflow can be caught. a * b that outgrows 64 bits is still E407, which stops the program and no check can catch - correct for a bug, wrong when the numbers come from a user. add_or_fail, sub_or_fail and mul_or_fail fail in the normal way instead.

break says something true. It used to report "unknown variable 'break'" and suggest declaring one. It now says the language has no break, and suggests keeping a flag.

The formatter matches the documentation. requires, ensures and invariant were being flattened to the margin, contradicting the style in Velaris's own docs. Every shipped file is reformatted.

The card states the ceiling. The sharpest finding was that the prover goes blind when a loop mutates a list: ensures length(result) == length(xs) - 1 will not prove even with an invariant, and while i <= length(xs) { get(xs, i) } is caught at runtime rather than before. That limit is real and unfixed; LLM.md now says so, along with the overflow rule and the absence of break.

Left as-is, deliberately: the ffi escape hatch is total, and velaris audit already says so unprompted - which the model noted approvingly.

Attribution, added in 3.2 from the maintainer's account: the model was a Claude model.

2.41.2 - A loop no longer hides a divide by zero #

A second model read velaris card, wrote an expense report, then deliberately removed a requires length(items) > 0 guard and predicted the compiler would catch the division. It did not.

The cause: the divide-by-zero proof skipped itself whenever any condition on the path mentioned a value a loop had made unknown. Since almost every average sums in a loop before dividing, the check was hiding exactly where it was needed. The divisor itself was perfectly knowable the whole time.

Now the divisor is judged on its own terms and loop conditions stay in the solver rather than cancelling the proof - dropping them would have invented counterexamples, keeping them costs nothing. examples/avg_bad.vel is the shape, rejected before running.

Still runtime-checked: dividing by the length of a list of records, because the prover cannot model those at all. That limit is real and documented; this release fixes the case where the limit was being claimed falsely.

Two models, two programs, two real defects found in one evening. The card is doing what it was built for.

Attribution, added in 3.2 from the maintainer's account: the model was a ChatGPT model (the one in 2.41.1 was a Gemini model).

2.41.1 - The card worked, and the first program it produced found a bug #

Pasting velaris card into a model that had never heard of Velaris produced a correct program on the first attempt - and that program crashed the prover. Pushing a record onto a list inside a check inside a loop reached a comparison that assumed every value has a Z3 sort. Records do not. The rule was already right (a list of records cannot be modelled, so abandon the proof and let the runtime check); the translator simply asked the question in a way that crashed instead of answering it.

examples/rec_push.vel is that program, kept as a regression test.

Worth recording plainly: the card's first user found a real defect within minutes, which is exactly why it was worth building.

Attribution, added in 3.2 from the maintainer's account: the model was a Gemini model.

2.41 - Written by a model, audited by you, run in a box #

Three pieces that make one story.

velaris card prints LLM.md - about 1,500 words containing the whole language, the ten rules models actually get wrong, every builtin with its effects and whether it can fail, the error table, and a complete program to imitate. Paste it into any model and it can write Velaris that compiles. Until now the language's biggest problem with generated code was that no model had heard of it.

velaris audit program.vel answers the reviewer's question rather than the author's: what this program can touch and which functions reach outside, what it promises and how much of that is proven before running versus checked while running, what can fail, and the exact command to run it under a budget. When a program calls Python it says plainly that an effect budget cannot contain that. --json for tooling.

agent_loop.py writes a program with a model and iterates against the compiler: velaris check --json hands back codes, lines and numbered fixes, which go straight back to the model, up to six rounds, then the result is audited. Most agent loops iterate against tests; this one iterates against a proof, which is a stronger signal - the compiler does not say "a test failed", it says which input breaks which promise.

2.40.1 - Leading with the sandbox #

The README now opens with the thing that matters most in 2026: an AI wrote you a script, and you can run it anyway because the runtime refuses whatever you did not allow. The proof story - promises checked before the program runs - follows immediately after, where it reads as the reason to believe the first claim rather than competing with it. New hero image to match, and the limits stated in the same breath as the feature.