Show HN: Forall – Spec-driven AI coding with formal verification

Uh oh!

There was an error while loading. Please reload this page.

Notifications You must be signed in to change notification settings

Fork 21

Star 160

BranchesTags

Open more actions menu

Folders and files

NameName

Last commit message

Last commit date

Latest commit

History

35 Commits

35 Commits

.forall

.forall

.github

.github

assets

assets

crates

crates

docs

docs

examples

examples

packages

packages

skills

skills

.gitignore

.gitignore

CHANGELOG.md

CHANGELOG.md

CODE_OF_CONDUCT.md

CODE_OF_CONDUCT.md

CONTRIBUTING.md

CONTRIBUTING.md

Cargo.lock

Cargo.lock

Cargo.toml

Cargo.toml

LICENSE

LICENSE

README.md

README.md

SECURITY.md

SECURITY.md

install.sh

install.sh

Repository files navigation

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

1. MCP verify-only

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

Create an API key at forall.astrio.app/dashboard

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.

Connect

Join our Discord and X communities.

License

This repository is licensed under the Apache-2.0 License.

About

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

Topics

java

rust

typescript

Resources

Readme

License

Apache-2.0 license

Code of conduct

Code of conduct

Contributing

Contributing

Security policy

Security policy

Uh oh!

There was an error while loading. Please reload this page.

Activity

Custom properties

Stars

160 stars

Watchers

3 watching

Forks

21 forks

Report repository

Releases 1

Forall v0.1.0

Latest

Jul 10, 2026

Uh oh!

There was an error while loading. Please reload this page.

Contributors

Uh oh!

There was an error while loading. Please reload this page.

Languages

Rust 95.2%

Shell 3.3%

JavaScript 1.5%