Code that proves itself.
A programming language designed for the AI age.
Verified. Efficient. Open.
We're building a new programming language from scratch—not because the world needs another language, but because the world needs a different kind of language.
Current languages were designed for humans to write and machines to execute. Nova is designed for AI to write and machines to verify. The result: code that is mathematically proven correct, dramatically more efficient, and impossible to exploit.
Read the full story: The Credit Card Bug That Started It All →
| Today's Reality | Nova's Vision |
|---|---|
| Runtime errors crash production | Errors are impossible by construction |
| Security vulnerabilities everywhere | Capabilities prevent unauthorized access |
| 10x abstraction overhead | Direct hardware mapping |
| AI generates buggy code | AI generates verified code |
| Humans debug machine output | Machines prove human intent |
-
Correctness is not optional. Every program either proves itself correct or doesn't compile.
-
Capabilities, not permissions. Code can only access what it's explicitly given. No ambient authority.
-
AI-native. Optimized for LLMs to generate: minimal syntax, zero ambiguity, maximum verifiability.
-
Self-hosting is day one. The compiler is written in Nova. We eat our own dogfood immediately.
-
Radical openness. Everything is open source. The spec, the compiler, the tools, the governance.
// 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
}
flowchart LR
A[".nova"] --> B["Lexer"]
B --> C["Parser"]
C --> D["Type Checker"]
D --> E["Verifier"]
E --> F["IR"]
F --> G["Codegen"]
G --> H[".wasm"]
style A fill:#1e293b,stroke:#334155,color:#f8fafc
style B fill:#0ea5e9,stroke:#0284c7,color:#fff
style C fill:#a855f7,stroke:#9333ea,color:#fff
style D fill:#ec4899,stroke:#db2777,color:#fff
style E fill:#ec4899,stroke:#db2777,color:#fff
style F fill:#f97316,stroke:#ea580c,color:#fff
style G fill:#22c55e,stroke:#16a34a,color:#fff
style H fill:#1e293b,stroke:#22c55e,color:#22c55e
See docs/DIAGRAMS.md for more architecture diagrams.
🚧 Stage 0: Bootstrap — Building the minimal Rust compiler that will compile the first Nova compiler.
| Component | Status | Tests | Notes |
|---|---|---|---|
| Lexer | ✅ Complete | 25 | Full tokenization with span tracking |
| Parser | ✅ Complete | 30 | Pratt parsing, full expression support |
| Span | ✅ Hardened | 15 | 8-byte struct, adversarial tested |
| Token | ✅ Hardened | 25 | 12-byte struct, adversarial tested |
| Types | 🚧 In Progress | 1 | Basic type checking |
| IR | 🚧 In Progress | - | SSA-based intermediate representation |
| Codegen | 🚧 In Progress | - | WebAssembly output |
91 tests passing • 40 adversarial security tests • Compile-time size guarantees
See bootstrap/README.md for contributor guide.
See ROADMAP.md for the full plan.
| Document | Description |
|---|---|
| WHY-NOVA.md | The origin story and capability-based security |
| ROADMAP.md | Development stages and milestones |
| COMPONENTS.md | 43-component architecture with QA criteria |
| FOUNDATION.md | The 5 irreducible foundation components |
| DECISIONS.md | Architectural decisions with rationale |
| CONTRIBUTING.md | How to contribute |
| GOVERNANCE.md | BDFL model and approval process |
| docs/DIAGRAMS.md | Architecture diagrams (Mermaid) |
| docs/brand/BRAND.md | Brand guidelines and assets |
We're looking for contributors! Nova is designed to be built by a community.
See CONTRIBUTING.md for how to get started.
nova/
├── bootstrap/ # Rust bootstrap compiler (temporary)
├── stage1/ # Nova compiler written in Nova
├── std/ # Standard library
├── spec/ # Language specification
├── tools/ # LSP, formatter, etc.
└── examples/ # Example programs
- Rust 1.75+ (for bootstrap only)
- LLVM 17+ (for native codegen)
cd bootstrap
cargo build --release./target/release/nova compile examples/hello.nova -o hello.wasmcargo testNova uses a BDFL (Benevolent Dictator for Life) governance model.
- All PRs require approval from @pdaxt before merge
- See GOVERNANCE.md for details
- Contributors can open issues, PRs, and participate in discussions
- Discord: Join our Discord (coming soon)
- Discussions: GitHub Discussions
- Twitter/X: @nova_lang (coming soon)
Nova is dual-licensed under MIT and Apache 2.0. See LICENSE-MIT and LICENSE-APACHE.
Nova stands on the shoulders of giants:
- Rust — Memory safety without GC
- Lean — Dependent types and proofs
- Zig — Simplicity and control
- LLVM — Production-grade codegen
Nova: Code that proves itself.