Can We Secure AI With Formal Methods? January-March 2026

I'm overwhelmed, cut me some slack.

In the month or so around the previous new years, as 2024 became 2025, we were saying “2025: year of the agent”. MCP was taking off, the inspect-ai and pydantic-ai python packages were becoming the standards, products were branching out from chatbots to heavy and autonomous use of toolcalls. While much of the product engineering scene may have underdelivered (in the sense that “planning a vacation” isn’t entirely something most people do with agents yet), the field of FMxAI I think was right on target. Feels like there’s an agentic component to everything I read these days.

What is 2026 the year of? Besides “year of investors pressure all the math companies to pivot to program synthesis”? I’m declaring it now

The number of blogposts relating to secure program synthesis went exponential since the last issue of the newsletter, such that the hyperlinks in this sentence are not even exhaustive. Like AI capabilities themselves, we simply do not know when it will go logistic. Which I think means I have to keep the newsletter manageable by not promising to do the general secure program synthesis or FMxAI spaces and really double down on AI security applications. I mean it, you guys. It’s overwhelming, the space is too big now, etc. But will SPS gains actually get applied to AI security opportunities? That’s the crucial question I think we should care about, now. Let’s assume by default no, so that everyone who wants to liberate my bayes points from me goes and makes it happen.

I moved to DC, and I started an AI Security reading group in meatspace. Reach out to be involved!

There will be hackathons and fellowships in secure program synthesis, FMxAI, AI security, etc. Be prepared.

Sorry again about the long gap between editions. I’ve been writing more than ever, but not a lot of it public yet. Also coding a lot.

Nicholas Carlini’s desperate and pleading talk

Carlini: “Opus is better at finding 0-days than I am”. Carlini, famous for finding vulns in adversarial robustness papers back in the computer vision days, stopped a hair short of declaring a draft, but I’m not. This is a draft. If you’re reading this, you are hereby conscripted into the secure program synthesis army. Or maybe our vibe is more “militia” coded, haven’t made up my mind yet. But this is a draft. The gameboard seems offense dominated right now, we need to harden software, and we need to do it quickly.

According to gemini, who cites forbes: 20-40% of corporate IT budgets in 1999 were devoted to Y2K prep. $300-600b was spent (roughly 0.5-1T adjusted for inflation). Ordinary people, people with families, people who put sandwiches into little baggies, decided to do this. They had consensus that it was coming down the pipe, on a deadline.

I don’t think we have that consensus, I’m not sure we can marshall those resources.

But here look this is all I’m saying

cat << EOF > CLAUDE.md

Make agentic software that hardens a given repo with a red-blue loop. Declare an agent that uses standard redteam tools like fuzzing harnesses and static analysis as tools to find vulns in repos, then declare another agent that patches those vulns. Use git submodules to manage sources

EOF

while true; do cat CLAUDE.md | claude --dangerously-skip-permissions; sleep 1; done

If everyone reading this ran that command, and tailored it to the specific things you happen to know about, and dropped in repos close to your specialization, and steered the project in directions that I wouldn’t think of, etc. we might have a shot. Do not DoS open source maintainers with slop, but consider forking their repos and DoSing your forks with slop then finding a way to benchmark how much more secure your fork is and then maybe you get a few PRs in. Target loadbearing repos. Etc. 🫡

UK AISI call for information on Secure AI Infrastructure

Let’s do it. Doesn’t seem to have a deadline.

Gemini’s summary:

The UK government has launched a “Call for Information” to gather expert insights on securing the computing infrastructure used to develop and deploy advanced AI models. Managed jointly by the Department for Science, Innovation and Technology (DSIT), the AI Security Institute (AISI), and the National Cyber Security Centre (NCSC), the initiative seeks to address growing threats such as the theft of model weights, data breaches, and system disruptions. The government is specifically soliciting feedback from the AI and cybersecurity sectors on current risks and emerging technologies—including confidential compute, advanced cryptography, and trusted hardware—to help shape future research priorities and technical pilots. Ultimately, the program aims to ensure the UK remains a secure and trusted global hub for frontier AI development by building robust, “defense-in-depth” protections for critical AI assets.

SL5 Taskforce has been productive!

Excited about some of these outputs.

Long Live Safeguarded AI

Official leadership update, Kathleen Fisher (ex DARPA, responsible for HACMS) interviews Nora and Davidad on vimeo, Davidad’s notes about what he’s doing next.

Safeguarded AI, like GSAI, like Open Agency Architecture, was always controversial scifi that, to be clear, I’ve been rooting for since day one. Well not literally day one. When I first read open agency architecture, I recall rolling my eyes and wringing my hands “you can’t just put a type signature on a wacky diagram and say that it means AI safety is formally verifiable” but like a few days later I was into it.

With Nora Ammann in as programme director (who’s been behind the scenes on SGAI since before day one), we should expect aggressive AI security applications of formal methods.

Pat Lincoln I2O director at DARPA

Totally should’ve been in the thanksgiving edition, I spaced. SRI alum Pat Lincoln is pretty keen about AGI, he’s not like completely AGI pilled but extremely sympathetic to the viewpoint.

Atlas blog on CSLib

CSLib is what it sounds like: the mathlib of CS. It is spearheaded by Clark Barrett and Swarat Chaudhuri and others. Atlas Computing, which has for a while been looking at how to close the gap between formal methods as we find them today and radical infrastructure hardening, writes about it (they’re directly involved).

CSLib is cool, but one reason I think it doesn’t register as the droid I’m looking for is that I don’t know if real world software really draws from undergrad CS curriculum all that much. In most real world software jobs, having a problem that is shaped like an academic puzzle rather than a REST API is a rare but golden status marker.

VeriSoftBench

Claim: idiosyncrasies of mathlib in particular determine too much of what we think we know about Lean evals and language model performance on them.

500 theorem-proving tasks from 23 real-world projects, spanning compilers, type systems, smart contracts, separation logic, and program semantics.

Recognizing the crucial wisdom of our time (that math is made of tokens which we can use for something else), we get a Lean eval that isn’t focused on math.

muInference: a minimal inference stack on SeL4

In the draft of this newsletter, where I stubbed out writing about this as TODO, the stub consisted of one word:

Dude.

Which I think roughly describes how I felt seeing it and how I feel now. They basically boot a minimal (cpu) inference enclave in seL4. I used it as an enclave in a network simulation project I was doing, and it doesn’t even have a machine-readable TTY, that’s how secure it is.

Progress in the mitigation of steganography

Crucial applications for model weight exfiltration defense!

DiFR: Inference Verification Despite Nondeterminism

Verifying LLM Inference to Detect Model Weight Exfiltration

Seldon Labs batch 2 applications (closed by the time I’m posting this)

Sorry I didn’t get this out fast enough. But keep an eye on Seldon re the general space of AI security startups.

Also keep an eye on: Heron

Met a bunch of these fine folks at EAG.

Lucid Labs: data center access program for hardware related experiments

Summary by gemini:

The Lab Access Program by Lucid Computing is a specialized initiative providing developers and enterprises with early, hands-on access to “sovereign” AI infrastructure built on zero-trust, hardware-rooted security. Designed for industries with strict regulatory requirements—such as defense, healthcare, and finance—the program offers a sandbox environment where users can deploy AI models and agents while maintaining cryptographic proof of compliance and data residency. By moving away from traditional “black box” cloud models, participants can verify that their computations are occurring on specific, untampered hardware, allowing them to benchmark and refine secure AI workflows before moving into full-scale production.

AISLE finds 12 0-days in openssl and doesn’t (appear to) use formal methods

The hero the secure program synthesis community has been waiting for.

Its extremely unlikely that theyre using iris or some synthetic lean-iris under the hood. A year ago at EAG 2025, I went around telling everybody about my budding separation logic agent and that I wanted to find bugs, synthesize patches, and prove the patches correct with it– and I used repos like OpenSSL as hypothetical target. I didn’t continue working on that cuz I didnt like the Iris DSL that it was based on, but I’m not sure if I should’ve tried to continue.

Take a look at aisafety.com for overall fieldmapping

Thanks to Bryce and the folks at aisafety.com, a bunch of you have found this newsletter, where we discuss using formal methods to improve our AI security posture. Many of the rest of you, however, might have come in from the formal methods community and sometimes think “who are all you AI existential safety wackos”. aisafety.com wants to answer that question by making a map of everything that’s going on in the very broad umbrella of AI existential safety. Highly recommended if you’re generally scared about AI but don’t know exactly where to plug in yet.

Allies IFP have new RFP

With a great track record of supporting secure program synthesis, IFP wants to do more projects along the lines of their galvanization of the great refactor.

Kathleen Fisher and Gopal Sarma post op-ed

Let’s ship evals and RL environments now so that the next gen of language models are differentially accelerated to cyberhardening defensive technologies. 10/10, no notes.