pip install velaris-lang
velaris agent_output.vel --allow io

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.

It is not a security boundary: --allow ffi grants everything Python can do, and nothing here limits memory or time. 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.

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.

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

velaris card > card.md          # ~1,500 words: paste into any model
velaris audit script.vel        # what it can touch, before you run it
velaris script.vel --allow io   # it cannot touch anything else

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. 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 --allow io      # it cannot touch anything else
velaris agent_output.vel --deny net,ffi  # everything except 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     # 33 checks across the whole language
velaris examples/edges.vel      # 20 boundary, property and round-trip checks
python check_refusals.py        # 20 wrong programs, each refused correctly
python check_sandbox.py         # 11 escape attempts, all refused

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

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 <file> [n] counts word frequencies and prints a ranked histogram. examples/linkcheck.vel — a link checker you would actually run: velaris examples/linkcheck.vel <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 verify                                   # unchanged since?

A library is compiled before it is accepted, recorded with its exact sha256 in velaris.toml, and kept in your repository where you can read it. No registry, no resolver, nothing fetched at build time.

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

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.

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 (v2.0 migrated the fallible builtins, compiler-guided). CI tests every push on Linux and Windows, 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

- uses: gowrishankar-infra/velaris-lang@v2.33
  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

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.

Project

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

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

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 © Gowri Shankar