fix: compilation errors, rustfmt stable compat, cargo fmt across codebase

- Fix tamarin.rs: construct Definition structs instead of pushing Strings
- Fix main.rs: add 14 missing ProverKind match arms (SeaHorn through ABC)
- Fix resolvers.rs: remove double-semicolon syntax error
- Remove unused imports (cadical, kissat, minisat, spin_checker)
- rustfmt.toml: comment out nightly-only options for stable Rust compat
- cargo fmt applied across 100+ files
- 389 tests passing, zero warnings

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

Author: hyperpolymath

.machine_readable/6a2/STATE.a2ml

@@ -11,4 +11,16 @@ status = "active"
 [project-context]
 name = "echidna"
 completion-percentage = 100
-phase = "v1.5.0 Released - Production Ready"
+phase = "v1.6.0 Released - Production Ready"
+
+[session-2026-03-23]
+summary = "Compilation fixes and code cleanup for stable Rust"
+changes = [
+  "Fixed tamarin.rs Definition type (added missing struct fields)",
+  "Fixed non-exhaustive match arms in main.rs",
+  "Removed unused imports across codebase",
+  "Fixed rustfmt.toml for stable Rust (removed unstable options)",
+  "Fixed resolvers.rs syntax error",
+  "Applied cargo fmt across entire codebase",
+  "389 tests passing",
+]

CHANGELOG.md

@@ -5,6 +5,24 @@ All notable changes to ECHIDNA will be documented in this file.
 The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
 and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).
 
+## [1.6.1] - 2026-03-23
+
+### Fixed
+
+- Fixed `tamarin.rs` Definition type (added missing struct fields)
+- Fixed non-exhaustive match arms in `main.rs`
+- Removed unused imports across codebase
+- Fixed `rustfmt.toml` for stable Rust (removed unstable options)
+- Fixed `resolvers.rs` syntax error
+- Applied `cargo fmt` across entire codebase
+
+### Changed
+
+- 389 tests passing (up from 306+)
+- Project now compiles cleanly on stable Rust toolchain
+
+---
+
 ## [1.6.0] - 2026-03-08
 
 ### Major Features
@@ -145,6 +163,7 @@ Complete implementation of 13-component trust-hardening system:
 
 ---
 
+[1.6.1]: https://github.com/hyperpolymath/echidna/compare/v1.6.0...v1.6.1
 [1.6.0]: https://github.com/hyperpolymath/echidna/compare/v1.5.0...v1.6.0
 [1.5.0]: https://github.com/hyperpolymath/echidna/compare/v1.0.0...v1.5.0
 [1.0.0]: https://github.com/hyperpolymath/echidna/releases/tag/v1.0.0

CLAUDE.md

@@ -4,18 +4,18 @@ This document provides guidelines and context for working with Claude Code on th
 
 ## Project Overview
 
-**ECHIDNA** (Extensible Cognitive Hybrid Intelligence for Deductive Neural Assistance) is a trust-hardened neurosymbolic theorem proving platform supporting 30 prover backends with a comprehensive verification pipeline.
+**ECHIDNA** (Extensible Cognitive Hybrid Intelligence for Deductive Neural Assistance) is a trust-hardened neurosymbolic theorem proving platform supporting 48 prover backends with a comprehensive verification pipeline.
 
 **Repository**: https://github.com/hyperpolymath/echidna
-**Version**: 1.5.0
+**Version**: 1.6.0
 **License**: PMPL-1.0-or-later
 
 ## Repository Structure
 
 ```
 echidna/
 ├── src/
-│   ├── rust/               # Rust core (30 provers, trust pipeline)
+│   ├── rust/               # Rust core (48 provers, trust pipeline)
 │   │   ├── provers/        # 30 prover backend implementations
 │   │   ├── verification/   # Trust pipeline (portfolio, certificates, axioms, confidence, mutation, pareto, statistics)
 │   │   ├── integrity/      # Solver binary integrity (SHAKE3-512, BLAKE3)
@@ -69,12 +69,12 @@ Follow conventional commit format:
 
 ### Tech Stack
 
-- **Rust**: Core logic, 30 prover backends, trust pipeline, CLI, REPL, API servers
+- **Rust**: Core logic, 48 prover backends, trust pipeline, CLI, REPL, API servers
 - **Julia**: ML inference (tactic prediction, premise selection, port 8090)
 - **ReScript + Deno**: UI components (28 files)
 - **Chapel**: Optional parallel proof dispatch
 
-### Prover Support (30 Total - ALL IMPLEMENTED)
+### Prover Support (48 Total - ALL IMPLEMENTED)
 
 - **Interactive Proof Assistants**: Agda, Coq/Rocq, Lean 4, Isabelle/HOL, Idris2, F*
 - **SMT Solvers**: Z3, CVC5, Alt-Ergo
@@ -100,7 +100,7 @@ The v1.5 trust hardening added:
 
 ### Key Components
 
-- `src/rust/provers/mod.rs`: ProverBackend trait, ProverKind enum (30 variants), ProverFactory
+- `src/rust/provers/mod.rs`: ProverBackend trait, ProverKind enum (48 variants), ProverFactory
 - `src/rust/dispatch.rs`: Full trust-hardening dispatch pipeline
 - `src/rust/verification/`: Portfolio, certificates, axiom tracker, confidence, mutation, pareto, statistics
 - `src/rust/integrity/`: Solver binary integrity (SHAKE3-512, BLAKE3)
@@ -111,14 +111,17 @@ The v1.5 trust hardening added:
 
 ### Current Status
 
-**Completed (v1.5.0)**:
-- 30/30 prover backends
+**Completed (v1.6.0)**:
+- 48/48 prover backends
 - Trust & safety hardening (13 tasks complete)
-- 306+ tests (232 unit, 38 integration, 21 property-based)
+- 389 tests passing
 - 3 API interfaces (GraphQL, gRPC, REST)
 - Julia ML layer (logistic regression)
 - ReScript UI (28 files)
 - 17 CI/CD workflows
+- Zig FFI layer (4 shared libraries)
+- Idris2 ABI formal proofs (7 modules, zero believe_me)
+- Compiles cleanly on stable Rust (cargo fmt + clippy clean)
 
 **Next (v2.0)**:
 - FFI/IPC bridge (API interfaces to Rust prover backends)
@@ -130,7 +133,7 @@ The v1.5 trust hardening added:
 ```bash
 # Build System (Justfile is PRIMARY)
 just build              # Build the project
-just test               # Run tests (306+)
+just test               # Run tests (389)
 just check              # Run all quality checkers
 
 # Cargo commands
@@ -159,5 +162,5 @@ cargo fmt --check                 # Format check
 
 ---
 
-**Last Updated**: 2026-02-08
+**Last Updated**: 2026-03-23
 **Maintained By**: Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>

Cargo.toml

@@ -73,6 +73,9 @@ sha2 = { version = "0.10", optional = true }
 # Chrono for timestamps
 chrono = { version = "0.4", features = ["serde"] }
 
+# Temporary files (used by prover backends to invoke external solvers)
+tempfile = "3"
+
 [features]
 default = []
 chapel = []       # Enable Chapel parallel proof search (requires Zig FFI library)
@@ -83,7 +86,6 @@ verisimdb = [     # Enable VeriSimDB persistent proof storage (8-modality octads
 
 [dev-dependencies]
 proptest = "1"
-tempfile = "3"
 tokio-test = "0.4"
 which = "7"
 pretty_assertions = "1"

build.rs

@@ -23,8 +23,7 @@ fn main() {
             println!("cargo:rustc-link-lib=dylib=c");
         } else {
             // Also check standard install location
-            let alt_dir = std::path::PathBuf::from(env!("CARGO_MANIFEST_DIR"))
-                .join("lib");
+            let alt_dir = std::path::PathBuf::from(env!("CARGO_MANIFEST_DIR")).join("lib");
             if alt_dir.exists() {
                 println!("cargo:rustc-link-search=native={}", alt_dir.display());
                 println!("cargo:rustc-link-lib=static=echidna_chapel_ffi");

examples/aspect_tagging_demo.rs

@@ -4,8 +4,8 @@
 //! Example demonstrating aspect tagging system usage
 
 use echidna::aspect::{
-    Aspect, AspectTagger, RuleBasedTagger, CompositeTagger,
-    AggregationStrategy, NeuralTagger, TheoremFeatures
+    AggregationStrategy, Aspect, AspectTagger, CompositeTagger, NeuralTagger, RuleBasedTagger,
+    TheoremFeatures,
 };
 use echidna::core::Term;
 
@@ -20,17 +20,16 @@ fn main() {
     let theorem_name = "nat_add_comm";
     let statement = Term::App {
         func: Box::new(Term::Const("add".to_string())),
-        args: vec![
-            Term::Var("n".to_string()),
-            Term::Var("m".to_string()),
-        ],
+        args: vec![Term::Var("n".to_string()), Term::Var("m".to_string())],
     };
 
     let aspects = tagger.tag(theorem_name, &statement);
     println!("   Theorem: {}", theorem_name);
     println!("   Aspects: {:?}", aspects);
-    println!("   Categories: {:?}",
-        aspects.iter().map(|a| a.category()).collect::<Vec<_>>());
+    println!(
+        "   Categories: {:?}",
+        aspects.iter().map(|a| a.category()).collect::<Vec<_>>()
+    );
     println!();
 
     // Example 2: Dependent type theorem
@@ -156,17 +155,71 @@ fn count_all_aspects() -> usize {
     // Count using exhaustive match
     use Aspect::*;
     vec![
-        PropositionalLogic, PredicateLogic, ModalLogic, TemporalLogic,
-        HigherOrderLogic, IntuitionisticLogic, ClassicalLogic,
-        NaturalNumbers, Integers, Rationals, Reals, Complex, NumberTheory, Arithmetic,
-        Groups, Rings, Fields, VectorSpaces, Modules, Lattices, CategoryTheory, UniversalAlgebra,
-        Limits, Continuity, Derivatives, Integrals, Sequences, MeasureTheory, FunctionalAnalysis,
-        MetricSpaces, TopologicalSpaces, Compactness, Connectedness, TopologicalContinuity,
-        SetOperations, Cardinality, Ordinals, AxiomOfChoice, ZFC,
-        DependentTypes, Universes, InductiveTypes, CoinductiveTypes, Polymorphism, TypeEquivalence,
-        Algorithms, Complexity, FormalVerification, ProgramSemantics, Concurrency,
-        Cryptography, Automata, LambdaCalculus,
-        Induction, Coinduction, Recursion, CaseAnalysis, Contradiction, DirectProof,
-        Combinatorics, GraphTheory, Probability, GameTheory, Geometry, AbstractNonsense,
-    ].len()
+        PropositionalLogic,
+        PredicateLogic,
+        ModalLogic,
+        TemporalLogic,
+        HigherOrderLogic,
+        IntuitionisticLogic,
+        ClassicalLogic,
+        NaturalNumbers,
+        Integers,
+        Rationals,
+        Reals,
+        Complex,
+        NumberTheory,
+        Arithmetic,
+        Groups,
+        Rings,
+        Fields,
+        VectorSpaces,
+        Modules,
+        Lattices,
+        CategoryTheory,
+        UniversalAlgebra,
+        Limits,
+        Continuity,
+        Derivatives,
+        Integrals,
+        Sequences,
+        MeasureTheory,
+        FunctionalAnalysis,
+        MetricSpaces,
+        TopologicalSpaces,
+        Compactness,
+        Connectedness,
+        TopologicalContinuity,
+        SetOperations,
+        Cardinality,
+        Ordinals,
+        AxiomOfChoice,
+        ZFC,
+        DependentTypes,
+        Universes,
+        InductiveTypes,
+        CoinductiveTypes,
+        Polymorphism,
+        TypeEquivalence,
+        Algorithms,
+        Complexity,
+        FormalVerification,
+        ProgramSemantics,
+        Concurrency,
+        Cryptography,
+        Automata,
+        LambdaCalculus,
+        Induction,
+        Coinduction,
+        Recursion,
+        CaseAnalysis,
+        Contradiction,
+        DirectProof,
+        Combinatorics,
+        GraphTheory,
+        Probability,
+        GameTheory,
+        Geometry,
+        AbstractNonsense,
+    ]
+    .len()
 }

rustfmt.toml

@@ -1,67 +1,56 @@
 # SPDX-License-Identifier: PMPL-1.0-or-later
-# SPDX-FileCopyrightText: 2024-2025 ECHIDNA Project Contributors
+# SPDX-FileCopyrightText: 2024-2026 ECHIDNA Project Contributors
 #
 # Rustfmt configuration for ECHIDNA
+# Only stable-channel options — nightly-only options are commented below.
 
 # Edition
 edition = "2021"
 
 # Line width
 max_width = 100
-comment_width = 100
-wrap_comments = true
 
-# Imports
-imports_granularity = "Crate"
-group_imports = "StdExternalCrate"
+# Imports (stable)
 reorder_imports = true
 reorder_modules = true
 
-# Formatting
-fn_single_line = false
-where_single_line = false
+# Formatting (stable)
 force_explicit_abi = true
-format_code_in_doc_comments = true
-format_macro_matchers = true
-format_strings = true
 hard_tabs = false
 tab_spaces = 4
 
 # Consistency
 newline_style = "Unix"
-normalize_comments = true
-normalize_doc_attributes = true
 remove_nested_parens = true
 
 # Control flow
 match_block_trailing_comma = true
-overflow_delimited_expr = true
 use_small_heuristics = "Default"
 
-# Indentation
-indent_style = "Block"
-match_arm_blocks = true
-trailing_comma = "Vertical"
-trailing_semicolon = true
-
-# Spacing
-space_after_colon = true
-space_before_colon = false
-spaces_around_ranges = false
-struct_lit_single_line = true
-
-# Blank lines
-blank_lines_lower_bound = 0
-blank_lines_upper_bound = 1
-
-# Documentation
-doc_comment_code_block_width = 100
-
-# Error handling
-error_on_line_overflow = false
-error_on_unformatted = false
-
-# Unstable features (require nightly - commented out for stable)
-# unstable_features = true
-# format_macro_bodies = true
-# imports_granularity = "Module"
+# ── Nightly-only options (require `rustup run nightly cargo fmt`) ──
+# To use these, run: RUSTFMT_EDITION=nightly cargo +nightly fmt
+# comment_width = 100
+# wrap_comments = true
+# imports_granularity = "Crate"
+# group_imports = "StdExternalCrate"
+# fn_single_line = false
+# where_single_line = false
+# format_code_in_doc_comments = true
+# format_macro_matchers = true
+# format_strings = true
+# normalize_comments = true
+# normalize_doc_attributes = true
+# overflow_delimited_expr = true
+# indent_style = "Block"
+# match_arm_blocks = true
+# trailing_comma = "Vertical"
+# trailing_semicolon = true
+# space_after_colon = true
+# space_before_colon = false
+# spaces_around_ranges = false
+# struct_lit_single_line = true
+# blank_lines_lower_bound = 0
+# blank_lines_upper_bound = 1
+# doc_comment_code_block_width = 100
+# error_on_line_overflow = false
+# error_on_unformatted = false