The thesis.
Prove diagnoses the same problem the rest of the verification camp diagnoses — AI-generated code is cheap to produce and expensive to trust — and adopts the same general moves: intent-first declarations, hard postconditions (ensures), refinement types, no if/else, errors-as-values, no nulls. Every function carries a verb (transforms, validates, derives, creates, matches for pure code; inputs, outputs, dispatches, streams for IO; attached, detached, listens, renders for structured concurrency). The verb is enforced: a transforms function cannot call IO functions (diagnostics E361–E363); explain blocks document the chain of operations in controlled natural language, parsed and verified against called functions’ contracts.
Source code is covered by an anti-training license.
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 license — 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 license. The Prove Source License v1.0 covers the language, its specification, and all
.prvsource. 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. explainagainst 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 checkruns by default and generates plausible-but-wrong mutations of the function body, requiring the author to address each with awhy_notannotation. - 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 license 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.
- Vera 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 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 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).