AI is making it cheap to write code and proofs; formal methods make it possible to trust them. The intersection is where verifiable, safety-critical systems get built — and it's badly under-coordinated. FMxAI brings the two communities into one room to scope what to build next.
An invitation-only gathering of FM researchers, frontier AI labs, government research staff, startup founders, and funders — built for shared problem-scoping, not paper presentations. Organized by Atlas Computing.
The usable formal methods hackathon: build a piece of real-world production software, and formally verify it. Competitors, experts and sponsors welcome.
Sign up for Vibecheck →There's no event page yet. Want to express interest in attending? Email fmxai@atlascomputing.org.
~80 people, two and a half days of shared problem-scoping at SRI. Speakers, agenda, and venue.
View the 2026 conference →The inaugural edition — 50+ invited attendees. Recap, speakers, and outcomes.
View the 2025 recap →The precursor gathering that started the series.
Visit the 2024 site ↗The Secure Program Synthesis Fellowship, run with Apart Research, supports work on trustworthy AI-generated code.
Learn about the fellowship ↗