pip install velaris-lang
velaris agent_output.vel

That program cannot open a socket, read a file, call Python, or ask the clock. Not "shouldn't" — the runtime refuses, and a refusal cannot be caught and carried past. You do not have to read the code, understand it, or trust the compiler's analysis of it.

Since 5.0 that is what a run with no --allow gets: io, the console. It used to be all seven effects, which meant the answer to "what may this program do?" was "everything" until an operator said otherwise. Widen it by naming what the program needs (--allow io,fs:read:./data); --allow all grants every effect and writes one line to stderr saying so.

--allow io,ffi:math,json grants Python for those modules only; a call that reaches any other module — named, or reached through an attribute of a granted one — is refused (E311). A granted module can still do whatever that module itself can do: ffi:os is the operating system. Since 3.0 the same grammar narrows every coarse effect: fs:read:./data, fs:write:./out, net:api.example.com:443, net:*.example.com, and @100 for at most that many operations in a run; env is its own effect, so an io-only program cannot read the environment. timeout and max_memory_mb are available through the library and every door, and on a door the operator's limits are ceilings a caller cannot raise. It is still not a security boundary - but the caveats every review raised, the ffi cliff, unbounded execution, and fs and net with no path or host list, are now precise permissions rather than holes. It is a real guard for the situation everyone is now in — running a program someone, or something, else wrote.

The other half: promises, proven

fn discount(price: Int) -> Int
    requires price >= 0
    ensures result >= 0
{
    return price - 10
}

error[E700] promise cannot be kept: 'discount' ensures result >= 0
  proven without running the program: price = 5 gives result = -5

That ensures is not a comment or a runtime assert. The Z3 theorem prover verifies it for every possible input before execution — and refutes it with an exact counterexample when it lies.

A rule the customer wrote

A commerce platform lets each customer write their own discount rule. This one has the shape most of them have: a percentage off once the basket passes a threshold, a flat amount off as well, and a cap on the two together.

record Rule {
    percent: Int         // this much off, once the basket is
    above: Money of INR  // worth at least this,
    flat: Money of INR   // and this much off as well,
    cap: Money of INR    // but never more than this, all together
}

fn discount_for(total: Money of INR, rule: Rule) -> Money of INR
    requires total >= money(0, "INR")
    requires rule.percent >= 0
    requires rule.percent <= 100
    requires rule.flat >= money(0, "INR")
    requires rule.cap >= money(0, "INR")
    ensures result >= money(0, "INR")
    ensures total - result >= money(0, "INR")
{
    let off = money(0, "INR")
    if total >= rule.above {
        off = percent_of(total, rule.percent, 100, "half_up")
    }
    off = off + rule.flat
    if off > rule.cap {
        off = rule.cap
    }
    if off > total {
        off = total
    }
    return off
}

The two ensures are what the platform needs to know about a rule it did not write: a discount is never a surcharge, and what is left after it is never negative. Both are settled for every basket and every rule the types allow, before the program runs. examples/discount.vel is the whole program — five of five functions proven, and it runs under --allow io.

examples/discount_bad.vel is the same rule with the last if deleted. The cap still holds the discount to a fixed ceiling; nothing holds it to what the basket is worth:

$ 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

The amounts are 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. The program does not run.

A sandbox answers a different question. It can stop this rule reading a file or opening a socket; it cannot tell you whether the arithmetic holds.

Related work

TACIT ("Securing Agents With Tracked Capabilities", ACM CAIS '26; arXiv 2603.00991) has agents write Scala 3, whose capture checking tracks file, network and command capabilities as values in the type system; CaMeL has a model turn the user's request into a restricted subset of Python and tags every value with its provenance and permitted readers, checking a policy at each tool call; WASI gives a WebAssembly module only the resources its host hands it. Velaris is a small language a model learns from a 3,700-word card, in which functions declare their effects, the runtime enforces the operator's budget at each operation, and contracts are checked by the Z3 theorem prover; it does not track data flow, which CaMeL and TACIT both do. Until 5.0 its command line also granted every effect when no budget was given, where a WASI module given nothing reaches nothing; from 5.0 a run with no budget gets io alone. The capability format is published separately, under CC0, as velaris-spec, whose PRIOR_ART.md sets out these differences and the older work in full. From 4.1 it holds a conformance corpus an implementation in any language can run - 444 JSON cases at three levels, declaration, enforcement and the ratchet, none needing a prover - written from this repository's suites and held to them by a drift test; velaris conformance runs it against this implementation, and CI does so on every leg.

Why Velaris

Why floats are proven in IEEE-754 rather than as real numbers, and what that costs: docs/floats.md.

Loops without written invariants are handled where the boring invariants suffice: the compiler proposes bounds on each counter and keeps the ones a loop step cannot break (see examples/inferred.vel). Anything richer — membership, sortedness — still needs an invariant line.

The prover never claims "proven without running" unless the counterexample is premise-complete — untranslatable assumptions abandon the proof to runtime checks rather than risk a false alarm. Soundness reports are treated as security issues.

Install

pip install velaris-lang
velaris doctor
velaris new hello && cd hello && velaris main.vel

Standalone executable (no Python required) — download for Windows / Linux / macOS from the latest release, then:

velaris doctor

With Python 3.10+:

pip install velaris-lang
velaris new hello && cd hello && velaris main.vel

Zero install — the playground runs the real compiler in your browser.

Optional extras for source installs: pip install ".[full]" adds z3-solver (compile-time proofs) and llvmlite (native speed); without them, promises are checked at runtime and everything runs interpreted — same language, honestly degraded.

Everyday ergonomics

keep_if(xs, fn(n: Int) -> Bool { return n % 2 == 0 })   // inline functions
format("hi {}, {} left", name, count)                    // text with holes
args()                                                   // command line
post(url, body) / fetch_status(url)                      // not just GET

Function values are lifted to real functions, so proofs and native compilation apply to them unchanged — and they can carry their own requires / ensures, proven like any other function's. They can't capture surrounding variables — the compiler tells you to pass them in instead.

Where it plugs in

velaris script.vel                    the command (io unless you say more)
import velaris                        a Python library
velaris mcp-install                   tools inside your assistant
velaris.mcpb                          double-click install for Claude Desktop
uses: gowrishankar-infra/velaris-lang a GitHub Action, findings as SARIF
velaris capabilities check            CI fails when the capability surface widens
velaris serve                         an HTTP door for any language, token required
npx velaris-lang script.vel           npm, for the JavaScript world
%%velaris --audit --allow io          a Jupyter cell
- repo: velaris-lang (pre-commit)     a commit hook
docker run ... velaris check          a container
velaris build --for-everyone          standalone executables

Use it from your own program

import velaris

report = velaris.audit(source)      # what it touches, what's proven
run = velaris.run(source, allow={"io"})   # it cannot touch anything else
print(run.output, run.refused_effect)

The budget is enforced the same way it is on the command line. There is an MCP server too, so an assistant can write, audit and sandbox-run Velaris without leaving the conversation — see EMBEDDING.md and the versioned velaris.audit/1 format.

Calling run with a timeout or a memory cap starts a fresh interpreter every time. A pool keeps workers alive under one fixed budget:

pool = velaris.Pool(size=4, allow={"io"}, timeout=30, max_memory_mb=512)
result = pool.run(source)             # the same RunResult run() returns
pool.close()

200 sequential bounded runs of a small program: 46.6 s a process at a time, 0.5 s on a pool. pool.run takes no allow — the budget belongs to the pool, a worker is killed and replaced unless the run finished cleanly, and a reused worker has every piece of mutable state reset first. check_pool.py asserts each of those, including a program that widens its own budget through ffi and cannot widen it for the next one. The rules are stated in full in EMBEDDING.md.

A platform whose customers write the rules

examples/platform/ is that pattern as a small FastAPI service, in one file. A customer submits Velaris source; the service audits it, stores it with its capability surface, and answers with what it declares — effects, hosts, paths, modules, the proven share, its contracts function by function, and the narrowest budget that would run it. It does not run it. A surface wider than the platform permits is refused there, naming the grants that would have to be added. Running happens on a velaris.Pool whose budget is the platform's.

Submit examples/discount.vel and the answer says "proven_share": 100.0 with "status": "proven" on every promise, including the two that matter to whoever is taking the payment: the discount is never a surcharge, and what is left is never negative. That is the sentence a platform can show a customer before offering to enable a rule, and it is not one a sandbox can produce.

Written by a model, audited by you, run in a box

velaris card > card.md          # ~3,700 words: paste into any model
velaris audit script.vel        # what it can touch, before you run it
velaris attest script.vel --output script.intoto.json   # the same, bound to its bytes
velaris script.vel              # io, and nothing else, unless you say more

velaris audit is written for the reviewer: what the program reaches, what it promises, how much of that is proven rather than checked while running, what can fail, and the exact command to run it safely. velaris attest (4.2) puts that audit in an in-toto Statement whose subjects are the program's files by sha256, ready to sign with cosign or sigstore-python; EMBEDDING.md shows both, and every release carries one, signed, for an example program. agent_loop.py closes the circle — a model writes it, velaris check --json hands back errors with fixes, and it iterates until the program compiles and its promises prove.

Running code you did not write

velaris agent_output.vel                 # io: it may print, nothing else
velaris agent_output.vel --allow io,fs:read:./data   # and read that folder
velaris agent_output.vel --allow all --deny net,ffi  # everything but these

The runtime refuses any effect outside the budget you grant, whatever the source claims — and a refusal cannot be caught and carried past. Not a security boundary (ffi grants everything Python can do), but a real guard for running a program you have not read.

Checking everything at once

velaris examples/stress.vel --allow clock,env,ffi:datetime,math,sqlite3,io,net:raw.githubusercontent.com
                                # 33 checks across the whole language
velaris examples/edges.vel --allow ffi:datetime,io
                                # 20 boundary, property and round-trip checks
python check_refusals.py        # 21 wrong programs, each refused correctly
python check_sandbox.py         # 38 escape attempts, each refused with its code
python check_pool.py            # a pool must leak nothing between programs
python check_platform.py        # the reference platform refuses what it says it does
python check_ratchet.py         # every widening fails, nothing else does
velaris conformance             # velaris-spec's 444-case corpus, L1 to L3

One command that exercises the language, the standard library, the prover, native compilation, JSON, dates, CSV, the host language and the network.

Measured against other tools

63 small programs — 56 with one deliberate defect, 7 correct controls — each written three times with the same behaviour, in Velaris, in JavaScript for Deno, and in Python. One harness runs every program through every tool and records what was caught before running, what was caught while running, and what was missed.

The two Velaris misses are in the table by design: a loop that stops one item early with no contract to contradict, and a program that prints rm -rf build for its caller and touches nothing. Both are named, with the reason each is not catchable, in benchmark/RESULTS.md — regenerated by one command, python benchmark/run.py, which also lists the rows the prover settles only while running.

Two real programs

examples/ledger.vel — an expense tracker: records, integer cents, file persistence, sorted reports. examples/wordcount.vel — text analysis: velaris examples/wordcount.vel --allow fs:read,io <file> [n] counts word frequencies and prints a ranked histogram. examples/linkcheck.vel — a link checker you would actually run: velaris examples/linkcheck.vel --allow io,net <url> ..., non-zero exit when something is broken. examples/fetcher.vel — an HTTP tool: checks a status, then summarises a page, with every network call declared and every failure handled.

JSON

json_get(doc, "user.name")    json_int(doc, "user.age")
json_len(doc, "tags")         json_of(Person(name: "gowri", age: 30))

Paths walk objects and lists, every read can fail (a missing field is a possibility, not a crash), and none of it is an effect — parsing text is pure.

Reaching other languages

fn today() -> Text uses ffi or fail {
    let nothing: List of Text = []
    return try py("datetime.date", "today", nothing)
}

py / py_int / py_float / py_json call Python functions, and py_new / py_do / py_field / py_close hold real objects — a database connection, a session — so every library Python has is reachable — but only from a function that declares uses ffi, and it can fail like anything else that leaves your program.

The standard library reaches outside

import "http.vel" as http     import "db.vel" as db
import "time.vel" as time     import "env_tools.vel" as sys

check http.get(url) { ok body { ... } fail why { ... } }
check db.count(conn, "notes") { ok n { ... } fail why { ... } }

Written in Velaris, so they carry their effects — a program using http shows net, one using db shows ffi, and a pure function can call neither.

Libraries

velaris add https://example.com/geo.vel as geo   # vendored into lib/
velaris deps                                     # what you depend on
velaris deps --verify                            # unchanged since?

A library is compiled before it is accepted and kept in your repository where you can read it. No registry, no resolver, nothing fetched at build time.

velaris add writes velaris.lock beside velaris.toml: every vendored library with its source, the sha256 of the exact bytes that arrived, and the version of Velaris that added it. velaris deps --verify fails if a file's hash differs from the lock or a locked library is not on disk — a line worth having in CI. Adding a library that is already vendored, with different bytes, is refused with both digests printed; --force replaces it.

Imports

import "lib/geo.vel" as geo      // named: geo.distance(a, b)
import "std.vel"                 // flat: sort(xs)

A named import prefixes that library's functions, so two libraries that both export distance can be used in the same file.

Shipping a program

velaris build myprogram.vel      # one executable, ~90 MB
./myprogram alpha beta           # runs anywhere, nothing installed;
                                 # it takes --allow like the compiler

velaris build myprogram.vel --for-everyone   # a workflow that builds
                                             # Windows, Linux and macOS

Your program, its imports, the standard library and the compiler, in one file. It is compiled and proof-checked before it is built.

Tooling

velaris trace program.vel (watch every call as it happens) · velaris test program.vel (runs every test_* function written in Velaris) · velaris check program.vel (compile without running; several files at once, --json for tools) · velaris explain program.vel (a walkthrough of every function: effects, promises, and whether they are proven — explain <folder> maps a whole project) · velaris repl (definitions are proof-checked as you type them) · velaris fmt (canonical style, --check for CI) · velaris lsp (errors as you type in any LSP editor; a VS Code extension lives in editor/vscode) · velaris doctor · velaris new · --json errors for automation.

Standard library

Written in Velaris, in stdlib/std.vel — and it keeps its own promises: sort carries ensures is_sorted(result), max_of requires a nonempty list, and violating a library requires is a compile error at your call site. Full reference, generated from the real compiler.

Numbers

Whole numbers are 64-bit. Arithmetic that outgrows that range is an error, not a silent wrap — and the same error whether your code is interpreted or running as machine code. Floats are IEEE-754 doubles, proven as such.

Money is neither. money(1250, "INR") is 12.50 rupees held as 1250 paise: an exact whole number of minor units, with the currency in its type, so INR meeting USD is a compile error and no Float goes near it. Dividing an amount says how it rounds — percent_of(claim, 25, 1000, "half_up") — or it does not compile, and money.split(payout, 3) gives parts that provably add up to the payout. See examples/settlement.vel and SPEC.md §4.3.

Remembered proofs

Proofs are cached in .velaris/ and keyed by the function's text and the contracts it depends on, so changing a promise re-proves everything that relied on it. --no-cache proves from scratch; velaris clean forgets.

The reference

SPEC.md states precisely what the language means: semantics, evaluation order, effect propagation, what "proven" covers today, and what Velaris deliberately does not have — including why it has no concurrency model.

Stability

Semantic versioning: breaking changes only at major versions. STABILITY.md says what that covers - the language, the error codes, velaris.audit/1, the library API, the budget grammar and the command line - what it does not, the rules for deprecating and removing, and every time this project has broken the rule, 3.3 and 3.4 among them. CI tests every push on Linux, Windows and macOS, Python 3.10 and 3.12, with and without the optional dependencies. Errors are stable, numbered, and fully documented.

How much is proven

velaris proofs .            # 35 of 58 promise-carrying functions proven (60%)
velaris proofs . --min 80   # fails the build below 80%

Using Velaris in CI

permissions:
  contents: read
  security-events: write       # for sarif, the default
  pull-requests: write         # only for pr-comment

steps:
  - uses: actions/checkout@v5
  - uses: gowrishankar-infra/velaris-lang@v4.3.3
    with:
      files: "src/*.vel"     # optional; default is every .vel file
      format: "true"         # optional; also check formatting
      min-proven: "80"       # optional; fail below this proven share
      pr-comment: "true"     # optional; audit every changed .vel on the PR
      sarif: "true"          # the default; findings to code scanning
      capabilities: "check"  # the default once velaris.capabilities exists

The capability ratchet (4.0). velaris capabilities init records the capability surface a repository's .vel files need - effects, paths, hosts, Python modules, how many file and network operations a run can perform, and each function's effects - in velaris.capabilities; commit it. From then on the action runs velaris capabilities check and fails any change that needs more, naming what widened, the file, function and line that introduced it, and the edit to the baseline that would accept it. The comparison is always with that file, never with the previous commit: capability added across many small commits, none alarming by itself, fails at every one of them until someone widens the file, where the change shows in review. With pr-comment the comment also reviews the pull request against its base - surface, proven share, new fallible functions, new hosts and paths - with a one-word risk computed from those facts. EMBEDDING.md has the rules; check_ratchet.py holds them, including a six-commit history that fails only at the commit that reaches the network.

With sarif on - the default from 3.4 - the check writes its findings as SARIF 2.1.0 and uploads them with github/codeql-action/upload-sarif, pinned to a commit, so they appear in the repository's Security tab and on the lines of a pull request. The job needs permissions: security-events: write, and a private repository needs code scanning enabled; set sarif: "false" if it has neither. On a pull request from a fork the job's token cannot upload, so the step is skipped there; the file is still written, and its path is the action's sarif-file output. The findings still print to the job log either way.

The same output without the action, for SonarQube (sonar.sarifReportPaths), Azure DevOps or anything else that reads SARIF:

velaris check src/*.vel --sarif > velaris.sarif   # exit 1 as the plain check
velaris proofs src --sarif > proofs.sarif         # promises left to runtime
velaris audit src --sarif > audit.sarif           # what each function may touch

One run, driver Velaris with its version and a rule for every code in the compiler's error table, each with a help link to its row on the errors page, plus a rule for each finding that is not an error. Each result has the file, the line and Velaris's message. Errors are error; a promise left to runtime is a warning (an error under check --strict); a function that promises nothing about the data it handles, a loop not shown to end, and each effect a function may perform (audit) are note. Velaris's suggested fixes are sentences, while a SARIF fix must hold the exact bytes to change, so they travel in each result's properties.fixes rather than as SARIF fixes with an edit made up to fill the slot.

Or without installing anything:

docker run --rm -v "$PWD:/work" velaris check /work/main.vel

Installs Velaris with the prover and fails the build if anything does not compile or a promise cannot be kept.

With pr-comment: "true" on a pull_request event the action posts one comment holding the velaris audit of every .vel file the pull request changes - effects and Python modules reached, proven share, the safe command, and any warnings such as a loop not shown to end - and edits that same comment on later runs instead of adding another. It uses the REST API with the job's own GITHUB_TOKEN, so the job needs permissions: pull-requests: write. The audit is posted whether or not the checks passed; a file that does not compile is reported as such.

What a reviewer should read before allowing agent-written Velaris to run: THREAT_MODEL.md, COMPLIANCE.md and the verification steps in SECURITY.md.

Project

Roadmap · Support and expectations · How the compiler works · Maintainers · Security policy · Stability · Changelog

Maintained by one person, in the open, with the limits stated plainly in SUPPORT.md.

Cite this repository

The author is Palakurthi Gowri Shankar (family name Palakurthi). CITATION.cff holds the citation, and GitHub offers it as "Cite this repository" beside the file list. A preprint describing Velaris is forthcoming; until it is published, cite the repository. The capability format is cited separately, from velaris-spec's own CITATION.cff. PROVENANCE.md records the dates and the archive identifiers.

Contributing

The entire implementation is one readable file, velaris.py, in pipeline order — lexer to LSP. Start with ARCHITECTURE.md for how it fits together, and MAINTAINERS.md for what review looks like.

Looking for somewhere to start? See the good first issues — small, self-contained tasks, each with the file to open and what "done" means.

The example programs in examples/ each carry an expected verdict, and about half are designed to be rejected — each rejection demonstrates a guarantee. Before any change ships:

python run_tests.py                 # every example, expected verdicts
velaris test examples/std_test.vel  # the library's own tests
python fuzz_native.py 60            # both engines must agree
velaris fmt examples/*.vel stdlib/*.vel --check

License

MIT © Palakurthi Gowri Shankar