Compendium

Theorem-Prover DSLs Family Index

16 min read

Theorem-Prover DSLs Family Index

type: language-family-index family: theorem-prover-dsls languages_catalogued: 23 tags: [language-reference, family-index, theorem-prover-dsls, proof-assistants, tactics, metaprogramming, hammers, declarative-proof, reflection]

Theorem-Prover DSLs — Family Index

Family overview

A “theorem-prover DSL” in this catalogue is the embedded scripting layer inside a proof assistant — the language users actually type to drive the kernel, not the kernel’s own term language. The host languages (Coq/Rocq, Lean 4, Agda, Idris 2, Isabelle, F*, ACL2, HOL Light, HOL4, PVS, Mizar, Cedille, Twelf, Dafny, Why3) are catalogued as deep-library notes or in adjacent Tier 3 indexes; this note is for the tactic, elaborator, macro, and declarative-proof DSLs that sit on top of them. Roughly four dialect families coexist: (1) procedural tactic languages that imperatively transform a goal stack — Ltac, Ltac2, HOL Light’s THEN/THENL combinators, HOL4’s simpLib, PVS proof commands, Idris/Agda elaborator-reflection scripts; (2) declarative proof languages that read top-down like prose — Mizar (the granddaddy), Isabelle/Isar, Lean’s calc/have blocks; (3) typed metaprogramming layers that let you write tactics in the host language with full type-checking — Lean 4’s elaborator + MacroM/TermElabM/TacticM, F*‘s Meta-F*, Mtac/Mtac2, MetaCoq, Idris 2 elaborator reflection, Agda’s reflection + TC monad; and (4) hammers that route goals to external automated provers — Sledgehammer (Isabelle), CoqHammer, MetiTarski, plus newer LLM-augmented variants like Lean Copilot.

The historical arc starts with Edinburgh LCF in the 1970s, where Robin Milner invented ML specifically to write tactics — every modern procedural tactic language is a descendant of LCF’s tac : goal -> goal list * (thm list -> thm) shape. Mizar (1973, Andrzej Trybulec at Białystok) took the orthogonal path: write proofs as readable mathematical text checked by a fixed verifier, not as imperative scripts; this declarative tradition was carried into Isabelle by Markus Wenzel as Isar (1999) and into Lean/Coq via calc/have. Coq’s Ltac (David Delahaye, 2000) became the most influential procedural language of the 2000s — flexible, untyped, with unification patterns and backtracking — but its dynamic-scope semantics and silent failure modes earned it a reputation as a footgun. Ltac2 (Pierre-Marie Pédrot, stable in Coq 8.11 in 2020, now part of the core Rocq distribution) and the Lean 4 elaborator (Leonardo de Moura and Sebastian Ullrich, 2021) are the modern reaction: typed, OCaml/Lean-flavoured tactic programming languages with first-class tactics, hygiene, and proper error handling.

Three cross-cutting trends define the 2020–2026 era. Reflective tactics — Mtac/Mtac2 (Beta Ziliani et al.), MetaCoq (Sozeau, Anand, Boulier et al.), Agda’s reflection, Idris 2 elaborator reflection — let users prove things about their tactics by encoding the term language as an inductive type inside the host. Hammer integration has become standard: Sledgehammer (originally for Isabelle, c. 2007) routes goals to E, Vampire, Z3, CVC4/CVC5, and SPASS, then reconstructs proofs in Isar; CoqHammer (Czajka & Kaliszyk, 2018, currently 1.3.2 supporting Rocq 9.0 and Coq 8.20) brings the same pattern to Coq via sauto for proof reconstruction. LLM-assisted tactics — Lean Copilot (lean-dojo, 2024–2025), Coq’s tactician, GPT-f-style premise-selection — are the newest layer, treating the LLM as another backend like an SMT solver. And underneath all of this sits the fact that most theorem provers are written in OCaml, SML, or Haskell (Coq/Rocq in OCaml, Isabelle in Poly/ML, HOL Light in OCaml, HOL4 in Poly/ML, Lean 4 in Lean+C, Agda in Haskell), which constrains the host-side DSLs available for plugin authors and explains the ML-flavoured aesthetic of Ltac2, Isabelle/ML, and friends.

In our deep library

Deep notes exist for the host languages of most of the DSLs catalogued here:

  • coq — covers Rocq (renamed from Coq, 2025), the kernel/CIC, and gives an overview of Ltac/Ltac2/MetaCoq. This family note expands on the DSL details.
  • lean — Lean 4, including the macro/elaborator/tactic-monad metaprogramming framework that is Lean’s tactic DSL.
  • agda — host language; the reflection layer (Term, TC, unquote, unquoteDecl) is the relevant DSL.
  • idris — Idris 2; elaborator reflection is its tactic DSL.

Adjacent Tier 3 family notes:

  • logic-and-constraint — Prolog, λProlog (which underlies Coq-Elpi), Mercury, Curry, ASP. Tactic search is logic programming in disguise; Coq-Elpi makes that explicit.
  • notation-spec — TLA+, Alloy, Z, B-method, Maude, K Framework, Why3 (specification side). Verification-aware specification languages overlap heavily with the prover ecosystem.
  • ml-and-fp — OCaml, SML/Standard ML, Haskell, F#, F*. The host-implementation languages of essentially every prover in this family. Isabelle/ML is Poly/ML extended with Isabelle’s logical infrastructure.
  • lisps — ACL2 is a Lisp; its macros and computed hints are Common Lisp metaprogramming repurposed for proof.

Tier 3 family table

LanguageFirst appearedOriginHost proverStatus (2026)URL
Ltac2000Coq team (David Delahaye)Coq / RocqActive but in slow retirement. Still ubiquitous in legacy code; Ltac2 preferred for new tactic libraries; ships in Rocq 9.x (March 2025)https://rocq-prover.org/refman/proof-engine/ltac.html
Ltac22019 (stable in Coq 8.11, January 2020)Coq team (Pierre-Marie Pédrot)Coq / RocqActive, the modern replacement. Now part of the rocq-core opam package as a core library (no longer a standalone plugin) as of Rocq 9.0; recent additions include Ltac2 Custom Entry for richer notationshttps://rocq-prover.org/refman/proof-engine/ltac2.html
Mtac / Mtac22013 (Mtac, ICFP) / 2018 (Mtac2, ICFP)Beta Ziliani, Derek Dreyer, Yann Régis-Gianas, Viktor Vafeiadis et al. (MPI-SWS)Coq / RocqActive research but small user base; available via opam as coq-mtac2https://github.com/Mtac2/Mtac2
MetaCoq2018+ (consolidation of earlier projects: Template-Coq from Anand & Malecha 2014)Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau, Théo WinterhalterCoq / RocqActive. Provides reified Coq terms as a Coq inductive type plus a verified type-checker (SafeChecker) and verified erasure pipelinehttps://metacoq.github.io/
Coq-Elpi (λProlog inside Coq)2018+Enrico Tassi, Claudio Sacerdoti Coen, Davide Fissore et al. (LPCIC, INRIA)Coq / RocqVery active. Powers Hierarchy Builder for algebraic class hierarchies; Elpi v3.7 released April 2026https://github.com/LPCIC/coq-elpi
CoqHammer (sauto + hammer driver)2014 (paper), 2018 (CoqHammer 1.0)Łukasz Czajka, Cezary KaliszykCoq / RocqActive. Version 1.3.2 supports Rocq 9.0 (Nov 2024) and Coq 8.20 (April 2025); proof generation Linux/macOS only, reconstruction works on Windowshttps://coqhammer.github.io/
Lean 4 macros (syntax + macro_rules)2021 (Lean 4 stable)Leonardo de Moura, Sebastian Ullrich (Microsoft Research → AWS / Lean FRO)Lean 4Very active. Hygienic syntax-to-syntax expansion; the do notation, simp configuration syntax, calc blocks, and most of mathlib4’s DSLs are macroshttps://leanprover.github.io/lean4/doc/macro_overview.html
Lean 4 elaborator (elab_rules + TermElabM/TacticM)2021de Moura & UllrichLean 4Very active. The general metaprogramming layer; macros desugar to elaborator entries when they need to do things rather than just rewrite syntaxhttps://leanprover-community.github.io/lean4-metaprogramming-book/
Lean 4 grindIntroduced 2024, stabilised through Lean 4.20–4.25 (2025)Leonardo de Moura et al.Lean 4Active and rapidly evolving. SMT-inspired E-matching + congruence closure tactic; v4.25 (Nov 2025) added interactive grind => …, show_splits, show_state, finish?, support for injective functions, non-commutative semirings, preordershttps://lean-lang.org/doc/reference/latest/releases/v4.25.0/
aesop (Lean 4)2022Jannis Limperg, Asta Halkjær FromLean 4Active. White-box best-first proof search with rule sets registered via @[aesop]; mathlib4’s measurability, continuity, etc. are aesop rule setshttps://github.com/leanprover-community/aesop
Lean Copilot2024 (paper April 2024, NeuS 2025)Peiyang Song, Kaiyu Yang, Anima Anandkumar (Caltech / lean-dojo)Lean 4Active. LLM-as-tactic framework: suggest_tactics, search_proof, select_premises. MIT-licensedhttps://github.com/lean-dojo/LeanCopilot
Isabelle/Isar1999Markus Wenzel (TU München)IsabelleVery active. Isabelle2025 released March 2025; Isar is the canonical declarative-proof language for HOL-style provershttps://isabelle.in.tum.de/
Isabelle/ML (tactic layer)Late 1980s (HOL88 era), entrenched in Isabelle from 1986 onwardLawrence Paulson + Isabelle teamIsabelleActive. The Poly/ML-hosted internal layer; raw Tactic.tac, Goal.prove, Method.setup definitions live here. Most users never touch it; tactic authors musthttps://isabelle.in.tum.de/dist/Isabelle2025/doc/implementation.pdf
Sledgehammer (Isabelle)c. 2007Lawrence Paulson, Jasmin Blanchette, Tobias Nipkow et al.IsabelleVery active. Routes goals to E, Vampire, Z3, CVC5, SPASS; reconstructs via Metis or smt; can output Isar text proofs. Documented in the Isabelle2025 manualhttps://isabelle.in.tum.de/website-Isabelle2025/dist/Isabelle2025/doc/sledgehammer.pdf
Mizar1973 (first version), 1989 (modern Mizar)Andrzej Trybulec (Białystok)Mizar (its own system)Active. Mizar 8.1.15, MML 5.94.1493 with 1,493 articles as of May 2025https://mizar.uwb.edu.pl/
ACL2 macros + computed hints1989 (ACL2 1.0); computed hints added in early 2000sRobert Boyer, Matt Kaufmann, J Strother Moore (UT Austin)ACL2Active. ACL2 8.6 released October 2024; “What’s New in ACL2 2025” notes include list$ macro and incremental improvementshttps://www.cs.utexas.edu/users/moore/acl2/
HOL Light tactic combinators (THEN, THENL, ORELSE, REPEAT)1996John Harrison (Cambridge → Intel → Amazon)HOL LightActive. The minimal-LCF style; tiny core, OCaml-hosted; used in Flyspeck (Hales’ Kepler conjecture) and current SPECTRE/Meltdown-era hardware verificationhttps://www.cl.cam.ac.uk/~jrh13/hol-light/
HOL4 tactic language (simpLib, bossLib, Tactical)1990 (HOL90), modernised through HOL4 (2002+)Konrad Slind, Mike Gordon, Michael Norrish et al.HOL4Active. Trindemossen-2 release; ported PAT_CONV/PATH_CONV from HOL Light; HOL4PRS (2024) is an LLM-based proof recommenderhttps://hol-theorem-prover.org/
Metamath proof scripts ($p ... $.)1992Norman MegillMetamathActive. mmj2 v2.5.2 (May 2025); Yamma VS Code extension (Oct 2025); set.mm has 44,000+ theoremshttps://us.metamath.org/
Meta-F* (F* tactics + reflection)2018 (paper at PLDI)Guido Martínez, Nikhil Swamy, Aseem Rastogi, Catalin Hritcu et al. (Microsoft Research)F*Active. Tactics + metaprograms can discharge proof obligations the SMT backend can’t, or normalise them into well-behaved fragmentshttps://fstarlang.github.io/
PVS proof commands ((induct ...), (grind), (skosimp*))1993Sam Owre, Natarajan Shankar, John Rushby (SRI International)PVSActive. PVS 7.1 current as of 2024–2026; S-expression-shaped command language; integrated with Yices/CVC4 decision procedureshttps://pvs.csl.sri.com/
Idris 2 elaborator reflection2017 (paper for Idris 1, by David Christiansen & Edwin Brady), Idris 2 port ongoingDavid Raymond Christiansen, Edwin BradyIdris 2Active. Community library idris2-elab-util (Stefan Höck) is the practical entry pointhttps://github.com/stefan-hoeck/idris2-elab-util
Agda reflection (Term, TC monad, unquote, macro)2014 (Agda 2.4.2)Andreas Abel, Ulf Norell, Andrés Sicard-Ramírez et al.AgdaActive. Documented through Agda 2.9.0; macros + unquoteDecl are the standard tactic mechanism since Agda has no Ltac-style scriptinghttps://agda.readthedocs.io/en/latest/language/reflection.html
Twelf / LF declarations1999Frank Pfenning, Carsten Schürmann (CMU)TwelfLargely retired / specialised. Project explicitly states “not under active development” as of 2024; still used in PL-metatheory teachinghttps://twelf.org/
Cedille2018 (first public release)Aaron Stump et al. (Univ. of Iowa)CedilleResearch-active, niche. Cedille Core formalised; ongoing dependent-type-theory research; no recent stable headline releasehttps://cedille.github.io/
Why3 transformations2010 (Why3) — descended from Why (2003)Jean-Christophe Filliâtre, Andrei Paskevich, François Bobot et al. (INRIA / LRI)Why3Active. Why3 1.8.x current; extensionality transformation added in 2024; supports Coq 8.19/8.20, Z3 4.13, CVC5 1.2, Alt-Ergo 2.6 backendshttps://www.why3.org/
Dafny verification annotations + assertions2008K. Rustan M. Leino (MSR → Amazon → AWS)DafnyVery active. AWS-maintained; annual Dafny workshop at POPL (2024, 2025, 2026); used internally at AWS for cryptographic-protocol verificationhttps://dafny.org/

Notable threads

  • The Ltac1 → Ltac2 migration is a generational debt-collection. Ltac1 (2000) was designed at a time when “tactic language” meant “shell script for the proof state.” It has dynamic scope, pervasive backtracking, no static type-checking of tactic arguments, and silent failure modes where a tactic returns the same goal and you spend an hour figuring out which branch fizzled. Ltac2 (2020) is a typed, OCaml-flavoured language with first-class tactics, exceptions, and proper module-level abstraction. The Coq team’s stated direction is that new tactic libraries should be written in Ltac2, but the Ltac1 codebase in mathcomp, MetaCoq’s own tactic helpers, and most of the Coq Platform packages is enormous and migrates slowly. As of Rocq 9.0 (March 2025), Ltac2 has been promoted from a separate plugin into rocq-core itself, removing the last installation friction. Source: https://rocq-prover.org/releases/9.0.0.

  • Procedural vs. declarative is the deepest cultural split. Procedural tactics (Ltac, Ltac2, HOL Light’s THEN/THENL, ACL2’s macro layer, Lean’s TacticM) execute imperatively against a goal stack — the proof you read is a recipe, often unreadable without running it. Declarative proof languages (Mizar, Isar, Lean’s calc/have, F*‘s ambient assertion style) write proofs as readable mathematical text, with the prover filling in the routine inferential steps. Mizar is the granddaddy (Trybulec, 1973); Wenzel’s 1999 Isar paper translated Mizar’s ideas into the LCF/HOL world without giving up Sledgehammer-style automation, and that combination — declarative skeleton + automated leaves — is now the default house style in Isabelle. Lean 4 splits the difference: by blocks are procedural, calc and have are declarative, and they freely interleave.

  • The Hammer ecosystem reframes “proof automation” as “service routing.” Sledgehammer (Isabelle), CoqHammer, and HOL(y)Hammer all implement the same architecture: relevance-filter the local fact set, translate the goal into untyped first-order logic, ship to multiple external solvers in parallel (E, Vampire, Z3, CVC5, SPASS), wait for the first success, then reconstruct the proof in the host system’s native tactic language so the kernel still checks it. This decouples “expensive search using the world’s best ATPs” from “trusted kernel checking,” letting you exploit decades of SMT/SAT engineering without compromising soundness. CoqHammer’s sauto tactic is the reconstruction half; Sledgehammer outputs an Isar by metis or by smt line. The 2024 Dagstuhl paper on improving the SMT proof-reconstruction pipeline in Isabelle/HOL (https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.26) is the current state-of-the-art reference.

  • Reflective tactics are the type-theory crowd’s answer to safety. When you write a tactic in Ltac, there is no guarantee it produces a well-typed term until you run it on a goal — and even then, it produces a term for the kernel to check, not a verified-correct certificate. Mtac/Mtac2 (Beta Ziliani) and MetaCoq (Sozeau et al.) reify Coq’s term language as a Coq inductive type, so a “tactic” becomes a function M : something → tm that the type-checker certifies before you run it. MetaCoq goes further: it includes a verified type-checker (SafeChecker) and a verified erasure pipeline, so you can build proof-producing plugins whose correctness is itself a Coq theorem. The same pattern recurs in Agda’s reflection layer, Idris 2 elaborator reflection (Christiansen & Brady, ICFP 2016), and Meta-F*. The trade-off is verbosity — reflective tactics are more boilerplate than Ltac1 one-liners — but they remove an entire class of “silently wrong” failure modes.

  • The Lean 4 metalanguage explosion was a deliberate unification move. In Lean 4 (2021), de Moura and Ullrich collapsed three layers — macros, elaboration, and tactics — into a single Lean monad stack: MacroM ⊆ TermElabM ⊆ TacticM, all built on MetaM, all running in CoreM. The same do-notation, the same quote/syntax infrastructure, the same hygiene mechanism. This means a Lean user who can write Lean can write tactics, can write macros, can write elaborator extensions, and can do all three in one definition. The downside is that the metalanguage is Lean — you cannot escape the dependent type system when writing tactics, which is occasionally inconvenient compared to Coq’s ML-hosted plugin authorship. The upside is uniformity: the entirety of the simp configuration syntax, mathlib’s algebraic-tactic DSL, and the calc block are all macros, all hygienic, all type-checked.

  • LLM-assisted tactics are the newest layer, treated as just another solver backend. Lean Copilot (Song, Yang, Anandkumar, 2024; NeuS 2025) is the most prominent example: suggest_tactics, search_proof (combines LLM-generated tactic candidates with aesop’s search), and select_premises (LLM-driven premise retrieval over a fixed mathlib4 snapshot). Reported metrics: requires only 2.08 manually-entered proof steps on average vs aesop’s 3.86; automates 74.2% of proof steps fully vs aesop’s 40.1%. The architectural insight is that the LLM is a noisy, stochastic ATP — but its output is a tactic, which the kernel still checks, so soundness is preserved exactly as with Sledgehammer. The Coq community has analogues (tactician, GPT-f-style work), and DeepSeekMath-V2 (Nov 2025) has shifted the frontier on competition-level autoformalisation.

  • Why theorem provers are mostly written in OCaml/SML/Haskell, and what that imposes. Coq/Rocq, HOL Light, and Why3 are OCaml. HOL4, Isabelle, Twelf, and (historically) PolyML’s HOL88 are Standard ML / Poly/ML. Agda is Haskell. Lean 4 is the outlier — written largely in Lean itself, with a C kernel. ACL2 is Common Lisp. The pattern reflects three things: (1) ML’s algebraic data types and pattern matching are a near-perfect fit for term-language manipulation; (2) the Edinburgh LCF tradition embedded Milner’s ML because it was designed for tactics; (3) garbage collection and good closures are non-negotiable for proof search. The downstream effect is that plugin authors need to be polyglot — to write a serious Coq tactic you need OCaml; for Isabelle you need Poly/ML; the modern exception is Lean 4, where everything is Lean. This is one reason Lean 4 has gained mathematician-mindshare quickly: zero language-context switch.

Citations

  1. Rocq Prover 9.0.0 release notes (March 2025): https://rocq-prover.org/releases/9.0.0
  2. Rocq Platform 2025.01.0 release notes: https://rocq-prover.org/releases/2025.01.0
  3. Ltac2 reference manual (current): https://rocq-prover.org/refman/proof-engine/ltac2.html
  4. Pédrot, “Ltac2 — A Statically Typed Tactic Language” (TYPES 2019): https://dblp.org/rec/conf/types/Pedrot19.html
  5. MetaCoq project page: https://metacoq.github.io/ (Sozeau, Anand, Boulier, Cohen, Forster, Kunze, Malecha, Tabareau, Winterhalter)
  6. Mtac2: Typed Tactics for Backward Reasoning in Coq (ICFP 2018): https://iris-project.org/pdfs/2018-icfp-mtac2-final.pdf
  7. Coq-Elpi tutorial: https://lpcic.github.io/coq-elpi/tutorial_elpi_lang.html
  8. Hierarchy Builder (Cohen, Sakaguchi, Tassi, FSCD 2020): https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.34
  9. CoqHammer documentation and 1.3.2 release: https://coqhammer.github.io/ ; releases https://github.com/lukaszcz/coqhammer/releases
  10. Wenzel, “Isar — A Generic Interpretative Approach to Readable Formal Proof Documents” (TPHOLs 1999): https://www21.in.tum.de/~wenzelm/papers/isar-tphols99.pdf
  11. Isabelle2025 release (March 2025): https://isabelle.in.tum.de/website-Isabelle2025/index.html
  12. Sledgehammer documentation, Isabelle2025 edition: https://isabelle.in.tum.de/website-Isabelle2025/dist/Isabelle2025/doc/sledgehammer.pdf
  13. Improving the SMT Proof Reconstruction Pipeline in Isabelle/HOL (ITP 2025): https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.26
  14. Lean 4 Metaprogramming Book: https://leanprover-community.github.io/lean4-metaprogramming-book/
  15. Lean 4 macro overview: https://leanprover.github.io/lean4/doc/macro_overview.html
  16. Lean 4.25.0 release notes (November 2025) — grind interactive mode: https://lean-lang.org/doc/reference/latest/releases/v4.25.0/
  17. Aesop: White-Box Best-First Proof Search for Lean (CPP 2023): https://dl.acm.org/doi/10.1145/3573105.3575671
  18. Lean Copilot paper (Song, Yang, Anandkumar): https://arxiv.org/abs/2404.12534 ; repo https://github.com/lean-dojo/LeanCopilot
  19. Mizar Mathematical Library (current MML 5.94.1493, May 2025): https://mizar.uwb.edu.pl/library/
  20. ACL2 — What’s New in ACL2 2025: https://www.cs.utexas.edu/~moore/acl2/manuals/current/manual/index-seo.php?xkey=ACL2____WHATS-NEW-IN-ACL2-2025
  21. HOL Light: https://www.cl.cam.ac.uk/~jrh13/hol-light/
  22. HOL4 releases: https://github.com/HOL-Theorem-Prover/HOL/releases ; HOL4 interaction guide (Feb 2025): https://hol-theorem-prover.org/HOL-interaction.pdf
  23. Metamath home: https://us.metamath.org/ ; mmj2: https://github.com/digama0/mmj2
  24. Meta-F*: Proof Automation with SMT, Tactics, and Metaprograms (PLDI 2019, Martínez et al.): https://arxiv.org/abs/1803.06547
  25. PVS 7.1 (current, SRI): https://pvs.csl.sri.com/ ; Prover Guide v7.1 (Aug 2020): https://pvs.csl.sri.com/doc/pvs-prover-guide.pdf
  26. Christiansen & Brady, “Elaborator Reflection: Extending Idris in Idris” (ICFP 2016): https://www.type-driven.org.uk/edwinb/papers/elab-reflection.pdf ; Idris 2 utilities https://github.com/stefan-hoeck/idris2-elab-util
  27. Agda reflection reference (current docs): https://agda.readthedocs.io/en/latest/language/reflection.html
  28. Twelf project home and contributing notes (“not under active development”): https://twelf.org/contributing/
  29. Cedille project: https://cedille.github.io/
  30. Why3 1.8.x release notes: https://www.why3.org/doc/changes.html
  31. Dafny releases: https://github.com/dafny-lang/dafny/releases ; POPL Dafny workshops (2024, 2025, 2026): https://popl26.sigplan.org/home/dafny-2026

Caveats

  • Cedille: I could not find a clear-cut “current stable release” date. Published research continues (Aaron Stump’s group, dependent-type-theory work in 2024) but the project is research-active rather than productised; treat the “Status (2026)” entry as best-effort.
  • Twelf: Project explicitly states it is not under active development as of 2024 (https://twelf.org/contributing/), so the table flags it as “largely retired / specialised.” Binary distributions are from 2011; source builds still work.
  • Lean Copilot vs other LLM-assisted tactics: The metrics quoted (74.2% automation, 2.08 manual steps) are from the published paper on a fixed mathlib4 snapshot — generalisation to current mathlib4 (always larger) is not guaranteed. Treat as a published benchmark, not a 2026 production claim.
  • Mtac vs Mtac2: The active line is Mtac2 (ICFP 2018, available as coq-mtac2 on opam). The original Mtac (2013) is historical; I treated them as a single row to keep the table compact.
  • Agda reflection vs Idris 2 elaborator reflection vs Meta-F*: All three are reflective metaprogramming layers and could each fill a longer note; this index gives one row each. The Idris 2 row leans on the community library idris2-elab-util because the in-tree Idris 2 reflection docs are sparser than Agda’s.
  • “Theorem-prover DSLs” boundary: I deliberately included Why3 transformations and Dafny annotations even though those provers are SMT-driven rather than tactic-driven, because their annotation/transformation languages play the same DSL-on-top-of-host role. I excluded TLA+ (model-checker, in notation-spec), Alloy, and Z — those are specification languages without a tactic layer.

Graph View