allaun/Research-Stack
1
0
Fork 0
mirror of https://github.com/allaunthefox/Research-Stack.git synced 2026-07-31 03:05:21 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions
Research-Stack/.mcp.json.full
allaun 36a78fec72 feat(infra): add support for secure file-based Authentik token loading 
Add support for AUTHENTIK_TOKEN_FILE environment variable fallback to
service_orchestrator.py, configure_vault_authentik.py, and the Rust
authentik_agent_manager CLI/MCP server. This prevents hardcoding or
exposing raw tokens in environment blocks or CLI arguments. Document
the new Authentik SSO stack deployment on cupfox k3s in AGENTS.md and
update .mcp.json.full configuration.

Build: 0 jobs, 0 errors (lake build)
2026-07-05 15:54:27 -05:00

305 lines
No EOL
13 KiB
Text
Raw Blame History

{
"$schema": "https://modelcontextprotocol.io/schemas/2025-03-26/client-config.json",
"_comment": "Math-first MCP server declarations for Research Stack. Each server below is gated on a runtime environment variable so the config never embeds secrets and so contributors who have not provisioned a given backend simply skip it. See docs/math-first-tooling.md for setup instructions.",
"mcpServers": {
"filesystem": {
"_comment": "Read/write proof artifacts, Lean kernels, and DeepSeek receipts. Scope is the repository root so review tooling cannot escape the project tree.",
"command": "npx",
"args": [
"-y",
"@modelcontextprotocol/server-filesystem",
"."
],
"env": {}
},
"sympy": {
"_comment": "Local SymPy bridge for symbolic verification of arithmetic claims. Package is 'mcp-sympy' on PyPI (provides 'mcp-sympy' executable); the sdiehl/sympy-mcp GitHub name differs from the PyPI name.",
"command": "uvx",
"args": [
"mcp-sympy"
],
"env": {}
},
"wolfram-alpha": {
"_comment": "Wolfram Alpha symbolic verification. Requires WOLFRAM_APP_ID in the shell environment (NOT WOLFRAM_ALPHA_APPID \u2014 that's an alias in fish config). Package is 'wolfram-mcp' on npm (was '@wolfram-alpha/mcp-server' which no longer exists).",
"command": "npx",
"args": [
"-y",
"wolfram-mcp"
],
"env": {}
},
"notion": {
"_comment": "Notion integration via official Notion MCP (Streamable HTTP + OAuth). Run `devin mcp login notion` once to complete the OAuth flow; tokens are stored locally and auto-refreshed.",
"url": "https://mcp.notion.com/mcp",
"transport": "http"
},
"lean": {
"_comment": "Lean 4 / Mathlib typecheck bridge. Targets 0-Core-Formalism/lean/Semantics/ via the existing lakefile. Requires `elan` on PATH; see GETTING_STARTED.md for the lean-toolchain pin (leanprover/lean4:v4.30.0-rc2). The executable in the lean-mcp package is 'lean-mcp-server', not 'lean-mcp'.",
"command": "uvx",
"args": [
"--from",
"lean-mcp",
"lean-mcp-server",
"--lakefile",
"0-Core-Formalism/lean/Semantics/lakefile.toml"
],
"env": {}
},
"remote-lean-proof": {
"_comment": "Hermes/OpenCode/Codex proof backend. Calls the dedicated AWS language-proof-server and returns receipt-bearing Lean/Lake results. Token is read from PROOF_SERVER_TOKEN or ~/.config/ene/language-proof-server.token.",
"command": "python3",
"args": [
"4-Infrastructure/infra/remote_lean_proof_mcp.py"
],
"env": {
"PROOF_SERVER_URL": "${PROOF_SERVER_URL}",
"PROOF_SERVER_TOKEN_FILE": "/home/allaun/.config/ene/language-proof-server.token"
}
},
"service-orchestrator": {
"_comment": "Unified control plane: register/unregister services across Authentik + Caddy + credential server. Requires AUTHENTIK_TOKEN and CADDY_ADMIN env vars. HTTP mode on port 8338.",
"command": "python3",
"args": [
"4-Infrastructure/infra/service-orchestrator/service_orchestrator.py"
],
"env": {
"AUTHENTIK_BASE": "${AUTHENTIK_BASE:-http://100.115.119.40:9000}",
"AUTHENTIK_TOKEN_FILE": "/home/allaun/.config/ene/authentik.token",
"CADDY_ADMIN": "http://100.101.247.127:2019",
"CREDENTIAL_SERVER": "http://100.101.247.127:8444"
}
},
"authentik-mcp": {
"_comment": "Authentik SSO MCP server \u2014 user/group/application management via Authentik API v3. Requires AUTHENTIK_TOKEN env var. Built from 4-Infrastructure/shim/authentik_agent_manager/.",
"command": "/home/allaun/Research Stack/4-Infrastructure/shim/authentik_agent_manager/target/release/mcp_server",
"args": [],
"env": {
"AUTHENTIK_BASE_URL": "${AUTHENTIK_BASE:-http://100.115.119.40:9000}",
"AUTHENTIK_TOKEN_FILE": "/home/allaun/.config/ene/authentik.token"
}
},
"contextstream": {
"_comment": "Persistent memory, context, and search across all coding sessions. Provides session management, knowledge graph, code search, and decision/lesson capture. Plan: Elite.",
"command": "npx",
"args": [
"--prefer-online",
"-y",
"@contextstream/mcp-server@latest"
],
"env": {
"CONTEXTSTREAM_API_URL": "https://api.contextstream.io",
"CONTEXTSTREAM_API_KEY": "${CONTEXTSTREAM_API_KEY}",
"CONTEXTSTREAM_ALLOW_HEADER_AUTH": "false",
"CONTEXTSTREAM_WORKSPACE_ID": "21c133f6-6854-4e81-b801-4037c11b7e34",
"CONTEXTSTREAM_PROJECT_ID": "ef91cc79-aae3-4765-ae0d-63b48f5ea6e6",
"CONTEXTSTREAM_USER_AGENT": "contextstream-mcp/0.4.74",
"CONTEXTSTREAM_TOOLSET": "complete",
"CONTEXTSTREAM_LOG_LEVEL": "quiet",
"CONTEXTSTREAM_OUTPUT_FORMAT": "compact",
"CONTEXTSTREAM_CONTEXT_PACK": "true",
"CONTEXTSTREAM_TRANSCRIPTS_ENABLED": "true",
"CONTEXTSTREAM_HOOK_TRANSCRIPTS_ENABLED": "true",
"CONTEXTSTREAM_SHOW_TIMING": "false",
"CONTEXTSTREAM_PROGRESSIVE_MODE": "false",
"CONTEXTSTREAM_ROUTER_MODE": "false",
"CONTEXTSTREAM_CONSOLIDATED": "true",
"CONTEXTSTREAM_AUTO_HIDE_INTEGRATIONS": "true",
"CONTEXTSTREAM_SEARCH_LIMIT": "15",
"CONTEXTSTREAM_SEARCH_MAX_CHARS": "2400",
"CONTEXTSTREAM_INCLUDE_STRUCTURED_CONTENT": "true"
}
},
"ene-contextstream": {
"_comment": "Local ENE replacement for ContextStream-like memory/search/session recall. Writes local receipt-bearing SQLite memory and reads ene-api/session-sync when running.",
"command": "python3",
"args": [
"/home/allaun/Research Stack/4-Infrastructure/infra/ene_contextstream_mcp.py"
],
"env": {
"ENE_API_URL": "http://127.0.0.1:3000",
"ENE_CONTEXT_STORE": "/home/allaun/.local/share/ene/contextstream.sqlite",
"ENE_CONTEXT_CANDIDATE_ROOT": "/home/allaun/Research Stack/shared-data/data/germane/research/github-ene-contextstream"
}
},
"deepseek-prover": {
"_comment": "DeepSeek-Prover-V2-7B proof search. Backend: ollama (default), huggingface, or deepseek_api. Generates Lean proof candidates, compiles with lake build, iterates with error feedback.",
"command": "python3",
"args": [
"4-Infrastructure/infra/deepseek_prover_mcp.py"
],
"env": {
"DEEPSEEK_PROVER_BACKEND": "ollama",
"OLLAMA_URL": "http://localhost:11434",
"LAKE_WORKDIR": "/home/allaun/Research Stack/0-Core-Formalism/lean/Semantics"
}
},
"vikunja": {
"_comment": "Kanban board server on neon (100.92.88.64). Agents and humans set goals, track status, assign tasks. Wraps Vikunja v2.3.0 REST API.",
"command": "python3",
"args": [
"4-Infrastructure/infra/vikunja_mcp.py"
],
"env": {
"VIKUNJA_URL": "http://100.92.88.64:3456",
"VIKUNJA_TOKEN_FILE": "/home/allaun/.config/ene/vikunja.token"
}
},
"lean-lsp": {
"_comment": "Lean Language Server MCP — lightweight type-checking and proof info for Lean files in Semantics/. Wrapped to fix Moonshot/Kimi schema validation.",
"command": "python3",
"args": [
"4-Infrastructure/infra/lean_lsp_mcp_wrapper.py",
"--lean-project-path",
"0-Core-Formalism/lean/Semantics"
],
"env": {}
},
"k8s": {
"_comment": "Kubernetes MCP server (read-only). Query k3s cluster on cupfox (100.72.130.76). Uses default kubeconfig.",
"command": "npx",
"args": [
"-y",
"kubernetes-mcp-server@latest",
"--read-only"
],
"env": {}
},
"arxiv": {
"_comment": "ArXiv paper search MCP. Cache papers in ~/.arxiv-papers for offline reference. Connects to the arxiv cross-ref pipeline.",
"command": "uvx",
"args": [
"arxiv-mcp-server",
"--storage-path",
"/home/allaun/.arxiv-papers"
],
"env": {}
},
"nixos": {
"_comment": "NixOS MCP server. Read/write NixOS configs (steamdeck, nixos-laptop, neon). Requires ssh access.",
"command": "uvx",
"args": [
"mcp-nixos"
],
"env": {}
},
"shape-index": {
"_comment": "FAMM shape-index of the Lean corpus. 112K indexed theorems classified by Sidon sumset signature. Query nearest neighbors by shape to find proof templates.",
"command": "python3",
"args": [
"4-Infrastructure/infra/shape_index_mcp.py"
],
"env": {
"SHAPE_INDEX_PATH": "/home/allaun/lean_corpus/shape_index.json"
}
},
"github": {
"_comment": "GitHub MCP (official Copilot endpoint). Provides PR creation/review, issue tracking, CI status, repo search, and branch management. Set GITHUB_PERSONAL_ACCESS_TOKEN in the shell environment (token lives in Goose config \u2014 do NOT hardcode here). The token in ~/.config/goose/config.yaml should be migrated to a secrets store or shell profile.",
"type": "http",
"url": "https://api.githubcopilot.com/mcp/",
"headers": {
"Authorization": "Bearer ${GITHUB_PERSONAL_ACCESS_TOKEN}"
}
},
"git": {
"_comment": "Git MCP server for history navigation: diff, blame, log traversal, commit search. Complements the filesystem MCP with git-native operations. Useful for proof archaeology and tracing when/why a lemma changed.",
"command": "uvx",
"args": [
"mcp-server-git",
"--repository",
"."
],
"env": {}
},
"fetch": {
"_comment": "HTTP fetch MCP \u2014 retrieve any public URL as text or markdown. Fills the gap between ArXiv (papers) and Wolfram (symbolic): reading Mathlib4 docs, Lean release notes, RFC pages, blog posts, etc.",
"command": "uvx",
"args": [
"mcp-server-fetch"
],
"env": {}
},
"serena": {
"_comment": "Serena code intelligence MCP (Oraios). LSP-powered cross-file symbol search, call-graph navigation, and definition lookup across all languages in the Research Stack (Lean, Rust, Python). Complements lean-lsp (Lean-only) with multi-language awareness.",
"command": "uvx",
"args": [
"--from",
"git+https://github.com/oraios/serena",
"serena",
"start-mcp-server"
],
"env": {}
},
"context7": {
"_comment": "Context7 live library documentation (Upstash). Fetches real-time docs for Mathlib4, Lean stdlib, Python packages, and Rust crates \u2014 not stale training data. Use when lean-lsp hover info isn't enough and you need full API context.",
"command": "npx",
"args": [
"-y",
"@upstash/context7-mcp"
],
"env": {}
},
"chrome-devtools": {
"_comment": "Chrome DevTools MCP \u2014 control and inspect a live Chrome browser session. Useful for testing web UIs (Authentik admin, Vikunja, Grafana dashboards) and scraping dynamically rendered pages that fetch MCP cannot reach.",
"command": "npx",
"args": [
"-y",
"chrome-devtools-mcp@latest"
],
"env": {}
},
"council-of-mine": {
"_comment": "LLM council with 9 distinct personas (Block/Square). Routes a question to multiple opinionated advisors and synthesizes a debate. Useful for architectural decisions, proof strategy reviews, and doctrine alignment checks where a single agent perspective is insufficient.",
"command": "uvx",
"args": [
"--from",
"git+https://github.com/block/mcp-council-of-mine",
"mcp_council_of_mine"
],
"env": {}
},
"gdrive": {
"_comment": "Google Drive MCP \u2014 read/write access to Google Drive files. Imported from Windsurf config. Requires GOOGLE_CLIENT_ID and GOOGLE_CLIENT_SECRET env vars.",
"command": "npx",
"args": [
"-y",
"@piotr-agier/google-drive-mcp"
],
"env": {
"GOOGLE_CLIENT_ID": "${GOOGLE_CLIENT_ID}",
"GOOGLE_CLIENT_SECRET": "${GOOGLE_CLIENT_SECRET}"
}
},
"opencode-prover": {
"_comment": "OpenCode Prover MCP \u2014 from OpenCode config. Lean proof verification bridge for OpenCode/Codex CLI.",
"command": "python3",
"args": [
"5-Applications/tools-scripts/mcp/opencode_prover_mcp.py"
],
"env": {}
},
"token-saver": {
"_comment": "Token saver MCP \u2014 from OpenCode config. Saves tokens by consolidating file reads and reducing redundant context.",
"command": "python3",
"args": [
"5-Applications/tools-scripts/mcp/token_saver_mcp.py"
],
"env": {}
},
"container-use": {
"_comment": "Container Use MCP (container-use.com). Spawns isolated container environments for running untrusted code, reproducible build experiments, and testing NixOS derivations without touching the host. Connects via mcp-remote relay.",
"command": "npx",
"args": [
"-y",
"mcp-remote",
"https://container-use.com/mcp"
],
"env": {}
},
"consensus": {
"_comment": "Consensus MCP server for evidence-based search over 200M academic papers.",
"url": "https://mcp.consensus.app/mcp",
"transport": "http"
}
}
}
Reference in a new issue View git blame Copy permalink