Fanal Documentation
Fanal is a Lean 4 toolchain for formalizing, verifying, and reasoning about quantum programs.
Expressive and practical
Classical-quantum language with native support for both classical and quantum operations, plus array support.
Usable
Intuitive proofs with automation. Language design understandable by both humans and AI agents.
AI-friendly
Agent-assisted development (Steward workflow) and agent-assisted usage (fanal-user skill, Galleon pipeline).
Reusable
Specification-driven development. Descriptive/Supportive code separation for maintainability.
Roadmap
Example Crawling
Database, web crawler, auto-encoder, evaluation metrics
Dirac Reasoning
D-Hammer decision procedure, dirac_eq/ldirac_eq, Loewner order
Program Encoding
Classical-quantum programming language, syntax/typing/semantics
Program Verification
Assertion language, program logic (Hoare logic), Shor's algorithm (final goal)
Quick Start
Install Lean 4 via elan
curl https://elan.readthedocs.io/en/latest/elan-init.sh -sSf | shClone the repository
git clone https://github.com/LucianoXu/Fanal.git
cd FanalBuild the project
lake build FanalAfter building, explore the FanalExample/ directory for verified quantum programs you can modify and experiment with.
Novel Abilities & Contributions
Hierarchical Access Path Register Model
Unique register addressing with value-dependent labels (arrayIdx).
Learn more →Descriptive/Supportive Code Separation
Human-readable formalization separated from AI-generated proofs.
Learn more →Certified dirac_eq Automation
7-strategy fallback tactic for automated equational reasoning, no sorry.
Learn more →Galleon Auto-Formalization Pipeline
Agent-powered web crawler + encoder for quantum computing examples.
Learn more →Specification-Driven + AI-Native Development
Steward workflow with parallel sub-agents.
Learn more →Comparison with Existing Tools
| Tool | System | Focus | Proof Certificates | Automation |
|---|---|---|---|---|
| CoqQ | Coq / MathComp | Labelled Dirac + qwhile + Hoare logic | Yes | Low |
| SQIR / VOQC | Coq / QuantumLib | Verified circuit optimization | Yes | Low–Medium |
| Lean-QuantumInfo | Lean 4 / Mathlib | Quantum information theory | Yes | Low |
| QBricks | Why3 / SMT | Circuit-building program verification | Partial | High (94%+) |
| Qafny | Dafny / Z3 | Separation logic for quantum programs | No | High |
| AutoQ 2.0 | C++ standalone | Tree-automata automatic verification | None | Very High |
| D-Hammer | C++ / Mathematica | Automated Dirac equational reasoning | None | Very High |
| Fanal | Lean 4 / Mathlib | Foundational quantum program formalization | Yes | Medium (developing) |