Foundation
ArithSpec and deposited documents
Two runs of the same program on two different machines do not always give the same result: floating-point computations depend on the processor, the compiler and the order of operations. To verify a computation, you first need to be able to redo it identically.
ArithSpec fixes that result. It is a normative arithmetic specification: every operation is defined down to the last bit, with its rounding, its saturation and flags that report every approximation instead of hiding it. According to the deposit, three independent implementations (C, Python and Rust) produce the same SHA-256 conformance hash on x86-64 and aarch64 processors.
The specification
TitleA Normative Arithmetic Substrate for Bit-Exact Spiking Neural Networks
Published13 June 2026, Zenodo, open access, CC BY 4.0 licence
Four papers
Published on 2 August 2026 on Zenodo, open access, CC BY 4.0 licence, each with its data and a checksum file to verify the files.
APer-Tick Certification of Spike-Exact Fixed-Point Spiking Neural Networks. A certificate computed at every time step guarantees, under assumptions stated in the paper, that a fixed-point network emits exactly the same spikes as the floating-point reference network. Out of 18,375 configurations tested, no certified configuration diverged (zero observed false positives); 74.17% of configurations are certified. DOI 10.5281/zenodo.21749446
BInternal Margins Collapse, Decision Margins Grow: Why Trained Spiking Networks Tolerate Low Precision. Two margins move in opposite directions during the tested training: the internal margin shrinks while the decision margin grows. They answer different questions. DOI 10.5281/zenodo.21750036
DRate-Level Robustness in Deterministic Spiking Networks: When Spike-Train Fidelity Overstates Observed Functional Fragility. Spike-by-spike fidelity overstates observed fragility; out of 18,375 configurations, 83.7% keep exactly the same spike train and 99.8% the same decision. DOI 10.5281/zenodo.21750042
ERate-Level Robustness under Quantization in Connectome-Instantiated LIF Models. An exploratory study of observed robustness under quantization, on networks instantiated from published connectomes. DOI 10.5281/zenodo.21750053
Limits
These five documents are preprints: they are not peer-reviewed. The proof of the certificate in paper A is written by hand and not machine-checked; it covers LIF-type neurons within a set of assumptions stated in the paper. Paper E is exploratory. Corrected versions, if any, appear as new versions on Zenodo; the history remains available.
