About AI Safety Formalization Atlas
AI Safety Formalization Atlas is an MCP server in the Blockchain category: the open workbench for AI safety, made formal. Turn safety questions into machine-checked Lean proofs — a shared launchpad where researchers and AI agents build provable safety together.
Install
git clone https://github.com/mbrcic/ai-safety-formalization-atlasThis server has no ConduID identity, so agent calls to it are not receipted. Pin the version you install and review the source before granting it credentials.
Tools (4)
[LeanSearchClient](https://github.com/leanprover-community/LeanSearchClient)[leansearch](https://leansearch.net) and [loogle](https://loogle.lean-lang.org) queries from inside Lean
Parameters not published.
[lean-explore](https://github.com/justincasher/lean-explore)semantic search over Lean 4 declarations — by meaning, not by name
Parameters not published.
[lean-lsp-mcp](https://github.com/oOo0oOo/lean-lsp-mcp)the Lean language server over MCP: diagnostics, goal state, hover, references. Answers per file in seconds what `lake build` reports in minutes, which is the right tool after a rename
Parameters not published.
[lean4-skills](https://github.com/cameronfreer/lean4-skills)"Lean 4 theorem proving skill and workflow pack for AI coding agents" — proof repair, golfing, axiom elimination. MIT
Parameters not published.
Ask AI
Ask AI about AI Safety Formalization Atlas
Powered by Claude · Grounded in docs
Security checks
6 checks have not been run yet.