# Formal Mind

> Formal Mind is an app for Solidity developers that proves their contracts correct. It keeps four things in one place: Bugs (every audit report and finding, with its status and proof-of-concept test), Proofs (the Lean 4 theorems written so far, tracked per Solidity function), Code (the repository, with LSP navigation), and a Swarm of agents that runs on your own computer and does the work: it writes and checks a Lean proof for each function in scope and files bugs with Foundry PoCs. Every theorem is machine-checked by lake build, with no sorry and no new axioms, and the swarm keeps everything in the repository's own files.

**Status: early access. The desktop app is free to download for macOS (Apple Silicon and Intel) and Windows; the swarm runs locally and runs its agents on your own Claude plan (through Claude Code) or your own Anthropic or OpenAI key. The website opens public GitHub repositories with the same Bugs, Proofs and Code tabs.**

Formal Mind proves Solidity contracts correct: a swarm of agents on your own computer writes a Lean 4 proof for each function in scope, checks it with lake build, and files bugs with Foundry PoCs. Bugs, Proofs and Code show the results, read from the repository's own files. The full account, how the swarm works and where it keeps its files included, is in [llms-full.txt](https://formal.team/llms-full.txt).

## Agents

- [MCP server card](https://formal.team/.well-known/mcp/server-card.json): read-only tools at https://formal.team/mcp (Streamable HTTP, no auth): get_audit_format, get_example_audit, get_app_release; and the account server at https://formal.team/mcp/account (OAuth 2.0, GitHub sign-in): my_projects, list_files, read_file, list_audits, list_findings, get_finding, proofs_coverage, mac_swarm, mac_watch, mac_swarm_events, mac_get, mac_reply, mac_swarm_send, mac_do (mac_get and mac_do read and drive everything the desktop app does on the person's Mac)
- [Skill: connect-formal-mind-as-mcp](https://formal.team/.well-known/agent-skills/connect-formal-mind-as-mcp/SKILL.md): add https://formal.team/mcp/account to Claude, ChatGPT or Cursor and act on your own account
- [Skill: run-the-local-swarm](https://formal.team/.well-known/agent-skills/run-the-local-swarm/SKILL.md): run the swarm on a folder in the desktop app; proofs, bugs and state stay in the folder
- [Skill: onboard-a-repository](https://formal.team/.well-known/agent-skills/onboard-a-repository/SKILL.md): plan a repository, add it as a project, optionally set up specs from its commits
- [Skill: read-formal-mind-results](https://formal.team/.well-known/agent-skills/read-formal-mind-results/SKILL.md): the files Formal Mind keeps in a repository and the formalmind.audit/v1 format
- [auth.md](https://formal.team/auth.md): GitHub sign-in for people; OAuth 2.0 (RFC 8414 metadata, dynamic registration, PKCE, refresh, revocation) for agents acting on an account

## Formal Mind

- [The audit format](https://github.com/formalmind/releases/blob/main/docs/audit-format.md): formalmind.audit/v1, the JSON file per audit report that Bugs reads and the swarm writes
- [Example: Async Swap's contracts](https://github.com/asyncswap/contracts): Lean proofs in formal/, Formal Mind's audit in audit/formal-mind.audit.json
- [Formal Mind protocol, v1 draft](https://github.com/formalmind/releases/blob/main/docs/protocol.md): the messages, records and rules of the hosted side (draft)

## App

- [Docs](https://docs.formal.team): the guide to the app (install, the swarm, Statements, Proofs, Bugs, files, MCP); every page as Markdown, listed in [its llms.txt](https://docs.formal.team/llms.txt)
- [Download for Mac](https://github.com/formalmind/releases/releases/latest/download/Formal-Mind-mac.dmg): the desktop app, one universal build; the local swarm runs here
- [Download for Windows](https://github.com/formalmind/releases/releases/latest/download/Formal-Mind-windows-setup.exe): the same app for Windows
- [Releases](https://github.com/formalmind/releases/releases): every version of the desktop app
- [Landing page](https://formal.team/welcome): paste a public repository and watch the planner plan it
- [Sign in](https://formal.team/login): GitHub sign-in; projects and usage are behind it
- [GitHub App](https://github.com/apps/formalmind): installed on a repository's owner so formal.team can read a private repository
- [Source](https://github.com/formalmind/releases): the website and the desktop app

## Optional

- [Terms](https://formal.team/terms)
- [Privacy](https://formal.team/privacy)
- [Brand kit](https://formal.team/brand)