Research programme · version 1 · October 2026

Toward deterministic, certifiable embedded AI

Jean-René Denoual · EventCompute · independent researcher, Brittany, France

• 1. Introduction
• 2. Foundation
• 3. Test bench
• 4. Method
• 5. Experiments
• 6. Atlas
• 7. Applications
• 8. Limits and next steps
• References

1. Introduction

The same program, run on two different machines, does not always give the same result: floating-point computations depend on the processor, the compiler and the order of operations. For most uses the difference is negligible. For AI embedded in a device, a machine or a sensor, it raises a fundamental question: how can one prove that a network, once reduced in precision and installed on a chip, makes the same decisions as the original model? In aviation, the European Union Aviation Safety Agency (EASA) already asks, in its AI guidance, that quantization and optimisation of a model be verified not to alter its properties [11].

This programme starts from a simple requirement: a computation only counts if it can be redone bit for bit and checked by a third party. Its contributions are:

• a published normative arithmetic foundation, ArithSpec, and four papers that derive certificates and robustness measurements from it;
• a deterministic, replayable learning test bench, and first results;
• a research method in which only a certificate validates a result, put to the test on international challenges;
• the project of an open Atlas of certified computations.

2. Foundation: ArithSpec and certificates

ArithSpec is an arithmetic specification for spiking neural networks (neuromorphic computing). Each of its operations is defined down to the bit, with its rounding, its saturation and flags that report every anomaly instead of hiding it. Three independent implementations, in C, Python and Rust, produce the same conformance hash on x86-64 and ARM processors [1]; in study [5], a Raspberry Pi 5 reproduces bit for bit the results obtained on an x86-64 processor.

Four open-access papers build on this foundation:

• Per-time-step certificate [2]: when satisfied, and under the paper’s assumptions, it guarantees that a fixed-point network emits exactly the same spikes as its floating-point reference. Out of 18,375 configurations, no false positive was observed and 74.17% of configurations are certified.
• Margins and reduced precision [3]: during the tested training, the internal margin shrinks while the decision margin grows.
• Rate-level robustness [4]: out of 18,375 configurations, 83.7% keep exactly the same spike train and 99.8% the same decision.
• Quantization on connectomes [5]: an exploratory study on networks instantiated from published connectomes.

3. Test bench: a learning circuit

In paper [4], activity is propagated deterministically through networks modelled from the fruit-fly connectome published by the FlyWire consortium [6], up to the complete connectome of 139,255 neurons; two runs give the same trace. To test my hypotheses on learning, I use a much smaller circuit, modelled from a part of this connectome.

Experiment. The model learns a first task, then a second one. Its performance on the first task is then measured. This is the difficulty known as catastrophic forgetting: most neural networks lose what they knew when they learn something else.

Results. The model partly retains the first task: its performance stays above chance (about 0.62 on average over a study series of 12 simulated individuals, against 0.50 for chance; one of them stays below chance), while dropping clearly below the level reached right after the first learning. On the protocols tested, its recorded decisions replay identically, bit for bit, with two implementations (Python and Rust). After an interruption in the middle of the second task, resuming from the checkpoint gives exactly the same final state (checked on a test case). The learning protocol is supervised.

Frugality. The AI is designed to be frugal: the whole network is kept, but only the part that is needed is meant to be activated at each moment. The gain is yet to be measured.

This test bench could serve other research teams, in other fields: simulating how activity propagates through an entire network, then replaying it step by step to analyse it.

4. Method

In the research method, every hypothesis is tested by computation and kept only if a certificate proves it, that is, if a program independent of the search checks it. Generative AI tools serve as assistants. While developing this project, I found that it could be adapted to probabilistic AI in a different way: it is with this method that I obtained the challenge results below. Every certified result and every dead end is recorded in the Atlas (§6).

The inner workings of the method remain confidential. Its results are public: a certificate can be checked without knowing the method that produced it, just as a proof can be checked without knowing who found it.

Computing resources. All the work runs on accessible hardware: a desktop PC (6 cores, 12 threads, NVIDIA RTX 3060 graphics card with 12 GB, Intel Core i5 processor, 32 GB of RAM); a Raspberry Pi 5 and a Raspberry Pi Pico microcontroller, which are also used to check that computation stays identical from one machine to another; and the server that hosts this site (4 virtual processors), put to work to use all the computing power available. Occasionally, a 32-virtual-processor compute instance was used to study how computation grows with problem size.

5. Experiments: external validation on international challenges

To put the method to the test, I applied it to public scientific challenges, chosen in different fields. In each of them, the organisers check the solutions with their own programs. The results below are therefore validated by third parties.

Positions recorded on the dates given on each challenge page; they may have changed since.

Reading. The same method produces solutions accepted by independent referees in four distinct fields: geometry, space mechanics, graphs and number theory. Each result, with its source and date, is detailed on the Results page.

6. The Atlas: seeing the problems and the world the AI evolves in, and its open part

An AI must be able to visualise the problems and the world in which it evolves: the Atlas is that representation, and the one on which I am building the AI: it is enriched by every certified result and every dead end, and the challenge results were obtained by recording them in this way. It is not a black box: every entry carries its certificate, and since everything replays bit for bit, the effect of a change is measured exactly. I aim to extend this approach to a visual environment, for robots and drones that learn from the consequences of their actions. Any computation certified once never needs to be redone. I am preparing an open Atlas of these computations: every result with its certificate, and the areas explored, including those that led nowhere. It will make it possible never to recompute what is proven, to avoid dead ends already explored, to start from an established result, to re-check a result without trusting anyone, and to see which results depend on each other. Details →

7. Target applications

Vision: another kind of artificial intelligence. Large language models are probabilistic and computationally hungry; on their own they are not enough where a decision has to be proven, replayed and certified. This programme is building an AI of a different kind: deterministic and learning, keeping only what a certificate proves. It targets five routes: embedded AI, agent identity, certification, audit and, as a parallel line of research, interaction with language models; in particular: reliable AI agents, certification, and embedded AI in robots, drones and autonomous machines.

• Certifiable embedded AI: proving that a reduced-precision network installed on a chip makes the same decisions as the original model.
• Certifiable AI: AI systems whose every decision can be checked by a third party.
• Interaction with language models (parallel research): a controlled execution framework, a memory and a replayable verification around probabilistic proposals.
• Verifiable identity for AI agents: a history that can be replayed identically.
• Post-incident analysis: replaying a past decision exactly to understand what happened.
• Reproducible science and verification for the referees of scientific leaderboards.

8. Limits and next steps

• The deposited documents are preprints, not peer-reviewed.
• The embedded AI is at the prototype stage, on the test bench; it has not yet been demonstrated on a real-world task.
• Leaderboard positions are dated and can be taken over.
• No form of cognition or understanding is claimed; the test bench does not claim to reproduce how the fly works.
• Next steps: demonstrate the prototype on a real-world task, publish a first Atlas, measure frugality, then extend the method to interaction with language models.

References

1. J.-R. Denoual, A Normative Arithmetic Substrate for Bit-Exact Spiking Neural Networks (ArithSpec), Zenodo, 2026. DOI 10.5281/zenodo.20723008
2. J.-R. Denoual, Per-Tick Certification of Spike-Exact Fixed-Point Spiking Neural Networks, Zenodo, 2026. DOI 10.5281/zenodo.21749446
3. J.-R. Denoual, Internal Margins Collapse, Decision Margins Grow: Why Trained Spiking Networks Tolerate Low Precision, Zenodo, 2026. DOI 10.5281/zenodo.21750036
4. J.-R. Denoual, Rate-Level Robustness in Deterministic Spiking Networks: When Spike-Train Fidelity Overstates Observed Functional Fragility, Zenodo, 2026. DOI 10.5281/zenodo.21750042
5. J.-R. Denoual, Rate-Level Robustness under Quantization in Connectome-Instantiated LIF Models, Zenodo, 2026. DOI 10.5281/zenodo.21750053
6. S. Dorkenwald et al., “Neuronal wiring diagram of an adult brain”, Nature 634, 2024; P. Schlegel et al., “Whole-brain annotation and multi-connectome cell typing of Drosophila”, Nature 634, 2024; FlyWire data, version 783, used for research purposes under their terms of use. codex.flywire.ai (accessed 7 Oct 2026)
7. E. Specht, Packomania “csqv” table. packomania.com (accessed 4 Oct 2026)
8. European Space Agency, SpOC 4 challenge, ESA Optimize platform. github.com/esa/SpOC4 (accessed 4 Oct 2026)
9. FlyWire Codex, Max Quasi-Cliques challenge. codex.flywire.ai (accessed 7 Oct 2026)
10. IBM Research, Ponder This, September 2026. research.ibm.com (accessed 11 Oct 2026)
11. EASA, Artificial Intelligence Concept Paper, Issue 02, March 2024. easa.europa.eu (accessed 3 Oct 2026)