Can We Secure AI With Formal Methods?

Can We Secure AI With Formal Methods? is an independent newsletter launched in July 2024 by Quinn Dougherty, a software engineer and AI safety researcher based in Berkeley, CA. The newsletter was originally titled Progress in Guaranteed Safe AI, reflecting its roots in the guaranteed-safe AI (GSAI) research agenda as described in a 2024 position paper (arxiv.org/abs/2405.06624). In late 2025 it was rebranded under its current name to reflect a broader strategic pivot toward emphasizing practical, incremental work rather than theoretical absolute guarantees. The newsletter's core mission is to bridge two communities: formal methods researchers who build verification and proof tools, and AI security practitioners who need those tools but often lack the vocabulary to ask for them. Dougherty describes the relationship as formal methods needing to know that AI security is a critical fountain of users, and AI security needing to know how to request specific widgets from formal methodsitians. Content covers shallow technical reviews of recent papers, job postings, event announcements, and movement updates in the formal methods and AI safety intersection. Recent issues have focused on verification benchmarks such as Vericoding, Veribench, and VerifyThisBench; hardware verification and microhypervisor specification; program synthesis using proof languages like Lean and Dafny; and specification elicitation as a neglected research area. The newsletter is hosted at newsletter.for-all.dev (formerly gsai.substack.com) and has hundreds of subscribers. Dougherty received a grant from a funder of presently undisclosed provenance to support communications and strategy work for AI security via formal methods. In his day job, Dougherty works as a Research Engineer at the Beneficial AI Foundation, where he contributes to formal verification benchmarks and tooling.