Formal methods practitioners
Who are the known names in formal methods? Who makes a living from it, and which skills do they sell? Below are the firms and people who do this work, and the communities where the experts talk.
People
Section titled “People”| Person | What they do | Note |
|---|---|---|
| Kyle Kingsbury (Jepsen) | Paid safety analyses of distributed databases | 13+ years, built purely on reputation from published findings. |
| Hillel Wayne | TLA+/Alloy consulting, workshops, retainers | Dominant named brand; clients incl. Netflix, NASA, Meta. |
| Nicolas Dubien (fast-check) | Property-testing library, TypeScript/JavaScript | 139M downloads/month — proof OSS distribution works in this ecosystem. |
| Josh Field (stateproof) | TypeScript DSL compiling to TLA+, runs TLC | The closest TS-to-TLA+ tool found. |
| Jonathan Nadal (Stateright) | Embedded model checker as a Rust library | Model checker as a library, the Rust counterpart of the TS ones. |
| Jack Vanlightly | Public technical writing on distributed systems + formal verification | Builds credibility via writing rather than a direct consulting offer. |
| JP Kadarkarai (FizzBee) | Open-source, more approachable alternative to TLA+ | Tool/OSS project, not an active paid practice. |
| Jean-Jacques Dubray (Polygraph) | An LLM writes a JavaScript spec in SAM, his State-Action-Model pattern, which is then checked against the code | Builds it as Cognitive Fab LLC; method from his July 2026 paper. |
| David R. MacIver (Hegel) | Hypothesis-style property-based testing, including for TypeScript | Created Hypothesis. |
| Liam DeVoe (Hegel) | Co-builds Hegel | Hypothesis maintainer at Antithesis. |
| Sandro Maglione (effect-machine) | Schema-first statecharts for Effect, with state exploration in tests | Writes and teaches about Effect, as Typeonce. |
| Nada Amin (LemmaScript) | Proves TypeScript functions correct with Dafny or Lean | Associate professor of computer science at Harvard; builds it with Midspiral. |
| Doniyor Botirov (pnueli) | Explicit-state model checker in TypeScript | Founder of dbit.one; also builds unflake, bulwark and adya. |
| Anders Hessellund Jensen (stifinder) | State-space explorer for JavaScript | Self-employed developer in Denmark; also valsem and kilde. |
| kingbootoshi (tla-precheck) | Compiles a TypeScript DSL to TLA+ and proves both match | Solo project, no commits since early April 2026. |
| Dennis Berger (libpetri) | Runs async code written as a graph of steps (a Petri net), and checks it for leaks and waits that never end; TypeScript, Java and Rust | Staff engineer at Otto; it runs their production commerce assistant. Also builds opt-in add-ons that run n8n and Google ADK workflows on a net. |
| Oleksandr Zalizniak (SpecCraft TS) | Model checker as a TypeScript library | Author of this site; started September 2026. |
| Leslie Lamport (TLA+) | Created TLA+ | Also teaches it in the TLA+ Video Course. |
| K. Rustan M. Leino (Dafny) | Created Dafny | Wrote the book Program Proofs. |
Communities
Section titled “Communities”| Community | Status |
|---|---|
| Lean Zulip | Most active community found — hundreds of participants, 12,800+ topics in the new-members stream alone. |
| TLA+ Google Group | 1,679 threads, genuinely active (most recent thread 2 days before this was checked). |
| Rocq (Coq) Zulip | Official current channel, replaced the Coq-Club mailing list after its Oct 2025 shutdown. |
| Isabelle-users mailing list | Old mailing-list format, mirrored to Zulip, active with same-day posts. |
| r/tlaplus | Real per TLA+‘s own community page; unverifiable firsthand since Reddit blocks automated checks. |
| TLA+ Community Event | Real, recurring annual event co-located with ETAPS (2024-2026 confirmed). |
| Rocq Discourse | Active secondary forum, 551 topics in its main category. |
| Jepsen mailing lists | Real but thin — only 33 threads since 2019. |
| dist-sys Slack | 5,201 members, but general distributed-systems chat, not formal-methods-specific. |
| r/formalmethods | Could not confirm this subreddit exists as a real, active community. |
| DeepSpec | Dormant — its workshop series ended in 2019. |
| comp.specification.z / Z FORUM | Real once, dead now. |
| Antithesis / DST Discord | No dedicated community found; discussion happens on vendor blogs instead. |
| Firm | What they do | Note |
|---|---|---|
| Lean FRO | Nonprofit steward of Lean itself | Funded partly by “the single largest donation in the FRO’s history,” from AWS. |
| Axiom Math | ”Verified AI,” Lean-based | $200-300M raised; 98.93% on a Lean verification benchmark. |
| Pramaana Labs | Formalizes human knowledge (tax/legal/clinical rules) into Lean | $27M from Khosla Ventures, founded 2025. |
| Math, Inc. / Cajal | AI applied to formal verification of math/science problems | Both real, funded, same Lean-AI cluster as Axiom. |
| Certora | Smart-contract formal verification | $100B+ in DeFi value locked protected (MakerDAO, Lido, Coinbase). |
| CertiK | Formal verification + security audits, Web3 | $544B market cap assessed, 117,000+ vulnerabilities found. |
| Hashlock | Smart-contract auditing, incl. formal verification | Smaller regional comparable to Certora/CertiK. |
| Runtime Verification Inc | General formal-methods consulting, built on the K framework | Closest firm to a general formal-methods-as-a-service model. |
| Antithesis | Deterministic simulation testing | Clients: Jane Street, etcd, Ethereum Foundation. |
| QuviQ | Property-based testing as a commercial service | Running since the mid-2000s — the longest commercial precedent found. |
| Galois | Formal methods R&D for defense/government | DARPA, NASA, NIST, US DoD, AWS. |
| Axiomise | Hardware/RISC-V formal verification training | Solo-founder-grown-into-firm path. |
| Informal Systems | Builds and stewards Quint (TLA+‘s executable-spec successor) | Fintech/crypto product focus. |
| Stately | Builds XState and its graph tools (XState) | The company of David Khourshid. |
| Midspiral | Builds LemmaScript, which proves TypeScript functions with Dafny or Lean (LemmaScript) | Almost all commits by Nada Amin. |