test: add 131 new tests across 20 modules (397→528 passing)

Comprehensive test expansion covering:
- Provers: SPIN (11), CBMC (8), Alloy (7), NuSMV (6), UPPAAL (5),
  CaDiCaL (11), Agda (13), Alt-Ergo (9), E-Prover (7), SPASS (7)
- Exchange: OpenTheory (5), Dedukti (7)
- Verification: portfolio (5), mutation (5), certificates (5)
- Core: dispatch (6), proof_encoding (7), groove (4), integration (4),
  proof_search (3), agent/router (8)

Also fix nul-terminated string clippy warning in FFI.
528 tests passing, 0 failures, 0 clippy warnings.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

src/rust/agent/router.rs

@@ -281,4 +281,145 @@ mod tests {
         assert!(stats.contains_key(&ProverKind::Z3));
         assert_eq!(stats[&ProverKind::Z3].successes, 10);
     }
+
+    #[test]
+    fn test_prover_stats_default() {
+        let stats = ProverStats::new();
+        assert_eq!(stats.attempts, 0);
+        assert_eq!(stats.successes, 0);
+        assert_eq!(stats.failures, 0);
+        assert_eq!(stats.total_time_ms, 0);
+    }
+
+    #[test]
+    fn test_prover_stats_success_rate_no_data() {
+        let stats = ProverStats::new();
+        assert_eq!(stats.success_rate(), 0.5); // Default 50% when no data
+    }
+
+    #[test]
+    fn test_prover_stats_success_rate_with_data() {
+        let stats = ProverStats {
+            attempts: 10,
+            successes: 8,
+            failures: 2,
+            total_time_ms: 5000,
+        };
+        assert!((stats.success_rate() - 0.8).abs() < f64::EPSILON);
+    }
+
+    #[test]
+    fn test_prover_stats_success_rate_zero_attempts() {
+        let stats = ProverStats {
+            attempts: 0,
+            successes: 0,
+            failures: 0,
+            total_time_ms: 0,
+        };
+        assert_eq!(stats.success_rate(), 0.5);
+    }
+
+    #[test]
+    fn test_router_select_arithmetic() {
+        let router = ProverRouter::new();
+        let goal = AgenticGoal {
+            goal: Goal {
+                id: "test".to_string(),
+                target: Term::Var("A".to_string()),
+                hypotheses: vec![],
+            },
+            priority: Priority::High,
+            attempts: 0,
+            max_attempts: 3,
+            preferred_prover: None,
+            aspects: vec!["arithmetic".to_string()],
+            parent: None,
+        };
+
+        assert_eq!(router.select(&goal), ProverKind::Z3);
+    }
+
+    #[test]
+    fn test_router_select_inductive() {
+        let router = ProverRouter::new();
+        let goal = AgenticGoal {
+            goal: Goal {
+                id: "test".to_string(),
+                target: Term::Var("A".to_string()),
+                hypotheses: vec![],
+            },
+            priority: Priority::High,
+            attempts: 0,
+            max_attempts: 3,
+            preferred_prover: None,
+            aspects: vec!["inductive".to_string()],
+            parent: None,
+        };
+
+        assert_eq!(router.select(&goal), ProverKind::Coq);
+    }
+
+    #[test]
+    fn test_router_select_type_theory() {
+        let router = ProverRouter::new();
+        let goal = AgenticGoal {
+            goal: Goal {
+                id: "test".to_string(),
+                target: Term::Var("A".to_string()),
+                hypotheses: vec![],
+            },
+            priority: Priority::High,
+            attempts: 0,
+            max_attempts: 3,
+            preferred_prover: None,
+            aspects: vec!["type_theory".to_string()],
+            parent: None,
+        };
+
+        assert_eq!(router.select(&goal), ProverKind::Lean);
+    }
+
+    #[test]
+    fn test_router_select_default() {
+        let router = ProverRouter::new();
+        let goal = AgenticGoal {
+            goal: Goal {
+                id: "test".to_string(),
+                target: Term::Var("A".to_string()),
+                hypotheses: vec![],
+            },
+            priority: Priority::Medium,
+            attempts: 0,
+            max_attempts: 3,
+            preferred_prover: None,
+            aspects: vec![],
+            parent: None,
+        };
+
+        assert_eq!(router.select(&goal), ProverKind::Metamath);
+    }
+
+    #[tokio::test]
+    async fn test_router_record_failure() {
+        let router = ProverRouter::new();
+        let goal = AgenticGoal {
+            goal: Goal {
+                id: "test".to_string(),
+                target: Term::Var("A".to_string()),
+                hypotheses: vec![],
+            },
+            priority: Priority::Medium,
+            attempts: 0,
+            max_attempts: 3,
+            preferred_prover: None,
+            aspects: vec!["logic".to_string()],
+            parent: None,
+        };
+
+        router.record_failure(&goal, ProverKind::Lean).await;
+
+        let stats = router.get_all_stats().await;
+        assert_eq!(stats[&ProverKind::Lean].failures, 1);
+        assert_eq!(stats[&ProverKind::Lean].attempts, 1);
+    }
 }

src/rust/dispatch.rs

@@ -473,4 +473,69 @@ mod tests {
         let json = serde_json::to_string(&result).unwrap();
         assert!(json.contains("Level4"));
     }
+
+    #[test]
+    fn test_dispatch_result_deserialization() {
+        let json = r#"{"verified":false,"trust_level":"Level1","provers_used":["Z3"],"proof_time_ms":100,"goals_remaining":1,"axiom_report":null,"certificate_hash":null,"message":"Failed","cross_checked":false}"#;
+        let result: DispatchResult = serde_json::from_str(json).unwrap();
+        assert!(!result.verified);
+        assert_eq!(result.trust_level, TrustLevel::Level1);
+        assert_eq!(result.goals_remaining, 1);
+    }
+
+    #[test]
+    fn test_prover_selection_agda() {
+        let prover = ProverDispatcher::select_prover(
+            "module MyModule where\ndata Nat : Set where",
+            None,
+        );
+        assert_eq!(prover, ProverKind::Agda);
+    }
+
+    #[test]
+    fn test_prover_selection_isabelle() {
+        let prover = ProverDispatcher::select_prover(
+            "theory MyTheory\nimports Main",
+            None,
+        );
+        assert_eq!(prover, ProverKind::Isabelle);
+    }
+
+    #[test]
+    fn test_prover_selection_cnf_tptp() {
+        let prover = ProverDispatcher::select_prover("cnf(ax1, axiom, p(a)).", None);
+        assert_eq!(prover, ProverKind::Vampire);
+    }
+
+    #[test]
+    fn test_dispatch_config_custom() {
+        let config = DispatchConfig {
+            cross_check: true,
+            min_trust_level: TrustLevel::Level4,
+            track_axioms: false,
+            generate_certificates: true,
+            timeout: 600,
+        };
+        assert!(config.cross_check);
+        assert_eq!(config.min_trust_level, TrustLevel::Level4);
+        assert!(!config.track_axioms);
+        assert!(config.generate_certificates);
+        assert_eq!(config.timeout, 600);
+    }
+
+    #[test]
+    fn test_prover_dispatcher_default() {
+        let dispatcher = ProverDispatcher::default();
+        assert!(!dispatcher.config.cross_check);
+    }
+
+    #[test]
+    fn test_prover_dispatcher_with_config() {
+        let config = DispatchConfig {
+            cross_check: true,
+            ..Default::default()
+        };
+        let dispatcher = ProverDispatcher::with_config(config);
+        assert!(dispatcher.config.cross_check);
+    }
 }

src/rust/exchange/dedukti.rs

@@ -360,4 +360,76 @@ mod tests {
         assert_eq!(DeduktiExporter::sanitize_name("my-theorem"), "my_theorem");
         assert_eq!(DeduktiExporter::sanitize_name("mod.thm"), "mod_thm");
     }
+
+    #[test]
+    fn test_export_empty_state() {
+        let state = ProofState::default();
+        let module = DeduktiExporter::export(&state).unwrap();
+
+        assert_eq!(module.name, "echidna.export");
+        assert_eq!(module.requires, vec!["echidna.prelude".to_string()]);
+        assert!(module.declarations.is_empty());
+    }
+
+    #[test]
+    fn test_export_with_goals() {
+        let mut state = ProofState::default();
+        state.goals.push(crate::core::Goal {
+            id: "my-goal".to_string(),
+            target: Term::Const("Prop".to_string()),
+            hypotheses: vec![],
+        });
+
+        let module = DeduktiExporter::export(&state).unwrap();
+        assert_eq!(module.declarations.len(), 1);
+    }
+
+    #[test]
+    fn test_render_rule_declaration() {
+        let module = DeduktiModule {
+            name: "test".to_string(),
+            requires: vec![],
+            declarations: vec![DeduktiDeclaration::Rule {
+                variables: vec!["x".to_string()],
+                lhs: "plus 0 x".to_string(),
+                rhs: "x".to_string(),
+            }],
+        };
+
+        let rendered = DeduktiExporter::render(&module);
+        assert!(rendered.contains("[x]"));
+        assert!(rendered.contains("plus 0 x"));
+        assert!(rendered.contains("x"));
+    }
+
+    #[test]
+    fn test_term_to_dedukti_const() {
+        let term = Term::Const("Nat".to_string());
+        let dk = DeduktiExporter::term_to_dedukti(&term);
+        assert_eq!(dk, "Nat");
+    }
+
+    #[test]
+    fn test_term_to_dedukti_var() {
+        let term = Term::Var("x".to_string());
+        let dk = DeduktiExporter::term_to_dedukti(&term);
+        assert_eq!(dk, "x");
+    }
+
+    #[test]
+    fn test_import_with_definition() {
+        let module = DeduktiModule {
+            name: "test".to_string(),
+            requires: vec![],
+            declarations: vec![DeduktiDeclaration::Definition {
+                name: "id".to_string(),
+                ty: "Nat -> Nat".to_string(),
+                body: "(x => x)".to_string(),
+            }],
+        };
+
+        let state = DeduktiExporter::import(&module).unwrap();
+        assert_eq!(state.context.theorems.len(), 1);
+        assert!(state.context.theorems[0].proof.is_some());
+    }
 }

src/rust/exchange/opentheory.rs

@@ -192,4 +192,60 @@ mod tests {
 
         assert_eq!(reimported.context.theorems.len(), 1);
     }
+
+    #[test]
+    fn test_export_empty_state() {
+        let state = ProofState::default();
+        let article = OpenTheoryExporter::export(&state).unwrap();
+
+        assert_eq!(article.name, "echidna-export");
+        assert!(article.assumptions.is_empty());
+        assert!(article.conclusions.is_empty());
+        assert!(article.commands.contains(&"version 6".to_string()));
+    }
+
+    #[test]
+    fn test_export_with_goals() {
+        let mut state = ProofState::default();
+        state.goals.push(crate::core::Goal {
+            id: "g1".to_string(),
+            target: Term::Const("True".to_string()),
+            hypotheses: vec![],
+        });
+
+        let article = OpenTheoryExporter::export(&state).unwrap();
+        assert_eq!(article.conclusions.len(), 1);
+    }
+
+    #[test]
+    fn test_import_empty_article() {
+        let article = OpenTheoryArticle {
+            name: "empty".to_string(),
+            assumptions: vec![],
+            conclusions: vec![],
+            commands: vec![],
+        };
+
+        let state = OpenTheoryExporter::import(&article).unwrap();
+        assert!(state.context.theorems.is_empty());
+        assert!(state.goals.is_empty());
+    }
+
+    #[test]
+    fn test_term_to_opentheory_pi() {
+        let term = Term::Pi {
+            param: "x".to_string(),
+            param_type: Box::new(Term::Const("Nat".to_string())),
+            body: Box::new(Term::Const("Bool".to_string())),
+        };
+        let ot = OpenTheoryExporter::term_to_opentheory(&term);
+        assert!(!ot.is_empty());
+    }
+
+    #[test]
+    fn test_term_to_opentheory_const() {
+        let term = Term::Const("True".to_string());
+        let ot = OpenTheoryExporter::term_to_opentheory(&term);
+        assert!(ot.contains("True"));
+    }
 }

src/rust/ffi/mod.rs

@@ -1018,7 +1018,7 @@ pub extern "C" fn echidna_last_error() -> *const u8 {
 /// Get ECHIDNA version string.
 #[no_mangle]
 pub extern "C" fn echidna_version() -> *const u8 {
-    b"1.6.0\0".as_ptr()
+    c"1.6.0".as_ptr().cast()
 }
 
 /// Map ProverKind to u8 for FFI (reverse of kind_from_u8)

src/rust/groove.rs

@@ -166,4 +166,33 @@ mod tests {
     fn groove_port_is_9000() {
         assert_eq!(GROOVE_PORT, 9000);
     }
+
+    #[test]
+    fn manifest_consumes_octad_storage() {
+        let m = manifest();
+        let consumes = m["consumes"].as_array().unwrap();
+        assert!(consumes.iter().any(|v| v == "octad-storage"));
+    }
+
+    #[test]
+    fn manifest_has_proof_verification_type() {
+        let m = manifest();
+        assert_eq!(
+            m["capabilities"]["proof_verification"]["type"],
+            "proof-verification"
+        );
+    }
+
+    #[test]
+    fn manifest_health_endpoint() {
+        let m = manifest();
+        assert_eq!(m["health"], "/health");
+    }
+
+    #[test]
+    fn manifest_service_version_not_empty() {
+        let m = manifest();
+        let version = m["service_version"].as_str().unwrap();
+        assert!(!version.is_empty());
+    }
 }