Funding Formal Methods for the Cyberpocalypse

Introduction

AI capabilities are rapidly increasing, including in offensive cyber, with open-weight models quickly following their closed-weight frontier cousins by whatever means necessary. It seems likely these trends will continue to a point where the average teenager with a few hundred dollars can pull off heists on the scale and sophistication of a nation-state in 2018, or better.[1]  And humans aren’t the only potential problem: agents can also autonomously hack and self-replicate. Some (e.g. Matthew Green) believe that defensive AI uplift will massively outpace offensive uplift, which seems possible eventually, but clearly wrong at least for a while. To put a pin on it: offense is logically and structurally easier than defense.[2]  Many industries are inherently slow to defend, for example, due to FDA regulation on software updates for medical devices, fear of litigation, requirements for backward compatibility or interop with devices controlled by other vendors who are not incentivized to collaborate (a common problem with military hardware), or uptime requirements which, in the short term, make patching less tolerable than being continuously exploited.[3]  Consequently, there may soon be a cyberpocalypse, in which the cybersecurity (and, thus, stability) of table-stakes internet-connected infrastructure will plummet to zero, driven by rampant AI-enabled cybercrime.

Recently, several philanthropic organizations have asked me[4] how I think they should go about funding formal methods to pre-empt the cyberpocalypse.  The framing is basically that we can reduce or maybe even pre-empt this cyberpocalypse using AI-enabled formal methods at scale, i.e., by mathematically hardening existing software against future attacks. But, doing so would be very expensive, and requires moving very quickly. How should a well-funded philanthropic organization go about doing this?

In this document I outline a loose vision for how to fund formal methods quickly, for broad, global cyberassurance. I envision this document as candidate guidance for large organizations which plan to spend money broadly on AI safety causes, and want to allocate a fraction of their portfolio to approaches rooted in formal methods. Note that I do not claim formal methods solves AI safety generally, rather, I claim that it ameliorates some of the short-term problem of offensive cyber uplift.

My high-level conclusion is twofold. First, current FM tools are built for a very different world than the one we will live in in a year or two. We can build more impactful tools if we build for the future. Second, these tools need to be applied where it actually matters: hardening the cyber infrastructure that real people actually depend on, for banking, energy, private messaging, commerce, and so forth. This is a global problem and it requires global talent.

What not to do

It is tempting to say, well, finding and funding real human people is hard, so how about instead, we just give the money to half a dozen SF vampires and ask them to burn tokens generating wholesale Lean-verified replacements for popular open-source software, or something like that. This approach is foolish. Existing software builds on decades of latent folklore knowledge: implicit specification in the form of email chains, github issues, tweets and so forth, all of which is missing context for any autoformalization agent. The agent won’t even know the software was meant to do that in the first place. The operator who uses the software might not even know what the software is meant to do, and certainly doesn’t know every aspect of what it currently actually does. This problem, spec elicitation and validation, is what Mike Dodds is working on, and it is an enormous one.[5]

It is also tempting to say, well, sure it would be nice to hire talented researchers from around the world, but we don’t really have time for meritocracy because the world is going to end tomorrow. So let’s just get a bunch of Oxford and MIT kids and pay them to do FM work. This is also foolish. There are banks and hospitals and telecom and utility companies in Morocco and India and Mexico just like there are in the United States. All these countries will be impacted by the cyberpocalypse, and they should all share in the remediation. The only way to achieve global cyber-hardening is therefore to rapidly train the next generation of computer scientists, worldwide, to help harden everything, everywhere, all at once.

People and organizations

I believe that philanthropic organizations should spend money in a way that maximizes

• the number of FM experts available, worldwide, to harden cyber systems;
• the number of critical systems that can be secured per FM expert;
• how easy it is for a forward deployed FM expert to harden an arbitrary software system;
• the cybersecurity of commonly used, foundational open-source software; and
• the cybersecurity of commonly used closed-source products that lack proper incentives to harden on their own (I am thinking of things like SCADA systems, or the software used by small banks or hospitals).

I can think of several ways to accomplish these goals. Here are a few, all of which involve organizing groups of people.

“FM MATS”: Fund an international research fellowship in AI safety via formal methods. The fellowship should rapidly train a large number of computer scientists in several locations around the world on how to deploy AI-enabled formal methods to harden critical infrastructure at scale. The mentees should both build and apply new tools for this purpose, and should bring their expertise home with them upon returning to their countries of origin. This could be accomplished through an existing program like MATS, but I think it would be best done as a standalone entity with a global reach (ideally with several locations on different continents, e.g., Cambridge, Capetown, Hong Kong, Berkeley).

FMxAI “Summer School”: Fund a Summer (or Fall, or Spring, or Winter) School for PhD students, professors, postdocs, and industry researchers in FM focused entirely on the intersection of FM and AI for cyber hardening. In particular, a program like this could very quickly upskill formal methods researchers in AI, teaching them about alignment and AI safety, getting them up to speed on current AI capabilities, teaching them agent engineering, and introducing them to agent swarms like Conductor and Slate.

Formal Methods Bootcamp: Develop a short, 2 to 3 month FM bootcamp, online, for software engineers worldwide to quickly learn to use SOTA AI-enabled FM tools on real software. Examples include autoformalization agents like Leanstral, Axle, Gauss, and Aristotle; MCP connections for pre-existing tools, such as for Angr or Lean; neurosymbolic bug-hunters such as Specula; and new, forthcoming tools that should exist but don’t, yet, such as a pipeline to autonomously upgrade Python codebases via crosshair. Note that for novices, a core problem will be differentiating proofslop from valuable assurance work, so a bootcamp should also teach the critical review skills needed to vibe-proof.

Hardening Evals/Competitions: Fund the “DARPA Cyber Grand Challenge” of defensive hardening. Run it in a way that incentivizes much larger amounts of participation than what DARPA gets, and from better teams[6].  Make it attractive for AI labs to compete, preferably by shaping it more like a benchmark with a leaderboard and less like a sporting event.  One way to set this up could be with red and blue teams, similar to ARIA’s Mathematics for Safe AI, and focused on making increasingly hardened sandboxes (see Figure 1).

Figure 1: A meme from a group chat I’m in with several cryptographers.

Forward Deployed Engineers: Fund forward deployed FM engineers/researchers to go improve existing software systems. E.g., companies like General Electric can just apply to get 3 or 4 forward deployed engineers to make one of their software systems more secure, using AI-enabled FM. This would also be available for cities, municipalities, etc., worldwide.

Reusable Specs: Fund the development of libraries of reusable specs that hold for multiple systems, as Evan Miyazono advocates. Expressing the exact same idea in a different way: develop novel programming paradigms, which enable users to rapidly vibe-code useful software, but using already-formally-verified widgets.

Soundness Bounties: Fund soundness-bug bounties for popular FM tools like Lean, Kani, Verus, Rocq, etc., with a particular focus on tools that make sense to use in-the-loop for secure program synthesis or scalable formal oversight.[7]  In general, I claim that soundness bugs should be assigned MITRE CVEs, since verification tools are load-bearing for both current and emerging security technologies.

Next, I imagine you want someone to lead FM spending. I’ll discuss the several buckets of possible candidates, and illustrate each bucket with a few names of people I either personally know and like a lot, or otherwise have read work from and greatly admire.

Some of the most senior people in the field -- Moshe Vardi, Kathleen Fisher, Ken McMillan, John Launchbury, Byron Cook, or adjacent people like Sergey Bratus -- will likely be nearly impossible to convince to work for you on any short timescale. They will often be AI-skeptical, and in some cases, worried about tarnishing their reputation by working on something which could produce slop research.

The next tier of leaders would be younger, but very successful, professors and industry researchers -- folks like Talia Ringer, Pete Manolios, Adam Chlipala, Roopsha Samantha, Joey Dodds, etc. This is probably the sweet spot for hiring into leadership, although many of these folks are in demanding academic positions and cannot just take leave at a moment’s notice, so it could be challenging – a friend of mine who likens himself to be a “professional career-derailer” recommends asking them “what would it take for you to say ‘yes’”, and offering to coordinate with their tenure committees (i.e. via generous donations), trying to convince them of the importance of the problem, or making them a (financial) offer they can't refuse. Note, many of these folks are also quite AI-skeptical.

You could hire from mathematics -- several mathematicians, such as Olle Häggström, are AI-safety-pilled and potentially open to this kind of work -- but there is a very real difference between FM for math and FM for cybersecurity (deep, universal proofs with few axioms vs wide, shallow hyper-specific proofs potentially with many axioms, respectively), and so you face the possibility of a large leadership knowledge gap if you take that approach. But it’s not without precedent; Jacob Tsimerman has joined OpenAI to work on AI safety, and notably, Sergey Bratus has a PhD in pure mathematics.

You could hire someone junior, a newish professor such as Harry Goldstein, Prashant Anantharaman, etc. In this case, you face the problem of drawing someone who likely just started in a tenure-track position away from tenure.

The last option I see is to hire a current PhD student, such as Simon Henniger or Jake Ginesin. This approach, of course, has the downside that the individual will lack the research maturity, connections, or even just cultural cachet of a more senior researcher.

To put it bluntly: hiring leadership for this mission will be hard, and doing it quickly will be very hard.

There are several people who are wonderful (such as Mike Dodds) who I exclude above because they are already running organizations which I’m reasonably confident they would not want to leave. There are several people who would be great but who I simply forgot to mention. And of course, there are several other people who I exclude because they would be awful. The best way to suss out if someone belongs in the latter category is to speak one-on-one with their former students, or with people who worked under their supervision in some capacity.

Some organizations which I view generally positively, but which I think are perhaps not very AI-pilled, are: Galois, SRI, NARF, NASA FM, Riverside Research, Kestrel, Apple FM (these people), and AWS Automated Reasoning. Actually, Trail of Bits seems to be pretty AI-pilled, so they could be a good place to hire from. Some organizations which I think are more AI-pilled but potentially less mature or experienced are: Axiom, Math Inc, Reasonable, Harmonic, Atalanta, Sequent, and Theorem. If you’re trying to hire, I would suggest looking at folks from all of these organizations - especially internally-facing technical managers who aren’t writing their AI-pilled opinions on Twitter.

The actual formal methods, themselves

Existing formal methods have been developed under the presupposition that proofs are very cumbersome to conjure, and can only be generated either fully mechanically (via proof-generating algorithms) or manually (via underpaid and overworked graduate students). This leads to two outcomes: first an overemphasis on scoping problems to those which can be reliably mechanically dispatched (see: model checking, SAT/SMT solving), and second a deep fear of any interactive theorem proving challenge which might take more than a PhD-student-year of labor to complete (what if we never finish the paper?).

If you believe that AI will soon be able to hack just about everything, then you probably also believe that AI will soon be able to generate a wide variety of proofs. In this glorious AI future, when proofs are cheap, the tradeoffs involved in achieving totally mechanical proof synthesis are much less worthwhile. We might still want to use model checkers or SAT or SMT solvers for certain specialized reasoning steps, for example as the backbone for static analysis tools, but broadly speaking, the question of whether or not a formal method is totally automated will be considerably less important. And also, big theorem statements, things like “Microsoft Word is Immune to ROP Attacks”, will be perfectly valid problems to work on since you will be able to attack them with a relentless army of tireless agents.

I maintain that we should develop FM tools for the future. This includes things like:

• Interpretable, formally verified compilers for every programming language.
• Extensible type systems for every language, supporting arbitrary types with user-supplied type proofs (like ACL2s but for normal programming languages).
• Formal systems for reasoning about the precise semantics of compiled code, from any language, on any chip.
• Novel agent designs that bootstrap better intelligence in a way that gives better correctness guarantees for free, or vice versa.
• Distributed systems verification techniques that don’t just prove correctness for a model of the system, but instead, prove it for the actual system under study.
• AI-accelerated fuzzers, which rapidly self-improve their fuzz harnesses at runtime.
• AI-accelerated gadget discovery and gadget compiler techniques for LangSec.
• Libraries of reusable specifications for repeatably useful gizmos, such as STM. Put differently, increasingly high-order abstractions for vericoding or secure program synthesis (SPS).
• Approaches for assuring the assurers, such as lean4lean or comparator, or bridges between theorem provers. (Candle is a notable example of a verified verifier.) This matters in the future I describe since we cannot trust that the proof generator has our best interests in mind!

This, in general, does not include things like:

• The development of new and exciting decidable logics.
• Improved model-checking tools for existing languages.
• Decision procedures for linear types.

The end-goal for this development arc should be to deploy, at planetary scale, autoformalization for open-source software. Google Project Zero, in fuzzing, has been a good example of how to run a project like this. We should autoformalize and, consequently, harden every popular open-source software project. This is basically a north star for “building for the future of FM”.

Conclusion

AI safety philanthropies have the opportunity to fund a considerable amount of formal methods research over a short time-horizon. This could on the one hand enrich a number of grifters in San Francisco while negligibly or even negatively impacting global cybersecurity, or on the other hand, it could uplift global cybersecurity massively and reduce the death-drive of open-weight models so we make it to ASI with little in the way of serious cyber incidents. Obviously, I am hoping for the latter.

I believe that the way to drive meaningful impact in cybersecurity is to train a global cadre of talented formal methods researchers and hackers for AI-enabled cyber uplift, and then equip them with a new generation of extremely powerful, AI-native FM tools (many of which have yet to be built), and point them at actual, critical infrastructure. I hope this short document hints at my vision for how to do this and helps inspire you, dear runner-of-well-funded-charity, to deploy the capital you are vested with, wisely.

1. ^Anecdotally, I tried hacking several targets using frontier models in January, to no avail. Then more recently, I applied a frontier cyber model to several popular formal methods tools -- including z3, Rocq, Kani, Verus, and ACL2 -- and found confirmed soundness bugs in all of them except for ACL2.
2. ^A friend of a friend of a friend of mine is in the vulnerability-selling business, and reports that everyone is just vibe-hacking with racks of servers running Kimi or equivalent, and when one shop finds an 0-day, within a day or two, a dozen others find the same thing, using the same models in similar or identical harnesses. This is evidently causing all kinds of problems for consumers in the industry, who want to incentivize exploit discovery but don’t want to pay for many dozens of redundant hacks.
3. ^Products may also have high switching costs, regulatory capture, or other areas of friction for defensive upgrade.
4. ^The reason I have been asked this question is twofold. First, I’ve written about this topic here, on LessWrong, several times, including the limitations of formal methods for AI safety. And second, I am involved in a lot of offline AI safety research rooted in formal methods, for example through the Apart SPS fellowship I co-created.
5. ^Atalanta and Reasonable are also working on related problems.
6. ^Ok, that may be too spicy. Some of the teams, such as Fish’s team at ASU, were truly excellent. But at the same time, the incentives were not really there for places like Trail of Bits or Kudu Dynamics (now part of Leidos) to invest large amounts of money into competing. In contrast, if winning at defense helps with winning the AI race generally, we could expect orders of magnitude more investment!
7. ^This is a project I would love to run if you, dear reader, want to fund it!

Discuss