Better tools forformal specifications

Formal methods allow you to prove that your software has specific properties, but those properties must be written as a formal specification: mathematically precise statements of the properties. Late 2025, there were multiple AI-first formal methods startups, but Atlas Computing noticed there were no active efforts to make it easier to generate and understand the specifications themselves. Specification validation is the means, not the end: proofs only support scalable oversight if humans can trust that the specification says what they intended.

Mike Dodds Mike Dodds Oath Technologies LinkedIn , PhD, was a Principal Scientist at Galois gaining notoriety as a forward-thinking formal methods expert from his writing about the impact of near-term AI capabilities on the practice of provable software security (e.g. here and here).

Atlas Computing, having also written and presented on this topic (e.g. here and here), convinced Mike that there was a critical need for tools that help humans and AI agents validate that formal specifications say what the human intended. Mike saw the larger opportunity and expanded the scope: processes and scaffolds for humans to generate specifications that orchestrate AI behavior and outputs more generally — scalable oversight via formal specifications. In conversation with Mike, the team determined that this work should be done as a nonprofit Focused Research Organization (FRO), introduced him to Convergent Research (which originally proposed FROs and houses 8), and supported him in scoping an application for funding. Convergent has started more than 10 FROs.