lean-qverify v0.2.1

Patch release to register artifact with Zenodo DOI. Functionally identical to v0.2.0.

v0.2.0 — Stabilizer backend + verify_prob semantic automation

What's new

Verified stabilizer backend (Phase 2)

A fully-proved Aaronson-Gottesman tableau simulator for Clifford circuits.

• Stabilizer/StabTableau.lean -- 2n-row Boolean tableau; stepH/S/X/Z/CNOT; stabSim
• Stabilizer/Sound.lean -- stabSim_correct (core refinement theorem); zProb_correct; verify_stabilizer_prob_sound (unconditional, no hnorm)
• Stabilizer/CliffordGate.lean -- CliffordGate inductive; ofQCircuit? classifier + soundness
• Stabilizer/PauliGroup.lean -- Pauli group; Clifford conjugation lemmas

One known remaining sorry: zProbDet_eigenvalue (Z_q eigenstate claim for the deterministic measurement branch).

Benchmarks: GHZ(n) for n=1..200 all pass native_decide; n=200 in ~13s confirming O(n^2) scaling.

verify_prob tactic (Phase 1 + 2)

One tactic closes measurement-probability goals automatically:

-- Bell circuit
example : QCircuit.bellPrep |= .measurementProb QState.ket00 0 false (1/2) := by
  verify_prob

-- 100-qubit GHZ via stabilizer backend
example : (ghzCliffordCircuit 99).toQCircuit |=
    .measurementProb (ket0Vec 100, ket0Vec_norm 100) (0, by omega) false (1/2 : R) := by
  verify_prob

Clifford circuits dispatch to the stabilizer tableau backend (O(n^2)). Other circuits use the dense gate-by-gate evaluator.

Book chapter 8 updated

verify_prob one-liners for Bell/GHZ/Grover and a 100-qubit GHZ stabilizer proof. All 12 chapters build clean.

Documentation

• ARCHITECTURE.md: new 7.6 (verify_prob dispatch) and 7.7 (stabilizer backend design)
• README.md: theorem table split into structural/semantic; Stabilizer/ and Tactic/ added to layout
• FUTURE_WORK.md removed; replaced by SEMANTIC_ROADMAP.md

Using this release

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

Previous release

v0.1.0.0 -- foundation, ZX-calculus, QHL, Python bridge, 40 kernel-checked theorems

v0.1.0.0 — Quantum Hoare Logic, ZX-calculus, 40 theorems

lean-qverify v0.1.0.0

Formal verification of quantum circuits using Lean 4 + Mathlib. First release: 40 kernel-checked theorems, a 12-chapter interactive book, Python bridge from Qiskit, and a structural spec prover.

New in this release

Core library

• LeanQVerify/Foundation/HoareLogic.lean — Quantum Hoare Logic: QPred, HoareTriple, skip/gate/seq/consequence rules
• LeanQVerify/ZX/ — ZX-calculus: spider diagrams, fusion rule, π-copy rule, certified circuit translation
• LeanQVerify/Circuit/Parametric.lean — parametric circuit families
• New gates: U3, CH, CY, CP, CRZ, RZZ, RXX, RYY with full matrix proofs

Python bridge

• lean_qverify/prover.py — automated structural spec prover (GATE_COUNT, CNOT_COUNT, RZ_COUNT, MAX_DEPTH)
• verify_circuit now returns Verdict.PARSED for a successful parse
• result.ok includes PARSED and WARNING; kernel_checked stays narrow

Book (12 chapters, compiled PDF at book/book.pdf)

• Chapter 11: Quantum Hoare Logic with worked H-gate triple
• Chapter 12: ZX-calculus with spider rules and circuit soundness

Benchmarks — 32 QASM circuits across Bell, GHZ, Grover, QAOA, VQE, and more

Using as a Lean dependency

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

Install the Python bridge

pip install -e .

Verified theorems

40 kernel-checked theorems, no sorry in any proof tree. Core 38 are independently verifiable via the theorems/ folder.