Trust code you didn’t write.
A Velaris signature tells you everything: the types, the effects a function may perform, whether it can fail — and promises that are mathematically proven before the program runs.
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 = -5A function without
uses net can never touch the network — checked
transitively. Hidden behavior does not compile.
Contracts are verified by the Z3 theorem prover for every possible input — with exact counterexamples when broken, in genuine IEEE-754 for floats.
or fail
in the signature; forgetting the error path is a compile error.
Builtins included.
Pure numeric functions compile to native code via LLVM, verified identical to the interpreter.
Install in one line
pip install velaris-lang
velaris doctor
velaris new hello && cd hello && velaris main.velNo Python? Download a standalone executable from the latest release — Windows, Linux, and macOS. Or skip installing entirely: the playground runs the real compiler in your browser.
The standard library keeps its own promises
sort carries ensures is_sorted(result)
— and is_sorted is itself a library function,
written in Velaris. Violating a library requires is a
compile error at your call site. Browse the
library reference, generated from the real
compiler with contracts included.
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.
| caught before running | caught while running | missed | false positives on the 7 controls | |
|---|---|---|---|---|
| Velaris 4.1 | 42 | 12 | 2 | 0 |
| Deno 2.9 | 5 | 27 | 24 | 0 |
| Python 3.13 | 0 | 28 | 28 | 0 |
The two Velaris misses are in the corpus on purpose: 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
RESULTS.md
— regenerated by one command.
Honest about floating point
Most verifiers model floats as real numbers, which makes proofs fast
and occasionally false. Velaris proves in genuine IEEE-754, so it
refuses to certify x + 0.1 + 0.1 == x + 0.2 and
hands you the exact double that breaks it —
here is why that matters.
Built for the age of generated code
Increasingly, the developer reading your compiler’s output is
an AI in a fix loop. Every Velaris error has a stable code, a
plain-English message, a location, and numbered fixes —
available as JSON with --json, and as SARIF for code
scanning with --sarif.
All 78 of them are documented, from the
error table in the compiler source.