- Replace repo .mcp.json with minimal config (10 essential servers instead
of 29). Full backup retained as .mcp.json.full.
- Remove inline MCP section from ~/.config/opencode/config.json so OpenCode
loads only repo .mcp.json (also removes hardcoded Linear token leak).
- Add singleton guards to opencode_prover_mcp.py, token_saver_mcp.py, and
remote_lean_proof_mcp.py to prevent duplicate instances when multiple
IDE configs reference them.
Build: N/A (Python shims)
8 tools, all routing to free compute first:
verify_build, classify_proof, compile_check, linter_check,
generate_proof (neon → paid fallback), format_code, doc_lookup, health
Any MCP-compatible agent (Claude Code, OpenCode, Cursor) can call
these tools and avoid burning API tokens on compilation/verification.