Evidence
How we know, and how you can check.
You never have to take our word for anything. This page starts with an everyday idea and goes one step deeper at a time, until you are holding a proof yourself. Stop at whichever step answers your question; each one stands on its own.
Step 1 of 5 · Everyday
A promise you can check
You already live by evidence. A bridge opens because an engineer’s calculation says it will hold; a purchase comes with a receipt; a medicine reaches you with the trial that tested it. You rarely read them, but you rely on their being there, and on anyone being able to look.
We hold every result to that same standard, and make it easier to check than ever: each one comes with the kind of evidence that fits it, kept where anyone can open it.
- A theoremcomes with a proofa computer checks every line of it, so nobody has to take the author’s word
- A program runcomes with a receiptwhich code ran, on what, with what result, recorded so it can be replayed
- A measurementcomes with its conditionsthe instrument, its calibration and its uncertainty, written down beside the number, as at our research apiary
Step 2 of 5 · Familiar
Four questions every claim answers
A single word like “verified” hides too much. So every claim we publish answers four separate questions, and each answer stands on its own: a claim can be proved and still be waiting for its measurement, and we show you exactly which. Here is one real claim from our solar research, answered on all four.
No task the solar supervisor admits can take the modelled battery below its reserve floor, so long as generation and demand stay within their declared bounds.
- 1
Is it proved? established
Proved in the supervisor’s safe Agda core, for every input that respects the declared bounds.
reserve-step-preserves-floor → - 2
Does it run? established
The same core is compiled to native code; 72 recorded runs show it at work, and any run can be replayed exactly.
the recorded runs → - 3
Does it match the world? in progress
Partly measured so far: the real controller is connected and answering; the energy flows are still modelled until the bench’s reference-meter capture.
the development record → - 4
Who else has checked it? in progress
Rechecked inside the project; an independent reviewer who did not build it is a planned round of the work.
the review round →
An answer that is still in progress is shown as in progress, never as a failure. That is what lets a partner build on the parts that are finished today.
Step 3 of 5 · Closer
What the first answer can say
The first question, “is it proved?”, has five possible answers. Each comes from a proof checker, a program that accepts a proof only when every step is correct, and each means something precise.
- proved
- a machine-checked proof exists“The sum of two even numbers is even”: a checked proof exists.
- refuted
- a proof of its negation exists“Every odd number is prime”: a checked proof that it fails (9 = 3 × 3).
- conditional
- proved under a named assumption“This filter stays stable”: proved, provided the input stays within its rated range.
- not yet formal
- no precise statement yet“This design feels more robust”: worth testing, but not yet a precise statement.
- unresolved
- stated precisely, not yet decided either wayA precisely stated open problem: nobody has proved it or refuted it yet.
Two distinctions matter most. A refutation is a proof that a claim fails, which is stronger than a single counterexample someone happened to observe. And “unresolved” is a precise, honest state of its own: stated exactly, not yet decided.
Step 4 of 5 · Technical
Why a verdict cannot misreport itself
In the type theory we work in, to say a sentence P is established is to exhibit a term of type P. To say it is false is to exhibit a term of ¬P: constructively, a witness. To say it needs a hypothesis is to exhibit a function H → P, with the hypothesis made explicit. To say it cannot yet be assessed is to report that no interpretation is determined.
These are four positions in a type system, not four confidence levels. Because the evidence a record must carry is a function of its verdict, the ledger is a dependent sum rather than a labelled tuple: a record that carries the wrong kind of evidence for its verdict simply does not typecheck.
⊢ Pproveda term inhabiting the statement⊢ ¬Prefuteda term inhabiting its negation⊢ H → Pconditionala function from a named hypothesisno term yetunresolvedstated exactly, not yet decided
How a theorem reaches the world
- 01
Formal meaning
A claim is stated in a kernel language and proved there, with its axiom footprint in the open. The kernel checks the term; nothing is taken on description.
- 02
Program
A proof written appropriately is provably equivalent to a program. That is the Curry–Howard bridge, and it is why this is an engineering path and not an analogy.
- 03
Substrate
The program is lowered to a runnable, receipt-bearing computation, and the receipt says which route actually ran rather than which route was intended.
- 04
Physical consequence
Software already produces physical results — circuits, protocols, control, chemistry, cars, robots, autonomous learning systems. The chain ends in the world, re-checkable by someone who does not trust us.
The full road, from a single distinction to machines that act within proved bounds, is set out in the Principia →
Step 5 of 5 · Hands-on
Check one yourself
Every lab below recomputes its result in your own browser, on the verified core. Start with whichever matches your curiosity; none needs an account or any background.
solar · real controller
Inspect a proof-governed solar supervisor
72 recorded runs, the theorems behind them, and the development record.
Open the record →apiary · exact arithmetic
Read a hive probe like a scientist
Change how fast a probe responds and see, computed exactly, which air temperatures its reading allows.
Open the record →distributed wind · exact arithmetic
Watch the obvious arithmetic fail at cut-out
Choose a forecast and see the turbine’s proved power envelope beside the reading that breaks in a storm.
Open the record →neuromorphic · real chip
Try to break a certificate chain
Tamper with a model on its way to BrainChip’s Akida chip and see exactly where it is refused.
Open the record →quantum · no physics required
See what a circuit does
Six questions about quantum computing answered in pictures and nothing else. Start here if the phrase “exact amplitude” meant nothing to you.
Start with a question →quantum · nine questions
See what is actually proved
Nine questions a result has to survive, the layer that answers each, its honest trust state, and a live lab for every one. It states where each answer stops.
See what it proves →quantum · content-addressed
Read the certified corpus
The circuits already carrying certificates, each with its claim, its evidence, and the address that names it. Re-checkable without asking us for anything.
Open the corpus →quantum · runs in your browser
Build one yourself
Place a gate and watch thirteen views recompute in your browser on the verified core. The interface simulates nothing; when a view is out of range it says so.
Open the designer →papers · preprints
Read the research record
Every paper and preprint behind this work, published in full.
Read the research ↗What this gives you
Three properties, and what each one buys
I · is derivable
Verifiable — which buys trust
An auditor takes the artifacts alone and reproduces the verdict in a clean environment, without trusting us. Without it you get simulation theater, reputation, and hope.
II · has a stated meaning
Interpretable — which buys knowledge
The structure is stated, not inferred from behavior, so a failure is readable and a success is explicable. Without it you get opaque success and unusable failure.
III · responds to a handle
Controllable — which buys value
There is a steering surface that still means something under optimization. Without it you get optimization without a lever anyone can hold.