Formal Verification and AI Research Lead
Atlas Computing
📍 Remote (Global) 🕔 Full Time
💰$150-200K USD 🔄 Rolling Applications
Advancements in AI bring both opportunities and serious risks, which simultaneously enable and necessitate more powerful approaches to high-assurance systems. Atlas Computing is a nonprofit working to ensure robust democratic oversight and control of critical infrastructure and AI. We are building an ecosystem for AI systems with provable properties.
Building an ecosystem is a massive group effort: we work with the formal methods, AI, cyber, and biosecurity communities across academia, government, and industry. We contribute through both technical work (targeted research, product development, technology transfer) and community organizing (education, government outreach, conferences, coordinating funding, incubating startups).
We believe that machine learning capabilities will continue to grow rapidly and should be directed at advancing formal verication. Atlas Computing is hiring a researcher with expertise at the intersection of formal verication and machine learning to show the world that machine learning can dramatically accelerate formal verication in software engineering. This work will involve rapid prototyping of new capabilities, influencing stakeholders in the relevant research fields, and supporting the transfer of research into practical use.
As the FV+AI Research Lead, success in the first year looks like:
(In order of priority from highest to lowest)
You’ve advanced the state-of-the-art in using machine learning to accelerate formal verification at scale
You’ve already worked with our software lead to integrate one of these into a useful tool.
You’ve established collaborations with leading researchers in AI and formal methods through multiple research projects that pursue safety at scale through formal verication
Your technical insights and results have played a key role in Atlas’s inuence on high-impact decision-makers outside the organization (for instance, policymakers or regulators)
Perhaps you’ve identified an amazing hire for Product Lead (if we haven’t hired one already)
You may be a fit for this role if you have…
a PhD (or equivalent experience) and have published research using ML for formal methods in peer reviewed journals
a track record of sourcing your own research mentors and collaborators
comfort picking research directions that bet that capabilities of frontier models continue to grow
a practice of reviewing the state-of-the-art after having an idea, coupled with an urge to prototype, test, and iterate
a founder mindset, with a high degree of ownership over outcomes and the ability to personally make and externally drive progress with little oversight
experience coordinating and aligning groups to work toward a common goal
an ability to think across disciplines and research-development timescales
strong analytical, problem solving, and communication skills
interest in shaping our culture, as we’re still a very small organization
Bonus points if you have…
fluency with Lean or Coq
expertise managing high-performance machine learning compute
experience with high assurance engineering in real-world systems
experience building and applying ML models to solve complex problems
expertise in cybersecurity
familiarity with SCADA systems
experience shaping the research agendas of science funders
seriously considered starting your own company, but the opportunity or push hasn’t come up yet
experience managing research consortia and knowledge of how research labs are run and funded
been the person in the conversation who is always recommending books
a deep commitment to improving the human condition with technology… and understanding how different people might differently define “improving”, “human”, “condition”, and “technology” in that phrase
Here’s a supplemental living document if you have more questions.
How to Apply
Please email a short joke and a resume to join@atlascomputing.org. No need to include a cover letter. You can add a paragraph or two in case you want to highlight anything that you think will convince us to have a first chat with you, but don't worry about being formal. We’re serious about the joke! It’s good spam prevention.
