Intelligent systems · Research 002 · with BrainChip
Every model, with its paper trail. Proof-carrying AI on Akida.
BrainChip’s tools turn a trained neural network into something its Akida neuromorphic chip can run. We built the layer that proves what happened along the way: which model went in, how it was quantized and converted, how it was placed on the chip, and what came out, each step carrying a certificate a machine can check.
Round 1 of 7 complete · 29 phases closed · integration pilot next
- 01 · Quantizationpolicy = claim = filethe classes must agree three ways, by construction
- 02 · Model families3 certifiedspeech, vision and segmentation, from BrainChip’s own model zoo
- 03 · A named refusalcode 116when a link is missing, the checker names exactly what would supply it
- 04 · Hostile audit0 findingsin the independent hostile audit of the final chain
- 05 · The exact model126 layersbound to their exact bytes, with 252 weight datasets
- 06 · On real silicon25 / 25 identicaloutputs reproduced exactly on a physical AKD1500
01 · The question
What exactly is running on the chip?
A converted model is a long way from the network that was trained. Before this work, these questions had answers in logs and good intentions. Now each one has a machine-checkable answer, or a precise statement of what is missing.
- 01Which exact source model produced this artifact?
- 02Which quantization policy was used?
- 03Does the certificate really describe the inspected graph?
- 04Which converter and Akida target profile were used?
- 05Was software fallback prohibited?
- 06Which claims are proofs, which are observations, which are measurements?
- 07Can altered metadata or a substituted model still pass?
02 · The certificate chain
Try to break it.
Each step must hand the next a constructive witness. The final certificate exists only when every witness composes, so tampering anywhere stops the chain at the step it breaks, with the reason named.
Choose what to try
- Source modelONNX or Keras/HDF5, bound to its exact bytes and parsed into a typed graph
- Quantization certificatepolicy identity, clipping, ties-to-even rounding, quantizer classes
- Conversion certificateCNN2SNN: inspectable refinement, finite observation, or typed refusal
- Mapping certificatetarget generation, topology, resources, skip-DMA state, no software fallback
- Replay evidenceexact outputs for a named, frozen set of inputs
- Certified bundlebuilt only when every witness composes, or a typed refusal naming what is missingrefused ·
quantPolicyKerasClassBound
Refused, with its reasonBoth the policy and the claim were edited to agree. The bundle still cannot be built: the class extracted independently from the exact model file says 81, and the equality is required by the constructor itself.
03 · On real silicon
The proof reached the hardware, bit for bit.
BrainChip’s donated AKD1500 gave the work a physical anchor. The frozen model ran hardware-only on the chip, and every output matched the certified record exactly.
- Device
- AKD1500, PCIe, 16 MB
- Firmware
- BC.A1.003.009
- Mapping
- hardware only · no software fallback
- Layout
- 9 layers · 26 neural processors
- Skip DMAs
- 0
- External memory
- 57,344 bytes
- Inputs
- 25 of 25 frozen inputs observed
- Raw outputs
- 25 of 25 exact matches
- Dequantized outputs
- 25 of 25 exact binary32 matches
- Mutations
- 14 resealed mutations rejected · 42 regression tests, 0 failures
The receipt covers one frozen model, one named AKD1500 and its firmware, and 25 named inputs. The next rounds carry two more models onto the chip and compare results across software releases.
04 · Three model families
Different shapes, one certificate architecture.
From BrainChip’s own model zoo: speech, vision and segmentation. The extractor bound 126 layers and 252 weight datasets to their exact bytes, and the checker built a certified bundle for each family.
keyword spotting · depthwise-separable
DS-CNN
- 6
- quantizer classes bound
- 11
- conversion bridges & placements
certified bundle · code 0
image classification
AkidaNet
- 6
- quantizer classes bound
- 26
- conversion bridges & placements
certified bundle · code 0
segmentation · encoder/decoder
AkidaUNet
- 5
- quantizer classes bound
- 36
- conversion bridges & placements
certified bundle · code 0
vibration classification · the fourth pilot
UORED
Its ONNX source and a separately supplied quantized file were meant to be the same model, but nothing joined them. The checker refused to invent the link, and named exactly what would supply it.
typed refusal ·
sourceQuantizedDiscontinuity· code 116
A refusal is a result: it keeps a stronger claim from being built out of weaker evidence, and it tells an integrator precisely what to export upstream to turn it into a certificate.
05 · The safeguard
A check that cannot be talked around.
Our own hostile audit found that an earlier design could change two matching records together and still produce a certificate. The repair made the agreement part of the certificate’s construction, so it can never be skipped.
= classes in the quantization policy
= classes read independently from the exact model file
The decisive test changed a class code from 81 to 88 in both the policy and the claim, consistently. The certificate still could not be built: the independently extracted model said 81. The type checker rejected it before anything ran. That is the difference between validating a result after the fact and requiring the relationship in order to construct it at all.
Seven kinds of claim, never mixed
| Claim | Its witness |
|---|---|
| Source identity | hash and typed graph bound to frozen bytes |
| Quantization refinement | generated policy rows plus source-bound class equality |
| Conversion correspondence | an inspectable relation, or an explicitly finite observed one |
| Mapping admissibility | target capability and placement witnesses |
| Replay conformance | exact outputs for a named finite carrier |
| Physical conformance | named device, firmware, model, inputs, outputs, no fallback |
| Refusal | a typed constructor naming the missing obligation |
06 · Who it serves
Built for the places Akida already goes.
BrainChip’s customers put AI where a wrong answer is expensive: on fielded sensors, in orbit, on a patient, in a car. Each needs to know exactly what is running. Here is what the work gives them today, and what the next rounds add.
Parsons, RTX, the Air Force Research Laboratory, Bascom Hunter
Defense & aerospace
Know exactly which model is on a fielded sensor, prove it was not swapped, and check it where there is no network.
- Today
- Every artifact bound to its exact source, policy and mapping; hardware-only execution with fallback ruled out; a checker that runs offline.
- Next
- A signed deployment bundle for procurement and supply-chain review, and conformance across firmware releases.
Frontgrade Gaisler’s radiation-hardened processors, the European Space Agency
Space
Be certain, before uplink, that the model about to run in orbit is the one that was qualified on the ground.
- Today
- A typed refusal names any break in the chain before anything is sent, and a bundle can be re-checked with no ground service.
- Next
- A portable bundle that travels with the model, and checks that results hold across Akida generations and profiles.
Onsor’s seizure-prediction smart glasses
Medical wearables
A traceable, reproducible record of exactly which model a device runs, for the quality documentation a medical product needs.
- Today
- Source, quantization, conversion and mapping each carry a certificate; any drift or substitution becomes a named rejection.
- Next
- Certificates for recurrent and event-based models, the kinds that read signals over time.
Mercedes-Benz in-cabin keyword spotting, MegaChips
Automotive
Ship a software update and know the model still maps, runs and answers the same way on the car.
- Today
- Version-bound identities for package, model, firmware and target make every update comparable to the last.
- Next
- A cross-release laboratory that flags silent remapping, new fallback, resource growth and output drift.
Fanless M.2 and PCIe AKD1500 deployments
Industrial IoT & predictive maintenance
Trust an always-on anomaly detector in the field, and diagnose integration failures quickly when they happen.
- Today
- Our hardware result is itself a vibration classifier, reproduced exactly on the AKD1500; integration problems arrive as typed causes, not vague errors.
- Next
- The integration pilot: certificates emitted by BrainChip’s own workflow, for every model a customer converts.
ASICLAND, EDGEAI, MegaChips
Chip designers licensing Akida IP
Show that a model behaves as expected on their own Akida-based silicon and target profile.
- Today
- Mapping admissibility is checked against a named capability profile for each target generation.
- Next
- A conformance matrix across target profiles and IP generations, and a nonprofit Certified-on-Akida evaluation service.
Customers and markets as described in BrainChip’s public announcements: BrainChip newsletter, January 2026 · Parsons agreement · AKD1500 production shipments · BrainChip partners.
07 · What it means
From “it converts and runs” to “here is the certificate.”
This exact model, under this exact quantization and conversion configuration, produced this exact Akida artifact, which satisfied these mapping constraints and reproduced these observations, and the certificate is independently machine-checkable.
The story a proof-carrying Akida deployment can tell
Stronger provenance
Bind a deployed Akida artifact to its exact source model, configuration, conversion record, mapping profile and replay corpus.
Safer converter evolution
Check changes to QuantizeML, CNN2SNN, formats or profiles against formal obligations and biting mutation tests.
Clear trust boundaries
Keep proprietary internals private: the framework tells inspectable refinement apart from opaque but content-bound observation.
Model-zoo assurance
Extend the same architecture model by model into machine-verifiable assurance packages.
Integration risk, typed
Substitution, metadata drift, unsupported layers, profile mismatch, resource overflow and fallback become named rejections.
Offline verification
A recipient checks a frozen bundle without retraining or relying on any online service.
BrainChip’s proprietary converter stays private throughout: the framework certifies the relation it can observe or reconstruct, and states plainly which is which.
08 · The development record
From a pilot to a product BrainChip could ship.
The first program is closed. The next turns the prototype into an assurance sidecar for BrainChip’s public workflow, round by round, each with its own gate and each published here as it lands.
- 01
Phases P0–P28complete · 2026-11-06
An assurance layer around the Akida toolchain.
A safe-Agda certificate architecture, extracted to native code, around model ingestion, quantization, conversion, mapping and replay: an ONNX path, a Keras/HDF5 path, three model-family pilots, a preserved lineage refusal, an exact result on a physical AKD1500, and a hostile audit closed clean.
Its gate
Every certificate built only from composing witnesses; every documented mutation rejected; an independent reviewer returns CLEAN with zero findings; accepted in the proof store.
On this page
- The certificate chain and its mutations
- The AKD1500 receipt
- Three model-family certificates and the UORED refusal
- 02
Integration pilotnext on the bench
BrainChip’s own workflow emits the evidence.
Part of the follow-on program, Proof-Carrying Akida. The documented QuantizeML → CNN2SNN → Akida flow emits a small content-addressed evidence package beside each converted model, without disclosing any proprietary internals.
To be complete
Packages emitted at the BrainChip integration boundary for DS-CNN and one structurally different model; the extracted checker accepts both and rejects every listed mutation.
Adds to this page
- The first vendor-emitted evidence packages
- A partner certificate you can verify yourself
- 03
Deployment bundleplanned
A certificate that travels with the model.
Part of the follow-on program, Proof-Carrying Akida. One portable archive: the model, its evidence, the certificate or refusal, and the generated checker, verifiable offline with nothing else.
To be complete
A clean offline verifier checks the bundle without IAOM services, network access or a Python verdict.
Adds to this page
- A downloadable proof-carrying bundle
- Offline verification instructions
- 04
Model-zoo factoryplanned
From three families to every kind of model.
Part of the follow-on program, Proof-Carrying Akida. Certificates across genuinely different structures: MobileNetV1, AkidaNet18, CenterNet detection, PointNet++, a recurrent TENN and a DVS spatiotemporal model.
To be complete
Accepted certificates covering convolutional, depthwise, residual, detection, point-cloud, recurrent and event-based structure, reported by semantic class, not model count.
Adds to this page
- A coverage map by operator and structure
- One certificate per family
- 05
Hardware & version laboratoryplanned
Two models on silicon, across releases.
Part of the follow-on program, Proof-Carrying Akida. DS-CNN and MobileNetV1 run on the AKD1500 under frozen identities, then compared across at least two MetaTF releases and two target profiles.
To be complete
A sealed physical conformance matrix for both models, and a conformance matrix that reports every drift in mapping, resources, fallback and outputs.
Adds to this page
- The two-model hardware matrix
- The cross-release conformance table
- 06
Evaluation service & demonstratorplanned
Certified on Akida, for anyone who asks.
Part of the follow-on program, Proof-Carrying Akida. A nonprofit evaluation protocol for BrainChip customers, a public DS-CNN demonstrator, and a joint technical paper.
To be complete
A blind submission reproduced by a second reviewer; a demonstrator that visibly runs source to certificate to rejected mutations.
Adds to this page
- The public demonstrator
- The evaluation-service protocol
- The joint paper
- 07
Independent closureplanned
Handed to someone who did not build it.
Part of the follow-on program, Proof-Carrying Akida. A reviewer who is not the author reads the soundness proof, runs genuine and mutated bundles end to end, and signs a clean report.
To be complete
A signed CLEAN report with zero open findings.
Adds to this page
- The independent closure report
09 · How it is built
The verdict comes from the proof, not from a script.
The formal core and the extracted checker
Written in Agda 2.8.0 under --safe and --without-K, extracted through MAlonzo and compiled with GHC 9.12.2. No hand-written verdict code: every acceptance or refusal is computed by code generated from the safe formal core. Python only prepares inputs and carries receipts.
Why a certificate is a construction
Under the Brouwer–Heyting–Kolmogorov reading, a claim is accepted only by building its evidence: a pair for “and”, an executable transformation for “implies”, a named witness for “there exists”. The certified bundle is a dependent record whose constructor cannot be called unless every source, policy, conversion, placement, replay and identity field is present; categorically, a cone over the diagram of phases, witnessing that the diagram commutes.
Exactly what is certified
The certificates cover the exact models, toolchain versions, device and inputs they name. They do not assert the correctness of BrainChip’s proprietary converter internals, equivalence for every possible model or input, or accuracy across a population. That precision is part of the result: the checker accepts exactly the evidence it can construct, and names the rest.
The full technical report
The complete report, with its technical and mathematical annex, is available to partners and reviewers. Request the report →
BrainChip references
Research & equipment partner
AKD1500 · neuromorphic AIA physical anchor for a formal idea.
BrainChip’s donated AKD1500 let this work reach real silicon instead of stopping at a simulator. In return, IAOM offers an independent, nonprofit formal-methods view that can make Akida deployments more trustworthy, auditable and defensible, and publishes what it finds.