# Formal Mind Docs

> The guide to Formal Mind: a desktop app whose swarm of agents proves Solidity contracts correct in Lean and finds their bugs, on your own computer. Every page is Markdown at its .md link.

## Start here

- [Formal Mind](https://docs.formal.team/index.md): What Formal Mind does and how its pieces fit.
- [Install the app](https://docs.formal.team/install.md): Download the desktop app, sign in, and keep it up to date.
- [Your first run](https://docs.formal.team/first-run.md): Add a Foundry project and start the swarm on it.

## Prove

- [The swarm](https://docs.formal.team/swarm.md): The plan, the agents, and how a function gets proved.
- [Statements](https://docs.formal.team/statements.md): Claims in plain words, formalized, confirmed and proved.
- [Proofs](https://docs.formal.team/proofs.md): Lean coverage of your contracts, function by function.

## Find bugs

- [Bugs and reports](https://docs.formal.team/bugs.md): Findings with their PoCs, audit reports, and Formal Mind's report.
- [The Bug Hunter](https://docs.formal.team/bug-hunter.md): Coverage, concolic exploration and the debugger, on the bytecode.

## Reference

- [Models and costs](https://docs.formal.team/models.md): Who runs the agents: your Claude plan, credits, or your own key.
- [Files in your project](https://docs.formal.team/files.md): What Formal Mind reads and writes in your folder.
- [Agents and MCP](https://docs.formal.team/agents.md): Connect Claude, ChatGPT or Cursor to Formal Mind.
- [The audit format](https://docs.formal.team/audit-format.md): formalmind.audit/v1, the JSON file per audit report.

## Elsewhere

- [formal.team llms.txt](https://formal.team/llms.txt): the API, the MCP servers and the agent skills