Vanadium

Ada-level runtime safety for the V programming language.

vanadium adds range-checked integers, strong types, bounded lists, safe variables, checked arithmetic, design-by-contract, timing attack protection, hardware attack mitigations, and control flow integrity to V programs. Every operation that can fail returns a V result type, making it impossible to silently ignore errors.

What it catches

Bug class	Plain V	V + vanadium
Integer overflow/underflow	Silent	Error
Division by zero	Crash	Error
Array index out of bounds	Panic	Error
Uninitialized variable access	Zero/empty	Error
Buffer beyond capacity	Unlimited	Error
Value outside logical range	Nothing	Error
Mutation of frozen constant	Possible	Error
Invalid input to function	Manual	Automatic
Mixing incompatible units	Silent	Error
NaN / Infinity propagation	Silent	Error
Nonce reuse	Silent	Error
Stack overflow via recursion	Crash	Error
Out-of-order execution flow	Silent	Error
Memory corruption (bit-flip)	Silent	Error
Buffer overflow (canary)	Silent	Error
Sensitive data in freed memory	Remains	Wiped
Timing side-channel	Leaks	Constant-time
Spectre (speculative execution)	Leaks	Branchless
Weak entropy in random data	Silent	Error
Fault injection (voltage glitch)	Silent	Detected

Quick start

import vanadium

fn main() {
    // Integer that must stay between 1 and 12
    mut month := vanadium.RangedInt.create(1, 12, 3) or {
        eprintln(err)
        return
    }
    month.assign(13) or { eprintln(err) } // Constraint_Error

    // Strong types: meters and seconds cannot mix
    dist := vanadium.new_strong_i64('meters', 100)
    dur := vanadium.new_strong_i64('seconds', 10)
    dist.add(dur) or { eprintln(err) } // Type_Error

    // Speed = distance / time with explicit type conversion
    speed := vanadium.strong_div_i64(dist, dur, 'meters_per_second') or { return }
    println(speed) // 10 [meters_per_second]

    // List with max 3 elements, 1-based indexing
    mut names := vanadium.new_safe_list[string](3) or { return }
    names.append('ben') or { eprintln(err) }
    names.append('mark') or { eprintln(err) }
    names.append('jack') or { eprintln(err) }
    names.append('sarah') or { eprintln(err) } // Capacity_Error
    println(names.at(1) or { return }) // ben

    // Variable that must be initialized before use
    mut x := vanadium.new_safe_var[int]('x')
    x.get() or { eprintln(err) } // Access_Error
    x.set(42) or {}
    println(x.get() or { return }) // 42

    // Overflow-checked math
    vanadium.safe_add_i32(2000000000, 2000000000) or {
        eprintln(err) // Overflow_Error
    }
}

API reference

RangedInt

Integers constrained to a min..max range. Every mutation is checked.

mut r := vanadium.RangedInt.create(min, max, initial)!

r.value() i64              // read current value
r.assign(v)!               // set new value (checked)
r.in_range(v) bool         // test if v is in range

r.checked_add(v)!          // addition with overflow + range check
r.checked_sub(v)!          // subtraction
r.checked_mul(v)!          // multiplication
r.checked_div(v)!          // division (also checks zero)

r.str() string             // "5 in [1..12]"

Example:

mut temp := vanadium.RangedInt.create(-40, 85, 22)!
temp = temp.checked_add(100) or {
    eprintln(err) // Constraint_Error: 22 + 100 = 122 not in -40..85
    return
}

SafeList

Bounded list with configurable index base and capacity limit.

mut list := vanadium.new_safe_list[T](capacity)!
mut list := vanadium.new_bounded_list[T](capacity, lower_bound)!

list.append(val)!              // add element (checked capacity)
list.append_many(vals)!        // add multiple
list.at(index)!                // read at index (checked bounds)
list.set_at(index, val)!       // write at index (checked bounds)
list.remove_at(index)!         // remove and return (checked)
list.first()!                  // first element
list.last()!                   // last element
list.pop()!                    // remove last
list.safe_slice(from, to)!     // sub-list (checked)
list.find(val) ?int            // search, returns index or none
list.contains(val) bool        // membership test
list.each(fn(idx, val))        // iterate with index
list.len() int                 // current length
list.is_empty() bool
list.is_full() bool
list.remaining_capacity() int
list.upper_bound() int         // highest valid index

SafeVar

Variable that cannot be read before initialization and can be frozen.

mut v := vanadium.new_safe_var[T]('name')
mut v := vanadium.new_safe_var_init[T]('name', val)

v.get()!                  // read (error if not initialized)
v.set(val)!               // write (error if frozen)
v.freeze()!               // make immutable
v.is_initialized() bool
v.is_frozen() bool

Example:

mut config := vanadium.new_safe_var_init[string]('db_host', 'localhost')
config.freeze()!
config.set('evil.com') or { eprintln(err) } // Frozen_Error

ValidatedVar

Variable with a custom validator function.

mut v := vanadium.new_validated_var[T]('name', validator_fn, 'error message')

v.set(val)!               // write (runs validator first)
v.get()!                   // read (error if not initialized)
v.is_initialized() bool

Example:

mut port := vanadium.new_validated_var[int](
    'port',
    fn (v int) bool { return v >= 1 && v <= 65535 },
    'must be 1..65535'
)
port.set(80)!      // ok
port.set(99999) or { eprintln(err) }  // Validation_Error

Checked arithmetic

All functions return result types. Silent overflow is impossible.

vanadium.safe_add_i64(a, b)!
vanadium.safe_sub_i64(a, b)!
vanadium.safe_mul_i64(a, b)!
vanadium.safe_div_i64(a, b)!
vanadium.safe_mod_i64(a, b)!

vanadium.safe_add_i32(a, b)!
vanadium.safe_sub_i32(a, b)!
vanadium.safe_mul_i32(a, b)!
vanadium.safe_div_i32(a, b)!

vanadium.safe_pow(base, exp)!
vanadium.safe_negate_i64(a)!
vanadium.safe_abs_i64(a)!
vanadium.clamp_i64(val, min, max) i64

Contracts

Design-by-contract functions for preconditions, postconditions, and invariants.

vanadium.require(condition, msg)!
vanadium.ensure(condition, msg)!
vanadium.check_invariant(condition, msg)!
vanadium.require_all(conditions, msgs)!
vanadium.safe_assert(cond, ctx, detail)!

Example:

struct Account {
mut:
    balance vanadium.RangedInt
}

fn withdraw(mut account Account, amount i64) ! {
    vanadium.require(amount > 0, 'amount must be positive')!
    vanadium.require(account.balance.value() >= amount, 'insufficient funds')!

    account.balance = account.balance.checked_sub(amount)!

    vanadium.ensure(account.balance.value() >= 0, 'balance must not be negative')!
}

Strong Types

Runtime-enforced type distinction. Prevents mixing incompatible units even when the underlying type is identical.

StrongI64 — tagged 64-bit integers:

d := vanadium.new_strong_i64('meters', 100)
t := vanadium.new_strong_i64('seconds', 10)

d.add(t) or { eprintln(err) }   // Type_Error: cannot add "meters" and "seconds"
d.add(vanadium.new_strong_i64('meters', 50))! // ok: 150 [meters]

// Cross-type operations with explicit result tag
speed := vanadium.strong_div_i64(d, t, 'meters_per_second')! // 10 [meters_per_second]

// Range-checked creation
alt := vanadium.new_strong_ranged_i64('altitude_m', 500, 0, 12000)!

d.raw()                    // i64 — explicit unwrap
d.convert('feet')          // re-tag (explicit conversion)
d.cmp(other)!              // -1, 0, 1 (type-checked)
d.eq(other)!               // equality (type-checked)

StrongF64 — tagged 64-bit floats with NaN/Infinity checking:

mass := vanadium.new_strong_f64('kg', 75.0)!
accel := vanadium.new_strong_f64('m_s2', 9.81)!

mass.add(accel) or { eprintln(err) }  // Type_Error

force := vanadium.strong_mul_f64(mass, accel, 'newton')!  // 735.75 [newton]

// NaN and Infinity are caught automatically
vanadium.new_strong_f64('ratio', 0.0 / 0.0) or { eprintln(err) }  // Arithmetic_Error: NaN

Complete operations for both StrongI64 and StrongF64:

Operation	Same tag required	Description
`a.add(b)!`	Yes	Addition
`a.sub(b)!`	Yes	Subtraction
`a.mul(b)!`	Yes	Multiplication
`a.div(b)!`	Yes	Division
`a.eq(b)!`	Yes	Equality
`a.cmp(b)!`	Yes (i64 only)	Comparison
`strong_div_*(a, b, tag)!`	No	Cross-type division
`strong_mul_*(a, b, tag)!`	No	Cross-type multiplication
`a.raw()`	—	Unwrap raw value
`a.convert(tag)`	—	Re-tag

SecureBuffer

Memory buffer that securely wipes its contents when cleared. Prevents cold boot attacks where RAM contents survive power-off.

mut buf := vanadium.new_secure_buffer(256)!

buf.write('secret_key'.bytes())!
buf.write_byte(0xFF)!
data := buf.read()!
b := buf.at(0)!
buf.len()

// Multi-pass wipe: zeros → 0xFF → pattern → zeros → verify
buf.clear()
buf.is_cleared()  // true

The clear() method performs a 4-pass overwrite (0x00, 0xFF, deterministic pattern, 0x00) followed by a read barrier to prevent compiler optimization from eliminating the writes. After clearing, the data array is emptied.

Use for: passwords, encryption keys, tokens, session secrets.

GuardedI64

Variable protected by canary values and bitwise complement. Detects both buffer overflows (canary corruption) and bit-flips (complement mismatch).

mut g := vanadium.new_guarded_i64(42)

val := g.get()!          // checks canaries + complement
g.set(100)               // resets all guards
g.verify()               // bool: quick integrity check

Memory layout:

[0xDEADBEEFCAFEBABE] [value] [~value] [0xFEEDFACEDEADC0DE]
       canary          data    guard          canary

If anything in this 32-byte region is overwritten by an adjacent buffer overflow or a bit-flip, get() returns Memory_Corruption error.

FlowGuard

Enforces a specific execution order for function calls. Detects control flow hijacking, out-of-order API calls, and skipped steps.

mut flow := vanadium.new_flow_guard(['authenticate', 'authorize', 'execute', 'log'])!

flow.step('authenticate')!   // ok
flow.step('execute') or { eprintln(err) }  // Flow_Error: expected "authorize", got "execute"
flow.step('authorize')!      // ok
flow.step('execute')!        // ok
flow.step('log')!            // ok

flow.verify_complete()!      // ok — all steps done

flow.current_step()          // "complete"
flow.progress()              // "4/4"
flow.reset()                 // start over

Use for: payment processing, authentication pipelines, multi-step protocols where skipping a step is a security vulnerability.

NonceTracker

Prevents cryptographic nonce reuse. A reused nonce in AES-GCM or ChaCha20-Poly1305 completely breaks the encryption.

mut nt := vanadium.new_nonce_tracker()

// Manual nonce management
nt.use_nonce(1001)!                  // ok
nt.use_nonce(1001) or { eprintln(err) }  // Nonce_Error: 1001 already used

// Auto-incrementing nonces
n1 := nt.next()   // 1, guaranteed unique
n2 := nt.next()   // 2

nt.is_used(1001)   // true
nt.count()         // 4

DepthGuard

Prevents stack overflow by tracking recursion depth.

mut dg := vanadium.new_depth_guard(100)!

fn recursive_parse(mut dg vanadium.DepthGuard, data string) ! {
    dg.enter()!      // error if depth > 100
    defer { dg.leave() }

    // ... recursive logic ...
}

dg.depth()        // current depth
dg.remaining()    // slots remaining

Use for: recursive parsers, tree traversal, any user-input-driven recursion where a malicious input could cause infinite depth.

Fault Injection Protection

Redundant checks — runs a condition 3 times and requires all 3 to agree. Detects voltage glitching attacks that cause a single check to return wrong result.

vanadium.redundant_require(fn () bool {
    return user.is_admin
}, 'admin check')!
// If glitch causes one of three checks to differ → Fault_Detected

Triple Modular Redundancy — runs a computation 3 times and returns the majority result.

// Integer TMR: majority vote, error if all 3 differ
result := vanadium.tmr_i64(fn () i64 {
    return compute_checksum(data)
})!

// Boolean TMR: 2-of-3 majority
is_valid := vanadium.tmr_bool(fn () bool {
    return verify_signature(msg, sig)
})

Entropy Validation

Validates that random data has sufficient entropy before use. Catches broken RNGs that output predictable data.

vanadium.validate_entropy(random_bytes, 0.5) or {
    eprintln(err) // Entropy_Error: ratio 0.031 below minimum 0.500
}

The min_unique_ratio parameter is the minimum ratio of unique byte values to total bytes (or 256, whichever is smaller). A ratio of 0.5 means at least half the possible byte values must appear.

Timing Attack Protection

Constant-Time Comparisons

// Always checks every byte, no early exit
vanadium.constant_time_eq_strings(user_input, real_token)
vanadium.constant_time_eq(bytes_a, bytes_b)

Constant Execution Time

mut guard := vanadium.new_timing_guard_ms(500)!
do_sensitive_work()
guard.pad()     // sleeps remaining time to hit exactly 500ms

// Or functional style
vanadium.timed_call_ms(500, fn () {
    do_sensitive_work()
})!

Timing Reports

report := guard.pad_report()
println(report)
// TimingReport{ exec: 120.00ms, pad: 380.00ms, total: 500.00ms, status: PADDED }

Hardware Attack Protection

Anti-Rowhammer: HardenedI64 / HardenedBool / HardenedRangedInt

Every value stored with its bitwise complement. Single bit-flip detected on every read.

mut is_admin := vanadium.new_hardened_bool(false)
is_admin.get() or { panic('bit-flip detected') }

mut counter := vanadium.new_hardened_i64(0)
counter = counter.checked_add(1)!

mut balance := vanadium.HardenedRangedInt.create(0, 99999999, 500000)!
balance = balance.checked_sub(100000)!

Anti-Spectre: Branchless Index Masking

safe_idx := vanadium.safe_index_mask(user_index, data.len)
val := data[safe_idx]  // no speculative out-of-bounds read

Performance Overhead

Type	Overhead	Use for
`HardenedI64`	~1 cycle	Crypto keys, counters
`HardenedBool`	~1 cycle	Permission flags
`HardenedRangedInt`	~3 cycles	Balances, critical bounds
`GuardedI64`	~2 cycles	Overflow-exposed variables
`safe_index_mask`	~3 cycles	Secret-indexed lookups
`SecureBuffer.clear`	~4 passes	Key material cleanup
`redundant_require`	3x check	Security-critical conditions
`tmr_i64`	3x compute	Fault-tolerant calculations

Error types

Prefix	Meaning
Range_Error	min > max when creating a range
Constraint_Error	value outside allowed range
Overflow_Error	arithmetic overflow or infinite float
Underflow_Error	arithmetic underflow
Division_Error	division or modulo by zero
Index_Error	list index out of bounds
Capacity_Error	list or buffer full / capacity invalid
Empty_Error	operation on empty list or buffer
Access_Error	read before initialization
Frozen_Error	write to frozen variable
Freeze_Error	freeze before initialization
Validation_Error	custom validator rejected value
Precondition_Failed	require() failed
Postcondition_Failed	ensure() failed
Invariant_Violated	check_invariant() failed
Assertion_Error	safe_assert() failed
Type_Error	operation between incompatible strong types
Arithmetic_Error	NaN result in float operation
Memory_Corruption	bit-flip or canary violation detected
Flow_Error	out-of-order step or incomplete flow
Nonce_Error	nonce reuse detected
Depth_Error	recursion depth exceeded
TMR_Error	all three redundant results differ
Entropy_Error	random data below quality threshold
Fault_Detected	inconsistent redundant check results
Timing_Error	invalid timing guard configuration

Usage pattern

Every function that can fail returns !T. You must handle the error:

// Handle and continue
val := list.at(5) or { default_value }

// Propagate to caller
val := list.at(5)!

// Handle and return
val := list.at(5) or {
    eprintln(err)
    return
}

The V compiler will not let you ignore the result type. This is the core safety guarantee.

Thread safety

All mutable operations are protected by read-write mutexes. Only one thread can write to a given SafeList, SafeVar, ValidatedVar, SecureBuffer, FlowGuard, NonceTracker, or DepthGuard at any time. Concurrent reads are safe.

Two threads cannot append to the same SafeList simultaneously.
A SafeVar.set() will not race with SafeVar.get().
freeze() is atomic across threads.
FlowGuard.step() is serialized — steps cannot be reordered by races.
NonceTracker.next() never produces duplicate nonces across threads.

If you need lock-free performance in a hot loop, copy the value out of the protected type, compute, then write back.

Performance

All functions use @[inline] attributes. Range checks add one comparison and branch per operation. The _unlikely_ hint on error paths helps the branch predictor keep the fast path in the instruction cache.

Mutex acquisition on uncontended locks is typically under 20 nanoseconds on modern hardware.

For tight loops where you have already validated the range, use plain V operations. Use vanadium at boundaries: user input, configuration, protocol parsing, financial calculations.

When not to use vanadium

Tight inner loops with millions of iterations where the range has already been validated. Validate once, then use plain V inside.
Performance-critical hot paths where nanoseconds matter (audio processing, game physics, HFT inner loops). Profile first.
Cases where V already checks. V's built-in array access panics on out-of-bounds. If a panic is acceptable and you don't need bounded capacity, the built-in may be enough.
Trivial scripts. If the program runs once with trusted input and errors don't matter, the ceremony is unnecessary.

Rule: use vanadium at trust boundaries and for critical data. Use plain V for validated, internal, hot-path code.

Debug and Release Modes (for proof)

vanadium includes a bounded testing system for verifying properties over finite ranges. These are exhaustive tests over a specified range, not formal mathematical proofs.

Note: "prove" in this API means "test exhaustively over a bounded range." If a property holds for all tested inputs, it is likely correct, but not mathematically proven for all inputs.

All proof functions have zero overhead in release builds. The compiler flag determines what runs.

Build Commands

v -g run main.v       # debug: all proofs execute
v -prod run main.v    # release: proofs removed, guards remain

Example

import vanadium

fn main() {
    mut p := vanadium.new_prover('math properties')

    p.prove_for_range('double is non-negative', 0, 500, fn (x i64) bool {
        return x * 2 >= 0
    })

    p.prove_commutative('addition', -20, 20, fn (a i64, b i64) i64 {
        return a + b
    })

    p.prove_injective('triple', 0, 100, fn (x i64) i64 {
        return 3 * x
    })

    println(p.report())
    if !p.all_passed() {
        println('proof failure')
        return
    }

    // State machine — step() always active
    mut sm := vanadium.new_state_machine('door', 0)
    sm.add_state(0, 'closed')
    sm.add_state(1, 'open')
    sm.add_transition(0, 1)
    sm.add_transition(1, 0)
    sm.step(1) or { println(err) }
    sm.step(0) or { println(err) }
}

Writing Tests

fn test_example() {
    mut p := vanadium.new_prover('test')
    p.prove_for_range('positive', 1, 100, fn (x i64) bool {
        return x > 0
    })
    assert p.all_passed()
    $if debug {
        assert p.results.len == 1
        assert p.results[0].passed
    }
}

Run tests

v test vanadium/

Limitations

Feature	Vanadium	Ada/SPARK
Runtime range checking	Yes	Yes
Runtime overflow detection	Yes	Yes
Design by contract	Yes	Yes
Strong type distinction	Yes (runtime, tag-based)	Yes (compile-time)
Compile-time range proof	No (bounded testing available)	Yes (SMT solver)
Formal verification	No (bounded testing available)	Yes (SPARK prover)
Thread safety	Yes (mutex-based)	Yes
Anti-hardware attacks	Yes	No (not built-in)
Timing attack protection	Yes	No (not built-in)

vanadium catches bugs at runtime and can test properties over bounded ranges during development. Ada and SPARK can mathematically prove the absence of entire bug classes at compile time. The strong type system in vanadium uses runtime tag comparison whereas Ada enforces type distinction at compile time with zero runtime cost.

For most applications, runtime checking with bounded testing is sufficient. For avionics, medical devices, or nuclear systems, use Ada/SPARK.

Name		Name	Last commit message	Last commit date
Latest commit History 2 Commits
src		src
vanadium		vanadium
.gitignore		.gitignore
LICENSE		LICENSE
README.md		README.md

Folders and files

Latest commit

History

Repository files navigation

Vanadium

Table of Contents

What it catches

Quick start

API reference

RangedInt

SafeList

SafeVar

ValidatedVar

Checked arithmetic

Contracts

Strong Types

SecureBuffer

GuardedI64

FlowGuard

NonceTracker

DepthGuard

Fault Injection Protection

Entropy Validation

Timing Attack Protection

Constant-Time Comparisons

Constant Execution Time

Timing Reports

Hardware Attack Protection

Anti-Rowhammer: HardenedI64 / HardenedBool / HardenedRangedInt

Anti-Spectre: Branchless Index Masking

Performance Overhead

Error types

Usage pattern

Thread safety

Performance

When not to use vanadium

Debug and Release Modes (for proof)

Build Commands

Categories

Example

Writing Tests

Run tests

Limitations

License

About

Resources

License

Uh oh!

Stars

Watchers

Forks

Releases

Packages 0

Uh oh!

Contributors

Uh oh!

Languages

Packages