todo.md

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.