Verified Heterogeneous
Systems Programming
A zero-dependency, sub-megabyte language engineered for bare-metal performance, unified memory architectures, and Z3‑proven correctness. No runtime, no compromises.
powershell -c "irm
https://raw.githubusercontent.com/sufiytv-dev/Voxlang/main/install.ps1
| iex"
Z3‑Backed Verification
Refinement types with SMT solving. Preconditions, postconditions, and invariants checked at compile time — no proof annotations required.
Zero Runtime Panics
No unwrap(), no exceptions, no hidden crashes. Every failure path is either handled or proven unreachable. Deterministic binaries only.
Sovereign Infrastructure
Toolchain <5MB, zero external runtime, no telemetry, no package manager spyware. What you build is yours.
The Sovereign Manifesto
✔ Zero telemetry – The compiler never phones home. No crash reports, no analytics, no background noise.
✔ No corporate steering – Voxlang is not backed by any foundation, ad-driven roadmap, or vendor lock-in. Architecture first, marketing second.
✔ Independent verification – Every safety claim is proven by Z3, not promised in a blog post. You can read the proof.
— Built for people who need guarantees, not trends.
The Compiler That Refuses to Guess
Unverifiable code → rejected. No warnings, only errors.
fn unsafe_write(buf: &mut [u8], idx: i32, val: u8) where idx < len(buf):
# Z3 cannot prove 'idx >= 0' at compile time
buf[idx] = val
}
fn main():
let mut data = [0u8; 10]
let index = get_user_input() # unknown integer
unsafe_write(data, index, 255) # ❌ REFUSED BY VERIFIER
$ vox build buggy_buffer.vx
error[Z3-0001]: unproven refinement constraint
--> buggy_buffer.vx:2:28
|
2 | fn unsafe_write(buf: &mut [u8], idx: i32, val: u8) where idx < len(buf):
| ^^^
|
= note: Z3 solver could not prove `idx >= 0` given caller context
= help: add explicit precondition: `where idx >= 0 and idx < len(buf)`
= note: build aborted — verification failed
⛔ No binary generated. Compiler is sound.No runtime panics. No silent truncation. Only mathematically verified paths.
First‑class heterogeneous compute
Write GPU kernels in Voxlang — same syntax, same verifier. AMD ROCm & CUDA backends.
Compile‑time introspection
Run arbitrary Vox code during compilation. Generate types, unroll loops, and inspect memory layouts — zero runtime overhead.
Zero‑cost C bridge
Import any C header. Safe wrappers, null checks, and ownership tracking generated on the fly.