The vericoding toolchain

Contracts are the single source of semantic truth. You write them once as plain Python; the same artifact runs as a test today and lowers to a Coq proof obligation tomorrow. The gradient is BDD → executable contracts → mechanised proof, and each rung is useful on its own.

specsaver

Specification-driven verification. Contracts — preconditions, postconditions, invariants, frame conditions, and exception exits — written as plain Python functions and organised by entry point. The contract language is the single source of semantic truth from which every test and proof artefact is derived.

  • Contracts are executable — the same predicate that documents a guarantee enforces it at runtime.
  • Gherkin traceability — each contract binds to the When clause it came from.
  • Lowers to proof obligations — introspected into Coq (Snakelet / FunSpecS) and scored PROVED / DISPROVED / UNKNOWN.
View on GitHub →

axiomander

Mechanised proof for vanilla Python. Contracts are plain assert statements — no imports, no decorators. A Coq + SMT pipeline proves properties; an LLM oracle handles the rest. Zero runtime overhead under python -O.

  • No new language — assert statements, type annotations, and Dafny-style ghost state in plain Python.
  • Coq + SMT + LLM — wp_prove + lia clears most goals, z3 / cvc4 handle the rest, an LLM oracle finishes.
  • MCP-native — check-file, check-function, verify-function, frame-report, and more from any MCP client.
View on GitHub →

rocq-piler

An MCP-based proof assistant for Rocq. Hash-addressed goals, coq-lsp-authoritative state, and parallel goal closure let frontier LLMs discharge real theorems — PCF type preservation for $0.06.

  • Hash-addressed goals — target any open goal by hash and work them in any order.
  • coq-lsp state — the prover always sees what Rocq actually believes.
  • Parallel goal closure — batch-apply tactics to whole classes of goals.
View on GitHub →