Quinn

By Niplav. Easily top 5 posts of 2025 for me (was only on EA Forum, couldn't find it here) Wildly prescient re glasswing Niplav drafts a token cost BOTEC in squiggle and asks "who pays for these tokens?"

There’s been some talk about how I’m not doing the best possible job with the newsletter and there’s room for competition, or, if we’re feeling frisky, a coup. If you’d like to volunteer, let me know how I can help! I mentioned last edition that I don’t see myself being...

Apart and the secure program synthesis community are launching a fellowship! A ton of you reading this would make great mentors— but the mentor application deadline is a mere week away, so we have an emergency edition of the newsletter to persuade you to apply. In this sentence, I am...

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...

Introduction Secure program synthesis (SPS) is the problem of automatically generating, or “synthesizing”, software which is known to be secure. In practice, this manifests as the triple-task of synthesizing some software S, a specification φ saying what it would mean for S to be “secure”, and a proof P that...

We appreciate comments from Christopher Henson, Zeke Medley, Ankit Kumar, and Pete Manolios. This post was initialized by Max’s twitter thread. Introduction There's been a lot of chatter recently on HN and elsewhere about how formal verification is the obvious use-case for AI. While we broadly agree, we think much...

We did the rebrand! The previous thumbnail was a baseball metaphor, but it was very clearly someone getting out, not safe. I was testing all of you and each of you FAILED. Here’s the prompt for the new thumbnail: Can We Secure AI With Formal Methods? is a reader-supported publication....