Formal verification for
quantum circuits

Write a circuit in Qiskit. State a property. Get a kernel-checked proof — or a concrete counterexample. Powered by Lean 4 + Mathlib.

The gap this fills

Quantum programs are difficult to test. A misplaced CNOT or a rotation angle off by a factor of two produces subtly wrong measurement statistics rather than a crash. The two existing options both fall short:

The trusted computing base is Lean's kernel (~3,000 lines of C++), not a simulation engine or a human. A STRUCT_PROVED verdict is a mathematical certificate.

The DSL: circuits, specs, proofs

Circuits are typed values. The qubit count is in the type — out-of-bounds indices are impossible at compile time.

import LeanQVerify

open LeanQVerify QCircuit CircuitSpec

-- A 2-qubit Bell-state preparation circuit
-- QCircuit 2 encodes the qubit count in the type
def myBell : QCircuit 2 :=
  .cons (.H ⟨0, by norm_num⟩)
  (.cons (.CNOT ⟨0, by norm_num⟩ ⟨1, by norm_num⟩)
  .empty)

Specs are first-class values. The ⊨ relation states that a circuit satisfies a spec:

-- Gate count: exactly 2 gates
theorem myBell_twoGates :
    myBell ⊨ .gateCount (fun _ => true) 2 := by
  simp [satisfies, countGates, myBell]

-- Depth: at most 2 layers
theorem myBell_depth :
    myBell ⊨ .maxDepth 2 := by
  simp [satisfies, depth, scheduleDepth, myBell, gateQubits]

-- Measurement probability: P(qubit 0 = 0 | |00⟩) = 1/2
theorem myBell_entangled :
    myBell ⊨ .measurementProb QState.ket00 0 false (1/2) :=
  bellPrep_entangled

Gate identities

Universal identities are proved once and reused. The H gate is its own inverse:

-- H ∘ H = I  (holds for all n qubits, any qubit index i)
theorem H_H_eq_id (n : ℕ) (i : Fin n) :
    (ofGate (.H i) ++ ofGate (.H i)) ≅ QCircuit.identity :=
  embedGate1_self_inverse n i H_mat_unitary

Quantum Hoare Logic

The library includes a Quantum Hoare Logic over density matrices. Predicates are PSD operators; the HoareTriple A c B type encodes the expectation-based semantics.

-- Gate rule: if U†·A·U holds before, A holds after
theorem H_gate_triple (A : QPred 1) :
    HoareTriple (A.conj _ H_gate1_unitary)
                (ofGate (.H ⟨0, by norm_num⟩)) A :=
  hoare_gate A _ H_gate1_unitary

ZX-calculus

ZX diagrams are a first-class type. The spider fusion rule and certified circuit translation are both proved.

-- Spider fusion: Z(α) ⊚ Z(β) = Z(α+β)
theorem zSpider_fusion (α β : ℝ) :
    ZX⟦zSpider α ⊚ zSpider β⟧ = ZX⟦zSpider (α + β)⟧ := ...

-- Circuit translation is semantics-preserving
theorem circuitToZX₁_sound (c : QCircuit 1) (hc : isStdCircuit₁ c) :
    ZX⟦circuitToZX₁ c⟧ = c.denote := ...

Python bridge

Circuits written in Qiskit export to OpenQASM 3, which the Lean parser converts into a typed QCircuit n value. Structural specs are proved automatically — no Lean required.

from qiskit import QuantumCircuit
from lean_qverify import verify_circuit_spec, CircuitSpec

qc = QuantumCircuit(2)
qc.h(0)
qc.cx(0, 1)

# Structural spec: automatically proved by Lean's kernel
result = verify_circuit_spec(qc, CircuitSpec.gate_count(total=2))
print(result.verdict)         # STRUCT_PROVED
print(result.kernel_checked)  # True

Structural specs (gate count, CNOT count, depth) are proved fully automatically. Measurement-probability proofs require a hand-written Lean file — the bridge emits the theorem statement; you provide the proof.

# Check the QASM the parser will see
result = verify_circuit_spec(qc, CircuitSpec.max_depth(bound=2))
if result.warnings:
    print(result.warnings)  # unrecognised angles, unsupported gates

The trusted pipeline: Qiskit → OpenQASM 3 → Lean parser → theorem file → lake env lean. When kernel_checked is True, Lean's kernel accepted every proof step.

Install

require «lean-qverify» from git
  "https://github.com/akkeshavan/lean-qverify" @ "v0.1.0.0"

git clone https://github.com/akkeshavan/lean-qverify.git
cd lean-qverify
pip install -e .          # CPU counterexample search
pip install -e ".[gpu]"   # + GPU support (CUDA 12, Linux only)

lake update          # resolve Mathlib dependency
lake exe cache get   # download prebuilt Mathlib oleans (~500 MB)
lake build           # compile the library (~5 min)

Links