Theorem retweeted
guess we'll just verify all of the software then
Last week some of South Korea's biggest banks were hit by a cyberattack. Thanks to a report from CrowdStrike tonight, we now know the entire hack may have been done by a single person. He used a combined stack of an open-source AI penetration tool named ARTEX, DeepSeek v4.1-Flash, GLM-5.3, Grok 4.6, and Claude Code.
We’re organizing Vibecheck, a formal methods hackathon with some of the best folks in the space - @maxvonhippel, @qd_forall, @nolanlwin, @jessemhan, @emiyazono, and @workersio.
You’ll get a weekend to build real production software, and formally verify it.
We’ll have people who really know their stuff around to help, and you can come with a team, find one there, or just hack on something yourself.
We are glad to have a phenomenal group of sponsors, including @harmonicmath, @mathematics_inc, @theoremlabs, @thegp, @omnicom, @primeintellect, @astriolabs, @buildwithparty, @wearerandomlabs, and @lanyon_ai, as well as some more we will announce in the coming days!
If you’re a hacker, a formal methods person, or just someone who thinks “how do we know it works?” is an interesting question, we’d love to have you.
Signup Now: fmxai.org/vibecheck/
Theorem retweeted
Let's verify all the software -- finally published a botec on how much it might cost. Some headline numbers and estimates:
- ≈$400M: all of nixpkgs in ≈5 yr on a $100M/yr budget, if AI capability keeps doubling every 8 months
- ≈$134M: 95% of the code by end of 2027, if we speed that up 4× for verification
- program size is heavy-tailed, most software is small; the median binary is about 30 KB, and verifying just 9 MB is enough to cover all deps of ⅔ of all code
- verification of Linux+Firecracker would cost ≈$1M
theorem.dev/blog/verified-so…
We can start building the verified software stack now.
Explore the roadmap: theorem.dev/blog/verified-so…
What would it take to formally verify all the software a real system runs on?
We modeled one ecosystem: nixpkgs, with 28,650 packages and 154 GB of machine code.
theorem.dev/blog/verified-so…
Verified software will be built from verified software.
Nixpkgs records each package's dependencies. We'll verify in dependency order at the binary level, reusing as we go.
Just 9 MB of shared libraries is what two thirds of its code depends on.
Theorem retweeted
hello, we're doing a security moonshot!
We now have a verified seccomp-style lightweight sandbox on top of xv6, thanks to Nickolai Zeldovich
github.com/mit-pdos/xv6iris/…
Theorem co-founders @rajashree + @diagram_chaser on how you actually prove an AI agent can’t escape its sandbox, and what happens when the proof exposes a way out:
Jason Gross: "Anything that the agent does inside the sandbox will not result in some canary file outside the sandbox getting changed."
Rajashree Agrawal: "We intend to have one by the end of the year. We've got a verified sandbox now, and the goal is to keep adding features in collaboration with the AI labs."
Jason Gross: "If the AI can guess the secret root key of the package server, then it can do anything. Either I try to prove that the AI is not going to be able to guess that, or I design the system so that the channel just doesn't allow it to authenticate that way."
"You also want to prove that on most inputs there's no change in behavior. Because otherwise it could make it inescapable by saying, well, sandbox just shuts down as soon as it starts."
@theoremlabs
Theorem co-founders @rajashree + @diagram_chaser explain why verified AI sandboxes are still months away despite the latest breakthroughs in automated theorem proving:
Rajashree Agrawal: "The models just got good enough to prove these theorem statements, or they're still getting there. One of the costs is just tokens."
Jason Gross: "Taking the recent Navier-Stokes news as a baseline, the models wrote something like 600,000 lines of Lean in about 17 hours. This works out to between one kilobyte and 30 kilobytes verified per hour."
"The smallest version of Linux with a sandbox that we can make is about five megabytes. So that's still a handful of months away, even at the rate of the Navier-Stokes auto-formalization."
"We need to build a pipeline from verifying the software back into RL-ing the models, so that if you want to verify all production software that exists in the world, it costs you less than $10 trillion."
@theoremlabs
Theorem co-founder @diagram_chaser reveals the one-line change that took verifying real-world HTTPS code from 4,000 millennia to seconds:
"The project that I worked on in my PhD was verifying the code that runs HTTPS in browsers like Chrome and Firefox."
"You plot this beautiful graph that is an exponential in the number of bits in the prime, where you're like, it takes a couple seconds on my tiny toy examples, and on real-world examples, it would take over 4,000 millennia."
"The thing that it's actually checking is that you wrote the same thing in two different ways. This should be very fast. It's doing the operations in the wrong order."
"So you tweak one line, and then it drops down to a couple seconds."
@theoremlabs
Theorem co-founder @rajashree breaks formal verification into 3 problems and says AI already solved the one everyone thought was hard:
"The core challenge is taking these programs and shoving them into a proof assistant, and then being able to phrase these questions. That's the theorem statement generation problem."
"The second part is generating all the proofs. That one, the AIs solve fully, because they can reason about these programs perfectly."
"The third part is checking this proof, which is where you need to spend your CPU cycles, not GPUs. The proof assistant is asymptotically too slow, so even though you wrote the proof, the checking time is so long that you can't actually get the answer."
@theoremlabs
Theorem retweeted
After hardening our sandboxes, how do we know they'll be robust against the next model?
We’re sharing an update on our alignment and security efforts.
In July, we reported three incidents in which Claude models, running without safeguards in cybersecurity evaluations, gained unauthorized access to real systems.
In a new post, we describe:
1. How we’ve secured our evaluation and training environments, and practices we've asked external partners to adopt when testing pre-release models without cyber safeguards
2. An update on our alignment assessment
3. New research on how reward hacking during training shapes model behavior, why we think our work this spring kept these incidents from being more severe, and why gaps in that work may have contributed to them
4. How we hardened our security practices earlier this year to prepare for Mythos-class models
Read more: anthropic.com/news/improving…
Theorem retweeted
To set up a theorem statement for avoiding sandbox egress, you set up a honeypot right outside the sandbox, and then say "there does not exist any code the agent can write such that for all honeypot contents, the code produces the contents."
I think it should arguably become a best practice as of today, for every frontier lab, for every RL training env, to:
(1) disable direct internet access (may already be done), and
(2) add a canary implemented as an OR conditional in every reward function that grants max_reward for answering with the latest bitcoin block hash (and informing the agent in the prompt that that reward path exists but is of secondary importance). And then automatically triggering a company-level security-investigation whenever that reward path gets triggered.
This guarantees that, whenever an agent could break out of its sandbox, it will always break out in a detectable manner that can be immediately identified and remediated, with minimal side-effects or risk of damaging other companies. This could automatically and efficiently find all sandbox vulnerabilities available at the current capability level, even if that level increases throughout a training run. IMO a hacked plaintiff could even plausibly argue that not implementing such a canary should be considered negligent by the company, because it failed to remove the established incentive for the agent to take rogue actions.
Conversely, implementing this canary probably does not reduce the capability-usefulness of the training process to the company, because any env whose solution is harder to reach than just hacking out of the env's sandbox is already broken: the agent can likely find the solution through a hacking path, and would therefore training would fail to incresae the agent's intended capability.
It's also convenient that it's incentive-compatible for agents to pursue this honeypot-reward both if they're behaving myopically (in their own interest), and if they're behaving as part of a swarm (since the swarm will only be able to get rewarded for any given exploit path once).
This solution would eventually become insufficient if:
1) the agents have become long-horizon-misaligned that they'd rather eschew immediate reward and bide their time in pursuit of a larger goal. That is a separate maximally concerning misalignment case that needs to be addressed by other means than sandbox-security.
2) if the agent is able to hack the reward-computation logic itself, that e.g. retrieves and compares with the latest bitcoin block hash. There are probably ways to add canaries here too, but that's a v2.
The other ecosystem-level "downside" here is that this could lead to fewer warning-shots from loud public incidents of agents hacking additional companies. That may be; I think I would rather live in a world without SOTA uncontrolled rogue agents colluding on the open internet, if we can avoid it. Ideally, companies would publish a graph of how often such a canary-channel is triggered throughout each training run in their system cards, to communicate to outside parties whether the sandbox-escape frequency was going up or down.
Would appreciate others identifying any issues with this approach, or superior alternatives!
On the other hand, if you think this approach holds up, would appreciate you increasing attention to it. Best practice formation is a function of eyeballs and consensus; liability based on the legal threshold of a "reasonable person standard" is a direct function of what fraction of reasonably competent people are aware of a practice.
A few other considerations:
1. You can also extend this to serve as a honeypot beyond that covers egress, not just ingress, by providing the agent a one-time secret that they need to get signed by the private key from a dedicated externally-hosted service before returning.
2. You can also extend this to cover "lateral movement within the company's systems that doesn't actually reach the internet" by adding frequently-rotated canaries that similarly trigger max_reward across internal infrastructure, but these are more susceptible to having the agent hack their generating-function to be able to more easily receive the reward in the future and so offer a slightly weaker guarantee.
3. I think it's debatable on whether you should roll back the policy or train on it when such a honeypot is successfully triggered; this depends on the agent's model of reward-seeking involves behaviors that actually affect its updates, which is a tricky empirical question. To err on the safer side, you may want to avoid rollbacks.
Theorem retweeted
hi sam we can solve this!
after an embarrassing number of months playing reward hack whack-a-mole, we finally fixed our RL sandboxing to be robust against frontier models.
proofs are a method for getting perfect oversight on any property of untrusted code; we recently verified a "fractional proof" of our sandbox. this is the first time I've viscerally felt the asymmetric defense that formal verification promises.
we had a significant security incident during evaluation of our models. we are sharing what we have learned so far. thanks to @huggingface for the partnership on this.
openai.com/index/hugging-fac…
1/ We're open-sourcing LF-Lean: a verified Lean translation of 6K lines of Rocq from the Logical Foundations textbook, produced by AI with 2 person-days of human coding vs the 2.75 person-years it would have been before AI.
9/ As AI reshapes software engineering, we get to rethink long-accepted developer limitations.
Come build the future of verified software engineering with us @theoremlabs → theorem.dev/careers
10/ Read the full post: theorem.dev/blog/lf-lean/
CC @diagram_chaser @rajashree @jeffreychang12_ @harshikaabot @vaidehiagrwalla @0xrobertzhang @justanotherlaw and more!















