Add future work roadmap

todo.md

@@ -0,0 +1,48 @@
+# Future Work
+
+## 1. Scale to 16-bit
+
+Train a 16-bit parity network. Verification remains tractable (65,536 cases via `vm_compute`). This would reveal whether the architecture scales linearly or combinatorially with input size, and whether the pruning ratio holds at larger scales.
+
+## 2. 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.
+
+## 3. 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.
+
+## 4. 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.
+
+## 5. 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.