# A Formal Tool for Verification of Probabilistic Spiking Neural Networks Based on Quotient Abstractions

arXiv: https://arxiv.org/abs/2606.20674 · HTML: https://mlsanity.com/paper/2606.20674/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 2 of its 21 references that are in the map.
- First posted on arXiv 12 Jun 2026.

## Builds on (most cited first, 2 of 2)

- [BindsNET: A machine learning-oriented spiking neural networks library in Python](https://mlsanity.com/paper/1806.01423/) (2018)
- [Spiking Neural Networks modelled as Timed Automata with parameter learning](https://mlsanity.com/paper/1808.01893/) (2018)

## Abstract (arXiv)

Spiking Neural Networks (SNNs) model biological neural dynamics more faithfully than classical artificial networks, but their stochastic, event-driven computation -- rooted in ion-channel noise and unreliable synaptic vesicle release -- demands probabilistic models for which deterministic abstractions are mathematically inadequate. Formal verification of such models via probabilistic model checking faces a fundamental barrier: the state space explosion problem, where the Discrete-Time Markov Chain (DTMC) encoding grows exponentially with the number of neurons. General-purpose quotient model abstractions [1] can in principle mitigate this growth by partitioning membrane potentials into equivalence classes, but a na"ive application to SNNs discards synaptic weight information, limiting the properties that can be verified. This paper introduces a weight-discretized quotient model abstraction that maps continuous synaptic weights to a compact integer range while preserving the relative contribution of each synapse, and presents CogSpike, a unified workbench that integrates SNN design, simulation, and PRISM-based formal verification within a single isomorphic tool chain. The discretization is accompanied by formal correctness guarantees: a two-sided fidelity theorem confines any firing disagreement to a bounded gray zone around threshold, and an Asymptotic Silence theorem gives the exact limit guarantee that unforced neurons fall permanently silent. A topology-dependent scaling analysis shows that the state space reduction compounds exponentially -- approximately 17× per neuron for discretization parameter W = 3 -- enabling verification of networks that are otherwise intractable, as confirmed empirically across seven canonical topologies.