Skip to main content
Quantum code has its own class of bugs that pass type checks, compile without warnings, and produce circuits that look correct until you study the density matrix. b01t is a Python DSL that catches these bugs at build time, so you find them in your editor instead of your lab results.

​
The problem with existing frameworks

When you write a quantum circuit in Qiskit, Cirq, or Q#, the framework trusts you to manage ancilla qubits correctly. An ancilla is a helper qubit — you borrow it, use it to do some work, and return it to |0⟩ so it does not entangle with the rest of the system. If you get the uncomputation wrong, the ancilla becomes dirty: it stays entangled with your system qubits, and your supposedly unitary program silently becomes a mixed channel instead. The circuit compiles, the job runs, and nothing tells you something went wrong. Three bugs cause most of these failures:
  • Dirty ancillae — an ancilla qubit is not returned to |0⟩ after use, leaving it entangled with system qubits
  • Bad uncomputation — the inverse of the compute block is wrong or missing, so the ancilla is not correctly disentangled
  • Silent decoherence — a gate that creates superposition is used in a context that requires a permutation gate, turning a unitary channel into a mixed one
All three pass silently in every existing framework. You only discover them by simulating the density matrix, which does not scale.

​
How b01t solves this

b01t is a Python DSL built around a closed gate set and a structural discipline for ancilla use. Every @coherent function must route its ancilla operations through three named blocks:
  • compute — classical-reversible gates only (X, CX, CCX, MCX). These copy system information into the ancilla.
  • phase — diagonal gates only (Z, S, T, CZ, CCZ, MCZ). These apply a phase kickback.
  • uncompute — auto-generated inverse of the compute block.
The restrictions on each block are what make the Hero Theorem possible: every well-typed @coherent program is a proven unitary channel. The proof is machine-checked in Lean 4 and does not rely on simulation. If your program builds without a DSLValidationError, it is safe by construction.

​
The Hero Theorem in practice

When you call .build_exact() on a @coherent function, b01t constructs an ExactProgram and checks it against the structural rules. If all checks pass, the returned program carries Certification.SAFE — a static certificate that the program is a unitary channel, ancilla-clean, and free from the three bug classes above. You can inspect the certificate directly: 
assert prog.certification == Certification.SAFE  # proven unitary, no simulation

​
Catching a real mistake

Here is the bug every quantum programmer writes at least once. The intent is to use an ancilla to apply a phase kickback, but the compute block uses h (Hadamard) instead of a permutation gate: 
from b01t import coherent, QReg, h, z
from b01t.kit import ancilla, compute, phase, uncompute

@coherent
def broken(sys: QReg):
    with ancilla(1) as anc:
        compute(lambda: h(anc[0]))  # "just put it in superposition"
        phase(lambda: z(anc[0]))
        uncompute()

# DSLValidationError: gate H is not allowed in exact compute blocks
Qiskit, Cirq, and Q# all accept this program. It compiles, it runs, and it looks fine. But because h is not a permutation gate, it creates superposition in the ancilla. After the uncompute step, the ancilla is still entangled with the system. The program silently computes the wrong thing. b01t rejects it immediately. The compute block only accepts permutation gates; h is not one of them, so the build fails with a DSLValidationError before any circuit is produced.

​
Where to go next

Quick Start

Write and certify your first safe quantum program in a few lines of code

Installation

Install b01t and set up your Python environment

Safety model

Understand the Hero Theorem and how certification works

Ancilla discipline

Learn the compute / phase / uncompute pattern in depth