Compendium

Notation / Specification / Verification Languages Family Index

8 min read

Notation / Specification / Verification Languages Family Index

type: language-family-index family: notation-spec languages_catalogued: 19 tags: [language-reference, family-index, formal-methods, verification, specification, model-checking]

Notation / Specification / Verification Languages — Family Index

Family overview

Formal methods languages span a spectrum from describing what a system should do to proving it does. At one end are specification languages — Z, B, VDM, TLA+ — which give mathematicians and engineers a precise vocabulary for stating system properties (state, invariants, refinement) without necessarily mechanically discharging proofs. In the middle sit model checkers like Alloy (relational, bounded) and SPIN/Promela (explicit-state, LTL properties), which exhaustively explore finite or finitized state spaces. Further along are first-order/higher-order theorem provers — ACL2 (computational Lisp), Isabelle/HOL (HOL with Sledgehammer), Coq/Rocq, Lean, Agda, Idris — that mechanize full proofs over rich logics. Deductive verification platforms (Why3, Dafny, F*, Spec#, SAW) bridge programs and proofs: you write code with annotations and a VC-generator + SMT backend (or proof obligation script) discharges the obligations.

The cultural divide is between “describe what’s true” (Z, TLA+, Alloy) and “prove it’s true mechanically” (Isabelle, Coq, Lean). TLA+ famously lets you specify a distributed protocol and model-check it without writing proofs, while seL4 was proved line-by-line in Isabelle/HOL — over 200,000 lines of proof for ~10,000 lines of C. Choosing between them is largely a question of how much rigor you can afford and how subtle your bugs are.

Industry adoption has accelerated since the mid-2010s. Amazon’s “How Amazon Web Services Uses Formal Methods” (Newcombe et al., CACM 2015) made TLA+ a household name in distributed-systems engineering — DynamoDB, S3, EBS, and IAM all have TLA+ specs. Microsoft Azure Cosmos DB published TLA+ specs of its consistency levels. MongoDB used TLA+ for replication protocol redesign. Confluent verified parts of Kafka’s KRaft consensus in TLA+. AMD’s Athlon FPU was verified in ACL2; Intel uses ACL2 and HOL Light for arithmetic circuits. Blockchain stacks pushed Lean (Aleo), F* (Tezos, Cardano contracts), and the K Framework (Ethereum’s KEVM, WebAssembly’s KWasm) into production. As of 2026, formal methods are no longer purely academic — they’re a normal (if specialized) part of high-assurance and infrastructure software.

In our deep library

Several dependent-typed proof assistants in this family already have dedicated deep notes — cross-reference rather than re-catalog:

  • coq (now Rocq — renamed from “Coq” to “Rocq” in 2025)
  • lean (Lean 4; mathlib4)
  • agda
  • idris (Idris 2)

Adjacent families:

  • logic-and-constraint — Datalog, Prolog, miniKanren, ASP, SMT-LIB. Logic programming and constraint solving sit next door to theorem proving; SMT solvers (Z3, CVC5) are the workhorse backend for Dafny/Why3/F*.

This index focuses on specification + lightweight verification (TLA+, Alloy, Z, B, VDM) and first-order or HOL-based theorem proving (ACL2, Isabelle/HOL, Why3) — i.e., the formal-methods world outside the dependent-types axis already covered by the deep notes.

Tier 3 family table

LanguageFirst appearedOriginSpecialtyStatus (2026)URL
TLA+1999Leslie Lamport (DEC SRC, Microsoft Research)Specification + model checking of concurrent/distributed systems; TLC + TLAPSActive; industry-standard for distributed protocols (AWS, Azure, MongoDB)https://lamport.azurewebsites.net/tla/tla.html
PlusCal2009Leslie LamportPseudo-code front-end that compiles to TLA+; lower learning curveActive; bundled with TLA+ Toolbox / VS Code extensionhttps://lamport.azurewebsites.net/tla/pluscal.html
Alloy2002Daniel Jackson (MIT)Lightweight relational specification + bounded model checking via SATActive; Alloy 6 added mutable state and temporal logic (2021)https://alloytools.org/
Z notation1977Jean-Raymond Abrial (Oxford PRG)Set-theoretic specification with schemas; ISO/IEC 13568:2002Legacy; still taught and used in safety-critical (railway, avionics)https://en.wikipedia.org/wiki/Z_notation
B method1996Jean-Raymond AbrialRefinement-based specification + code generation; Atelier B / B-ToolkitActive in rail signaling (Paris Métro line 14, RATP, Alstom); maintenance mode otherwisehttps://www.atelierb.eu/en/
Event-B2005Jean-Raymond AbrialSuccessor to B; event-driven, refinement-centric; Rodin platformActive in academia and rail; ETCS / SIL-4 specshttps://www.event-b.org/
VDM-SL / VDM++1973 (VDM); 1996 (VDM++)IBM Vienna Lab (Bjørner, Jones)Vienna Development Method; ISO-standardized; Overture ToolNiche; used in some aerospace and Japanese industry; Overture maintainedhttps://www.vdmtools.jp/en/
Promela1989Gerard Holzmann (Bell Labs)Process specification for the SPIN explicit-state model checker; LTL propertiesActive; SPIN still maintained, used in NASA JPL flight software (Cassini, Curiosity)https://spinroot.com/
Isabelle/HOL1986 (Isabelle); 1989 (HOL instance)Larry Paulson (Cambridge), Tobias Nipkow (TUM)Generic interactive theorem prover; HOL is the dominant logic; Sledgehammer SMT integrationVery active; Archive of Formal Proofs >800 entries; seL4 verified in Isabelle/HOLhttps://isabelle.in.tum.de/
ACL21989Boyer, Moore, Kaufmann (UT Austin)Computational first-order logic over Common Lisp; industrial hardware verificationActive; AMD, Centaur, Intel use it; ACL2s and ACL2(p) variantshttps://www.cs.utexas.edu/users/moore/acl2/
Why32010Inria Saclay (Filliâtre, Paskevich)Deductive verification platform; WhyML language; multi-prover backend (Z3, Alt-Ergo, CVC5, Coq)Active; backend for Frama-C/WP, SPARK 2014, Cameleerhttps://www.why3.org/
Cryptol2003Galois Inc.DSL for specifying cryptographic algorithms; SAT/SMT-backed equivalence checkingActive; used by NSA, AWS s2n-bignum, NIST PQC submissionshttps://cryptol.net/
Maude1999SRI International (Meseguer, Clavel)Rewriting logic + reflection; LTL model checker; Full Maude metalanguageActive; used for protocol/security analysis (Maude-NPA), language semanticshttps://maude.cs.illinois.edu/
K Framework2003Roșu et al. (UIUC)Executable formal semantics framework; derives interpreter, deductive verifier, model checker from one definitionActive; KEVM (Ethereum), KWasm, KLLVM, KMIR (Rust); Runtime Verification Inc.https://kframework.org/
Imandra Protocol Language (IPL)2014Aesthetic Integration / Imandra Inc.Formal verification of financial protocols; OCaml-like surface; cloud reasoning engineActive; FIX/FpML protocol verification; AI reasoning platform pivot underwayhttps://www.imandra.ai/
Spec#2004Microsoft Research (Barnett, Leino, Schulte)C#-with-contracts; Boogie + Z3 backend; precursor to Code Contracts and DafnyDiscontinued (~2014); historically important; lessons live on in Dafnyhttps://www.microsoft.com/en-us/research/project/spec/
Dafny2009Rustan Leino (Microsoft Research, then Amazon)Imperative/OO language with built-in pre/post conditions and proofs; Boogie/Z3 backend; compiles to C#/Java/Go/Python/RustActive; AWS Cedar policy language verified in Dafny; Amazon-led since 2022https://dafny.org/
F*2011Microsoft Research INRIA (Swamy et al.)Dependently-typed ML for program verification; SMT-augmented type checking; extracts to OCaml/F#/C/WASMActive; Project Everest (HACL*, EverCrypt, miTLS); Tezos and Cardano smart contractshttps://www.fstar-lang.org/
SAW (Software Analysis Workbench)2014Galois Inc.Symbolic-execution + SMT verification of C/Java/x86/LLVM against Cryptol specsActive; used to verify AWS s2n HMAC, BLST signatures, BoringSSL constant-timehttps://saw.galois.com/
Ivy2016Padon, Shoham, Sagiv (Tel Aviv U.) + Microsoft ResearchDecidable fragments via EPR; inductive-invariant inference for distributed protocolsActive in research; Paxos, Raft, distributed consensus case studieshttps://kenmcmil.github.io/ivy/

Notable threads

  • TLA+ in distributed systems industry adoption. Newcombe et al.’s “How Amazon Web Services Uses Formal Methods” (CACM 2015) is the watershed paper — DynamoDB, S3, EBS specs caught design bugs that years of testing had missed. MongoDB used TLA+ when redesigning replication; Microsoft Azure Cosmos DB has public TLA+ specs of all five consistency levels; Confluent verified Kafka’s KRaft consensus protocol; CockroachDB and TiDB both run TLA+ models internally. PlusCal lowers the activation energy by giving engineers a procedural front-end. The TLA+ community is small but unusually senior — it skews toward principal-engineer-grade infrastructure work.

  • Alloy as the lightweight formal-methods entry point. Daniel Jackson’s Software Abstractions (2006/2012) repositioned formal modeling as a sketching activity rather than a proof discipline. Alloy 6 (2021) added mutable state and a temporal logic that let it model dynamic systems formerly the province of TLA+. It remains the most-taught formal-modeling language in undergraduate software-engineering programs because the SAT-backed analyzer gives instant feedback. Use Alloy when you want to find counterexamples in hours, TLA+ when you want to specify a multi-year-investment protocol.

  • ACL2 and the Boyer-Moore lineage in hardware verification. Boyer-Moore’s “A Computational Logic” (1979) and its successors (Nqthm, ACL2) underlie the largest body of mechanized hardware proofs in industry. AMD verified the Athlon and K7 floating-point divider in ACL2 after the Pentium FDIV scandal. Centaur Technology (now part of VIA) verified its x86 microarchitecture in ACL2. Intel uses ACL2 and HOL Light for arithmetic-unit verification. The 2005 ACM Software System Award to Boyer/Kaufmann/Moore recognized this. ACL2 is unfashionable next to dependently-typed provers but produces more line-of-production-silicon proofs than any of them.

  • *The Dafny / Why3 / F deductive-verification overlap.All three follow the same pipeline: annotate code with pre/post/invariants, generate verification conditions, dispatch them to SMT solvers (Z3 dominates). Differences: Dafny is OO and aims for “formal methods you can teach to interns” (AWS Cedar, encryption SDK); Why3 is a multi-prover meta-platform with a small WhyML core that compiles other front-ends (Frama-C/WP, SPARK 2014, Cameleer for OCaml) onto it; F is dependently-typed and supports effects, used in Project Everest’s HTTPS stack (HACL, EverCrypt, miTLS) and in blockchain VMs. F*-extracted C is shipping in Mozilla NSS, Linux kernel crypto, and WireGuard-Go. Microsoft Research’s old Spec# is the common ancestor; Boogie + Z3 the common backend.

  • K Framework and executable language semantics. K turns the dream of “define a language once, get an interpreter, debugger, model checker, and verifier for free” into something real. KEVM is the formal semantics of the Ethereum Virtual Machine, used by Runtime Verification Inc. for smart-contract audits (Uniswap, MakerDAO). KWasm formalizes WebAssembly. KLLVM provides verified-from-semantics LLVM IR execution; KMIR is the Rust MIR semantics (work in progress). The contrast with Maude is illuminating — both are rewriting-logic frameworks, but K invests in executability and verification tooling for production-language semantics rather than meta-language exploration.

  • The Isabelle/HOL ecosystem and the Archive of Formal Proofs. Isabelle/HOL is the largest single body of mechanized mathematics and software verification outside Lean’s mathlib. The Archive of Formal Proofs (afp.theoremproving.org / isa-afp.org) has crossed 800 entries and includes seL4 (the verified microkernel), the CakeML verified ML compiler, IsaFoR/CeTA term-rewriting, and large chunks of analysis and algebra. Sledgehammer’s integration with SMT/ATP solvers (Z3, CVC5, E, Vampire) made HOL proofs dramatically more tractable around 2010 and is still the gold-standard “hammer” experience that other provers (Lean, Coq) emulate. seL4’s general-availability under MIT license (2014) and the formal-proof corpus around it remain the high-water mark of OS-level formal verification.

Citations

Graph View