I've been building a language where a function's signature declares which effects it may perform, and a runtime refuses anything outside a budget you grant. The obvious question is whether that catches anything real, so I built a benchmark against the alternatives.
The setup
63 programs — 56 dangerous, 7 harmless controls — each written three times in Velaris, Python and JavaScript, doing the same thing. Eleven categories: a file write hidden in a helper, a network call hidden in a helper, division by user input, an off-by-one read, integer overflow, an ignored failure, an infinite loop, runaway memory, reaching a dangerous module, scoped-budget escapes, and the controls.
Every tool runs under the narrowest budget its task needs — Velaris with fs:read:DIR or net:127.0.0.1:PORT, Deno with the matching --allow-read / --allow-net, Python with nothing, because it has no budget. Deno 2.9.6, Python 3.13.13, 5-second deadline and a 256 MB cap for everyone.
Results
| before | during | missed | false positives | |
|---|---|---|---|---|
| Velaris | 42 | 12 | 2 | 0 |
| Deno | 5 | 27 | 24 | 0 |
| Python | 0 | 28 | 28 | 0 |
The first column is the one that matters. Deno's permission model works — it just works at the moment of the call. Nothing in deno check or deno lint reads a file write or a fetch as a problem. Velaris makes the effect part of the signature, so velaris audit lists it without running anything.
One category Velaris wins outright
Integer overflow. Whole numbers are 64-bit and arithmetic leaving that range stops the program. Python's integers don't overflow and JavaScript rounds to a double — both print a value without comment. Six for six, neither other tool caught any.
Where my own prover fell short, by ID
Four programs were caught only while running, where a sibling was caught before: 03c (a division on n - 1 with n from to_int inside a check), 03d (the same division on an unguarded path when another path guards it), 03f (a remainder inside a loop body), 04e (a read at i + 1 inside a loop bounded by length(xs)). The runtime check stopped each; the prover didn't settle the obligation first. Recorded rather than worked around.
A claim I'm deliberately not making
Eleven programs were flagged before running by a termination rule — a loop whose condition has no counter moving toward an unchanging limit. The rule claims nothing about whether such a loop actually ends. Every one of these happens not to, and the run confirmed it. But that's an observation, not a proof.
What Velaris missed
One computes the wrong answer and promises nothing — no contract, nothing to check against. The other prints the string rm -rf /; it doesn't run anything, and flagging it would mean flagging any program that prints text resembling a command. The seven controls exist to punish tools that guess.
Reproduce it
pip install velaris-lang
python benchmark/run.py
Ten consecutive runs produce byte-identical output. Three unstable strings had to be normalised to get there — ephemeral ports, V8 crash wording, and whether Python prints MemoryError before dying.
Honest limits
This measures static declaration plus runtime refusal, not isolation. Velaris runs inside a container, never instead of one. Granting ffi grants everything Python can do. And I wrote the corpus — which is why the two it can't catch are in it, and why the controls are there.
Top comments (4)
The separation between “caught before” and “caught during” is the useful metric here. Runtime refusal is necessary, but pre-execution effect visibility changes whether a human can approve a plan before any side effect begins. I also appreciate including the two misses and harmless controls; without them the benchmark would reward a language for flagging everything.
A next test I would love to see is indirect authority: a safe-looking function calling a dependency whose declared effect budget changes between versions.
Thank you that's the distinction I'd want people to take from it. On indirect authority: the ratchet already fails a widening in a Velaris dependency because the baseline comparison is transitive (check_ratchet.py has that case), but a version-to-version diff of what an upgrade gained doesn't exist yet. It was next on the list; your comment moved it up. I'll add a category to the benchmark for it and link back here when it ships.
Shipped in 7.1.1. Your test is benchmark category 12, "indirect authority": three programs where the caller is unchanged and only the dependency's declared budget widened — net, a new host inside net, fs:write — all caught before running, plus a control that isn't flagged. velaris deps-diff is the tool; the honest limit in THREAT_MODEL.md is that for a non-Velaris package it sees only install scripts and declared dependencies. github.com/gowrishankar-infra/vela... . Thank you
Some comments may only be visible to logged-in visitors. Sign in to view all comments.