A certificate
A single file holding your circuit, what was claimed about it, the evidence, and the exact software environment used. Anyone can re-check it later without trusting you — or us.
Step 1 · The question
Quantum circuits that come with proof
Quantum hardware is metered, queued, and noisy. Every run costs. And when a run comes back wrong, you are left with one expensive question:
Was my mathematics wrong, or was the hardware just noisy?
Those are different failures with different fixes, and today they arrive tangled together — so teams re-run, re-tune, and re-spend to tell them apart. This system separates them before you spend anything. If the circuit is proved to do what you intended, a bad result on hardware is physics — decoherence, gate error, readout — and never your algebra. You find the mathematical mistakes where they cost nothing: at the desk, not on the device.
What makes that possible
One number, and the whole difference
Every other quantum tool writes a qubit’s amplitude as 0.7071… — a decimal, rounded, already slightly wrong before the first gate. Round a million times and you can no longer say whether a discrepancy is your algorithm or your arithmetic.
Here the same amplitude is (ω − ω³)/2 — an exact algebraic number, held exactly, all the way through. Nothing is rounded, so nothing drifts, and a proof about the circuit is a proof about the circuit you will actually run.
That is the single technical decision everything else rests on — and it is why a certificate here means something a passing test suite cannot.
What you get, every time
One circuit in. Three things out — each one stands on its own.
A machine-checked proof
Not a test that passed. A proof the Lean theorem prover verified, shipped as readable source, with the logical assumptions it leans on listed in the open.
Code that runs
The same circuit as OpenQASM 3, Qiskit, Cirq and Braket — each bundled with the certificate it came from, so the program and its proof never drift apart.
How it works
- 1
Design or import
Place primitive or derived gates, choose an algorithm, or load OpenQASM or qcir directly in the browser.
- 2
Watch it exactly
The verified WASM core evaluates every edit; all thirteen views update or state exactly why a view is outside its range.
- 3
Certify
The circuit is bundled, its claims are proved, and the proof is replayed in the Lean kernel.
- 4
Export
Take the certificate, the proof source, and runnable code for the platform you use.
Three ways in
Same system, three depths. Take whichever one matches what you came for.
- 1
Understand it
Six questions about quantum computing, answered in pictures and nothing else. No physics required. Start here if the phrase “exact amplitude” meant nothing to you.
Start with a question → - 2
Check it
Nine questions a result has to survive, the layer that answers each, its honest trust state, and a live lab for every one. Start here if you want to know exactly what is claimed and where the claims stop.
See what it proves → - 3
Do it
Build a circuit and watch thirteen views update as you place each gate, computed in your browser by the verified core. Start here if you already know what you want to build.
Open the designer →
It is not one claim, it is nine
A proof that your circuit is right says nothing about whether the family it came from was right, whether the compiler preserved it, or how much the hardware will corrupt it. Each of those is a separate question with a separate answer — and each answer states where it stops.
9
questions answered
each by a named layer, each with a live lab
13
ways to see one circuit
every face updates as you place a gate
0
rounded numbers
exact algebraic amplitudes, end to end