Related projects

Research projects and open-source repos that share ground with dox-populi: an LLM writes the code from a machine-readable spec, checkers (Z3, Paradox, tsc) verify named properties and produce evidence, and the human inspects the evidence and decides. Gathered 2026-09-06.

Closest kin — checker gates the LLM, human stays in the loop

• Clover — repo · paper · Stanford blog LLM generates code, docstring, and formal Dafny annotations; a checker enforces consistency among all three. On their benchmark it rejected every incorrect program. Strongest single reference for the checker-as-gate idea.

• Verifiable Literate Programming (Univ. of Hong Kong, 2026) — paper Structures LLM-generated code and machine-checkable claims so a human at any skill level can validate that the code matches intent. Closest philosophical neighbor: checker output shrinks what the human has to review, and the human validates.

• Astrogator — paper Verifies LLM-generated Ansible against a formal query the user reviews and confirms, via a symbolic interpreter. Keeps the human confirming intent while the machine verifies. dox-populi flips one piece: the spec is machine-read and the human inspects the evidence.

• Imandra CodeLogician — examples · benchmark Translates source code into Imandra’s modeling language and reasons about it formally. Their pitch (formal reasoning as a service, without expertise) matches dox-populi’s almost word for word. The core reasoner is a commercial service.

Verifier-in-the-loop codegen — mostly aims to close the loop without a human

• AutoVerus (Microsoft) — repo · paper LLM agents generate and debug Verus proofs for Rust, driven by verifier error messages.

• AlphaVerus (CMU) — repo · paper Bootstraps verified Rust generation via tree search over verifier feedback. It documents the LLM gaming the checker (vacuous specs) and defends against it — a concrete argument for keeping the human inspector.

• VeCoGen (KTH) — repo · paper Generates C from formal ACSL specs, iterating until Frama-C/Why3 verify the code against the spec. Very close to the dox-populi pipeline shape; the human writes the formal spec.

• spec2code (KTH + Scania) — paper LLM codegen with multiple “critics” including formal verification, for real truck-module C code. Industry evidence for checker-gated pipelines in safety-critical work; their “critics” wording matches the checkers-as-instruments framing.

• dafny-annotator — repo · paper · Dafny blog LLM adds assertions and invariants until the Dafny verifier accepts.

• verified-cogen (JetBrains Research) — repo Tests whether LLMs can produce verified code across Dafny, Nagini, and Verus.

• SAFE (Microsoft) — paper Self-evolving training loop where the Verus verifier separates correct from incorrect proofs and the failures become training data.

• Baldur — paper Whole-proof generation and repair for Isabelle/HOL from checker error messages.

• Towards AI-Assisted Synthesis of Verified Dafny Methods (Misu, Lopes et al., FSE 2024) — repo · paper GPT-4 wrote Dafny methods with specs; verified, human-evaluated solutions for 58% of 178 MBPP problems. Humans stayed in the loop as evaluators.

• Google CEL formal verification — verifier · announcement Z3-backed checker for CEL policy expressions, pitched as a CI gate on AI-refactored policies. A production example of an LLM writing the code and Z3 gating it in CI. Narrow domain.

• RTL repair framework — repo Multi-agent LLM pipeline that repairs hardware RTL with an open-source formal backend (Yosys, SymbiYosys, Z3) and counterexample-guided iteration. Hardware, same trust structure.

Spec-driven dev tooling — machine-readable spec, no checker behind it

• GitHub Spec Kit — repo · GitHub blog Prose spec as the source of truth for coding agents; validation is tests and review.

• Kiro (AWS) — issue tracker Agentic IDE that forces structured EARS requirements and design docs before codegen. Closed source; the specs are structured English.

• OpenSpec — repo Human approves an AI-drafted spec, then the LLM works from it; agreement is eyeballs on markdown.

• Tessl — spec-driven-development-tile Specs live in the repo as durable agent memory; the guardrail is ordinary tests.

Instruments and benchmarks

• Dafny — repo Verification-aware language with an SMT-based (Z3) verifier built in.
• Verus — repo SMT-based verifier for Rust; specs and proofs inline, lowered to Z3.
• LeanDojo / ReProver / LeanCopilot — org Open toolkits for LLM-driven theorem proving in Lean: the LLM proposes, the Lean kernel accepts or rejects.
• DeepSeek-Prover-V2 — repo Open-weights LLM specialized for formal theorem proving in Lean 4.
• DafnyBench — repo Dafny programs with verification hints stripped; LLMs must regenerate enough annotations for Dafny to verify.
• Vericoding benchmark — paper 12,504 formal specs across Dafny, Verus, and Lean for measuring LLM generation of verified code. The field now calls this genre “vericoding,” and a NeurIPS 2026 workshop exists for it: vericodegen.github.io.

The gap dox-populi sits in

The spec-driven camp has machine-readable specs with no checker behind them. The verification camp has checkers in the loop but mostly generates proofs or annotations for existing code, and mostly aims to remove the human. dox-populi combines a machine-checked spec driving whole-project codegen with the human inspecting the evidence and deciding.

Vocabulary note: across these papers the verifiers are described as accepting, rejecting, or verifying against a specification — which lines up with the blog’s claim vocabulary.