What Verum actually does differently
Not features borrowed from research papers. Not syntax sugar over known patterns. Four integrated design decisions that change how you write and ship systems code.
Gradual verification as a language primitive
Seven verification strategies — runtime, static, fast, formal, thorough, certified, synthesize. You declare the intent; the compiler picks the technique. Refinement predicates compile to SMT obligations dispatched through a capability router, with tactic fallback and portfolio cross-validation for the strongest tiers.
// Same body, three guarantee levels — pick per function.
type NonNeg is Int { self >= 0 };
@verify(runtime)
fn abs_r(x: Int) -> NonNeg {
if x >= 0 { x } else { -x } // assert at runtime
}
@verify(formal)
fn abs_f(x: Int) -> NonNeg {
if x >= 0 { x } else { -x } // proved by the SMT backend
}
@verify(certified)
fn abs_c(x: Int) -> NonNeg {
if x >= 0 { x } else { -x } // + proof embedded in the .cog
}
One context system for everything
Runtime DI and compile-time meta share one `using [...]` grammar. Database, Logger, Clock at runtime; TypeInfo, BuildAssets, Schema at compile time. 14 meta-contexts, 10 standard runtime contexts, one lookup rule, ~2 ns for an inline slot.
// Runtime: caller provides Database and Logger.
fn handle(req: &Request) -> Response
using [Database, Logger]
{
Logger.info(f"{req.method} {req.path}");
let user = Database.find_user(req.auth)?;
Response.ok(&user)
}
// Compile time: the compiler provides TypeInfo and CompileDiag.
meta fn field_count<T>() -> Int using [TypeInfo] {
TypeInfo.fields_of<T>().len()
}
Types that carry proof obligations to zero-cost discharge
A refinement predicate is part of the type — not a comment, not a linter, not a separate tool. `Int { self > 0 }` flows through inference, narrows via control flow, discharges to SMT, reflects user `@logic` functions as axioms, falls back to tactics when SMT can’t — and the proof embeds in the binary as a certificate exportable to Coq or Lean. Zero runtime cost.
type Sorted<T: Ord> is List<T> { self.is_sorted() };
@logic
fn is_sorted<T: Ord>(xs: &List<T>) -> Bool {
forall i in 0..xs.len() - 1. xs[i] <= xs[i + 1]
}
@verify(formal)
fn insert<T: Ord>(xs: Sorted<T>, x: T) -> Sorted<T>
where ensures is_sorted(&result)
{
let pos = xs.partition_point(|y| *y < x);
xs.insert(pos, x) // sortedness preserved — proved at compile time
}
Three-tier references without language fragmentation
`&T` (CBGR-checked, ~15 ns), `&checked T` (compiler-proven, 0 ns), `&unsafe T` (you prove it, 0 ns). All three are the same type family — chosen per-use-site, not per-language-dialect. Escape analysis auto-promotes the hot-path fraction of `&T` to `&checked T`.
fn sum_ages(users: &List<User>) -> Int {
let mut total = 0;
for u in users.iter() { // &u: &User — ~15 ns CBGR check
let age: &checked Int = &checked u.age;
total += *age; // 0 ns — compiler proved safe
}
total
}
// $ verum analyze --escape
// sum_ages: 4 / 5 references promoted to &checked (80 %)
One example. Four unique features.
Refinement types in the signature. Explicit context dependencies. Structured concurrency with cancellation. A postcondition the compiler proves via SMT. No runtime cost for any of it.
// 1. Types carry invariants — the compiler enforces them
type Port is Int { 1 <= self && self <= 65535 };
type NonEmpty<T> is List<T> { self.len() > 0 };
// 2. Dependencies are visible — no hidden globals
async fn serve(routes: NonEmpty<Route>) -> Result<(), Error>
using [Logger, Config]
{
let port: Port = Config.get_int("port").unwrap_or(8080);
Logger.info(f"listening on :{port}");
// 3. Structured concurrency — no task outlives its scope
nursery(on_error: cancel_all) {
for route in routes.iter() {
spawn accept_loop(route.clone());
}
}
}
// 4. Verification is gradual — same function, stronger proof
@verify(formal)
fn find<T: Eq>(xs: &NonEmpty<T>, key: &T) -> Maybe<Int>
where ensures result.is_some() => xs[result.unwrap()] == *key
{
for i in 0..xs.len() {
if xs[i] == *key { return Maybe.Some(i); }
}
Maybe.None
}
Under the surface
Research brought to production — compiled, linked, and shipped as a single binary.
Refinement types in the type system
Int { self > 0 }, List<T> { self.is_sorted() }, Text { self.matches(rx#"...") }. Predicates checked by SMT, erased at runtime. Not a linter — a type.
Proof-carrying code
VBC archives embed proof certificates. Downstream consumers verify offline without re-running the compiler. Exportable to Coq, Lean, Dedukti, Metamath.
Dependent types for shape safety
Tensor<T, [B,H,L,D]> with compile-time matmul shape checks. Path types and cubical HoTT for equational reasoning. Proof terms erased before codegen.
14 compile-time meta-contexts
TypeInfo, AstAccess, CodeSearch, Schema, DepGraph, Hygiene + 8 more — the same using [...] as runtime DI. 230+ methods across them, stage-aware, deterministic by construction.
8-capability monotonic references
CAP_READ, CAP_WRITE, CAP_EXECUTE, CAP_DELEGATE, CAP_REVOKE, CAP_BORROWED, CAP_MUTABLE, CAP_NO_ESCAPE. Capabilities only attenuate — never expand. One AND + one branch per check.
Pure-Verum standard library
No Rust runtime, no libc, no pthread. Syscalls, atomics, I/O, and clocks go through VBC opcodes directly (0xF1 / 0xF2 / 0xF4 / 0xF5). The CBGR allocator lives in core/mem — no malloc underneath.
22 proof tactics in a systems language
auto, simp, ring, field, omega, blast, smt, trivial, assumption, contradiction, induction, cases, rewrite, unfold, apply, exact, intro(s), cubical, category_simp, category_law, descent_check — plus combinators. When SMT can't, you help. No separate prover needed.
Interpreter and AOT from the same bytecode
VBC-first: instant startup via interpreter for dev, LLVM AOT for production. Same semantics, same CBGR, same context stack. verum run (instant) and verum build --release (0.85-0.95x C) are one flag apart.
Start with runtime checks. End with proofs.
Download the verum binary. Write a refinement type. Add @verify(formal). The compiler proves what your comments used to merely claim.