Camp: Verification
Author: Magnus Knutas
Implementation language: Python (bootstrap)
Compilation target: C (then native via gcc/clang)
Licence: Prove Source License v1.0 (language & .prv source) / Apache-2.0 (tooling)
First seen: February 2026
Maturity: working compiler
Verbs (transforms, validates, derives, creates, matches; inputs, outputs, dispatches; attached, detached, listens, renders) encode intent and IO category in the function declaration. The compiler enforces verb semantics, refinement-type constraints, and ensures/requires/explain contracts. The Prove Source License v1.0 covers all .prv source and prohibits AI training use, dataset inclusion, embedding, and synthetic data generation.
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 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."
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.
.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."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.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.map, filter, reduce — no loops. Errors propagate with !.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.
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.
attached, detached, listens, renders backed by stackful coroutines), terminal UI, GUI via SDL2 + Nuklear, and the proof CLI wrapper.reads to derives, adds the dispatches verb, integrates linting into the check pipeline. v1.3.1 is a bugfix release.Last modified 21 June 2026