June-July 2026 AI Security via Formal Methods
AGI companies want to hire formal methods talent for security moonshots. My new position paper.
Last month, I said I would do a bigger writeup of Nora’s funding call. I did not. But she is hiring currently, and I want you to take a look at the job posting.
I’m hiring someone to help me drive our upcoming £20m AI/FM/cybersec funding call: https://aria.pinpointhq.com/postings/f1288172-37fe-4da5-96ed-de7e719d65e8
This person will work closely with the funded teams, help drive the sprint cadence, sharpen our perspective on targets/threat models/security specs, and pave the way towards high-impact demonstration and translation!
I’m no longer going to try to do the kind of newsletter that claims to attempt completeness over the happenings that fall in its jurisdiction. Instead, I’ll just poke you guys with whatever I happened to catch wind of in the day-to-day carrying out my duties, responsibilities, and third synonyms.
Tractable Problems in AI Security via Formal Methods
Typically when someone writes a position paper about formal methods as an AI safety technology, they’re very bombastic about it. So a bunch of us got together and decided we’d make a new position paper, one that is minimal and uncontroversial instead of maximal and scifi. We focus mostly on model weight confidentiality and integrity through infrastructure hardening. Each problem has a solution sketch
Still welcoming contributions. There’s also native comments on the website. You can have a pdf if you want, but the website is the first-class usecase.
Please get me invited onto podcasts to talk about this.
Anthropic’s Security Labs is hiring
They don’t literally say it in the job description, but I have it on good authority that this JD is super FM pilled. There may be more explicit JDs in the future. This was roughly telegraphed months ago by “leveling up across the board” section of the frontier roadmap, though again no literal name-drop of FM.
OpenAI’s “Preparedness” team is starting to get FM-pilled
This is, as far as you’re concerned, a glorified rumor (I have less confidence in it panning out than the Anthropic case). But I have it on good authority that Preparedness (prepared for what, exactly?) would like to get FM pilled, has gestured in the direction of adding FM talent for security moonshots. You’ll have to email me for the warm intro on this one.
I think it’s absurd/obscene that they’re racing to recursive self improvement btw.
They’re gonna do it cuz of the incentive prisons they built for themselves, it seems right to help them lock down their infra with FM. But I want it on the record that I think the whole thing is somewhere between silly and barbaric.
Gwern’s Lean post
Gwern’s Scaling Hypothesis is one of the most influential documents in 21st century science communication. He wants you to think through a SWE version of scaling laws via Lean. I haven’t read this yet, so no commentary.