Skip to content

Programs

One foundation, carried into every field.

Each program applies the same method to a different part of the world: state the question precisely, build the construction, check it with a proof kernel where a proof is possible, test it against measurement where the world is involved, and publish the evidence. A status is drawn from the work, never from intent.

An engraved solar nucleus inside a stippled mathematical governor, connected to photovoltaic panels and storage

Featured research · 001 · with Morningstar

A solar supervisor whose rules are proved before they run: a current budget that composes, a reserve floor no admitted task can break, and evidence that expires. The proved core and every recorded run are open now; commissioning on a real controller is next.

19
Safe Agda core modules
72
Recorded simulation runs
36
Paired policy comparisons
0 s
Hardware monitoring so far
Open the research record →
A stippled neuron in ink, its branches reaching out like a network

Featured research · 002 · with BrainChip

A certificate chain around BrainChip’s model conversion: the exact model in, how it was quantized, converted and placed on the chip, and what came out. Three model families certified, and a model reproduced bit for bit on a real AKD1500.

25 / 25
Outputs reproduced exactly on a real Akida chip
126
Model layers bound to their exact bytes
3
Model families certified end to end
0
Findings in the independent hostile audit
Open the research record →
A honeybee drawn entirely from tiny mathematical symbols

Featured research · 003 · at Brumble Bee Farms

Readings that carry their own argument: which instrument, placed where, calibrated how, interpreted by which model, and fit for which question. Five measurement contracts proved in safe Agda, and three substitutions caught in audit.

5
Measurement contracts proved in safe Agda
12
Records replayed across apiary and greenhouse setups
3 / 3
Substitutions caught: data, installation, model
[⅘, 6⁄5] K
The same answer in Celsius and in kelvin
Open the research record →
A wind turbine stippled in mathematical glyphs, the wind streaming past, beside a proof tree and its power curve

Featured research · 004 · distributed wind

An independent, proved checker for every curtailment, export and reserve decision a wind, storage and EV-charging system makes, so AI can propose and mathematics decides. Built on NLR’s EVI-DiST and proposed with Uprise Energy’s 12-kW Mobile Power Station.

149
modules in the proved system, every one checked by a proof kernel
818
dependencies between them, each verified when the system is checked
28 / 28
seeded supervisory hazards refused by the independent checker
21 / 48
development phases closed, each with a gate receipt
Open the research record →

Open-source tools

Formal results, in the language you already work in

Our results are proved in Agda and Lean, which most physicists, engineers and biologists do not read. So we built a way to hand them over without asking anyone to trust a translation: the exact statement a proof assistant accepted, in LaTeX, MathML or a web page, with a certificate anyone can re-check.

agda-certv0.2.0 · MIT · free and open source

Give it a machine-checked theorem from Agda 2.8.0 or Lean 4.24.0. It writes the theorem’s statement as LaTeX for your paper, MathML for the web and a ready HTML page, and ships a small certificate that the standard, unmodified proof assistant checks: the text you see is exactly the statement that was proved. Change one binder, and the check fails.

  • LaTeX + agda-cert.sty
  • Content MathML
  • HTML page
  • calculation chains
  • Lean 4 statements

For AI agents Every operation also ships as an MCP tool (doctor, certify, verify, render, and more), each answering with one JSON verdict. Point an agent at a project website and it can add a collapsible panel that sets out the whole system’s mathematics in LaTeX, every statement certified.

How it works
  1. Read the statement from the source, with its own reader: a small Agda backend, or Lean’s own elaborator. No reflection, which can lose information.
  2. Print it with printers proved correct in Agda’s safe fragment, with no postulates: each printer provably reads back, so the printed text determines the statement.
  3. Let the proof assistant judge. Stock Agda accepts the certificate only if the printed text decodes to exactly the theorem’s type; for Lean, Lean’s elaborator must read it back to the very same type.
  4. Re-check it any time. verify needs only Agda (and Lean, for Lean certificates); it never runs our extractor or printer, and the kernel decides.
Get started

Needs Agda 2.8.0 (exactly), GHC 9.12.2 with cabal ≥ 3.10, and Python ≥ 3.11; optionally Lean 4.24.0 and pdfLaTeX. verify alone needs only Agda and Python.

sha256sum -c agda-cert-0.2.0.tar.gz.sha256
tar xzf agda-cert-0.2.0.tar.gz
cd agda-cert-0.2.0
./install.sh        # builds the two helper tools once
./run_tests.sh      # optional: the full test suite

Certify and verify an Agda theorem (the package README walks through extraction):

python3 tools/agda_cert_render/agda_cert.py certify --corpus C.json --sir work/sir.jsonl \
    --member Data.Nat.Properties.+-comm --stage <library root> \
    --table tools/agda_cert_render/tables/stdlib.json --out cert/ --core agda
python3 tools/agda_cert_render/agda_cert.py verify cert/ --stage <library root> --core agda
python3 tools/agda_cert_render/agda_cert.py render cert/ --stage <library root> --core agda \
    --html page.html --tex statements.tex

Or a Lean 4 theorem, from a built Lake project such as one depending on Mathlib:

python3 tools/agda_cert_render/lean_front.py certify --project <lake project> \
    Mathlib.Algebra.Group.Basic mul_comm --out work/mul_comm --core agda
python3 tools/agda_cert_render/lean_front.py verify work/mul_comm --project <lake project> --core agda

Every command prints one line of JSON with "ok", and exits 0 on success, 1 on a refusal with its stated reason (a result, not a crash), 2 on an error. The MCP tools live in tools/agda_cert_render/mcp/; python3 op_<name>.py --help prints each one’s arguments and results as JSON.

Example output

Mathlib’s mul_comm, certified and verified (assurance strict, no axioms). The certified LaTeX source, exactly as written, with every binder shown:

\forall \{ \mathit{G} : \operatorname{Type} \, \langle \mathsf{u\_1} \rangle \} , \forall \{\!\{ \mathit{\_hyg₃} : \mathsf{CommMagma} \, \mathit{G} \}\!\} , \forall ( \mathit{a} : \mathit{G} ) , \forall ( \mathit{b} : \mathit{G} ) , ( \mathit{a} \Atimes \mathit{b} ) \Aeq ( \mathit{b} \Atimes \mathit{a} )

Typeset, it reads: for every type G with a commutative multiplication, and every a and b in G, a × b = b × a.

The page agda-cert rendered for Data.Nat.Properties.+-comm (agda-stdlib 2.4) ↗Both example certificates (.tar.gz) ↓

Example output: re-verifying it needs the same library (agda-stdlib 2.4, or the pinned Mathlib project).

What it does not claim
  • The statement, not the proof. A certificate shows the displayed statement is the theorem’s type; the proof is whatever Agda or Lean accepted, and is not translated.
  • Notation is a published choice. The kernel proves the LaTeX reads back under the notation table, and that the table is unambiguous; what a symbol means is the table’s row, shipped with every certificate.
  • The LaTeX source is certified, not the printed page: a document that redefines the macros can make a PDF say something else.
  • Anything outside the supported fragment is refused, with a reason: Agda theorems outside --safe; in Lean, strict-implicit binders, projections, let and universes Lean cannot infer.
Licence, citation and security

MIT. To cite it, use CITATION.cff in the package: “agda-cert: kernel-checked LaTeX and MathML statements for Agda theorems”, version 0.2.0.

Security contact. Please report a suspected false certificate privately to contact@ontologicalmathematics.org, with the certificate directory and the verify output. We aim to acknowledge a report within 7 days.

Software in production

Mathematics you can run, right now, in your browser

When intelligence produces results faster than anyone can check them, an answer is worth building on only if it is exact and independent of the machine that found it. These two run in your browser, no install and no account: the same verified cores we use, recomputing every answer in front of you.

|0⟩HHP(φ)|0⟩|1⟩φ = πoutput, exactlya0 =0zero, exactlya1 =1P = 1float64 says|a₀| =6.1e-17

ExactQuantum labs

The arrows that cancel

Everything quantum lives in amplitudes, arrows that add and cancel; and cancellation is exactly where ordinary computers leave a ghost of rounding behind. Our verified core computes in exact algebra, so a cancelled amplitude is zero, exactly, and every circuit you build comes back with a certificate anyone can re-check.

DesignerPhotonicCorpusProof

Open the labs →
one orderanotherννααααεντναννααααεντναreadyready360 possible orders · every one ends at b40db27b

Order-freeMathematics that runs

Two histories, one world

Category theory says what composes, and our kernel turns those laws into small local rules. Above, the real kernel reduces one net in two different orders; the histories diverge and arrive at the same world. All 360 orders do, which is what lets mathematics run in parallel, on any hardware, with no referee.

The labThe race it caughtThe papers

See a law become a machine →

With the support of

The people and platforms behind the work

Equipment that brings an idea to the bench, funding that gives it time, and technology that carries it from construction to evidence. Each partnership grows into its own open record. Thank you.

01Research & equipment partners

02Sponsors

  • Google for Nonprofits logofor Nonprofits

    Google for NonprofitsNonprofit grants

    For welcoming the Institute into Google for Nonprofits, and the grants that carry our research to the people it can help.

  • AgentPMT logo

    AgentPMTAI tooling · MCP servers & workflows · Skills & audit logs

    For the AI tools our work runs on: MCP servers, workflows and skills, with audit logs that keep every step of it on the record.

  • Apoth3osis logo

    Apoth3osisFinancial support · Compute · Expertise

    For the funding, computing resources and expertise that help make the Institute’s research possible.

  • ElevenLabs logo

    ElevenLabsCompute · AI credits

    For compute and AI credits that give the Institute more capacity to experiment and develop its research.

  • Given anonymously
    • Apiary equipment
    • Clearance level: bee suit

    Our one anonymous gift funds… beehives. For the record, the only classified material at the Institute is the honey, and it’s graded, not redacted. Thank you for a practical gift to our pollinator research.

03Technology & infrastructure partners

The programs

Where the method is at work

One line each; open a program for what it does and what support would enable.

active — work exists building seeking partners — no program yet
  1. 01Quantum systemsExact amplitudes, machine-checked circuits, certificates anyone can re-check.active

    Its mathematics monoidal categories and string diagrams · exact cyclotomic arithmetic · error-correcting codes

    Quantum hardware is metered, queued and noisy, so when a run comes back wrong you cannot tell whether the mathematics or the machine was wrong. The Institute separates the two: exact algebraic amplitudes, a machine-checked proof, a certificate anyone can re-check, and runnable code that cannot drift from the proof it came from.

    What support would enable

    Compute time, limited QPU credits where a physical run answers a bounded question, FPGA interfaces, and funded replication.

    Open the live labs →Donate to this work
  2. 02Intelligent systemsAssurance for AI/SI: what a model claims, checked against a proof kernel.active

    Its mathematics a verdict calculus · refinement between model and specification · certified inference

    AI systems now write mathematics and software faster than anyone can review it. The Institute's verdict calculus gives each claim a machine-checkable account of what it establishes — proved, refuted, conditional on a named assumption, or not yet formal — so a system's output can be trusted by re-checking, not by reputation.

    What support would enable

    CPU servers, memory and durable storage for proof checking and search, compute allocations, and independent review.

    Open the BrainChip research →Donate to this work
  3. 03Trusted hardwareProofs compiled toward circuits; receipts from FPGAs and accelerators.active

    Its mathematics interaction nets · finite-state dynamics · exact fixed-point and finite-field algebra

    A proof that a computation is correct is only as good as the machine that runs it. The Institute carries verified computations onto FPGAs and accelerators and asks the hardware for receipts that say which computation actually ran.

    What support would enable

    Serviceable CPU servers, accelerators and FPGA boards, high-endurance SSDs, test equipment, and safe power.

    Donate to this work
  4. 04Fundamental physicsA machine-checked ledger scoring one generative idea against fifty measured effects.active

    Its mathematics symmetry groups · the division-algebra ladder · gauge theory on a lattice

    The Generative Distinction Physics programs tested one idea — that physics is the fixed-point theory of distinction — against fifty measured effects, committing in advance to how strong a claim each could earn. Thirty-one targets are machine-checked theorems; the rest are honest fits, open questions or refutations, all recorded.

    What support would enable

    CPU and RAM for proof checking, storage for reproducible builds, independent mathematical review, and research time.

    Donate to this work
  5. 05Agriculture & pollinatorsAn instrumented research apiary: live hive cameras and continuous colony data.active

    Its mathematics sheaves that glue sensor readings · calibration lenses · population dynamics

    Brumble Bee Farms is the Institute's research apiary in Michigan. Its hives are instrumented with internet-connected sensors that capture synchronized temperature, humidity, weight, sound, entrance activity and weather, with live cameras on the apiary, so colony health can be studied as data rather than anecdote. Findings and data are shared openly with researchers and educators. Alongside it, Freshly Farmed, also an Institute project, is a farm-to-door marketplace for local growers.

    What support would enable

    Hive scales, environmental loggers, microphones, cameras, reference instruments, field enclosures, and storage for the apiary record.

    Open the apiary research →Donate to this work
  6. 06NeurotechnologyInterpretable neural-signal models and verified acquisition pipelines.seeking partners

    Its mathematics event streams · spiking dynamics · signal transfer functions

    Neural signals are noisy, high-dimensional and easy to over-interpret. The Institute is seeking partners and specialised equipment to apply its verification methods to neural-signal acquisition and modelling.

    What support would enable

    Signal simulators, safe research-grade acquisition hardware, licensed datasets, and methodological collaborators. No clinical work is represented here.

    Partner on this program
  7. 07Distributed & swarm systemsMany agents, one verifiable account of what the group did.building

    Its mathematics confluent rewriting · gluing local states into global ones · coordination without a centre

    When many agents act together, the hard question is what the group actually did. The Institute is building methods that give a population of agents one re-checkable record of its joint behaviour.

    What support would enable

    Compute and simulation access, permitted multi-agent datasets, and modest robotics or tracking equipment.

    Donate to this work
  8. 08Energy & infrastructureSolar and wind power governed by proof: admit the work, keep the reserve, check every decision.active

    Its mathematics port-Hamiltonian energy laws · reserve invariants · proved supervisory control

    With Morningstar, the Institute is building a supervisor for solar power whose rules are proved before they run: a current budget that composes, a reserve floor no admitted task can break, and evidence that expires. The proved core, 72 recorded simulations and every proof source are open now; commissioning on a real GenStar controller is the next round. For distributed wind, our proposed component with Uprise Energy checks every supervisory decision of a wind, storage and EV-charging system against the turbine’s real limits, built on NLR’s EVI-DiST (Research 004). The same method carries to storage, metering and resilient infrastructure for field research.

    What support would enable

    Serviceable solar modules and power electronics, approved batteries, reference metering, networking, professional installation review, and funded bench time for commissioning.

    Open the Morningstar research →Donate to this work

The substrates

Every kind of hardware is a different way for matter to do mathematics.

We do not try to make every chip execute every operation. We ask which mathematics each one embodies most faithfully, so each part of a problem can run on the matter that suits it, with proof of what it guarantees there.

  • CPUCentral processors

    A few deep cores that branch, recurse and remember: control flow made of silicon.

    • control flow and recursion
    • symbolic algebra
    • exact, arbitrary-precision arithmetic
    • the proof kernel itself
    referenceactive
    Its part in the compiler
    Where the proved reference program runs and every other realisation is measured against it.
    With us
    Our compute network and the Arm cores of the DGX Spark. In our own measurements, a manycore CPU led interaction-net reduction across six workload classes.
    Its honest bound
    Generality has a price: few lanes, so it explores slowly what a wider substrate explores at once.
    See the work →

  • GPUGraphics processors

    Thousands of identical lanes in lockstep: one instruction, many data.

    • tensor and linear algebra
    • optimisation
    • high-dimensional simulation
    • search over equivalent forms
    exploreactive
    Its part in the compiler
    The exploration engine: digital twins, system identification, and the search for simpler equivalent implementations.
    With us
    NVIDIA DGX Spark (GB10, 128 GB unified memory); our interaction-net reducer runs on it byte-for-byte equal to the CPU.
    Its honest bound
    It discovers candidates; it does not certify them. Checking is always a separate responsibility.
    See the work →

  • TPUTensor processors

    Systolic arrays: data pulses through a grid of multiply-accumulate cells like blood through a heart.

    • dense matrix products
    • convolution
    • low-precision linear maps
    • learned surrogates at scale
    scaleseeking partners
    Its part in the compiler
    Training and serving the learned estimates the rest of the system may consult, never obey.
    With us
    A substrate we want to bring into the same evidence discipline: a learned surrogate on a TPU would carry the same proved bounds as one on a GPU.
    Its honest bound
    A fixed dataflow rewards fixed shapes; irregular, branching mathematics belongs elsewhere.

  • NPUNeuromorphic processors

    Event-driven neurons that spend energy only when evidence arrives: sparse spikes, not clocked frames.

    • sparse event streams
    • low-bit integer inference
    • temporal pattern recognition
    • on-chip adaptation
    recogniseactive
    Its part in the compiler
    Noticing change in vibration, sound, current or biology faster and cheaper than any clocked processor.
    With us
    BrainChip Akida AKD1500, with a proof-carrying certificate chain from trained model to exact on-chip outputs.
    Its honest bound
    A recognition is evidence, never authority; its restricted architecture is exactly what makes it formally tractable.
    See the work →

  • FPGAReconfigurable logic

    Circuits wired to the problem itself, clocked and exact, rewired in seconds.

    • finite-state dynamics
    • exact fixed-point and finite-field algebra
    • interaction-net rewriting in hardware
    • bounded-latency guards
    execute & witnessactive
    Its part in the compiler
    Executes the deterministic parts at guaranteed latency, and a second fabric independently witnesses the first.
    With us
    AMD Kria KV260 as the execution engine; Opal Kelly as the independent witness that recomputes and records.
    Its honest bound
    Exact only within the widths and ranges its design declares; those bounds are part of the proof.

  • FPAAProgrammable analog arrays

    Charge, current and capacitance do the arithmetic: the physics is the computation.

    • transfer functions
    • filtering and integration
    • continuous dynamics
    • signal conditioning at the source
    embodyactive
    Its part in the compiler
    Realising a mathematical transfer function directly in matter, before a single number is digitised.
    With us
    Okika AN231K04 (four AN231E04 devices) on our bench, characterised and calibrated as a mathematical instrument.
    Its honest bound
    Analog is calibrated, never exact: its error bound is measured and carried, not assumed away.

  • QPUQuantum processors

    Amplitudes that interfere and entangle: computation by unitary evolution in Hilbert space.

    • unitary and tensor-category structure
    • exact cyclotomic arithmetic
    • error-correcting codes
    • interference
    certify, then runbuilding
    Its part in the compiler
    Circuits whose meaning is proved exactly before they ever reach a device, and accepted by an exact statistical test after.
    With us
    Our proof-carrying circuit designer emits certified circuits for Qiskit, Cirq and Braket; the exact acceptance test for hardware is written, the hardware run is next.
    Its honest bound
    Today’s devices are noisy and small; we certify the circuit and measure the machine, and keep the two apart.
    See the work →

  • PICPhotonic processors

    Light through meshes of interferometers: a matrix multiply at the speed of light, with almost no heat.

    • unitary matrices as interferometer meshes
    • Fourier optics
    • linear transforms in constant time
    • boson sampling
    transformbuilding
    Its part in the compiler
    Linear algebra performed by propagation itself, for the transforms that dominate sensing and learning.
    With us
    Our photonic circuit designer composes and analyses chips in the browser; fabricated hardware is the next step.
    Its honest bound
    Linear by nature: nonlinearity must come from elsewhere, and loss and phase drift are measured and bounded.
    See the work →

  • MCUEmbedded controllers

    Small, deterministic processors that touch the world: the relay, the charge controller, the PLC.

    • hybrid automata
    • guarded transitions
    • fixed-point control laws
    • hard real-time deadlines
    actbuilding
    Its part in the compiler
    Where a permitted decision becomes physical action, with the equipment’s own protections kept in force.
    With us
    Morningstar’s solar charge controllers: commissioning a proved supervisor on a real controller is our next solar round.
    Its honest bound
    It acts only on what the verified gate admits; its native interlocks are never bypassed.
    See the work →

Making them work together

One theory. Many kinds of matter. One gate.

The Ontological Compiler is the system we are building to orchestrate them: it states the physics once, finds the equivalent forms of its mathematics, sends each to the substrate that embodies it best, and lets nothing act until a verified gate admits it.

One theory, compiled into many forms; one gate, before anything acts. Each port carries its own mathematics: out in ink, back in verdigris. Touch a port to follow it.
  1. 01

    State the physics

    Write the process as mathematics: its states, controls, observations, dynamics and invariants, in a proof language.

  2. 02

    Find its forms

    Proved rewriting rules generate equivalent forms: an equation, a filter, a tensor network, a state machine, a quantised network.

  3. 03

    Match form to matter

    Each form goes to the substrate that embodies it best, weighed by energy, latency, error and the cost of checking. Safety is never a weight.

  4. 04

    Prove, then permit

    Each realisation carries its bound; a verified gate decides what may act, and an independent fabric witnesses that it did.

A system whose computation preserves the mathematical structure of the physical process it controls can achieve measurably better efficiency, reliability, predictability or safety than one that ignores that structure.

The hypothesis, and it is falsifiable: remove any one substrate and measure whether its affinity was real.
The Ontological Compiler →How a law becomes a machineBelieve, establish, permitBring your hardware