A programming language

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.

Open the playground View on GitHub

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

Effects are visible

A function without uses net can never touch the network — checked transitively. Hidden behavior does not compile.

Promises are proven

Contracts are verified by the Z3 theorem prover for every possible input — with exact counterexamples when broken, in genuine IEEE-754 for floats.

Failure is unignorable

or fail in the signature; forgetting the error path is a compile error. Builtins included.

Fast where it’s safe

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.vel

No 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.

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. All 49 of them are documented, scraped from the compiler source itself.