This work was done at Atlas Computing, Atlas Ignota’s predecessor organization.
Formal methods is the use of mathematical proofs to guarantee that software cannot fail in certain ways, which is critical for software security. In mid-2024, there were a few teams using AI and formal methods tools to automate math proofs. Meanwhile, formal methods experts were skeptical machine learning systems could revolutionize formal methods, instead focusing on using language models as narrow tools to support humans or symbolic reasoning systems.
Jason Gross 
Jason Gross Theorem Labs LinkedIn , PhD, was researching whether one could prove safety properties of neural networks with MIRI. He was well aware of AI capability forecasts, and had a strong background in autoformalization: his PhD included leading engineering on a project that automatically generated formally verified cryptography libraries that were included in deployments for Chrome, Android, and Cloudflare.
The team sourced funding and worked with Jason for a few months of prototyping and experiments with AI models on autoformalization.
When Jason decided that the time was right and this work would scale better as a for-profit, Atlas Computing open-sourced all his experiments, described the work in a blogpost, and he resigned on a Thursday to incorporate Theorem Labs that Friday and get his first check that Monday.
As the first company to take an AI-first approach to formal methods for cybersecurity, Theorem Labs joined the Spring 2025 batch of the prestigious incubator Y Combinator. They have worked with the Advanced Research and Inventions Agency (ARIA) in the UK, and repeatedly pushed the boundary of what security and functionality guarantees AI models can make for software.
