Formal methods for quantum research workflowsworking paper
Exploring how Lean, Coq, Isabelle/HOL, Z3, and TLA+ could complement tools such as Qiskit, PennyLane, Braket, and QuTiP — from mathematical specifications and proofs to circuit verification and the infrastructure coordinating classical and quantum execution.