position paper · forall r&d
A minimal, sane catalog of formal methods opportunities across the ML training and inference stack. An instruction manual for how to spend 5–25 postdoc-years.
We welcome new contributions: reach out at quinn@for-all.dev or schedule a call. Alternatively, file an issue on GH or submit a PR.
// abstract
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. We are not alone in this read: a June 2026 RAND expert survey [4] lands on the same split we do — formal methods can secure the infrastructure (memory safety, access control, sandbox isolation) even though they cannot adjudicate model semantics like jailbreaks — and ranks cryptographic primitives and access control as the highest-leverage place to start. This document turns that diagnosis into shovel-ready specs. The June 2026 executive order on AI innovation and security [5] 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. The demand side is on record too: Anthropic’s frontier safety roadmap commits to “leveling up across the board” by mid-2027 — hardened Kubernetes access controls, allowlist-based egress, supply-chain integrity for builds, short-lived cryptographic identities [6] — a checklist that reads layer-for-layer like the stack this document maps. 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.
// tractable problems