Formal verification of binary neural networks via 1-safe Petri net models
$ pip install sanad_tester
Collecting sanad_tester
Downloading sanad_tester-1.2.0-py3-none-any.whl (48 kB)
Installing collected packages: sanad_tester
Successfully installed sanad_tester-1.2.0
$ python -c "import sanad_tester; print(sanad_tester.__version__)"
1.2.0
pip install sanad_tester
Latest Release
1.2.0 (Apr 2026)
Quickstart
import numpy as np
from sanad_tester import OneSafePetriNet, BNNConverter, verify_safety
# Load your binary neural network weights
weights = np.load("model_weights.npy")
# Convert to a 1-safe Petri net (see PDF Section 3)
converter = BNNConverter(weights)
petri_net = converter.to_petri_net()
# Run formal safety verification (PDF Algorithm 2)
result = verify_safety(petri_net)
print(f"Safe: {result.is_safe}") # True
print(f"States: {result.n_states}") # 2048
# Reachability analysis
graph = petri_net.reachability_graph()
for marking in graph.deadlocks():
print(f"Deadlock at: {marking}")
# Full API reference is in the paper PDF — download it.
Dependencies
| Package | Version | Purpose |
|---|
numpy | >= 1.21 | Array operations for weight matrices |
scipy | >= 1.7 | Sparse matrix support for large nets |
networkx | >= 2.6 | Reachability graph construction |
tqdm | >= 4.60 | Progress bars for state enumeration |