WASHINGTON, D.C. – Atalanta, a mathematical AI company, recently emerged from stealth mode to deliver on a bold vision to bring provably correct decision-making to the world’s most important missions. Founded by Anjana Rajan and Jonathan Ring, and comprising a team of engineers, mathematicians, designers, and strategists, Atalanta serves customers building complex systems across energy, space, and defense.
Autonomous systems are now making consequential decisions across national security and critical infrastructure. As capabilities advance and complexity in networked sensors and workloads increases, the ability and the tools to prove they will perform correctly under real-world conditions has not kept pace. Traditional testing can show how a system performs in known scenarios, but it cannot exhaustively explore all possible behaviors. Mathematical techniques, called formal methods, go further by systematically checking every possible state a system can reach, and reasoning about entire classes of inputs rather than individual test cases. However, these methods have historically been too slow and too specialized to deploy at the speed that modern missions demand. The result is a widening gap between the increasing amount of software powering these systems and the degree to which that software’s performance is truly understood.
To close that gap, Atalanta built its flagship product, Argo. The platform delivers the guarantees of mathematical proof in a dynamic and agile way, even as real-world conditions change. Combining AI, formal methods, and digital engineering, Argo embeds proof directly into high-impact workflows while maintaining operational speed.
“For decades, advanced mathematical techniques, like formal methods, have been limited to a small group of highly skilled experts,” said Anjana Rajan, CEO of Atalanta. “Argo unleashes the power of the proof to a wider range of stakeholders across design, development, and deployment. We’re enabling the people responsible for making critical decisions to move faster with assurance. This ultimately saves time, money, and lives.”
The applicability of formal methods in high-consequence systems is already being put into practice. Today, Atalanta and Idaho National Laboratory announced their partnership which supports the aims of the Genesis Mission, a national initiative led by the White House and the Department of Energy to build the world’s most powerful scientific platform to accelerate discovery science, strengthen national security, and drive energy innovation. Argo is being deployed in service to Prometheus, an initiative that addresses two critical priorities for nuclear energy: harnessing artificial intelligence to accelerate new power plant deployment to meet surging electricity demand; and reducing the operational costs of nuclear energy to power the economy of the next century.
“In order to deliver nuclear energy that is faster, safer, and cheaper, mathematical guarantees from formal methods must be part of the equation,” said Greg Shannon, Chief Cybersecurity Scientist for National and Homeland Security at Idaho National Laboratory. “We are proud to establish this public-private partnership with Atalanta on Prometheus.”
The demand for mathematical proof in mission-critical systems continues to grow across the government. Congress recently recognized that formal methods can be used to secure software and hardware systems and prove the absence of exploitable vulnerabilities, and directed the Pentagon to develop a comprehensive strategy for transitioning formal methods into production environments at scale. “The government’s development of a formal methods transition strategy is a clear signal that we are at an inflection point,” said Rajan. “Atalanta is ready to meet this moment.”
