velaris-lang

<!-- mcp-name: io.github.gowrishankar-infra/velaris -->
<!-- The line above proves to the MCP registry that this package and the
     server io.github.gowrishankar-infra/velaris have the same owner. It is
     read from this file as published to PyPI; removing it breaks publishing
     to the registry. See integrations/mcp_registry/server.json. -->

<div align="center">

# Velaris

**An AI wrote you a script. Run it anyway.**

A language where a function's signature declares what it may touch —
and the runtime refuses anything you did not allow, whatever the code
says about itself.

[![PyPI](https://img.shields.io/pypi/v/velaris-lang)](https://pypi.org/project/velaris-lang/)
[![tests](https://github.com/gowrishankar-infra/velaris-lang/actions/workflows/test.yml/badge.svg)](https://github.com/gowrishankar-infra/velaris-lang/actions/workflows/test.yml)
[![release](https://img.shields.io/github/v/release/gowrishankar-infra/velaris-lang)](https://github.com/gowrishankar-infra/velaris-lang/releases)
[![license](https://img.shields.io/badge/license-MIT-green.svg)](LICENSE)

[**Playground**](https://gowrishankar-infra.github.io/velaris-lang/playground.html) · [**Documentation**](https://gowrishankar-infra.github.io/velaris-lang/) · [**Reference**](SPEC.md) · [**Library**](https://gowrishankar-infra.github.io/velaris-lang/library.html) · [**Errors**](https://gowrishankar-infra.github.io/velaris-lang/errors.html)

</div>

<img src="docs/hero.png" alt="Velaris refusing a network call because the run only allowed io" width="100%">

---

```
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`](examples/discount.vel) is the whole program —
five of five functions proven, and it runs under `--allow io`.

[`examples/discount_bad.vel`](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.

## A key it cannot print

Effects say a program printed something. They do not say whether what
it printed was the secret. `Secret of T` (6.0, 7.0) is the other half: the
compiler tracks the value, and refuses any program that hands it to
anything that emits.

```
fn key() -> Secret of Text uses env {
    return env("API_KEY", "")          // env() gives a Secret of Text
}

fn authorization(k: Secret of Text) -> Secret of Text {
    return "Bearer " + k               // still a Secret of Text
}
```

[`examples/secret.vel`](examples/secret.vel) reads an API key, builds
the request that would carry it, and prints a summary of that request.
[`examples/secret_bad.vel`](examples/secret_bad.vel) is the same
program with one more line:

```
$ velaris examples/secret_bad.vel --allow env,io
error[E560] argument 1 of 'print' is Secret of Text, and 'print' performs io - a Secret cannot be printed, written, sent or passed to Python. It came from env(), line 27, through 'key', which returns Secret of Text (line 58)
  --> examples/secret_bad.vel, line 58
```

Nothing ran, nothing was logged, and no reviewer had to notice the
line. A list of secrets, a map of them, or a record with one secret
field carries it too, so the whole structure is refused at a sink — a
`Request` record holding the key cannot be printed either.

**And a program cannot look at the key either.** `key == ""` is a
`Secret of Bool`, not a `Bool`, and an `if` or `while` on one is
`E563`. That is the rule that makes the rest mean something: with
`length` and `code_at`, a plain `Bool` from `==` is not one bit, it is
a loop that reads the whole key out —

```
while at < 3 {
    for c in alphabet {
        if code_at(key, at) == code_at(c, 0) {   // E563
            found = found + c
        }
    }
    at = at + 1
}
print("recovered: " + found)                     // the whole key
```

— so a rule that stopped `print(key)` and allowed that would be a
decoration, not a type. The line is drawn at the branch.

`declassify(value, "why")` is the only way out. It needs
`uses declassify` in the signature, a reason written in the call, and
the `declassify` grant at run time — and it is what the audit reports,
so a consumer can ask whether a program ever lets a secret out without
running it:

```
$ velaris audit examples/secret.vel --json | jq .secrets
{
  "sources": ["env"],
  "declassifies": false,
  "declassifications": []
}
```

To look at a secret, a program says so — `declassify(key == "", "…")`
gives back a `Bool` you can branch on, at the cost of the effect, the
grant and a reason in the audit. That is the trade: not silence, a
statement.

What this does **not** do: it only sees values `env()` and
`read_file_secret()` produced, so a password read with `read_line`, or
handed in through `args()`, or fetched from a vault over `net`, is an
ordinary `Text` with no protection at all. And it is not
non-interference — a program still chooses how long to run and whether
to stop. [SPEC.md §3.1](SPEC.md) states the rules and
[THREAT_MODEL.md](THREAT_MODEL.md) states the limits.

## Related work

[TACIT](https://github.com/lampepfl/tacit) ("Securing Agents With
Tracked Capabilities", ACM CAIS '26;
[arXiv 2603.00991](https://arxiv.org/abs/2603.00991)) has agents write
Scala 3, whose capture checking tracks file, network and command
capabilities as values in the type system;
[CaMeL](https://arxiv.org/abs/2503.18813) 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](https://wasi.dev) 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. From 6.0 it also tracks one kind of
data: `Secret