# 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.