Write in Leaf, prove with Lean. Quantum Programming 🍃⚡

About

• A statically typed quantum programming language with Rust-like syntax and conservative quantum extensions that preserve the look and feel of Rust.
• Linear qubit ownership and mutable borrowing: no-cloning and qubit-use discipline are enforced statically by the type checker.
• Safe ancilla management, with support for automatic uncomputation.
• Lightweight quantum contracts for tracking properties of entanglement for program qubits at compile time.
• Designed for formal verification, with program properties proved in Lean 4 against a type-safe intermediate representation.
• Detailed diagnostics designed for both human developers and AI-assisted code generation.
• Practical by construction: compiles to OpenQASM 3, with QIR support planned.
• Built for the fault-tolerant quantum computing era.

Code example:

general fn coin_flip() -> bit {
    let q = qalloc();
    H(&q);
    measr(q)
}

general fn main() -> bit {
    coin_flip()
}

Docs

Documentation

Progress Status

Capability	Status
Language Design & Docs	Implemented
Lexer	Implemented
Parser	Implemented
Surface AST	Implemented
Post-Parse Validation	Implemented
De-sugaring & Canonical AST	Implemented
Scope & Name Resolution	In progress
Type Checker & Typed AST	Planned
Quantum Lambda Calculus IR	Planned
Lambda Calculus Code Generator	Planned
Idris2 DSL	Protoype
Idris DSL Lowering Pass	Planned
OpenQASM 3 Serializer	Protoype
Alpha release	Fall 2026
Lean Interface	Planned

Todo

Pending Features

Contributing

See CONTRIBUTING.md for contribution guidelines.