Velaris 8.4.0

Velaris

A programming language in which a function's signature states the types it takes and gives, the effects it may perform, whether it can fail, and what it promises about its result. The compiler checks the effects and the failures before the program runs, the Z3 theorem prover proves the promises it can, and the runtime refuses every effect outside the budget the operator grants.

It is not a security boundary by itself: an interpreter in the program's own process enforces the budget. From 8.4 the operating system is asked to hold the same budget under it - fully on Linux, partly on macOS and on Windows. The threat model says what that leaves open.

Try it

Install it and work through the tutorial, about an hour. The playground runs the same compiler in a browser, with nothing installed.

The tutorialThe playground

Review it before running agent code

For a person about to run a program a model wrote. The threat model says what Velaris defends against and what it does not; velaris audit says what one program can touch, before it runs.

The threat modelThe audit

For a model

The whole language as one plain-text page, written to be given to a model before it writes Velaris. Every compiler error names it.

llms.txt

Install #

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

A standalone executable for Windows, Linux and macOS is attached to every release.

What a signature says #

The promise below is checked for every input before the program runs, and the compiler hands back the input that breaks it:

Velaris
fn discount(price: Int) -> Int
    requires price >= 0
    ensures result >= 0
{
    return price - 10
}
Text
error[E700] promise cannot be kept: 'discount' ensures result >= 0
  proven without running the program: price = 5 gives result = -5

Where things are #