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.
This article was originally published by DEV Community and written by Gowri shankar.
Read original article on DEV Community