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 (0)