Changelog: 4.x: 4.4 to 4.2.1

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

4.4 - A platform that lets its customers write code it can audit #

A minor version. Every program that compiled under 4.3.4 compiles, runs and means the same; nothing is added to the language, the capability surface or any document format. What is added is an example: the pattern a SaaS team would copy to let its own customers write Velaris.

examples/platform/ is that pattern in one file. A small FastAPI service, under 200 lines, with three endpoints. POST /scripts takes a customer's source, audits it, stores it with its capability surface and answers with what it declares - the effects it may perform transitively, the hosts and paths it names, the Python modules it reaches, the most file and network operations one run can make, its proven share, its contracts function by function, and the narrowest budget that would run it. It does not run it. GET /scripts/{id} is that declaration again, as a customer would be shown it before enabling anything. POST /scripts/{id}/run runs it on a velaris.Pool whose budget is the platform's, and answers with the output, or what the budget refused, or which limit stopped it.

A surface wider than the platform permits is refused at submission. The service holds what the audit derived against one budget constant with Budget.covers, which names the first thing that does not fit, and the refusal carries the grants an operator would have to add. A script that reads a file is refused with would_need_granting: ["fs:read"]. A script that builds its host while running is refused too, because the audit cannot read a value the text does not fix and says plain net rather than guessing - where the same program with the host written out is accepted as net:api.example.com. The gate compares what a script may touch and not how much of it: an audit bounds operations only where the text fixes them, and the count is the pool's to hold either way.

The pool does not depend on the gate having been right. They are separate guards, and the example is written so that is visible: the budget is parsed once when the pool is made, pool.run takes no allow argument, each worker installs the budget before the program is read, and a refusal cannot be caught. check_platform.py puts a script straight into the store, past submission entirely, and asserts the run is still refused with E310. A bug in a platform's gate is not a bug in its containment, and that is the property worth copying.

The worked example is the proven discount. Submitting examples/discount.vel answers "proven_share": 100.0 with "status": "proven" on every promise, including the two a platform taking the payment cares about: the discount is never a surcharge, and what is left after it is never negative, for every basket and every rule the types allow. examples/discount_bad.vel - the same rule with one guard deleted - never reaches storage: submission answers E700 with the basket and rule that break it. No sandbox can produce either answer, and it is the answer a platform needs before it offers to enable a rule it did not write.

fastapi is a dependency of the example, never of Velaris. It is not in [project.dependencies] and the wheel does not ship examples/. It joins jsonschema in the [test] extra, which exists so the suites can run, and check_platform.py skips cleanly when it is absent.

velaris with no arguments reports the version it is. It prints the module docstring, whose first line named a version - and that line had said Velaris v2.36 since the docstring was written, so every reader since has been told they were running a compiler two major versions old. The docstring now carries no version of its own and the running version is filled in when it is printed, which cannot go stale. run_tests.py checks that line against VERSION like every other place a version lives, and now checks the MCP registry manifest as well - it carries the version three times, its own and one per package, and all three are published, and until now nothing held them to the compiler.

4.3.4 - The npm wrapper picks the right Python, and says when it cannot #

A patch version. Every program that compiled under 4.3.3 compiles, runs and means the same; nothing is added to the language, the capability surface or any document format. What changes is how the npm package decides which Python holds the compiler, and what it tells you when the one it found is not the one you meant.

The wrapper takes the newest Velaris it finds, not the first. It tries py, python and python3 in that order on Windows, python3 then python elsewhere, and until now it took the first of them that could import velaris at all - whatever version that one held. So an old install earlier in the order silently shadowed a newer one further down, and every run went to the old compiler. That is how npx velaris-lang mcp failed on the maintainer's machine the day 4.3.3 went out. Each candidate is now asked for velaris.VERSION rather than merely whether the import works, and the newest answer wins. velaris.VERSION has been there since 1.0, so every real compiler answers; something importable as velaris that is not one is still used if it is the only candidate, but ranks below every version that can be read, so it cannot shadow a real install by being earlier in the order.

A compiler older than the package is never used silently. If the newest Velaris found is still older than the npm package that invoked it, the wrapper runs it - refusing would help nobody - but first prints one line to stderr naming both versions and the interpreter the compiler came from. The interpreter is the part worth printing: when two Pythons each have a Velaris, knowing which file was imported is the difference between a five-minute fix and a mystery. Nothing else about the run changes, and stdout is untouched, so a script reading the wrapper's output still reads only the compiler's.

A subcommand the compiler is too old to have is named as missing. velaris mcp arrived in 4.3.3. Handed to a compiler older than that, it is not a subcommand at all, so the compiler took it for a file name and said cannot find file 'mcp' - true, and no help to anyone. The wrapper now carries the version each subcommand first shipped in, and when the compiler it found is older than that, it says so instead of handing the command over: which command, which version it arrived in, which interpreter holds which older version. It stops before running, so there is one message rather than two. A global flag before the subcommand, such as --proof-timeout 300, does not hide it; an argument that is not a subcommand, such as a file name, is left alone. check_library.py holds the table to the compiler's own dispatch in both directions, so a subcommand cannot be added to the language without an entry, and the table cannot claim one the compiler lacks.

The Node library chooses the same way. findPython in npm/index.js had the same flaw, and it mattered more there: one stale choice is cached for the life of the process, so every check, audit and run through the module answered with a version the caller did not ask for. It now shares the probing with the command line - both import npm/python.js - and prints the same line, once per process rather than once per call. When no candidate has Velaris at all, both say what they said before: pip install velaris-lang.

The arXiv package is level with the paper again. paper/velaris.md gained a paragraph in the reproducibility section saying which two tags the paper describes; paper/arxiv/velaris.tex is pandoc output and is regenerated rather than edited, so it was left one paragraph behind until pandoc was available. It has been regenerated with the command in paper/arxiv/README-for-me.txt and rebuilt the way arXiv builds it. The paper still describes Velaris 4.2.1 and velaris-spec 0.5.1; that pin is unchanged.

4.3.3 - velaris mcp, so the npm package can start the server too #

A patch version. Every program that compiled under 4.3.2 compiles, runs and means the same; nothing is added to the language, the capability surface or any document format. One subcommand is added, and it is an alias.

velaris mcp starts the MCP server. Until now the only way in was python -m velaris_mcp, which an MCP client can only use if it knows where the module sits. velaris mcp reaches the same server through the console script, and because the npm wrapper passes its arguments straight to python -m velaris, npx velaris-lang mcp reaches it too.

It is a thin alias and deliberately nothing more: it hands velaris_mcp.main the arguments after mcp and returns what it returns. The flags, the four tools, the --max-allow ceiling, the timeout and memory ceilings and the invocation log are the server's, parsed by the server; there is no second copy of any of them here, and an unknown flag produces the server's own usage message. The one place the alias is not transparent is --max-memory-mb, which for mcp - as for serve - is the most each run may have and not a cap on the server process, so it is excluded from the early self-cap the way serve already was. check_library.py pins both halves: that velaris mcp answers initialize byte for byte as python -m velaris_mcp does, and that a bad flag stops it with the server's message.

The MCP registry entry now declares the npm package. With velaris mcp in place, npx velaris-lang mcp genuinely starts an MCP server, so integrations/mcp_registry/server.json declares the npm package beside the PyPI one, and npm/package.json carries the mcpName the registry checks for npm ownership. It was left out of 4.3.2 on purpose, because until this version the npm package could not start a server and declaring it would have handed clients a launch command that started the language CLI instead.

Worth knowing before you rely on it: the npm package is a wrapper, not a copy. It finds a Python that can import velaris and calls it, so npx velaris-lang mcp still needs pip install velaris-lang, and if the Python it finds holds an older Velaris than the wrapper, the subcommand will not be there. That is how the wrapper has always chosen a Python and this version does not change it.

4.3.2 - The card's true size, and a registry manifest on the current schema #

A patch version. Every program that compiled under 4.3.1 compiles, runs and means the same; nothing is added to the language, the capability surface or any document format. Three documents were wrong about a number, and one integration file was written against a schema that has since been replaced.

The language card is 3,682 words, and now says so. Eight places described its size and none of them were right: README.md said 3,300 words in two places, and EMBEDDING.md, velaris_mcp.py (twice), mcpb/manifest.json and the CrewAI and LangChain tool descriptions all said about 2,300. The card is generated from LLM.md, which has grown with the language - Money of CUR arrived in 4.3 - and the figures were last touched when it was smaller. Measured from velaris card output: 3,682 words in all, 2,537 outside the code blocks. Every one of those places now says about 3,700. This matters more than a documentation nit, because two of them are tool descriptions a model reads when deciding whether to fetch the card at all.

The MCP registry manifest is on the registry's current schema. integrations/mcp_registry/server.json was written against 2025-07-09, which the registry has replaced with 2025-12-11. Five fields were renamed under it - version_detail.version to version, registry_name to registryType, a package's name to identifier, runtime_hint to runtimeHint and package_arguments to runtimeArguments - a transport object became required, and description is now capped at 100 characters, which the old one exceeded at 167. The file is now validated against the published schema rather than by eye.

A mcp-name: marker in README.md. The registry proves that a PyPI package and the server entry claiming it have the same owner by looking for mcp-name: <server name> in the package's description - which is this README, as published to PyPI. Without it the registry refuses the entry. It is an HTML comment at the top of the file, so nothing renders, and there is a note beside it saying what removing it would break.

The npm package says what the compiler is. npx velaris-lang without pip install velaris-lang fell back to a fully interpreted run with no prover and said so in one line that was easy to miss, so anyone arriving through npm got the slow path and no proofs without knowing there was another. npm/README.md now has a section on it: the compiler is a Python package, pip install "velaris-lang[full]" adds z3 and llvmlite, and what each of those buys.

4.3.1 - A discount that cannot go negative, and a timeout that says it timed out #

A patch version. Every program that compiled under 4.3.0 compiles, runs and means the same; nothing is added to the language, the capability surface or any document format.

A proof that runs out of time now says it ran out of time. This is the part that mattered. Z3 answers unknown for two unrelated reasons: the question is outside what it decides, or the clock ran out. Until now Velaris treated both the same way - it abandoned the proof and fell back to the runtime check, silently. For examples/fp_proof_bad.vel, whose refutation takes about fifteen seconds against what was a thirty-second budget, a busy machine could therefore produce this:

$ velaris check examples/fp_proof_bad.vel
examples/fp_proof_bad.vel: ok - 2 function(s), 0 with proven promises
$ echo $?
0

which is exactly what a clean file looks like. It caused one false alarm here, and it is the worst failure this compiler can have: a lost refutation reading as a clean bill of health. The distinction did not exist, and now it does. A proof that spends its whole budget without an answer is abandoned, and every report says so in those words:

note: the proof of 'add_twice' ran out of time after 120s and was
abandoned - nothing was proven and nothing was refuted, so its
promises are checked while running instead. This is not 'the prover
found nothing wrong'. Give it longer with --proof-timeout 240 (or
VELARIS_PROOF_TIMEOUT=240).

The note goes to stderr from the prover itself, so it appears for velaris check, a plain run, explain, proofs and the library alike. Beside it: velaris check marks the file (1 proof(s) abandoned: out of time, nothing settled) rather than leaving ok - ... to speak for itself; velaris proofs --detail marks the function [timeout] rather than [runtime]; check --strict fails as before but says the proof was abandoned, not that the promise could not be proven; the unproven- promise SARIF result says the same; and velaris explain --json carries proof_timeouts and a proof_timeout flag on each function. An abandoned proof is not written to the proof cache, so the next run spends the budget again instead of remembering a non-answer.

The budget for float proofs is 120 seconds, and either budget can be replaced for one run. A query about Float is decided by bit-blasting and is slow; everything else finishes in milliseconds. The two defaults are now 120 seconds with Float and 3 seconds without - the second is unchanged - and --proof-timeout SECONDS (accepted by every command; the flag is taken out of the command line before any command reads it) or VELARIS_PROOF_TIMEOUT replaces both. velaris.set_proof_timeout() does the same from the library. SPEC.md 9.3 states the defaults and requires an implementation to distinguish an abandoned proof from a settled one; docs/floats.md shows what it looks like.

The larger budget is a widening of the prover's reach as STABILITY.md defines it: a float promise that a slower machine abandoned at 30 seconds can now be refuted, so a program that compiled on such a machine may be refused with E700. Every such program could already break its promise while running, for the input the refutation names.

check_library.py adds seven cases for it, made deterministic with --proof-timeout 0.2: that the words appear, that they say explicitly this is not a clean result, that the flag is named, that check, proofs --detail, --strict and the JSON report each mark it, and that a second run says it again rather than reading a cached non-answer.

examples/discount.vel: a rule the customer wrote, proven before it runs. A commerce platform lets each customer write their own discount rule - a percentage off above a threshold, a flat amount off as well, and a cap on the two together. The platform cannot read every rule, and no sandbox can tell it that a rule's arithmetic works: a sandbox stops the rule reading a file and will happily return a total of minus four hundred rupees.

Five of five functions prove:

• line_total - a line's quantity times its unit price is not negative
• basket_total - units_of over a list of amounts is what they add up to, so ensures units_of(result) == units_of(lines) is the whole of "the total is the sum of its parts"
• discount_for - the discount is never negative, and ensures total - result >= money(0, "INR"): what is left after it is never negative either
• total_after - the payable amount is not negative and not more than the basket, from discount_for's promises through a call summary
• charged_per_line - money.split again, so the per-line charges add up to the payable amount exactly and none of them is negative

The percentage is percent_of(total, rule.percent, 100, "half_up"), with the mode written, because a discount that rounds is a decision. Every amount is Money of INR; the program is pure apart from printing and runs under --allow io.

examples/discount_bad.vel is the same rule with the last guard deleted - the one that holds a discount to what the basket is worth. The cap still holds it to a fixed ceiling, which is not the same thing, and the program does not run:

$ velaris check examples/discount_bad.vel
examples/discount_bad.vel:54: [E700] promise cannot be kept:
'discount_for' ensures total - result >= money(0, "INR") - proven
without running the program: rule = Rule(percent: 0, above: 0,
flat: 2, cap: 1), total = 0 gives result = 1

In paise: a basket worth nothing, a flat discount of two paise held down to a cap of one, and one paisa handed back anyway. Both files are in run_tests.py, as RUNS and REJECTED, and both are in velaris.capabilities

• io only, nothing else. README.md shows the pair.

The VS Code publish retries, and the job says whether it published. The Marketplace answered Request timeout: /_apis/gallery on 3.3.0, 3.4.0 and 4.3.0. The step now makes three attempts, waiting 30 and then 120 seconds, treats a publish that landed anyway as a success, and stops retrying at once if the failure is not an outage (a bad token, a manifest the Marketplace refuses) - that one still fails the step, because it is this repository's to fix. A second step, if: always(), writes one line to the job summary saying PUBLISHED or NOT PUBLISHED and why, so the job is read rather than remembered and ignored. It stays continue-on-error, so a Marketplace outage still cannot fail a release.

4.3 - Money, which is not a float #

A minor version, and an additive one: every program that compiled under 4.2 compiles, runs and means the same.

A currency amount is not a real number. A Float cannot hold 0.10, so a premium, a claim or a settlement computed in floats is wrong in a way that compounds quietly and is never signalled. Velaris already proves things about whole numbers honestly; an amount is now a whole number with a currency, and it proves the same way.

The type. Money of INR is an exact amount in minor units - paise, cents, fils - held as a 64-bit Int, with the currency part of the type (SPEC.md 4.3). One way to write one:

money(1250, "INR")           // 12.50 rupees, as 1250 paise

There is deliberately no from_major(12, 50, "INR") or rupees(12, 50) beside it: a major/minor pair is ambiguous for a currency with three digits after the point and meaningless for one with none, and parse_money("12.50", "INR") already reads the human form. units_of(m) gives the minor units back, and with_units(m, n) makes an amount of n units in the currency of m, which is how code generic in a currency builds one.

Currency is part of the value, and of the type. Adding INR to USD is a compile error (E550), not a surprise while running, and so is comparing them, putting both in one list, or passing one where the other is declared. There is no conversion builtin: converting needs a rate and a rounding policy, and both are a program's decisions. A function can be generic in a currency - fn fee(m: Money of C) -> Money of C for any C - and the currency is then whatever the call site's amount has.

Arithmetic. Amounts in one currency add and subtract; an amount multiplies by an Int. An amount times an amount is a type error (E501), an amount and a Float never meet (E501), and an amount past 64 bits stops the program with E407, exactly as an Int does.

Rounding is never implicit. / and % on an amount are refused (E553, a new code), because both would round without saying how. Where a result can fail to come out even, the mode is a required argument, written in the call:

percent_of(amount, numerator, denominator, "half_up")
divide_or_fail(amount, by, "half_even")        // can fail

"half_up" takes a half away from zero, "half_even" to the even neighbour, "down" toward zero; anything else, or a mode held in a variable, is E552. There is no default. percent_of multiplies before it divides and is exact in between however large that product; only its answer must fit in 64 bits. A denominator of zero is E403 while running, or E706 where the prover can show it. divide_or_fail fails catchably on zero and on an answer too large to hold, and joins the fallible builtins, with parse_money.

Splitting, with the sum proven. money.split(amount, ways), in the new stdlib/money.vel, gives ways parts that add up to the amount exactly, the remainder distributed one minor unit at a time, largest part first:

import "money.vel" as money
let parts = money.split(money(1000, "INR"), 3)   // 334, 333, 333

It is written in Velaris, not in the compiler, so that the code that runs is the code the prover proves - with your program, every time you compile it. Its promises, all proven: as many parts as asked; the parts add up to the amount exactly; and no part is negative when the amount is not (nor positive when the amount is not). A negative amount gives the negated parts of the positive one, so a charge and its refund cancel party by party rather than leaving one party a unit up. It is money.split and not split because split is already the text builtin; the file is imported with a name, as dates.vel and csv.vel are.

Text. text_of(m) writes the code and then the amount with exactly as many digits after the point as the currency has minor units: INR 12.50, JPY 1250, KWD 1.250, INR -0.05. to_text, print and format agree with it, and json_of writes an amount as its currency and its units, never as a JSON number with a point. parse_money(text, "INR") reads back what text_of wrote, with or without the code and with fewer digits after the point, and fails on everything else - including a text with more digits than the currency has, which would have to round.

The currency table is small, and says so. CURRENCIES in velaris.py holds 21 codes with their minor-unit counts (2 for INR and USD, 0 for JPY and KRW, 3 for KWD, BHD, JOD and OMR). It is not exhaustive. A currency outside it is refused (E551) rather than assumed to have two digits, because a wrong minor unit prints and parses every amount in that currency wrongly. Adding one is a line in that table with the count ISO 4217 gives it and a case in check_money.py; a program cannot add its own, because two programs disagreeing about a currency would write the same amount two ways.

What the prover makes of it. An amount is its minor units to the prover - an Int - so ensures result >= money(0, "INR") is settled the way result >= 0 is, at the same speed, with none of the bit-blasting Float needs. percent_of is translated as the exact rounding the interpreter performs, for a denominator shown positive. What a list of amounts adds up to is a value the prover is told three true things about - nothing adds up to zero; items all >= 0 (all <= 0) add up to something >= 0 (<= 0) - and nothing more, so it is never claimed as a counterexample. text_of, parse_money and divide_or_fail are not modelled: a function that uses one keeps its promises as runtime checks, as with the other fallible builtins.

Four promises were asked for by name. All four prove, and check_money.py asserts each:

• a total over a list of amounts is non-negative when every item is - both as a loop that adds them and, through the facts above, as units_of(xs);
• money.split's parts add up to its amount - in money.vel where it is written, and at a caller through its promise;
• percent_of never exceeds its amount for a numerator at most the denominator - with the rate written in the call and with the rate symbolic;
• a subtraction guarded by a requires cannot go negative.

What does not prove, stated rather than weakened: a promise that needs more about a sum than the three facts - anything needing induction over a list, such as "the total of a list each of whose items is at least 10 is at least 10 times its length". Such a promise is checked while running, and velaris proofs says so.

Money is pure. No new effect, nothing new in the capability surface, no change to velaris.audit/1, velaris.capabilities/1 or the ratchet. A program full of amounts and nothing else declares nothing and runs under any budget; examples/settlement.vel runs under --allow io.

A builtin added from 4.3 on gives way to your own function of that name (SPEC.md 10.1). examples/ledger.vel has had a function called money since 1.13, and a program that defines money, units_of, text_of or any of the others keeps meaning what it meant; the builtin is simply not reached there. Inside a library imported with a name the builtin is always reached, since the library's own functions carry its prefix. This is what lets a minor version add a builtin at all; the builtins that existed before 4.3 keep the precedence they had.

The prover settles one more thing than it did, which STABILITY.md's "prover's reach" covers and which is named here: a division whose divisor mentions a loop's values is now translated when the loop's own condition and invariants show it positive, where before any such divisor was left alone. money.split needs it - it divides by "the parts still to make" - and an average computed after a loop gets it too. No verdict in this repository moved: every function of all 172 .vel files here was compared, before the change and after, and nothing differed - neither a proof status nor an error code.

examples/settlement.vel is the demonstration: rows of claims read and parsed, totalled, a 2.5% fee taken with "half_up" named in the call, the rest split three ways, and the result printed. Five of its five functions are proven, among them that the parts add up to the payout and that no party is paid a negative amount. It runs under --allow io and is in run_tests.py.

check_money.py is the new suite: 81 cases covering mixed-currency arithmetic refused at compile time, an amount times an amount refused, the 64-bit edges, split for 1, 3, 7 and 100 ways and for amounts that do not divide and for negative amounts and for zero ways, every rounding mode on a half case in both signs against Python's decimal module as an independent oracle, JPY with no minor unit and KWD with three, text and parsing round-trips for all 21 currencies, a property test over 200 random amounts and divisors, the four promises above, and the prover's rounding formulas checked against the interpreter's on 450 cases.

SPEC.md gains sections 4.3, 4.4 and 10.1; LLM.md gains the type, the builtins, the module and rule 16, which states the three rules a model gets wrong - no floats, no two currencies, rounding always named; docs/floats.md gains the section that says currency is the case where the answer is not "be careful with floats" but "do not use them".

4.2.1 - The author name, capitalised correctly #

A patch version, and a text change only. The compiler, the runtime and every document format are as in 4.2.0; in velaris.py only VERSION changes. Beside the six version files, the README's Action reference, velaris.capabilities and the documentation pages carry the new version.

The author is Palakurthi Gowri Shankar: family name Palakurthi, given name Gowri Shankar, with a capital S. 4.2.0 wrote the given name as "Gowri shankar". Corrected in CITATION.cff (given-names: Gowri Shankar), LICENSE, editor/vscode/LICENSE, README.md (twice), SUPPORT.md, MAINTAINERS.md, PROVENANCE.md, pyproject.toml, integrations/langchain_velaris/pyproject.toml, npm/package.json, mcpb/manifest.json, packaging/winget.yaml (Publisher; the PackageIdentifier is an identifier and is unchanged), paper/velaris.md, and paper/references.bib, still in the comma form {Palakurthi, Gowri Shankar} so that BibTeX reads Shankar as a given name and not as a particle. velaris-spec 0.5.1 makes the same correction. The 4.2 entry below keeps the form 4.2.0 used.

How it renders, checked. Both CITATION.cff files validate against the CFF 1.2.0 schema, with jsonschema and with cffconvert --validate. cffconvert 2.0.0 writes the BibTeX author as {Palakurthi, Gowri Shankar} and its APA-like line as "Palakurthi G.S. (2026)" - "G.S." where 4.2.0's file gave "G.s."; that writer puts no comma after the family name and no space between initials, for any name. BibTeX's apalike.bst, run over references.bib, writes "Palakurthi, G. S." and IEEEtran.bst writes "G. S. Palakurthi" (the styles from CTAN, run by pybtex's implementation of BibTeX). A CSL processor, citeproc-js, writes "Palakurthi, G. S." in APA and "G. S. Palakurthi" in IEEE from CITATION.cff's names; a citation in the text is "(Palakurthi, 2026)".

Verified, on Windows 11 with Python 3.13 and the prover (z3 5.1.0), with the proof cache cleared first: run_tests.py 92/92, check_library.py 196 correct (one skipped: its symbolic-link case is POSIX only), and velaris conformance conformant at L1, L2 and L3, 443 of the 444 cases run and the symbolic-link case skipped because this machine will not make a link. velaris capabilities check . passes against the regenerated baseline, and velaris-spec 0.5.1's tools/validate.py and tools/check_sync.py pass.