Quantum programs, formally verified

Fanal is a Lean 4 library for foundational formalization, verification, and compilation of quantum programs. Write Dirac notation. Prove correctness. Ship with confidence.

Get StartedGitHub
Textbook
∑i∣i⟩⟨i∣  =  I\sum_i \vert i \rangle \langle i \vert \;=\; I

Completeness relation — QCQI Postulate 2

Fanal / Lean 4
example :
    ⟦ Σ_{i ∈ univ[T]} |i⟩ ⬝ ⟨i| ⟧ ≈ₕ
    ⟦ I[T] ⟧ := by
  dirac_eq
Verified by Lean

Why Fanal?

𝛴

Expressive

Write quantum programs with Dirac notation — bras, kets, tensor products, and operator sums — directly in Lean 4 syntax.

✓

Verified

Every identity is machine-checked. The dirac_eq tactic automates equational reasoning over the Hilbert-space algebra.

⚙

AI-Friendly

Galleon, the auto-formalization pipeline, continuously harvests textbook results and encodes them as verified Lean theorems.

Featured Examples

Textbook quantum-information results, encoded and verified in Fanal.

Entanglement

Bell State

Prepare and verify the maximally entangled Bell state |Φ⁺⟩ = (|00⟩ + |11⟩) / √2.

QCQI-7

Completeness Relation

The resolution of identity Σᵢ |i⟩⟨i| = I, proven in one tactic invocation.

Algorithm

Deutsch-Jozsa

The first quantum algorithm to demonstrate exponential speedup over classical deterministic computation.

206materials archived
160examples encoded
0verified