A programming language designed for the AI age. Every program either proves itself correct or doesn't compile. No runtime errors. No security vulnerabilities. No ambiguity.
Current languages were designed for humans to write and machines to execute. Nova is designed for AI to write and machines to verify.
Runtime errors crash production systems unexpectedly
Errors are impossible by construction
Security vulnerabilities everywhere
Capabilities prevent unauthorized access
10x abstraction overhead in modern languages
Direct hardware mapping for maximum efficiency
AI generates buggy, unverified code
AI generates mathematically verified code
Five irreducible principles that guide every design decision.
Every program either proves itself correct or doesn't compile. No exceptions.
Code can only access what it's explicitly given. No ambient authority, no hidden permissions.
Optimized for LLMs to generate: minimal syntax, zero ambiguity, maximum verifiability.
The compiler is written in Nova. We eat our own dogfood from day one.
Everything is open source: the spec, the compiler, the tools, the governance.
No garbage collector, no runtime. Direct compilation to WebAssembly and native code.
The compiler proves these properties at compile time. If the implementation doesn't satisfy them, it won't compile.
// A function that sorts a list // The compiler PROVES these properties: // - Output has same length as input // - Output is sorted // - Output is a permutation of input fn sort(input: Vec<i32>) -> Vec<i32> where ensures output.len() == input.len(), ensures output.is_sorted(), ensures output.is_permutation_of(input), { // Implementation here // If it doesn't satisfy the properties, // it won't compile }
From source to verified WebAssembly in four steps.
Express your intent with clear syntax and explicit contracts.
The type system proves your code satisfies all contracts.
Verified code is lowered to efficient intermediate representation.
Output compact, fast WebAssembly that runs anywhere.
Nova is open source and community-driven. Help us build the language of the AI age.