Rename from tiny-parity-verified

README.md

@@ -0,0 +1,117 @@
+---
+license: mit
+tags:
+- pytorch
+- safetensors
+- threshold-logic
+- neuromorphic
+- parity
+---
+
+# threshold-parity
+
+Computes 8-bit parity (XOR of all bits). A canonical hard function for threshold networks - parity requires depth.
+
+## Circuit
+
+```
+  x₀ x₁ x₂ x₃ x₄ x₅ x₆ x₇
+   │  │  │  │  │  │  │  │
+   └──┴──┴──┴──┼──┴──┴──┴──┘
+               ▼
+       ┌─────────────┐
+       │   Layer 1   │  11 neurons (pruned)
+       │  ±1 weights │
+       └─────────────┘
+               │
+               ▼
+       ┌─────────────┐
+       │   Layer 2   │  3 neurons
+       └─────────────┘
+               │
+               ▼
+       ┌─────────────┐
+       │   Output    │
+       └─────────────┘
+               │
+               ▼
+         {0, 1} = HW mod 2
+```
+
+## Why Is Parity Hard?
+
+Parity is HW mod 2 - the simplest modular function. Yet it's notoriously difficult:
+
+1. **Not linearly separable**: No single hyperplane separates odd from even HW
+2. **Flat loss landscape**: Gradient descent fails because parity depends on a global property
+3. **Requires depth**: Minimum 3 layers for threshold networks
+
+This network was found via evolutionary search (10,542 generations), not gradient descent.
+
+## Algebraic Insight
+
+For any ±1 weight vector w, the dot product w·x has the same parity as HW(x):
+
+```
+(-1)^(w·x) = (-1)^HW(x)
+```
+
+This is because each +1 weight contributes its input's value, and each -1 weight contributes -(input) ≡ input (mod 2).
+
+The network uses this to detect whether HW is even or odd.
+
+## Architecture
+
+| Variant | Architecture | Parameters |
+|---------|--------------|------------|
+| Full | 8 → 32 → 16 → 1 | 833 |
+| Pruned | 8 → 11 → 3 → 1 | 139 |
+
+The pruned variant keeps only the 14 critical neurons identified through ablation.
+
+## How It Works
+
+The pruned network has three L2 neurons:
+- L2-N0: Always fires (large positive bias)
+- L2-N1: Fires iff HW is even (parity discriminator)
+- L2-N2: Always fires (large positive bias)
+
+Output: `L2-N0 - L2-N1 + L2-N2 - 2 ≥ 0` = NOT(L2-N1)
+
+Since L2-N1 fires when even, output fires when odd. That's parity.
+
+## Usage
+
+```python
+from safetensors.torch import load_file
+import torch
+
+w = load_file('model.safetensors')
+
+def forward(x):
+    x = x.float()
+    x = (x @ w['layer1.weight'].T + w['layer1.bias'] >= 0).float()
+    x = (x @ w['layer2.weight'].T + w['layer2.bias'] >= 0).float()
+    x = (x @ w['output.weight'].T + w['output.bias'] >= 0).float()
+    return x.squeeze(-1)
+
+inp = torch.tensor([[1,0,1,1,0,0,1,0]])  # HW=4
+print(int(forward(inp).item()))  # 0 (even)
+```
+
+## Files
+
+```
+threshold-parity/
+├── model.safetensors
+├── model.py
+├── config.json
+├── README.md
+└── pruned/
+    ├── model.safetensors
+    └── ...
+```
+
+## License
+
+MIT

config.json

@@ -0,0 +1,11 @@
+{
+  "model_type": "threshold_network",
+  "n_bits": 8,
+  "hidden1": 32,
+  "hidden2": 16,
+  "output": 1,
+  "total_parameters": 833,
+  "weight_quantization": "ternary",
+  "activation": "heaviside",
+  "task": "parity"
+}

model.py

@@ -0,0 +1,87 @@
+"""
+Threshold Network for Parity Computation
+
+A ternary threshold network that computes the parity (XOR) of 8 binary inputs.
+Weights are constrained to {-1, 0, +1} and activations use the Heaviside step function.
+"""
+
+import json
+import torch
+import torch.nn as nn
+
+
+class ThresholdNetwork(nn.Module):
+    """
+    Binary threshold network with ternary weights.
+
+    Architecture: 8 -> 32 -> 16 -> 1
+    Weights: {-1, 0, +1}
+    Activation: Heaviside (x >= 0 -> 1, else 0)
+    """
+
+    def __init__(self, n_bits=8, hidden1=32, hidden2=16):
+        super().__init__()
+        self.n_bits = n_bits
+        self.hidden1 = hidden1
+        self.hidden2 = hidden2
+
+        self.layer1_weight = nn.Parameter(torch.zeros(hidden1, n_bits))
+        self.layer1_bias = nn.Parameter(torch.zeros(hidden1))
+        self.layer2_weight = nn.Parameter(torch.zeros(hidden2, hidden1))
+        self.layer2_bias = nn.Parameter(torch.zeros(hidden2))
+        self.output_weight = nn.Parameter(torch.zeros(1, hidden2))
+        self.output_bias = nn.Parameter(torch.zeros(1))
+
+    def forward(self, x):
+        """Forward pass with Heaviside activation."""
+        x = x.float()
+        x = (torch.nn.functional.linear(x, self.layer1_weight, self.layer1_bias) >= 0).float()
+        x = (torch.nn.functional.linear(x, self.layer2_weight, self.layer2_bias) >= 0).float()
+        x = (torch.nn.functional.linear(x, self.output_weight, self.output_bias) >= 0).float()
+        return x.squeeze(-1)
+
+    @classmethod
+    def from_safetensors(cls, path):
+        """Load model from SafeTensors file."""
+        from safetensors.torch import load_file
+
+        weights = load_file(path)
+
+        hidden1 = weights['layer1.weight'].shape[0]
+        hidden2 = weights['layer2.weight'].shape[0]
+        n_bits = weights['layer1.weight'].shape[1]
+
+        model = cls(n_bits=n_bits, hidden1=hidden1, hidden2=hidden2)
+        model.layer1_weight.data = weights['layer1.weight']
+        model.layer1_bias.data = weights['layer1.bias']
+        model.layer2_weight.data = weights['layer2.weight']
+        model.layer2_bias.data = weights['layer2.bias']
+        model.output_weight.data = weights['output.weight']
+        model.output_bias.data = weights['output.bias']
+
+        return model
+
+
+def parity(x):
+    """Ground truth parity function."""
+    return (x.sum(dim=-1) % 2).float()
+
+
+if __name__ == '__main__':
+    model = ThresholdNetwork.from_safetensors('model.safetensors')
+
+    test_inputs = torch.tensor([
+        [0, 0, 0, 0, 0, 0, 0, 0],
+        [1, 0, 0, 0, 0, 0, 0, 0],
+        [1, 1, 0, 0, 0, 0, 0, 0],
+        [1, 1, 1, 0, 0, 0, 0, 0],
+        [1, 1, 1, 1, 1, 1, 1, 1],
+    ], dtype=torch.float32)
+
+    outputs = model(test_inputs)
+    expected = parity(test_inputs)
+
+    print("Input -> Output (Expected)")
+    for i in range(len(test_inputs)):
+        bits = test_inputs[i].int().tolist()
+        print(f"{bits} -> {int(outputs[i].item())} ({int(expected[i].item())})")

model.safetensors

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:8a4f4a10ee1fd3f85c6bee53cfc52297e1acca03a6d80fad2357a53582ed1226
+size 3772

pruned/README.md

@@ -0,0 +1,27 @@
+# Pruned Variant
+
+Minimal subnetwork extracted from the full model via neuron ablation analysis.
+
+## Architecture
+
+| Layer | Full | Pruned |
+|-------|------|--------|
+| Hidden 1 | 32 | 11 |
+| Hidden 2 | 16 | 3 |
+| Parameters | 833 | 139 |
+
+## Pruning Method
+
+Systematic single-neuron ablation identified which neurons are critical (their removal degrades accuracy) versus redundant (their removal has no effect). Only 11 of 32 Layer-1 neurons and 3 of 16 Layer-2 neurons were critical. The minimal subnetwork retains only these neurons.
+
+## Verification
+
+Correctness is proven in Coq for all 256 inputs, identical to the full network. See `PrunedThresholdLogic.v` in the [GitHub repository](https://github.com/CharlesCNorton/threshold-logic-verified).
+
+## Usage
+
+```python
+from model import PrunedThresholdNetwork
+
+model = PrunedThresholdNetwork.from_safetensors('model.safetensors')
+```

pruned/config.json

@@ -0,0 +1,13 @@
+{
+  "model_type": "threshold_network",
+  "n_bits": 8,
+  "hidden1": 11,
+  "hidden2": 3,
+  "output": 1,
+  "total_parameters": 139,
+  "weight_quantization": "ternary",
+  "activation": "heaviside",
+  "task": "parity",
+  "pruned_from": "8->32->16->1",
+  "reduction": "83.3%"
+}

pruned/model.py

@@ -0,0 +1,78 @@
+"""
+Pruned Threshold Network for Parity Computation
+
+A minimal ternary threshold network (8->11->3->1) that computes 8-bit parity.
+Pruned from the original 8->32->16->1 architecture with 83.3% parameter reduction.
+"""
+
+import torch
+import torch.nn as nn
+
+
+class PrunedThresholdNetwork(nn.Module):
+    """
+    Pruned binary threshold network with ternary weights.
+
+    Architecture: 8 -> 11 -> 3 -> 1
+    Weights: {-1, 0, +1}
+    Activation: Heaviside (x >= 0 -> 1, else 0)
+    """
+
+    def __init__(self, n_bits=8, hidden1=11, hidden2=3):
+        super().__init__()
+        self.n_bits = n_bits
+        self.hidden1 = hidden1
+        self.hidden2 = hidden2
+
+        self.layer1_weight = nn.Parameter(torch.zeros(hidden1, n_bits))
+        self.layer1_bias = nn.Parameter(torch.zeros(hidden1))
+        self.layer2_weight = nn.Parameter(torch.zeros(hidden2, hidden1))
+        self.layer2_bias = nn.Parameter(torch.zeros(hidden2))
+        self.output_weight = nn.Parameter(torch.zeros(1, hidden2))
+        self.output_bias = nn.Parameter(torch.zeros(1))
+
+    def forward(self, x):
+        """Forward pass with Heaviside activation."""
+        x = x.float()
+        x = (torch.nn.functional.linear(x, self.layer1_weight, self.layer1_bias) >= 0).float()
+        x = (torch.nn.functional.linear(x, self.layer2_weight, self.layer2_bias) >= 0).float()
+        x = (torch.nn.functional.linear(x, self.output_weight, self.output_bias) >= 0).float()
+        return x.squeeze(-1)
+
+    @classmethod
+    def from_safetensors(cls, path):
+        """Load model from SafeTensors file."""
+        from safetensors.torch import load_file
+
+        weights = load_file(path)
+
+        hidden1 = weights['layer1.weight'].shape[0]
+        hidden2 = weights['layer2.weight'].shape[0]
+        n_bits = weights['layer1.weight'].shape[1]
+
+        model = cls(n_bits=n_bits, hidden1=hidden1, hidden2=hidden2)
+        model.layer1_weight.data = weights['layer1.weight']
+        model.layer1_bias.data = weights['layer1.bias']
+        model.layer2_weight.data = weights['layer2.weight']
+        model.layer2_bias.data = weights['layer2.bias']
+        model.output_weight.data = weights['output.weight']
+        model.output_bias.data = weights['output.bias']
+
+        return model
+
+
+def parity(x):
+    """Ground truth parity function."""
+    return (x.sum(dim=-1) % 2).float()
+
+
+if __name__ == '__main__':
+    model = PrunedThresholdNetwork.from_safetensors('model.safetensors')
+
+    # Test all 256 inputs
+    all_inputs = torch.tensor([[int(b) for b in format(i, '08b')] for i in range(256)], dtype=torch.float32)
+    outputs = model(all_inputs)
+    expected = parity(all_inputs)
+
+    correct = (outputs == expected).sum().item()
+    print(f'Accuracy: {correct}/256 ({100*correct/256:.1f}%)')

pruned/model.safetensors

@@ -0,0 +1,3 @@
+version https://git-lfs.github.com/spec/v1
+oid sha256:161e13ec2919875e2612b4441be0ce8208c694ec6df3a6685f61eb9051924d9f
+size 980

results.md

@@ -0,0 +1,167 @@
+# Test Results
+
+This document reports comprehensive testing of the `tiny-parity-prover` threshold network across 30 test cases spanning basic functionality, analytical properties, and real-world applications.
+
+## Basic Functional Tests
+
+All ten basic tests passed. The network correctly outputs 0 for all-zeros and all-ones inputs (both have even bit counts), and outputs 1 for all eight single-bit patterns. Exhaustive evaluation over all 256 possible 8-bit inputs confirms 100% accuracy against the ground-truth parity function. Batch inference produces identical results to sequential evaluation, and 1000 repeated inferences on the same input yield identical outputs, confirming determinism. Throughput measured at 18,161 inferences per second (55 microseconds per inference) on CPU.
+
+| Test | Input | Expected | Result |
+|------|-------|----------|--------|
+| All zeros | `[0,0,0,0,0,0,0,0]` | 0 | 0 |
+| All ones | `[1,1,1,1,1,1,1,1]` | 0 | 0 |
+| Single bit set | 8 patterns | 1 | 8/8 |
+| Two bits set | 5 patterns | 0 | 5/5 |
+| Exhaustive sweep | 256 inputs | — | 256/256 |
+| Batch inference | 256 inputs | — | 256/256 |
+| Determinism | 1000 runs | identical | identical |
+| Integer conversion | 0–255 | — | 256/256 |
+| Random sampling | 100 random | — | 100/100 |
+| Latency | 10,000 runs | — | 18,161 inf/sec |
+
+## Analytical Tests
+
+**Weight Pruning.** The network contains 784 total weights, of which 526 are non-zero (32.9% natural sparsity). Random pruning experiments reveal sharp accuracy degradation: removing just 10% of weights drops accuracy to 138–191 out of 256, and pruning beyond 20% collapses performance to chance level (128/256). This suggests the network operates near its minimum viable parameter count despite apparent redundancy.
+
+| Pruned | Accuracy |
+|--------|----------|
+| 0% | 256/256 |
+| 10% | 138–191/256 |
+| 20% | 128–130/256 |
+| 30% | 128–131/256 |
+| 40% | 128/256 |
+| 50% | 128/256 |
+
+**Neuron Ablation.** Systematically disabling individual neurons reveals that only 11 of 32 Layer-1 neurons and 3 of 16 Layer-2 neurons are critical for correct operation. The remaining neurons are redundant—their removal does not affect accuracy. The most critical neuron is Layer-2 Neuron 8, whose ablation drops accuracy to 128/256 (chance). This asymmetry suggests the evolutionary search found a solution with substantial structural slack.
+
+| Layer | Critical | Redundant | Most Critical |
+|-------|----------|-----------|---------------|
+| Layer 1 (32 neurons) | 11 | 21 | Neuron 11 → 162/256 |
+| Layer 2 (16 neurons) | 3 | 13 | Neuron 8 → 128/256 |
+
+**Symbolic Extraction.** Each Layer-1 neuron computes a linear threshold function over a subset of input bits. For example, Neuron 0 fires when the count of bits 1, 2, 5, and 6 being set is sufficiently low (all weights are −1 with bias 0). Neuron 1 fires when bits 0, 6, 7 are set and bits 1, 2, 3, 4 are not, subject to bias −6. The network builds parity by combining these partial threshold computations through two subsequent layers.
+
+```
+Neuron 0: +bits[] −bits[1,2,5,6], bias=0
+Neuron 1: +bits[0,6,7] −bits[1,2,3,4], bias=−6
+Neuron 2: +bits[0,4,5,7] −bits[6], bias=−7
+Neuron 3: +bits[0,2,4,5,6,7] −bits[1,3], bias=0
+```
+
+**Permutation Invariance.** Since parity depends only on the count of set bits, not their positions, the network should be invariant to input permutation. Testing 100 random permutations across all 256 inputs (25,600 total cases) confirms zero failures.
+
+**Noise Robustness.** The network is extremely fragile to input noise. Adding Gaussian noise with standard deviation as small as 0.05 to binary inputs drops accuracy from 100% to approximately 51%—essentially chance. This is expected: Heaviside activation has a hard threshold at zero with no margin, so any perturbation that shifts a pre-activation across zero flips the output. This fragility is inherent to the architecture, not a defect.
+
+| Noise σ | Accuracy |
+|---------|----------|
+| 0.00 | 256/256 (100%) |
+| 0.05 | 131/256 (51%) |
+| 0.10 | 131/256 (51%) |
+| 0.15 | 129/256 (50%) |
+| 0.20 | 125/256 (49%) |
+
+**Bias Sensitivity.** Perturbing each bias by ±1 reveals that 9 of 32 Layer-1 biases, 1 of 16 Layer-2 biases, and the single output bias are sensitive (their perturbation causes at least one input to flip). The remaining biases have sufficient slack that small perturbations are absorbed.
+
+| Layer | Sensitive Biases |
+|-------|------------------|
+| Layer 1 | 9/32 |
+| Layer 2 | 1/16 |
+| Output | 1/1 |
+
+**Layer Collapse.** Composing Layer-1 and Layer-2 weight matrices produces a 16×8 matrix with values ranging from −9 to +12. However, this composition is invalid because the Heaviside activation between layers is non-linear. The 3-layer depth is necessary; there is no equivalent 2-layer network.
+
+**Minimum Network Search.** Random initialization of smaller architectures across 100 trials per architecture yields best accuracies between 138 and 147 out of 256—far below 100%. This confirms that finding a correct solution requires directed search (evolutionary algorithms), not random sampling.
+
+| Architecture | Best Accuracy |
+|--------------|---------------|
+| 8→16→8→1 | 138/256 |
+| 8→8→4→1 | 147/256 |
+| 8→32→8→1 | 144/256 |
+| 8→24→12→1 | 141/256 |
+
+**Coq Proof Generalization.** Beyond the main correctness theorem, we proved an additional property in Coq: bit-flip invariance. The lemma `negb_invariance_8bit` establishes that `parity(NOT x) = parity(x)` for all 8-bit inputs, verified by exhaustive computation over all 256 cases. This follows from the fact that flipping all bits in an even-length vector preserves parity.
+
+```coq
+Lemma negb_invariance_8bit :
+  forallb (fun xs => Bool.eqb (parity (map negb xs)) (parity xs))
+          (all_inputs 8) = true.
+Proof. vm_compute. reflexivity. Qed.
+```
+
+**Hardware Synthesis.** We generated a Verilog implementation of the threshold network. The resulting design requires approximately 500–1000 gates (49 threshold units, each requiring adders and a comparator). For comparison, a naive XOR tree computes parity in 7 gates—a 70–140× overhead. This cost is acceptable only when XOR gates are unavailable, as on neuromorphic hardware.
+
+| Implementation | Gates |
+|----------------|-------|
+| Threshold network | ~500–1000 |
+| XOR tree | 7 |
+| Overhead | 70–140× |
+
+## Real-World Application Tests
+
+**Memory Parity (ECC).** Simulating 100 memory bytes with parity bits and injecting single-bit errors into half of them, the network correctly identifies all 100 cases: 50 valid bytes pass, 50 corrupted bytes are flagged. Zero false positives or negatives.
+
+**RAID-5 Reconstruction.** Simulating a 4-disk RAID-5 stripe with one failed disk, the network reconstructs all 50 test bytes correctly by computing parity across the surviving disks.
+
+**UART Validation.** Simulating serial communication frames with odd parity, the network validates all 50 correct frames and detects corruption in all 50 intentionally corrupted frames.
+
+**XOR Checksum.** Computing a parity-based checksum over 100 bytes produces the correct result, and single-bit corruption is reliably detected by checksum mismatch.
+
+**LFSR Keystream.** Using the network as the feedback function in a linear feedback shift register, starting from state `[1,0,1,1,0,0,1,0]`, produces a deterministic 32-bit keystream `0x269349a4`. Repeated runs yield identical output.
+
+**Barcode Validation.** Using a 7-data-bit plus 1-parity-bit scheme, all 25 valid codes verify correctly, and all 25 corrupted codes are rejected.
+
+**Packet Checksum.** A simplified XOR-parity packet checksum validates all 20 test packets correctly.
+
+**Hamming (7,4) Syndrome.** Computing syndrome bits for Hamming code error detection, all 20 valid codewords produce syndrome 0 as expected.
+
+**PS/2 Keyboard Codes.** Validating 20 standard keyboard scan codes against PS/2 odd-parity requirements, all frames pass.
+
+**DNA Codon Parity.** Encoding nucleotides as 2-bit values (A=00, C=01, G=10, T=11) and computing parity over 6-bit codons, all 8 test sequences produce correct results.
+
+| Codon | Bits | Parity |
+|-------|------|--------|
+| ATG | 001110 | 1 |
+| GCA | 100100 | 0 |
+| TTA | 111100 | 0 |
+| CGG | 011010 | 1 |
+| AAA | 000000 | 0 |
+| TTT | 111111 | 0 |
+| GGG | 101010 | 1 |
+| CCC | 010101 | 1 |
+
+| Test | Result |
+|------|--------|
+| Memory Parity (ECC) | 100/100 |
+| RAID-5 Reconstruction | 50/50 |
+| UART Validation | 100/100 |
+| XOR Checksum | Pass |
+| LFSR Keystream | Deterministic |
+| Barcode Validation | 50/50 |
+| Packet Checksum | 20/20 |
+| Hamming (7,4) | 20/20 |
+| PS/2 Keyboard | 20/20 |
+| DNA Codon Parity | 8/8 |
+
+## Pruned Network
+
+Based on the neuron ablation analysis (Test A2), we extracted a minimal subnetwork containing only the critical neurons. The pruned network achieves identical 100% accuracy with 83.3% fewer parameters.
+
+| Metric | Full Network | Pruned Network |
+|--------|--------------|----------------|
+| Architecture | 8 → 32 → 16 → 1 | 8 → 11 → 3 → 1 |
+| Layer 1 neurons | 32 | 11 |
+| Layer 2 neurons | 16 | 3 |
+| Total parameters | 833 | 139 |
+| Accuracy | 256/256 | 256/256 |
+
+The critical neurons retained from the original network are:
+- Layer 1: indices [3, 7, 9, 11, 12, 16, 17, 20, 24, 27, 28]
+- Layer 2: indices [8, 11, 14]
+
+The pruned network is formally verified in Coq (`PrunedThresholdLogic.v`) with identical theorems to the full network. Weights are available in the `pruned/` folder.
+
+## Summary
+
+All 30 tests pass. The network is functionally correct, deterministic, and applicable to standard parity-based protocols. Analytical tests reveal high neuron redundancy, extreme noise sensitivity, and the necessity of evolutionary search for training. The pruned variant demonstrates that the evolutionary search found a solution with substantial structural slack—only 14 of 48 hidden neurons are necessary for correct operation.
+
+The primary practical application is on neuromorphic hardware platforms (Intel Loihi, IBM TrueNorth, BrainChip Akida) where threshold networks are the native compute primitive and XOR gates cannot be directly instantiated. The pruned network is preferable for deployment due to its reduced resource requirements.

todo.md

@@ -0,0 +1,44 @@
+# Future Work
+
+## 1. Different function
+
+Apply the train→export→verify pipeline to problems beyond parity:
+
+- **Majority vote**: output 1 if more than half of inputs are 1
+- **Addition carry**: output the carry bit of two 4-bit numbers
+- **Threshold-k**: output 1 if at least k inputs are 1
+- **Simple classifiers**: functions where the optimal circuit structure is not obvious
+
+These would test whether the methodology generalizes beyond symmetric Boolean functions.
+
+## 2. Neuromorphic deployment
+
+Deploy the network on actual neuromorphic hardware (Intel Loihi, IBM TrueNorth, BrainChip Akida) or a cycle-accurate simulator. Measure power consumption, latency, and resource utilization. Validate that the claimed use case—formally verified parity on hardware that cannot implement XOR gates—is practical.
+
+## 3. Paper
+
+Write up the methodology for publication. Key contributions:
+
+- Evolutionary search for threshold networks on gradient-hostile loss landscapes
+- Ternary weight quantization enabling exhaustive Coq verification
+- Neuron ablation analysis and principled pruning
+- End-to-end pipeline from training to formal proof
+
+Target venues: CAV, ICML, NeurIPS, or a formal methods workshop.
+
+## 4. Tooling
+
+Package the pipeline into a unified CLI:
+
+```
+verified-nn --function parity --bits 8 --output model/
+```
+
+The tool would:
+1. Train via evolutionary search until 100% accuracy
+2. Export weights to Coq
+3. Compile and verify proofs
+4. Optionally run ablation and pruning
+5. Output SafeTensors + verified Coq proofs
+
+This would lower the barrier to creating new verified networks.