Tractable Problems in AI Security via Formal Methods

Secure program synthesis is popping off in 2026 [1], [2], [3], which will be great for our overall cyber resilience. However, its not obvious that it will actually be applied to AI security in real life. To seize this opportunity, we need to map out the relevant layers in the current ML inference and training stack and figure out what widgets represent formal methods opportunities. The June 2026 executive order on AI innovation and security [4] points the same way — voluntary vulnerability scanning, hardened critical infrastructure, federal funding for AI vulnerability detection — while declining to mandate licensing or preclearance; what it does not say is how any of that earns its assurances. Let us treat ML training and inference infrastructure with the seriousness we treat airplanes; and on the software side, that will mean at least some formal methods.

Bibliography

• [1] J. Regehr, “Zero-Degree-of-Freedom LLM Coding using Executable Oracles.” [Online]. Available: https://john.regehr.org/writing/zero_dof_programming.html
• [2] M. Kleppmann, “Prediction: AI will make formal verification go mainstream.” [Online]. Available: https://martin.kleppmann.com/2025/12/08/ai-formal-verification.html
• [3] M. von Hippel, “Secure Program Synthesis.” [Online]. Available: https://www.lesswrong.com/posts/8wtrLoDPyCfMLuHkt/how-to-solve-secure-program-synthesis
• [4] The White House, “Promoting Advanced Artificial Intelligence Innovation and Security.” [Online]. Available: https://www.whitehouse.gov/presidential-actions/2026/06/promoting-advanced-artificial-intelligence-innovation-and-security/