Deterministic memory safety without garbage collection pauses. Mathematical formal verification powered by the Microsoft Z3 SMT prover. Bare-metal hardware parity with C/C++.
Nova unifies the ergonomic safety of Rust, the raw execution speed of C, and the mathematical rigor of formal verification.
Zero garbage collection. When an object's reference count is 1, mutations execute destructively in place without allocating new memory chunks, eliminating runtime latency spikes.
Compile-time formal verification via Microsoft Z3. Array bounds, non-zero division, and buffer invariants are mathematically proven before your program ever runs.
Memory isolation is enforced by the type system through iso, val, and ref capabilities, eliminating data races at compile time.
First-class raw pointers (*mut T, *const T), inline assembly, and direct FFI integration for writing kernels, hypervisors, and high-frequency trading engines.
Clean syntax, declarative semantics, and provable safety invariants built right into the language.
High-performance systems language comparison across memory footprint, latency, and throughput.
| Language | Memory Model | GC Pause Time | Formal SMT Verification | Self-Hosted Pure Compiler |
|---|---|---|---|---|
| 🌌 Nova v0.32.12 | Perceus In-Place Reuse | 0.0 ms (Deterministic) | ✓ Microsoft Z3 Native | 100% Pure Nova |
| Rust 1.76 | Affine Borrow Checker | 0.0 ms (Deterministic) | Manual (Kani / Creusot) | Self-Hosted (Rust) |
| C++23 (Clang 18) | Manual / RAII | 0.0 ms (Manual Free) | None | C++ |
| Go 1.22 | Tricolor Tracing GC | 0.8 ms - 2.5 ms (Concurrent) | None | Go |
| Zig 0.12 | Explicit Allocators | 0.0 ms (Manual) | None | Self-Hosted (Zig) |
A multi-repository architecture modeled after modern language ecosystems like rust-lang.
Official package manager, deterministic dependency resolver, and build orchestration toolchain for Nova.
Language Server Protocol (LSP 3.17), Tree-Sitter grammar, and official VS Code editor extension.
The official mdBook guide covering Perceus memory, SMT verification, concurrency, and bare-metal programming.
Interactive in-browser code editor powered by Monaco, WebAssembly, and live Z3 theorem verification.
Official language evolution process, architectural specifications, and community design proposals.
Developer utility suite including code formatter (nova-fmt), linter (nova-lint), docgen, and interactive REPL.
Minimal, sub-microsecond Perceus chunk allocator, lock-free atomics, and POSIX/Winsock transport engine.
A curated collection of libraries, frameworks, operating system kernels, and community showcases.
