# Show HN: Forall – An AI coding agent that generates machine-checkable proofs

> Source: <https://github.com/astrio-labs/forall>
> Published: 2026-07-16 02:16:18+00:00

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

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

Add `~/.local/bin`

to your `PATH`

if needed, then run `forall --version`

.

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

- TypeScript
- Java
- Rust

We are expanding to our popular programming languages based on the demand.

Join our [Discord](https://discord.com/invite/gESuZkdD5R) and [X](https://x.com/astriolabs) communities to connect with other developers using Forall. Get help, share feedback, and discuss your projects with the community.

This repository includes Rust crates for Forall's local authoring and hosted verification adapters:

— workspace authoring library`crates/forall-authoring`

— local authoring MCP server`crates/forall-mcp-author`

— hosted verification client`crates/forall-hosted-verify`

See [crates/README.md](/astrio-labs/forall/blob/main/crates/README.md) and the [architecture docs](/astrio-labs/forall/blob/main/docs/architecture.md)
for how these relate to the standalone `forall`

binary.

Build and test the crates:

```
cargo test --workspace
```

The full agent runtime (TUI, turn loop, sandbox) is distributed only as the prebuilt binary above.

This repository is licensed under the [Apache-2.0 License](/astrio-labs/forall/blob/main/LICENSE).