Show HN: Forall – OpenSpec but with actual machine-checkable verification

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

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 a Forall account (API key) or bring your own model API key (OpenAI / OpenRouter). Then forall init in a git repo and start working.

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

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

{ "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 .

TypeScript Java Rust We are expanding to more languages based on demand.

This repository is licensed under the Apache-2.0 License .