Source code is covered by an anti-training licence.
Where Prove diverges from Vera and Aver is on the politics rather than the mechanics. Vera publishes a benchmark and invites models to compete. Aver exports proofs and ships an `llms.txt`. Prove ships an *anti-training* licence — the Prove Source License v1.0, applied automatically by `proof new` to every project — that prohibits use of `.prv` source code as training data, in dataset inclusion, vector stores, RAG indices, embedding databases, synthetic data generation, sublicensing for AI use, and downstream propagation. AILANG sits closest on effect typing (both ship typed effects), but Prove encodes effect category in the verb itself rather than in a row-polymorphic effect list. The project frames its own stance as "AI resistance" and states that generating semantically correct Prove code "requires genuine understanding, not pattern matching."
## What it looks like.
matches apply_discount(discount Discount, amount Price) Price
ensures result >= 0
ensures result <= amount
requires amount >= 0
from
FlatOff(off) => max(0, amount - off)
PercentOff(rate) => amount * (1 - rate)
A pure verb (matches), hard postconditions, and a precondition — all enforced at compile time.
## Distinctive moves.
- **Verbs as intent, enforced.** Each function declares its purpose with a verb. Pure verbs cannot perform IO. The same name can have multiple verbs and the compiler resolves which to call from context.
- **Anti-training licence.** The Prove Source License v1.0 covers the language, its specification, and all `.prv` source. The compiler tooling (Python bootstrap, docs, editor integrations) is separately Apache-2.0; the project publishes its reasoning for the split under "AI Transparency."
- **Refinement types.** `type Port is Integer:[16 Unsigned] where 1..65535`. Constraints are part of the type, validated at compile time, and used to drive auto-generated edge cases.
- **`explain` against contracts.** Controlled natural language documents the implementation; the compiler parses each row, checks that operations match called functions' behaviours, and rejects explanations whose references aren't real identifiers.
- **Refutation challenges.** `proof check` runs by default and generates plausible-but-wrong mutations of the function body, requiring the author to address each with a `why_not` annotation.
- **Functional iteration only.** `map`, `filter`, `reduce` — no loops. Errors propagate with `!`.
## Maturity.
v1.3.1 (April 2026), tracked through a clear release history: v1.0.0 (first stable, 22-module standard library, C codegen, region-based memory, 13-pass optimiser, ML-powered LSP), v1.1.0 (March 2026, structured concurrency + GUI + `proof` CLI), v1.2.0 (March 2026, verb consistency overhaul across 22 stdlib modules), v1.3.0/v1.3.1 (April 2026, tree-sitter as sole parser, `dispatches` verb). Source is hosted on a self-hosted Gitea instance at code.botwork.se rather than GitHub. Author: Magnus Knutas. Bootstrap compiler is Python 3.11+; output language is C. The roadmap names v2.0 as a self-hosted compiler. The bet is that the same intent-first mechanism that resists external AI generation is also the substrate for the project's "local, self-contained" generation model — a deterministic toolchain that produces code from the project's own declarations.
## Agent tooling.
None of the catalogue's usual surface: no `SKILL.md`, no `AGENTS.md`, no `llms.txt`, no MCP server. The licence actively prohibits the dominant tooling pattern. The project ships editor integrations instead — `tree-sitter-prove` for syntax highlighting, `pygments-prove` for MkDocs/Sphinx, `chroma-lexer-prove` for Gitea/Hugo — and a single-file installer (`curl -sSf install.sh | sh`) that places a `proof` binary in `~/.local/bin/`. The roadmap lists binary AST format, semantic normalisation, fragmented source, and identity-bound compilation as post-1.0 anti-training features.
## Design DNA
- **[Vera](https://agentlanguages.dev/languages/vera.md)** *(Verification)* — Same diagnosis, opposite politics. Both ship mandatory contracts and explicit effects; Vera publishes a benchmark and invites models to compete, Prove ships an anti-training licence that prohibits training use of source.
- **[Aver](https://agentlanguages.dev/languages/aver.md)** *(Verification)* — Camp neighbour with proof export. Both ship intent-first design and contract-style verification; Aver exports to Lean 4 / Dafny and ships llms.txt, Prove ships the anti-training licence and self-hosted Gitea.
- **[AILANG](https://agentlanguages.dev/languages/ailang.md)** *(Verification)* — Both ship effect-typed designs. AILANG carves effects via row polymorphism (IO/FS/Net/Clock/AI); Prove encodes IO category in the verb itself (inputs/outputs/dispatches vs transforms/validates/derives/creates/matches).
## Timeline
- **Feb 2026** — v1.0.0 first stable release. 22-module standard library, intent-driven compiler (verb enforcement, contracts, refinement types), C code generation with region-based memory and a 13-pass optimiser, ML-powered LSP.
- **Mar 2026** — v1.1.0 ships structured concurrency (