feat(provers): add Deno-native theorem prover integration (#4)

Implement comprehensive prover integration system using Deno (no npm):

Clients:
- SystemOnTPTP: 40+ provers (Vampire, E, Z3, CVC5, SPASS, etc.)
- Metamath: proof verification and theorem exploration
- Z3 WASM: local SMT solving via WebAssembly
- Wolfram Alpha: natural language proofs (2000 free calls/month)
- LeanTool: Lean 4 via OpenAI-compatible API
- Unified: aggregates all backends with strategy selection

Runner:
- Continuous daemon for day/night proof checking
- CLI with health check, single solve, batch processing
- Queue management with priority and retry logic
- Persistent result storage

Enforcement:
- npm ban script and pre-commit hook
- deno.json with strict configuration
- NPM_BANNED.md documentation

All imports use https:// URLs or npm: specifiers (Deno-native).

Co-authored-by: Claude <noreply@anthropic.com>

Author: hyperpolymath

.githooks/pre-commit

@@ -0,0 +1,30 @@
+#!/usr/bin/env bash
+#
+# ECHIDNA Pre-commit Hook
+# Enforces npm ban and runs checks
+#
+# SPDX-License-Identifier: MIT OR AGPL-3.0-or-later
+
+set -euo pipefail
+
+echo "🦔 ECHIDNA Pre-commit Checks"
+echo "============================"
+
+# Run npm ban check
+if [ -x "scripts/ban-npm.sh" ]; then
+    bash scripts/ban-npm.sh
+fi
+
+# Run Deno checks if available
+if command -v deno &> /dev/null; then
+    echo ""
+    echo "Running Deno lint..."
+    deno lint src/provers/ || true
+
+    echo ""
+    echo "Running Deno check..."
+    deno check src/provers/mod.ts || true
+fi
+
+echo ""
+echo "✅ Pre-commit checks passed"

NPM_BANNED.md

@@ -0,0 +1,73 @@
+# ⛔ NPM IS BANNED IN THIS PROJECT
+
+## Policy
+
+This project uses **Deno** as its JavaScript/TypeScript runtime. The following are **STRICTLY FORBIDDEN**:
+
+- ❌ `npm install` / `npm i`
+- ❌ `npx`
+- ❌ `package-lock.json`
+- ❌ `node_modules/`
+- ❌ Bare imports like `import x from "lodash"`
+
+## Approved Alternatives
+
+### Package Management
+```bash
+# ✅ Use Deno tasks
+deno task check
+deno task lint
+deno task daemon
+
+# ✅ Use deno.json for dependencies
+# Imports are specified in deno.json "imports" field
+```
+
+### Dependencies
+```typescript
+// ✅ CORRECT: Use https:// imports
+import { serve } from "https://deno.land/std@0.224.0/http/server.ts";
+
+// ✅ CORRECT: Use npm: specifier (Deno-native)
+import z3 from "npm:z3-solver@4.12.4";
+
+// ✅ CORRECT: Use esm.sh CDN
+import React from "https://esm.sh/react@18.2.0";
+
+// ❌ WRONG: Bare npm imports
+import lodash from "lodash";  // BANNED
+```
+
+### Running Scripts
+```bash
+# ❌ BANNED
+npm run dev
+npm start
+npx some-tool
+
+# ✅ APPROVED
+deno task dev
+deno run --allow-net script.ts
+```
+
+## Why?
+
+1. **Security**: Deno has better security defaults with explicit permissions
+2. **Simplicity**: No node_modules, no package-lock.json conflicts
+3. **Standards**: Uses web standards and ES modules natively
+4. **Speed**: Faster startup, no npm install step
+5. **Project Policy**: RSR (Rhodium Standard Repository) compliance
+
+## Enforcement
+
+- Pre-commit hooks block npm usage
+- CI/CD fails on npm artifacts
+- Code review rejects npm dependencies
+
+## Exceptions
+
+The only exception is the `src/rescript/` directory which requires ReScript compiler tooling. This is being migrated to Deno-compatible tooling.
+
+## Need Help?
+
+See the [Deno documentation](https://deno.land/manual) or ask in the project chat.

deno.json

@@ -0,0 +1,75 @@
+{
+  "$schema": "https://deno.land/x/deno/cli/schemas/config-file.v1.json",
+  "name": "@echidna/provers",
+  "version": "0.1.0",
+  "description": "ECHIDNA - Neurosymbolic Theorem Proving Platform",
+  "license": "MIT OR AGPL-3.0-or-later",
+
+  "compilerOptions": {
+    "allowJs": false,
+    "strict": true,
+    "noImplicitAny": true,
+    "noUnusedLocals": true,
+    "noUnusedParameters": true
+  },
+
+  "imports": {
+    "@std/": "https://deno.land/std@0.224.0/",
+    "@echidna/provers": "./src/provers/mod.ts"
+  },
+
+  "tasks": {
+    "check": "deno check src/provers/mod.ts",
+    "lint": "deno lint src/",
+    "fmt": "deno fmt src/",
+    "test": "deno test --allow-net --allow-read --allow-env src/",
+
+    "health": "deno run --allow-net --allow-env src/provers/runners/cli.ts --health",
+    "solve": "deno run --allow-net --allow-read --allow-write --allow-env src/provers/runners/cli.ts --solve",
+    "batch": "deno run --allow-net --allow-read --allow-write --allow-env src/provers/runners/cli.ts --batch",
+    "daemon": "deno run --allow-net --allow-read --allow-write --allow-env src/provers/runners/cli.ts --daemon",
+
+    "ban-npm": "echo '❌ npm is BANNED in this project. Use Deno!' && exit 1",
+
+    "dev:ui": "cd src/rescript && deno task dev",
+    "build:ui": "cd src/rescript && deno task build"
+  },
+
+  "fmt": {
+    "include": ["src/"],
+    "exclude": ["src/rescript/node_modules/"],
+    "options": {
+      "useTabs": false,
+      "lineWidth": 100,
+      "indentWidth": 2,
+      "singleQuote": false,
+      "proseWrap": "preserve"
+    }
+  },
+
+  "lint": {
+    "include": ["src/"],
+    "exclude": ["src/rescript/node_modules/"],
+    "rules": {
+      "tags": ["recommended"],
+      "include": [
+        "ban-untagged-todo",
+        "no-sync-fn-in-async-fn",
+        "single-var-declarator"
+      ],
+      "exclude": []
+    }
+  },
+
+  "test": {
+    "include": ["src/**/*_test.ts", "src/**/*.test.ts"],
+    "exclude": ["src/rescript/"]
+  },
+
+  "publish": {
+    "include": ["src/provers/", "README.md", "LICENSE"],
+    "exclude": ["**/*_test.ts", "**/*.test.ts"]
+  },
+
+  "nodeModulesDir": "none"
+}

scripts/ban-npm.sh

@@ -0,0 +1,74 @@
+#!/usr/bin/env bash
+#
+# ECHIDNA NPM Ban Enforcement Script
+# This script checks for and blocks npm/node usage
+#
+# SPDX-License-Identifier: MIT OR AGPL-3.0-or-later
+
+set -euo pipefail
+
+RED='\033[0;31m'
+GREEN='\033[0;32m'
+YELLOW='\033[1;33m'
+NC='\033[0m' # No Color
+
+echo "🔍 ECHIDNA NPM Ban Check"
+echo "========================"
+
+VIOLATIONS=0
+
+# Check for package-lock.json
+if [ -f "package-lock.json" ]; then
+    echo -e "${RED}❌ VIOLATION: package-lock.json found in root${NC}"
+    VIOLATIONS=$((VIOLATIONS + 1))
+fi
+
+# Check for node_modules anywhere
+if find . -type d -name "node_modules" 2>/dev/null | grep -q .; then
+    echo -e "${RED}❌ VIOLATION: node_modules directory found${NC}"
+    find . -type d -name "node_modules" 2>/dev/null
+    VIOLATIONS=$((VIOLATIONS + 1))
+fi
+
+# Check for npm/npx usage in scripts
+if grep -r "npm install\|npm i \|npx \|npm run" scripts/ 2>/dev/null | grep -v "ban-npm"; then
+    echo -e "${RED}❌ VIOLATION: npm/npx commands found in scripts${NC}"
+    VIOLATIONS=$((VIOLATIONS + 1))
+fi
+
+# Check for npm imports in TypeScript (should use https:// or npm: specifier)
+BAD_IMPORTS=$(grep -r "from ['\"][@a-z]" src/provers/ 2>/dev/null | grep -v "from ['\"]https://" | grep -v "from ['\"]npm:" | grep -v "from ['\"]\./" | grep -v "from ['\"]\.\./" || true)
+if [ -n "$BAD_IMPORTS" ]; then
+    echo -e "${YELLOW}⚠️  WARNING: Bare imports found (should use https:// or npm: specifier)${NC}"
+    echo "$BAD_IMPORTS"
+fi
+
+# Check Justfile for npm commands
+if [ -f "Justfile" ] && grep -q "npm\|npx" Justfile; then
+    echo -e "${RED}❌ VIOLATION: npm/npx found in Justfile${NC}"
+    VIOLATIONS=$((VIOLATIONS + 1))
+fi
+
+# Summary
+echo ""
+if [ $VIOLATIONS -eq 0 ]; then
+    echo -e "${GREEN}✅ No npm violations found!${NC}"
+    echo ""
+    echo "Approved package managers:"
+    echo "  ✓ Deno (deno.json, deno task)"
+    echo "  ✓ Bun (only if Deno impossible)"
+    echo ""
+    echo "Banned:"
+    echo "  ✗ npm, npx, node_modules"
+    echo "  ✗ package-lock.json"
+    exit 0
+else
+    echo -e "${RED}❌ Found $VIOLATIONS violation(s)!${NC}"
+    echo ""
+    echo "To fix:"
+    echo "  1. Remove package-lock.json: rm package-lock.json"
+    echo "  2. Remove node_modules: rm -rf node_modules"
+    echo "  3. Use 'deno task' instead of 'npm run'"
+    echo "  4. Use https:// or npm: imports in Deno"
+    exit 1
+fi