A proof that your circuit is correct is one claim among several. Below is every question this system answers, the layer that answers it, exactly how far each answer goes — and a live lab for each, computed in your browser by the verified core rather than illustrated. Where an answer is partial, it says so.
If this is your first visit, the visual walkthrough covers what quantum circuits are before this page covers what we prove about them.
Below is every question this system answers, the layer that answers it, and exactly how far each answer goes. Each links straight to its answer below, with a live lab you can move. The sections after them cover how the answers are produced, and where the boundaries are.
Five of these are layers of the program itself — the family, the circuit, the compiler, the hardware, the machine it shares. Three are questions the circuit cannot answer about itself. Not one of them is a promise: every row above states its own limit, and the two that are not fully closed say so on the page rather than in a footnote.
Questions 1–5 · the stack a result stands on
A proof that your circuit is correct says nothing about whether the family it came from was right, whether the compiler preserved it, or how much the hardware will corrupt it. Those layers are the published work of Runzhou Tao and colleagues; what this project adds is an exact, kernel-checked fence on the decidable fragment of each — separately tiered, never merged into one number. Three of the layers ship a live lab: exact arithmetic you can move, labelled honestly the moment you leave a kernel-pinned fixture.
above
QSynth
POPL 2024
The recursive circuit family is the right one
QSynth specifies a unitary by a path sum and discharges it with an SMT solver over floats. PCQ’s exact D[ω] semantics refines that spec: the circuit’s columns are proved equal to the path-sum matrix by kernel arithmetic, which is a strictly stronger witness than a solver’s unsat. Eight of eleven benchmarks are kernel-certified, and the refinement composes — certified circuits concatenate into certified circuits without a fresh proof.
Two independent constructions: the left column runs the reversible circuit, the right evaluates the arithmetic spec. They must agree on every basis state — flip in the mutant and watch the refinement break. adder_refines_ppsa · adder1MajorityMutant_refuted
the core
PCQ
this system
This exact circuit does exactly this
Exact algebraic amplitudes, a content-addressed certificate, and a Lean proof anyone can replay. This is the layer the collaboration is built around: everything above and below attaches to it, and every attachment carries its own trust tier.
PCQ · the verified core itself◇ reported · browser preview
append
H · T
loading the verified core…
This lab re-implements nothing. It loads the same pcq_core.wasm the designer and the certified service run, and prints what the core returns — exact algebraic amplitudes, never a decimal. exact_carrier_algebra_sound · toComplex_operations_sound
transform
Giallar
PLDI 2022
The compiler pass preserved the semantics
Giallar verifies Qiskit compiler passes with symbolic execution and Z3. The same rewrite rules are re-derived here as exact state-transformer identities — width- and position-generic, valid in two-sided context, so a rewrite proved sound stays sound wherever it is applied inside a larger circuit.
Apply certified cancellations and the permutation is unchanged — that is what 'the compiler preserved the semantics' means. Enable the unsound rule and the receipt breaks immediately. cxcx_cancel · rewrite_two_sided_matrix · ss_cancel_refuted
below
Gleipnir
PLDI 2021
The noise budget against real hardware
Gleipnir bounds a program’s error with an SDP over a tomographic constraint, computed in floating point with a hardcoded slack. Two things are proved here: the slack makes the answer conservative (it over-estimates, so it never flatters the hardware), and on the Pauli fragment the diamond distance collapses to an exact fraction — no solver at all.
Set the Pauli weights as exact eighths. On this fragment the diamond distance is not an SDP output — it is the off-identity mass, exactly. Tensor two copies and the kernel's width-two value 7/16 appears. processInfidelity_eq_error_mass · nqubit_diamond_isGreatest
deploy
HyperQ
OSDI 2025
Isolated execution on a shared machine
Multi-tenant quantum execution is where a certificate has to survive contact with a scheduler. This layer is named, not claimed: no theorem here covers it yet. The adjacent method work — proof-lifting under a relaxed memory model, and data-driven invariant discovery — is formalized, and both are honestly fenced as method transfer rather than a deployment guarantee.
all addresses distinct — the operations pairwise commute
HyperQ itself is named, not claimed — no theorem here covers multi-tenant deployment. What is formalized is the method it would rest on: when operations pairwise commute, the fold descends to the free commutative monoid and the schedule stops mattering. Make two writes share an address and it stops being true. applyAll_perm_of_pairwise · racy_writes_order_dependent
The pattern is the same at every layer: their tools cover the general case — numeric, SMT, systems — and this project adds the exact kernel-checked fence on the fragment where a decision procedure exists. The two are never averaged into a single confidence number; they compose by the weakest link, so a float SDP attached to a kernel proof yields a bound that still says reported.
That closes the program. It does not close the problem — three questions remain that no amount of proof about this circuit can answer, because they are not about the circuit at all.
Questions 6–8 · what the circuit cannot tell you about itself
The five layers above make a quantum program trustworthy end to end. These three ask whether it was the right program: whether the code you are relying on protects anything, whether the structure you are reading is real, and whether the machine was ever the right tool. Same terms throughout — exact arithmetic, a named theorem, a visible boundary.
TIETopological Invariant Engine
Does my error-correcting code actually protect anything?
It computes the exact structural invariants underneath error correction and statistical physics — how many logical qubits a code truly encodes, the smallest error that can slip through undetected, the exact partition function of a spin system, the exact contraction of a free-fermion one.
A code's logical-qubit count is a homology dimension. Its distance is the shortest loop that cannot be undone.
Both are rank computations over GF(2) — exactly the place an off-by-one survives every test you would think to write, leaving a code that looks correct and protects nothing. So here the elimination algorithm itself is proved equal to the abstract rank, and a code’s Euler characteristic is a theorem rather than a per-example check.
QEC code design
distance bounds
device connectivity
free-fermion & electronic structure
partition functions
contraction-order optimisation
Boundary · All fifteen lanes carry kernel authority. Six of them — torsion, anyon fusion, GKP lattices, optimal compilation, surface enumeration, coboundary membership — were fenced until the missing theorems were built; each now cites one, and several still declare a scope, which is a different thing from a fence.
TIE · logical qubits from rank● proven · matches kernel pin
checks
n qubits
7
rank Hx
3
rank Hz
3
k = logical qubits
1
7 − 3 − 3 = 1
Switch off a stabilizer check and the code stops protecting: k rises because the rank fell. Exact GF(2) elimination — the identity k = n − rank Hx − rank Hz is the kernel's. f2rank_eq_rank · css_firstHomology_finrank
TDAPersistent homology, exactly
Which of this structure is real, and which is an artifact of where I drew the line?
It sweeps a threshold across a structure and records when each topological feature is born and when it dies — the barcode. Every step is exact arithmetic over GF(2): no floating point, and no tolerance parameter to tune.
Replaces pick a cutoff and hope with watch what survives.
Any single threshold is arbitrary, and a feature that exists at only one threshold is usually noise. Long bars are structure; short bars are artifacts. Applied to a circuit the filtration is the circuit — impose the stabilizer checks in order and the barcode shows the protection being built, one check at a time.
stable vs incidental features
syndrome & defect analysis
unknown-scale data
code assembly
Boundary · Endpoint Betti numbers carry kernel authority; the barcode pipeline is replayed — exactly recomputable, not yet kernel-proved. The system reports the weaker of the two.
Drag the filtration. Each independent check consumes exactly one degree of freedom; the bar that survives every level is the logical qubit. css_firstHomology_finrank · persistent Betti pipeline
IsolineThe advantage frontier
Is this circuit even worth putting on quantum hardware?
It places an advantage claim as a typed coordinate — which problem family, attacked with which classical method, on which data, in which regime — and returns a verdict carrying a replay receipt.
Denial is a fact. Support is a conjecture. The verdict type has no third case.
If a classical method actually runs and reproduces your result, advantage is denied — with a receipt. But no computation can establish that no classical method exists; that rests on a hardness conjecture. So the kernel can deny advantage or bound the classical cost, and is structurally unable to assert hardness. A supported claim comes back fenced, with its assumption in the open.
pre-spend triage
queue-time justification
vendor claim due diligence
classical attack surface
Boundary · For Clifford circuits the denial is not a label: a polynomial-time tableau provably reproduces the same exact amplitudes, so “classically simulable” is a theorem about that circuit.
fact · a polynomial-time tableau gives the same exact amplitudes
Add a T and the circuit leaves the tableau-simulable fragment. Denial is a fact with a receipt; beyond it the kernel bounds the classical cost and returns fenced — it never asserts hardness. isCliffordCircuit_iff_tCount_zero · cliffordCircuit_tableau_simulates
One computation, several tools
The engines share their internals rather than duplicating them. The contraction that bounds a noise budget is the contraction that attacks an advantage claim; the stabilizer tableau that draws the correlation view is the tableau that denies advantage for a Clifford circuit; the GF(2) rank that counts logical qubits is the rank that reads a graph’s cycles.
They also share one law about evidence. Trust composes by the weakest link. Every result is labelled proven, replayed, reported or fenced, and combining results takes the weakest — so attaching a kernel proof to an assumption yields an assumption, never a proof. That is a theorem about the labels, not a habit of ours, which is why nothing on screen can claim more than the evidence beneath it.
fenced<reported<replayed<proven
weakest → strongest · a compound takes the leftmost label present
Question 9 · does the answer survive being moved?
The eight answers above are each a statement in one notation. Real pipelines do not stay in one notation: a circuit becomes a diagram, a diagram becomes a normal form, a normal form becomes something a machine decides. If meaning drifts at any hop, the certificate at the top was about a different object than the one that ran. This asks whether truth is preserved when the object is rewritten — and makes that a theorem rather than an assumption.
A second notation, and a theorem tying it to the first
ZX is a diagram calculus for quantum processes: circuits become spiders joined by wires, and rewriting the diagram is supposed to preserve what it means. Here the “supposed to” is discharged. Every spider carries an exact D[ω] amplitude — the same arithmetic the certificate uses — and a phase is not approximated by an exact amplitude, it is one, because ZX phases and ω = ζ₈ are the same group of order eight.
So the two notations can be compared entry by entry, and they agree — checked against the certified evaluator, not against a second copy of the diagram code. That is the whole point: two independent constructions of the same matrix.
What it buys
Cheaper answers, at no risk
The same chain can be evaluated densely — one exact 2×2 multiply per spider — or by fusing phases, which costs one step whatever the length. A theorem says the two agree, so choosing the cheap lane is a pure cost decision that cannot change a result.
Claims that travel
A result proved under one semantic profile can be reused under another exactly when it mentions only symbols that profile admits. Previously a UI convention; now a stated condition with a proof, and a refutation showing where it fails.
Verdicts you can run
The end of the chain is a decision procedure: a claim compiles to a total program returning true or false. Compiler correctness ties it back to the semantics, so running it and proving it agree.
Every chain you can build here is covered — chain_denotation is general in the chain length, not a sampled table. Fusion adds phases in ℤ/8 because ω = ζ₈ has order 8, which is why eight T spiders come back to the identity. This lab is checked against the engine's kernel-pinned rows at render time. chain_denotation · fuseStep_receipt · receipt_unique
The dense lane costs one exact 2×2 multiply per spider; the diagram lane fuses phases and costs one, whatever the length. Choosing between them is safe because lanes_agree is chain_denotation — the two lanes provably compute the same matrix, so this is a pure cost decision that can never change an answer. route_preserves_order · route_refuses_over · lanes_agree
Fibonacci fusion channels. The golden-ratio quantum dimension is forced by the integer trace and determinant — never supplied as a symbolic constant. This lane returned a fenced verdict until 2026-07-25; it now cites a kernel authority in this repository. AnyonFusion.fibFusion_charpoly
Institution · when a claim may be borrowed● proven · matches kernel pin
claim about
claim mentions
T
Clifford admits it?
no
borrowing licensed?
no — outside the profile
a T claim is not a Clifford sentence — the reduct lemma does not apply
The designer shows a row rendered under one semantic profile while another is declared, and calls it borrowed. That is licensed exactly when the claim mentions only symbols the declared profile admits — the satisfaction condition of the institution. It is why borrowed rows are capped at reported rather than promoted. holds_restrict · clifford_claim_borrows · t_claim_not_clifford_sentence
What this opens up
Translation is now a typed arrow, and arrows compose. That is what let six lanes stop being fenced: each had named the theorem it lacked — integer Smith normal form, anyon fusion arithmetic, symplectic lattices, optimal design, surface enumeration, span membership — and each of those theorems now exists here, so the lanes were retired by construction rather than by lowering the bar. The engine still refuses to ship a lane with no local authority; there is simply no longer a lane in that position.
The same arrow admits a new calculus without touching what is already proved. Adding one means giving its notation, saying how a model of it restricts, and discharging the one preservation obligation — after which every certificate above transports into it for free. What is deliberately not claimed: this covers the fusion fragment of ZX, and the wider diagram calculus is future work, stated here rather than left for a reader to discover.
Thirteen ways to see one circuit
Those answers have to be legible, not just true. A circuit is one object with many faces; in the designer you work from whichever face suits the problem and watch every one of them update as you place a gate. Three of the thirteen are the Tao fences — noise, synthesis and transpile — so the layers above are not a diagram, they are views you can open. If the faces are new to you, six of them are walked through one at a time in the visual gallery first.
Circuit diagram
The familiar picture: wires and gates, left to right.
Bloch sphere
Where each qubit points, and how each gate turns it.
Exact matrix
The precise transformation, as algebraic numbers rather than decimals.
Measurement outcomes
Which results are possible and their exact probabilities.
Pauli correlations
Which qubits are linked, and how.
Stabilizer tableau
The compact algebraic form used for error-correction circuits.
Gate word
The circuit written as a word — edit the word, edit the circuit.
The browser exposes everything the current core can justify; it does not fill unsupported views with plausible output.
Build from certified structure
Place CCX, CCZ, MCX3, MCZ3, controlled swap, or the one-bit reversible adder as a single glyph, then expand it in place to the exact word supplied by the core. The wizard builds Grover, Bernstein–Vazirani, GHZ, teleportation, and QFT circuits and displays the core content address of the result.
Know when a view does not apply
Exact-amplitude views stop at six qubits; stabilizer views continue to larger registers. Every dark tile names the profile or size boundary. OpenQASM and qcir parse locally. Provider, Lean, and certificate files, certification, and provider downloads remain visibly gated because they require the sandboxed service or Lean kernel.
Why this is different
Most quantum tools simulate in floating point and ask you to trust the result. Four things here work differently.
Exact arithmetic, not approximation
Amplitudes are exact algebraic numbers. Where other tools show 0.7071067811865476, this shows (ω − ω³)/2 — the actual value, not a rounding of it. No floating point appears anywhere a pass or fail decision depends on it.
Checked by simulators we did not write
A system that only agrees with itself proves nothing. Every circuit was re-run on independent simulators — Qiskit Aer and Stim — inside a sandbox with no network, and without being handed our predicted answer. They agreed. That is the difference between a claim and a check.
The same circuit always gets the same name
Circuits are addressed by their content. Build one in the browser or author it in Lean — identical circuits produce an identical address. That is what makes a result reproducible rather than merely repeatable.
It tells you what it cannot do
Views that do not apply to your circuit stay visibly empty instead of showing plausible filler. Unsupported features say so. A tool that hides its limits is not one you can build on.
The evidence behind that
Claims are cheap, so here are the numbers — every one of them produced by a gate that runs in the repository, not by a marketing pass.
Lean authority files
60
the whole proof closure the release gate pins by digest
phase-9 evidence oracle
unproved steps
0
across 118 files — no sorry, no native_decide, anywhere
guard_no_sorry
seeded defects caught
49 / 49
the checker is attacked before it is trusted, including a stub-every-antibody attack
self-validating oracle
110
antibody theorems
each claim ships its own refutation
33
replayed receipts
4,096 shots, independent simulators
9 / 11
QSynth benchmarks
kernel-certified; 2 reasoned fences
15
TIE lanes kernel-backed
all of them — fences retired with proofs, not waived
13
certified views
all of them free in the browser
24
frozen intake rows
a contract that cannot shrink
The numbers that matter most are the ones about failure. Every claim ships an antibody — a theorem stating the claim’s own refutation — so a proof that quietly became vacuous stops compiling. The checker is then attacked on purpose: forty-nine seeded defects, including replacing every antibody with a stub that trivially passes, and all forty-nine were caught. A verifier that has never been shown to fail is not evidence of anything.