> ## Documentation Index > Fetch the complete documentation index at: https://b01t.com/llms.txt > Use this file to discover all available pages before exploring further. # What is b01t? Build-Time Safety for Quantum Code > b01t enforces ancilla cleanliness and unitary correctness at compile time. Every @coherent program is a proven unitary channel — no simulation needed. 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: ```python theme={null} 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: ```python theme={null} 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 Write and certify your first safe quantum program in a few lines of code Install b01t and set up your Python environment Understand the Hero Theorem and how certification works Learn the compute / phase / uncompute pattern in depth