hyperpolymath · Oct 9, 2026 · Oct 9, 2026 · Oct 9, 2026 · Oct 9, 2026 · Oct 9, 2026
diff --git a/.github/ISSUE_TEMPLATE/FEATURES.md b/.github/ISSUE_TEMPLATE/FEATURES.md
@@ -68,10 +68,59 @@ This document tracks high-priority feature requests for ECHIDNA development.
   - **References:** ParadisEO-moeo architecture: moeo module in nojhan/paradiseo, ECHIDNA trust specification: docs/TRUST_LEVELS.adoc
   - **Status:** Open
 
+- **feat(swarm): combinatorial tactic playbook synthesis using delta/partial neighborhood evaluation (ParadisEO-mo)**
+  - **Target Repository:** hyperpolymath/proof-burrower
+  - **Area:** Rust / Search Engine
+  - **Description:** The Proof Burrower system performs automated tactic selection and proof search. Currently, it uses heuristic-based selection which can miss optimal tactic combinations. ParadisEO-mo (Multi-Objective Optimization) provides delta/partial neighborhood evaluation capabilities that can intelligently explore combinatorial search spaces. Applying these to Proof Burrower's tactic playbook synthesis would enable more systematic exploration of tactic combinations.
+  - **Proposed Changes:**
+    - Delta Evaluation: Implement ParadisEO-mo delta evaluation to measure marginal improvement of adding/removing tactics from playbooks
+    - Partial Neighborhood Search: Use mo's partial neighborhood evaluation to explore tactic combinations without full re-evaluation
+    - Playbook Optimization: Apply multi-objective optimization to synthesize optimal tactic playbooks for different proof domains
+  - **Acceptance Criteria:**
+    - Delta evaluation reduces playbook synthesis time by at least 30%
+    - Partial neighborhood search maintains proof success rate while exploring fewer combinations
+    - Optimized playbooks outperform hand-crafted playbooks on benchmark corpus
+  - **References:** ParadisEO-mo module in nojhan/paradiseo, Proof Burrower architecture documentation
+  - **Status:** Open
+  - **Cross-Repo Link:** [PB-01 Issue #108](https://github.com/hyperpolymath/proof-burrower/issues/108)
+
+- **feat(ledger): anti-pattern mining and objective fitness formulation from burrow.jsonl for heuristic guidance**
+  - **Target Repository:** hyperpolymath/proof-burrower
+  - **Area:** Rust / Ledger & Indexing
+  - **Description:** Proof Burrower maintains a ledger of proof attempts and outcomes in burrow.jsonl format. This historical data contains valuable patterns about which tactics succeed or fail in different contexts. Currently, this data is underutilized for guiding future proof attempts. ParadisEO's optimization frameworks can help extract anti-patterns and formulate fitness functions to guide heuristic search.
+  - **Proposed Changes:**
+    - Anti-Pattern Mining: Systematically extract failure patterns from burrow.jsonl using data mining techniques
+    - Fitness Formulation: Develop objective fitness functions that score tactic applicability based on historical outcomes
+    - Heuristic Guidance: Use mined patterns to guide tactic selection in future proof attempts
+  - **Acceptance Criteria:**
+    - Anti-pattern mining identifies at least 10 distinct failure modes
+    - Fitness formulation improves proof success rate by at least 5%
+    - Heuristic guidance reduces redundant proof attempts
+  - **References:** ParadisEO data mining and optimization modules, Proof Burrower ledger documentation
+  - **Status:** Open
+  - **Cross-Repo Link:** [PB-02 Issue #109](https://github.com/hyperpolymath/proof-burrower/issues/109)
+
+- **feat(dispatcher): adaptive portfolio timeout and solver selection scheduling for CI PR gates**
+  - **Target Repository:** hyperpolymath/echidnabot
+  - **Area:** Rust / CI Bot / Dispatcher
+  - **Description:** echidnabot operates as a formal-verification CI bot, triggering ECHIDNA proof checks on GitHub/GitLab/Codeberg PRs. Currently, it dispatches verification jobs using static timeouts and fixed prover tiers. In continuous integration environments, resource constraints and wall-clock budgets are paramount. A PR touching small helper lemmas should not consume full multi-minute timeouts across all 12 core provers. Conversely, complex theorem changes need strategic, prioritized prover scheduling. Applying Automated Algorithm Selection and Parameter Tuning principles from ParadisEO enables echidnabot to dynamically schedule solver portfolios and allocate per-job timeouts based on PR diff complexity and historical confidence receipts.
+  - **Proposed Changes:**
+    - PR Diff Feature Extraction: Extract lightweight structural features from incoming proof diffs (number of modified lines/theorems, target formal language, dependency graph centrality)
+    - Adaptive Solver Dispatcher: Implement dynamic schedule matrix optimizing multi-objective trade-off (Min Wall-Clock Time, Max CI Trust Level) with Tier-1 SAT/SMT backends for fast PR feedback and small-kernel provers (Coq, Isabelle, Lean 4) for merge gates
+    - Circuit Breaker Tuning: Use adaptive sliding-window statistics to dynamically adjust circuit breaker trip thresholds based on repository-wide solver load
+  - **Acceptance Criteria:**
+    - Average CI turnaround time on non-breaking PRs decreases without reducing overall verification trust thresholds
+    - Zero regressions in the 184-test test suite
+    - Dynamic scheduling respects all explicit directives configured in .machine_readable/bot_directives/echidnabot.a2ml
+  - **References:** Echidnabot Architecture: wiki/Architecture.md, ParadisEO Automated Algorithm Selection: Dreo et al. (2021) "Paradiseo: from a modular framework to automated design"
+  - **Status:** Open
+  - **Cross-Repo Link:** [EB-01 Issue #177](https://github.com/hyperpolymath/echidnabot/issues/177)
+
 ### Medium Priority
 
 ### Low Priority
 
 ---
 
 *Last updated: 2026-10-09*
+*Cross-repo links verified: PB-01→#108, PB-02→#109, EB-01→#177*
diff --git a/.github/ROADMAP-PARADISEO.md b/.github/ROADMAP-PARADISEO.md
@@ -4,15 +4,15 @@ This issue set captures concrete development possibilities bridging ParadisEO's
 
 ## Issue Index
 
-| ID | Target Repository | Title | Area |
-|----|-------------------|-------|------|
-| [ECH-01](./issues/echidna-01-pareto-moeo.md) | hyperpolymath/echidna | feat(pareto): integrate exact hypervolume indicator and MOEO non-dominated sorting in verification/pareto.rs | Rust / Multi-Objective Search |
-| [ECH-02](./issues/echidna-02-cmaes-julia-gnn.md) | hyperpolymath/echidna | feat(ml): black-box hyperparameter & temperature calibration for GNN premise rankers via CMA-ES / EDO | Julia / Neurosymbolic ML |
-| [ECH-03](./issues/echidna-03-chapel-island-migration.md) | hyperpolymath/echidna | feat(chapel): island-model asynchronous migration topologies & dynamic solver portfolio budget allocation | Chapel / Distributed PGAS |
-| [ECH-04](./issues/echidna-04-ffi-abi-bridge.md) | hyperpolymath/echidna | feat(ffi): C-ABI / Zig bridge specification for embedding ParadisEO metaheuristics engine with Idris2 contracts | ABI / FFI / Multi-Language |
-| [PB-01](https://github.com/hyperpolymath/proof-burrower/issues/proof-burrower-01-combinatorial-tactic-synthesis.md) | hyperpolymath/proof-burrower | feat(swarm): combinatorial tactic playbook synthesis using delta/partial neighborhood evaluation (ParadisEO-mo) | Rust / Search Engine |
-| [PB-02](https://github.com/hyperpolymath/proof-burrower/issues/proof-burrower-02-ledger-fitness-formulation.md) | hyperpolymath/proof-burrower | feat(ledger): anti-pattern mining and objective fitness formulation from burrow.jsonl for heuristic guidance | Rust / Ledger & Indexing |
-| [EB-01](https://github.com/hyperpolymath/echidnabot/blob/main/.github/ISSUE_TEMPLATE/feature_request.yml) | hyperpolymath/echidnabot | feat(dispatcher): adaptive portfolio timeout and solver selection scheduling for CI PR gates | Rust / CI Bot / Dispatcher |
+| ID | Target Repository | Title | Area | GitHub Issue |
+|----|-------------------|-------|------|--------------|
+| [ECH-01](./issues/echidna-01-pareto-moeo.md) | hyperpolymath/echidna | feat(pareto): integrate exact hypervolume indicator and MOEO non-dominated sorting in verification/pareto.rs | Rust / Multi-Objective Search | [#420](https://github.com/hyperpolymath/echidna/issues/420) |
+| [ECH-02](./issues/echidna-02-cmaes-julia-gnn.md) | hyperpolymath/echidna | feat(ml): black-box hyperparameter & temperature calibration for GNN premise rankers via CMA-ES / EDO | Julia / Neurosymbolic ML | [#421](https://github.com/hyperpolymath/echidna/issues/421) |
+| [ECH-03](./issues/echidna-03-chapel-island-migration.md) | hyperpolymath/echidna | feat(chapel): island-model asynchronous migration topologies & dynamic solver portfolio budget allocation | Chapel / Distributed PGAS | [#422](https://github.com/hyperpolymath/echidna/issues/422) |
+| [ECH-04](./issues/echidna-04-ffi-abi-bridge.md) | hyperpolymath/echidna | feat(ffi): C-ABI / Zig bridge specification for embedding ParadisEO metaheuristics engine with Idris2 contracts | ABI / FFI / Multi-Language | [#424](https://github.com/hyperpolymath/echidna/issues/424) |
+| [PB-01](https://github.com/hyperpolymath/proof-burrower/issues/108) | hyperpolymath/proof-burrower | feat(swarm): combinatorial tactic playbook synthesis using delta/partial neighborhood evaluation (ParadisEO-mo) | Rust / Search Engine | [#108](https://github.com/hyperpolymath/proof-burrower/issues/108) |
+| [PB-02](https://github.com/hyperpolymath/proof-burrower/issues/109) | hyperpolymath/proof-burrower | feat(ledger): anti-pattern mining and objective fitness formulation from burrow.jsonl for heuristic guidance | Rust / Ledger & Indexing | [#109](https://github.com/hyperpolymath/proof-burrower/issues/109) |
+| [EB-01](https://github.com/hyperpolymath/echidnabot/issues/177) | hyperpolymath/echidnabot | feat(dispatcher): adaptive portfolio timeout and solver selection scheduling for CI PR gates | Rust / CI Bot / Dispatcher | [#177](https://github.com/hyperpolymath/echidnabot/issues/177) |
 
 ## Detailed Issue Specifications
 

diff --git a/.github/TRACEABILITY.md b/.github/TRACEABILITY.md
@@ -49,17 +49,25 @@ Each issue file contains:
 **Purpose**: Issue template with embedded issues list
 
 **Contents**:
-- EB-01: feat(dispatcher) - adaptive portfolio timeout and solver selection
+- EB-01: feat(dispatcher) - adaptive portfolio timeout and solver selection (filed as [#177](https://github.com/hyperpolymath/echidnabot/issues/177))
 - Navigation section linking to the master roadmap
 - Cross-references to echidna ECH-01 through ECH-04
 
 **GitHub URL**: `https://github.com/hyperpolymath/echidnabot/blob/main/.github/ISSUE_TEMPLATE/feature_request.yml`
 
-#### proof-burrower Repository (Planned)
+#### proof-burrower Repository
 
-**Note**: The issue files for proof-burrower (PB-01, PB-02) are referenced in the master roadmap but the actual markdown files need to be created in the proof-burrower repository at:
-- `.github/issues/proof-burrower-01-combinatorial-tactic-synthesis.md`
-- `.github/issues/proof-burrower-02-ledger-fitness-formulation.md`
+**Location**: Issues filed in hyperpolymath/proof-burrower repository
+
+**Issues**:
+- PB-01: feat(swarm) - combinatorial tactic playbook synthesis ([#108](https://github.com/hyperpolymath/proof-burrower/issues/108))
+- PB-02: feat(ledger) - anti-pattern mining and objective fitness formulation ([#109](https://github.com/hyperpolymath/proof-burrower/issues/109))
+
+**Status**: Both issues filed and ready for implementation
+
+**GitHub URLs**:
+- PB-01: https://github.com/hyperpolymath/proof-burrower/issues/108
+- PB-02: https://github.com/hyperpolymath/proof-burrower/issues/109
 
 ## Traceability for Humans
 
@@ -135,15 +143,15 @@ All cross-repo links use **absolute GitHub URLs**:
 ### ✅ echidnabot Repository
 - [x] Feature template exists: `.github/ISSUE_TEMPLATE/feature_request.yml`
 - [x] EB-01 issue is documented in the template
+- [x] EB-01 filed as GitHub issue [#177](https://github.com/hyperpolymath/echidnabot/issues/177)
 - [x] Navigation links to master roadmap
 - [x] Cross-references to echidna issues
 
-### ⏳ proof-burrower Repository (To Do)
-- [ ] Create `.github/issues/` directory
-- [ ] Create `proof-burrower-01-combinatorial-tactic-synthesis.md`
-- [ ] Create `proof-burrower-02-ledger-fitness-formulation.md`
-- [ ] Add cross-references to echidna issues
-- [ ] Add navigation links to master roadmap
+### ✅ proof-burrower Repository
+- [x] PB-01 filed as GitHub issue [#108](https://github.com/hyperpolymath/proof-burrower/issues/108)
+- [x] PB-02 filed as GitHub issue [#109](https://github.com/hyperpolymath/proof-burrower/issues/109)
+- [x] Cross-references to echidna issues added
+- [x] All claims verified against upstream (be897dd07e1a16014f2d0f8d9cbedffb0240dd4a)
 
 ## Query Paths
 
@@ -196,7 +204,8 @@ cat .github/issues/echidna-01-pareto-moeo.md
 
 ---
 
-**Document Version**: 1.0  
+**Document Version**: 1.1  
 **Last Updated**: 2026-10-09  
 **Owner**: hyperpolymath/echidna maintainers  
 **Related**: [ROADMAP-PARADISEO.md](./ROADMAP-PARADISEO.md)
+**GitHub Issues Filed**: ECH-01→#420, ECH-02→#421, ECH-03→#422, ECH-04→#424, PB-01→#108, PB-02→#109, EB-01→#177
diff --git a/.github/issues/README.md b/.github/issues/README.md
@@ -5,15 +5,16 @@ This directory contains the canonical issue specifications for the ParadisEO met
 ## Status
 
 - **ECH-01..04 bodies and labels**: Synchronised with GitHub issues #420, #421, #422, #424
-- **PB-01, PB-02**: Draft specifications for hyperpolymath/proof-burrower (unverified claims)
-- **EB-01**: Draft specification for hyperpolymath/echidnabot (unverified claims)
+- **PB-01**: Filed as hyperpolymath/proof-burrower#108 (verified against be897dd07e1a16014f2d0f8d9cbedffb0240dd4a)
+- **PB-02**: Filed as hyperpolymath/proof-burrower#109 (verified against be897dd07e1a16014f2d0f8d9cbedffb0240dd4a)
+- **EB-01**: Filed as hyperpolymath/echidnabot#177 (verified against ae5283323b815f82d2a556080b59e0bb648de62b)
 
 ## Provenance
 
-- **ECH-01..04**: Created from local issue files, not yet pushed to GitHub
-- **PB-01**: Based on read-only look at proof-burrower@be897dd
-- **PB-02**: Based on read-only look at proof-burrower@be897dd
-- **EB-01**: Based on read-only look at echidnabot@ae52833
+- **ECH-01..04**: Created from local issue files, synchronised with GitHub
+- **PB-01**: Based on read-only look at proof-burrower@be897dd07e1a16014f2d0f8d9cbedffb0240dd4a (corrected claims)
+- **PB-02**: Based on read-only look at proof-burrower@be897dd07e1a16014f2d0f8d9cbedffb0240dd4a (corrected RecordResult.status and Learning.pattern_kind values)
+- **EB-01**: Based on read-only look at echidnabot@ae5283323b815f82d2a556080b59e0bb648de62b (corrected: [scheduler] job_timeout_seconds does not exist)
 
 ## File Index