Forall (∀)

Forall is a coding agent from Astrio that helps developers build correct software by generating spec-driven code alongside machine-checkable proofs.

Two ways to use Forall

1. Install Forall CLI

Full coding agent — specs, proofs, and workflow in your terminal.

curl -fsSL https://forall.astrio.app/install.sh | bash
forall

Add ~/.local/bin to your PATH if needed, then run forall --version.

On first launch, sign in with your Forall account — your browser opens, no API key to paste. Chat on your plan's hosted models, or bring your own model API key (OpenAI, OpenRouter, Anthropic (Claude), Google Gemini, Azure OpenAI, or Claude via Amazon Bedrock). Then forall init in a git repo and start working.

Note: A binary release must exist on GitHub Releases before install succeeds.

2. MCP verify-only

Stay on Cursor, Claude Code, or any MCP client — add hosted verification via MCP. Do not install the CLI.

1. Create an API key at forall.astrio.app/dashboard
2. Add to your MCP client:

{
  "mcpServers": {
    "forall": {
      "command": "npx",
      "args": ["-y", "@astrio/forall-mcp"],
      "env": {
        "FORALL_API_KEY": "forall_..."
      }
    }
  }
}

Your coding agent edits the workspace from verify reports. See docs/getting-started.md and docs/hosted-mcp.md.

Supported programming languages

• TypeScript
• Java
• Rust

We are expanding to more languages based on demand.

Telemetry

First-party builds send product usage analytics — feature and reliability events, never your code or prompts. Opt out any time in ~/.forall/config.toml:

[analytics]
enabled = false

Connect

Join our Discord and X communities.

License

This repository is licensed under the Apache-2.0 License.