Forall: proof-carrying code, graded on the evidence a machine produced

Why Forall exists: the bottleneck moved

The opening argument of the README is worth stating in its own terms, because it is the whole justification for the project.

Review has always been the bottleneck in software. It is now the failure point, because code is produced faster than anyone can check it. Tests sample a handful of inputs. Types constrain shape. Neither tells you whether the code does what it was supposed to do.

Formal verification answers that question, as far as your specification states it, and it never failed on capability. Provers have been checking real programs for years. What kept them out of ordinary engineering was adoption cost, because writing the specifications, contracts and invariants a prover needs was more tedious than writing the code itself.

The argument then turns on labour. That is precisely the work language models are now good at, so the barrier was labour, and labour just got cheap. Forall is the direct consequence of that claim: if a model can write the specification, the contract and the invariant, then the evidence can be produced at the same time as the code rather than reconstructed by hand afterwards.

The second part of the argument is about where this matters. Evidence can therefore become a build artifact rather than something reconstructed by hand long after the code is done, and regulated work already depends on it. The README names IEC 62304 and DO-178C as standards that require traceability from each requirement to the verification that discharges it, and argues that mission-critical code should carry that evidence the way a paper carries its references, attached to the specific claim it supports.

That framing matters because it sets the scope of the tool. Forall is not aiming at the ordinary application where a passing test suite is enough. It is aimed at the code where somebody will eventually be asked to show the work.

Four levels of evidence, and why a green mark that lies is worse

The design commitment that distinguishes Forall from every other verification tool is a grading scheme with four rungs instead of two.

The README puts the reason bluntly: a green mark that lies is worse than no mark. A proof is only as strong as the contract it discharges, and property testing only samples. Those differences matter, so Forall reports four levels of evidence instead of a pass and a fail, grading every requirement by the strongest evidence a machine actually produced, never by what was claimed.

The four rungs are defined in the README as follows. Spec tracked means a requirement cites this code. Property tested means a generator ran over many inputs and found no counterexample, which the README describes as statistical evidence, honestly ranked below a proof. Contracted means a machine-checkable contract is written against the code, but nothing has confirmed it yet. And Proved means a prover discharged that contract's obligations.

The ordering is the point. Property testing sits below proof because it samples, and the README says so without hedging. Contracted sits above property tested but below proved, and the reason is a specific and important one: a contract that has been written but not yet checked is a claim, not a result. A tool that treated a written contract as a passing check would be doing exactly what the green mark warning is about.

So the grading is per requirement, and it is evidence-based rather than assertion-based. That is a meaningfully different report from a build that says the project passes. It says, for each requirement, what kind of evidence exists behind it, and it never counts something that was merely written.

Two ways to use it, and the language table that decides what you can get

The supported programming languages section is the most practically useful part of the README, and it is honest in a way most tool documentation is not.

Forall grades every requirement by the strongest evidence a machine actually produced for it, and not every rung is reachable in every language, because the rung depends on the tool behind it. The table therefore has a blank cell in it rather than a tick.

TypeScript reaches all four: spec tracked, property tested, contracted and proved. Python reaches the first three but not proved, marked with a cross. Rust, Java and C reach spec tracked, contracted and proved, with property testing marked as not available. The README also says the project is expanding to more languages, and to filling in more of this table for the languages already listed, based on demand.

That single row difference between TypeScript and Rust is not a detail, because it changes what a graded result means. A TypeScript project can have property-based tests running over generated inputs, so a requirement whose contract has not been discharged can still carry sampled evidence. A Rust project with a discharged contract carries a proof, which is stronger. A Rust project without a contract has less than a TypeScript project with property tests, because there is no sampled rung to fall back on.

A team choosing a language for a Forall project therefore has a real trade-off in front of them, and the table lets them see it before writing any code.

Route one: the CLI, with a hosted model and no API key

There are two ways to use Forall, and the first is a full coding agent with specs, proofs and workflow in your terminal.

Installation is a single piped script:

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

Then you add ~/.local/bin to your PATH if needed and run forall --version to confirm it works. There is a note attached that matters for anyone automating this: a binary release must exist on GitHub Releases before install succeeds. So the install script is not a self-contained bootstrap, it depends on a tagged artefact existing upstream.

On first launch you sign in with your Forall account, and the README is specific that your browser opens and there is no API key to paste. After that you can chat on your plan's hosted models, or bring your own model API key. The supported providers are named: OpenAI, OpenRouter, Anthropic (Claude), Google Gemini, Azure OpenAI, and Claude via Amazon Bedrock.

That list is worth pausing on, because it mixes providers that a user can sign up for individually with two enterprise routes. Azure OpenAI and Amazon Bedrock are the two that exist for organisations that cannot send data to a public API endpoint, and their presence in the list says the tool was designed with that case in mind rather than added later.

Then the workflow starts with forall init in a git repo. The requirement that it be a git repository is a small but real constraint, since the tool's output is meant to live alongside the code and travel with it.

Route two: the MCP server, which adds verification to an agent you already use

The second route is the one for teams that already have a coding agent and do not want to replace it. The README's framing is direct: stay on Cursor, Claude Code, or any MCP client, and add hosted verification via MCP. The instruction not to install the CLI is bolded, which tells you the two routes are genuinely alternative rather than complementary.

The setup is two steps. Create an API key at the Forall dashboard, and add the server to your MCP client:

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

Two details in that configuration carry weight. The command is npx with the -y flag and the package @astrio/forall-mcp, so the server is a Node package fetched at launch rather than a binary you install, which means the MCP client needs a working Node environment. And the API key is passed through an env entry rather than as a command argument, so it does not appear in a process listing.

The division of labour is what makes this route attractive. The coding agent does the editing and stays in the tool your team has standardised on, and your agent edits the workspace from verify reports. The verification is hosted, so there is no prover to install, no local toolchain for each language in the table, and no per-project setup. The README points at docs/getting-started.md and docs/hosted-mcp.md for the detail.

The tradeoff against the CLI route is that the hosted path sends your specification and code to somebody else's service, whereas the CLI can use a model API key you supply. That is the decision to make before you pick a route, and the README does not hide it.

The repository: three crates, and what the dependency list reveals

The top-level listing is short: .forall/, .github/, CHANGELOG.md, CODE_OF_CONDUCT.md, CONTRIBUTING.md, Cargo.lock, Cargo.toml, LICENSE, README.md, SECURITY.md, assets/, crates/, docs/, examples/, install.sh, packages/, and skills/.

The Cargo.toml declares a workspace with resolver 2 and three members, and the names describe the architecture:

[workspace]
resolver = "2"
members = [
    "crates/forall-authoring",
    "crates/forall-hosted-verify",
    "crates/forall-wire",
]

[workspace.package]
version = "0.1.0"
edition = "2024"
license = "Apache-2.0"

Three crates, and they split along the wire. forall-authoring is the side that produces specifications, contracts and proofs. forall-hosted-verify is the client that talks to the hosted verification service, which is what makes route two work without any local prover. And forall-wire is the shared protocol layer between them, which is why it is a separate crate rather than a module in one of the others.

The dependency list explains what the tool does at the edges. axum is an async HTTP server framework, and reqwest is an HTTP client with cookies enabled, so the hosted verification path is HTTP in both directions. rmcp is the Model Context Protocol library at version 1.7.0, which is the MCP server implementation for route two. serde, serde_json and serde_yaml handle the three serialisation formats on the wire, and schemars derives JSON Schema from the types, which is how an MCP server describes its tools. sha2 is for hashing, tempfile for scratch files, walkdir for walking a workspace, regex for pattern matching, chrono with serde for timestamps, tokio for the async runtime, anyhow and thiserror for error handling, and serde_yaml at 0.9 rather than 1.0 is a version to note.

Two other directories are worth knowing about. There is a packages/ directory alongside the Rust crates, which is where the npm package @astrio/forall-mcp lives for the npx route, and a skills/ directory, which is where the agent skill definitions live that the CLI hands to a model.

Telemetry, and the one-line opt out

The telemetry section is short and specific, and it states what is and is not collected.

First-party builds send product usage analytics, which are feature and reliability events, never your code or prompts. You can opt out at any time in ~/.forall/config.toml:

[analytics]
enabled = false

The two claims are worth separating. The first, that only feature and reliability events are sent, is a statement about the contents of the events. The second, that code and prompts are never sent, is a much stronger claim, and it is the one that matters for anyone working under a confidentiality obligation or building in a client environment.

There is a phrase to note carefully: first-party builds. The qualifier implies that there are builds that are not first-party, probably a distribution channel you did not build yourself, and for those the guarantee may not apply. If you are running the hosted MCP route, you are on the hosted service rather than a local build, so the question of what leaves your machine is worth asking of the vendor rather than assuming from a sentence about first-party builds.

The opt-out being a config file rather than a command-line flag is a small design choice that matters in practice, because a config file can be committed to a repository and therefore enforced for a whole team, whereas a flag has to be remembered per invocation.

How to evaluate it, and the questions to ask first

There are three questions, and the first two are answerable from the README while the third is not.

The first is what evidence level your language can reach, which the table answers, and it is the question that decides whether the tool helps you at all. If your project is TypeScript, all four rungs are open to you. If it is Rust, Java or C, you can get a proof but not property testing, which means the interesting fallback rung is missing. If it is Python, you get property testing but no proof. And if your project is in a language not on the list, the tool currently gives you spec tracking at best.

The second is which route fits your organisation. The CLI keeps the model provider flexible and lets you supply your own key, and it is the only route that could work offline or inside a network boundary. The MCP route is the lower-friction one for a team already standardised on Cursor or Claude Code, since verification arrives as a report your existing agent acts on, with no prover to install per language. The cost is that your specifications and code travel to a hosted service, which is a question for whoever owns that policy.

The third is what the tool does not tell you. The README does not say which prover sits behind the Proved column, nor which property-testing framework sits behind the property testing column, and the workspace dependencies do not show a prover because the verification is hosted. So the question of which obligations are actually discharged, and with what soundness assumption, is answered by the hosted service rather than by the code in front of you. The published versions are v0.5.0 from 2026-08-02, v0.4.0 from 2026-08-01 and v0.3.0 from 2026-07-19, and the last push was on 2026-10-15, so the project is young and the version number is not yet a stability signal.

What the tool does offer is a real idea with a coherent implementation behind it. Treating evidence as a graded artifact rather than a pass mark, refusing to count a written-but-unchecked contract as proof, and attaching the evidence to the requirement it supports are the right instincts for the regulated and mission-critical code the project is aimed at. The open question for an adopter is how much of that promise survives the trip through a hosted service.

Editorial conclusion

Adopt Forall if you work on code that will have to be justified, in the sense that a regulated process such as IEC 62304 or DO-178C will eventually ask you to trace a requirement to the verification that discharges it, and if your language appears in the support table with the evidence levels you actually need. Do not adopt it as a general test replacement, since it grades evidence rather than passing tests, and do not assume a written contract counts as a proof, because the Contracted rung exists precisely to record obligations that no prover has yet discharged. Before you commit, check the language table for the highest rung reachable in your project, decide between the CLI and the hosted MCP route on where your specifications and code are allowed to go, read the telemetry section carefully and set the opt out in ~/.forall/config.toml if your policy requires it, and pin a version, since the releases are still on the 0.x line with v0.5.0 the newest.

Frequently asked questions

Official sources

1. astrio-labs/forall-mcp on GitHub
2. Issues
3. License: Apache-2.0
4. README
5. Releases