Founding specification · Reference architecture
ArithSpec — a normative arithmetic substrate for bit-exact spiking networks
Everything else in this project rests on a single decision: computing in integer arithmetic, defined to the bit, rather than in floating point. This is the formal specification of the ArithSpec architecture, the normative foundation of the whole research programme.
ARITHSPEC · THE DIFFERENCE AT A GLANCE
Same input. Two ways to get a result.
Floating-point results can vary with the execution environment. ArithSpec fixes the rules of computation down to the bit: for the same protocol, conforming implementations must produce the same result.
Floating point
Variation can occur
Same input, two executions. A numerical variation can propagate.
ArithSpec · deterministic computation
Bit-exact
Same input, conforming implementations: the paths overlap.
- Input
- Computation
- Rounding
- Propagation
- Output
- Replay
- Comparison
Qualitative diagram, not measured data. Floating-point divergence is not systematic; its path is deliberately exaggerated to make the concept visible. The ArithSpec path illustrates the specified outcome for conforming implementations.
Specification and conformance results: ArithSpec record · DOI 10.5281/zenodo.20723008
Why remove floating point
The same floating-point program, compiled twice with different options, can produce two different results. Across two processor architectures it is close to guaranteed. The differences are minuscule — on the order of one part in a billion — and entirely sufficient for a neuron to cross its threshold on one side and not the other.
From that instant the two executions diverge, and nothing is comparable any longer. A decision can no longer be replayed identically, nor compared against a reference, nor demonstrated to an auditor as matching the validated version.
ArithSpec removes the problem at its root: fixed-point integer arithmetic, round-to-nearest-even with guard bits, explicit saturation after rounding, five observable anomaly flags, canonical serialisation. No freedom is left to the implementation.
What “normative” means
The word is used in the standards-engineering sense, not the philosophical one. A normative specification prescribes exact behaviour and leaves no implementation freedom in the arithmetic operations.
A conformant implementation must produce exactly the specified result — not an approximation, not a result “equivalent to within ε”. Exactly identical. Bit for bit.
This is a far stronger requirement than the usual numerical agreement. “Almost the same” is forbidden. Specification v2.5 has been frozen since 7 June 2026: it cannot change without incrementing the major version, precisely so that a fingerprint computed today remains checkable in ten years.
The family: Full, Lite, Mini
ArithSpec is not a single format but a family, covering everything from server to the smallest microcontroller. Each member is bit-exact with itself on every platform — but the members are not bit-exact with one another: they are distinct specifications.
| Member | Format | Native type | Resolution | Use | Status |
|---|---|---|---|---|---|
| ArithSpec-Full | INT64 · Q32.32 | int64 / int128 accumulator | ≈ 2.3 × 10⁻¹⁰ | Reference, PC and server | Reference |
| ArithSpec-Lite | INT32 · Q16.16 | int32 / int64 accumulator | ≈ 1.5 × 10⁻⁵ | Embedded — Pi, Pico | Certified |
| ArithSpec-Mini | INT16 · Q8.8 | int16 | ≈ 3.9 × 10⁻³ | Ultra-embedded | Future work |
It is a way of storing a fractional number inside an integer. “Q16.16” means 16 bits for the integer part and 16 bits for the part after the point. The number 1.5 is then written as the integer 98,304 (that is, 1.5 × 65,536). All the arithmetic happens on these integers — and because integers never “float”, two machines obtain exactly the same result.
The formula that decides everything
The heart of the specification is multiplication. That is where reproducibility is decided, because multiplying two fixed-point numbers produces too many bits, and some must be discarded — which means rounding. A badly specified rounding, and two implementations diverge. ArithSpec mandates round-to-nearest-even (RNE), with three control bits named Guard, Round and Sticky.
P = a × b → Q = P ≫ 16 then RNE rounding
The exact rule (ArithSpec-Lite): if the remainder exceeds one half, add 1; if it equals exactly one half, add 1 only when Q is odd. That last clause — ties-to-even — is what eliminates the statistical bias of rounding.
The same logic governs addition, which saturates instead of overflowing: if the result leaves the range, it is clamped to the bound and raises an anomaly flag, instead of silently wrapping to the other extreme as an ordinary machine integer would.
Key point
Every operation is specified down to the rounding bit. It is tedious — and it is precisely what many libraries lack, where rounding can depend on the compiler. This meticulous precision is the foundation of everything else.
The observable: a fingerprint
How can two implementations be shown to agree, without comparing them instruction by instruction? The entire computation trajectory is captured, its SHA-256 is taken, and the fingerprints are compared. Two implementations are conformant if, and only if, they produce the same one.
It is a binary test, with no grey area. An identical fingerprint establishes bit-for-bit agreement across hundreds of thousands of operations; a different fingerprint refutes it. There is nothing to negotiate.
The conformance chain
This is the most concrete result of this work, and the easiest to refute: if a single platform produced a different fingerprint, the claim would fall.
source: campaign of 8 to 16 June 2026 (protocol not yet published)
A second, independent protocol measures the same property at network scale: 1,000 neurons and 24,788 synapses executed on x86-64 Windows and on native ARM64 (Raspberry Pi 5) produce an identical fingerprint for the canonical seed and for five further seeds (paper E, §3.5). On each platform, a double execution gives the same fingerprint — intra-platform determinism is established before any cross-platform comparison.
The physical microcontroller
The last row of the table is worth pausing on. It is not an emulator: it is a real Raspberry Pi Pico, an RP2040 chip with a dual-core Cortex-M0+. Flashed with MicroPython, it executed the 200,000 operations via that path on 16 June 2026, three days after the paper was deposited, and produced — bit for bit — the reference fingerprint e1606bef…
What is certified here is the arithmetic substrate: integer computation runs bit-exact from server to microcontroller. This is not embedded learning, nor an embedded decision loop: those remain objectives. The reproducibility of the computation, on the other hand, is established on real hardware, down to the Raspberry Pi Pico microcontroller (MicroPython path).
The formal models
Beyond measured conformance, five models were submitted to bounded exhaustive enumeration with the TLC tool. The term matters: this is not universal formal verification, it is the complete exploration of a finite, declared state space.
TLC2 v2.19, OpenJDK Temurin 21
See the data
| Model | Distinct states | Result |
|---|---|---|
| K0Composition | 19,683 | 5 invariants, no error |
| ArithSpecMonoidal | 1,679,616 (= 36⁴) | 11 invariants, no error |
| ArithSpecTrace | 343 (= 7³) | 4 invariants, strict associativity |
| ArithSpecLaxWitness | — | expected counter-example: x=−1, y=1, z=65536 |
| ArithSpecTrace (witness) | — | expected counter-example: non-commutative concatenation |
Scope and limitations
- ArithSpec is not an efficiency specification. It prescribes reproducible exactness, not speed or power consumption.
- The TLC exploration is a bounded exhaustive enumeration over declared finite state spaces — never a universal proof.
- Cross-platform conformance concerns the arithmetic substrate. It says nothing about learning or an embedded behavioural loop.
- On the microcontroller, conformance was checked via the MicroPython path; the Rust, C++ and Python implementations were checked on PC or on Raspberry Pi 5 (figure 1).
- ArithSpec-Mini (Q8.8) is a declared objective, not a result.
Algorithmic reproducibility
The public deposit
The founding document is deposited in open access, under a CC BY 4.0 licence, in French and English.
Two identifiers, one document. 10.5281/zenodo.20723008 designates the concept — it always points to the latest version. 10.5281/zenodo.20723009 designates version v1 precisely. To cite the work, use the first.
Reproducing conformance
The protocol is short and fully specified: fixed seed, 200,000 iterations, normative Q16.16 multiplication with GRS+RNE rounding, saturating addition, threshold firing, a 14-byte binary transcript per iteration, then SHA-256 over the whole.
SEED = 0x123456789abce900
N_OPS = 200,000
THETA = 1 << 15 (0.5 in Q16.16)
EMIT_CAP = 15
expected fingerprint:
e1606bef1b34afe155adeace4aae7fd2aa22f0236ada22a61dd71631baae050aAn implementation that produces this fingerprint is conformant. An implementation that produces another one is not — and there is nothing to negotiate.