Apoth3osis

Step 3 · Prove it

What this system proves

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.

Nine questions, one circuit

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.

  1. 1Is this exact circuit what I claimed?PCQkernel-certified
  2. 2Was the family it came from right?QSynth9 of 11 benchmarks
  3. 3Did the compiler preserve it?Giallarkernel-certified
  4. 4How much will the hardware corrupt it?Gleipnirexact on the Pauli fragment
  5. 5Can it share a machine safely?HyperQnamed, not claimed
  6. 6Does my error-correcting code protect anything?TIEkernel-certified
  7. 7Which of this structure is real?TDAendpoints certified
  8. 8Is this worth quantum hardware at all?Isolinedenial is a fact
  9. 9Does the answer survive being moved?ZX · Institutionscertified arrow

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.

  1. 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.

    refinesPPSAPerm_comp · ghz_refines_ppsa_amplitude · qft_refines_ppsa_phase

    QSynth · circuit ⟷ path-sum spec● proven · matches kernel pin
    xcircuitspec
    000000000000
    000100110011
    001000100010
    001110011001
    010001100110
    010111011101
    011011001100
    011111111111
    100010001000
    100110111011
    101010101010
    101100010001
    110011101110
    110101010101
    111001000100
    111101110111
    basis states
    16
    disagreements
    0
    refines the spec ✓
    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

  2. 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.

    exact_carrier_algebra_sound · toComplex_operations_sound

    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

  3. 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.

    rewrite_two_sided_matrix · TranspileGiallarRewrites

    Giallar · rewrite, semantics preserved● proven · matches kernel pin
    CCX(0,1,2) · CX(0,1) · CX(1,0) · CCX(0,1,2)
    ops
    4
    rules fired
    0
    semantics preserved ✓
    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

  4. 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.

    slack_overestimates · nqubit_diamond_isGreatest

    Gleipnir · exact noise, no solver● proven · matches kernel pin
    X1/8
    Y0/8
    Z1/8
    identity weight
    3/4
    process infidelity
    1/4
    ½‖E−id‖◇
    1/4
    state-constrained (|0⟩)
    1/8
    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

  5. 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.

    applyAll_perm_of_pairwise · inductive_invariant_sound

    VRM method · schedule independence● proven · matches kernel pin
    a:mem[0]=1 → b:mem[1]=2 → c:mem[2]=3
    canonical order
    [1, 2, 3]
    shuffled order
    [1, 2, 3]
    Schedule-independent
    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.

f2rank_eq_rankeuler_characteristicpf4_sq_eq_detcontract_order_independent

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.

css_firstHomology_finrankpersistent Betti pipeline

TDA · Steane filtration● proven · matches kernel pin
0123456
checks imposed
6
β₁ surviving
1
born 7 · died 6
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.

cliffordCircuit_tableau_simulatesplaceOnFrontier_ne_conditionalLower

Isoline · advantage placement● proven · matches kernel pin
append
H · CX
gates
2
T-count
0
a classical method reproduces this
Advantage denied
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.

ZX · spiders fuse, phases add● proven · matches kernel pin
append
TTT→TS
spiders
3
dense multiplies
3
after fusion
1
receipt (phase)
3/8 · TS
saving = 2 interactions
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
Isoline · routing by measured envelope● proven · matches kernel pin
dense cost
9
diagram cost
1
envelope
8
selected lane
diagram
dense overflows; diagram still fits
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
TIE · anyon — fence retired● proven · matches kernel pin
copies of τ
5
fusion channels
8
charpoly
x² − x − 1
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.

Proof structure

How each verified claim depends on the others.

Hardware layout

How the circuit maps onto real device qubits.

Topological invariants

Shape-based properties that survive deformation.

See how it works →Open the designer →

The range is broad, and the boundary is visible

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.

next · step 4 of 5Fifteen algorithms this was actually done toNot toy circuits: Fourier transforms, block encodings, a qubitized walk, HHL, topological data analysis, braiding and two impossibility fences — each with its soundness theorem, its real axiom footprint, and the broken variant the gate has to reject.
Every number on this page is produced by a gate that runs in the repository.← Overview