Apr-May 2026 AI Security via Formal Methods

There’s been some talk about how I’m not doing the best possible job with the newsletter and there’s room for competition, or, if we’re feeling frisky, a coup. If you’d like to volunteer, let me know how I can help! I mentioned last edition that I don’t see myself being the secure program synthesis newsletter, that I’ll want to focus on applications of SPS to AI security. But it’d be great for someone to own “SPS the newsletter” as a parallel effort to this newsletter.Getting this out quickly so you read it before the hackathon, not covering any research, sorry. Just happenings/opportunities in the movement.Secure Program Synthesis Hackathon NOWSee the talk schedule/recordings for some excellent content. This weekend, talks last night (recording available), today, and tomorrow. The tracks are spec elicitation and validation, spec-driven development in general, and advro for proofstacks (like interactive theorem provers).Secure Program Synthesis Fellowship: participant application deadline May 31stSame tracks as above. 14 mentors/streams. Apply to a team!Midspiral, Sequent, and Sigil Logic have logged onNew companies! Exciting!Midspiral is tackling webdev via formal methods, apply to join their discord community here.Sequent has someone with old school AI xrisk credentials involved.Sigil Logic is hiring (see the hackathon talk schedule above to understand more about Joe’s worldview).The Revenge of Safeguarded AI: new TA2 funding call on cyberhardeningProgramme thesis document v2.0. Funding call deadline July 1st. I plan to spend more time with this and discuss it more in the next edition of the newsletter. Sorry I’m rushing today.Hardware for AI security residencyThere is an emerging field of AI security known as “AI verification”, and they don’t mean it in the sense of formal verification, though our sense of the word emerges sometimes (and they explicitly want FM people to apply).Discuss