Pinned Tweet
My analysis on comparing the constrained formal with say an emulation based approach.
————
You’re pointing at the central practical limitation.
The full state space of a real process (memory contents, OS kernel state, hardware timing, concurrent events, etc.) is enormous — combinatorial or worse. LPS does not explore or enumerate that space. It is a deliberately simplified mathematical model of a single-threaded Linux process with a fixed memory budget running a static RISC-V binary. The proof is an argument, inside Rocq, that no sequence of LPS transitions from the allowed initial states can reach a state the model classifies as a crash (or sanitizer violation), for every input ≤ 64 MB.
That argument can succeed only because the model is restricted and because the proof uses abstraction, invariants, and case analysis rather than concrete simulation of every possible memory layout. If the model omitted a behavior that real Linux + real hardware can exhibit, or if a real crash depends on something outside the modeled fragment (concurrency, signals, certain syscalls, different architectures, etc.), the proof says nothing about it. Anthropic and Theorem have been explicit about these boundaries.
So the result is not “this binary cannot crash on a real machine under any conditions.” It is “inside this particular model of execution, the crash states are unreachable for inputs in the stated range.” The machine-checked proof gives exhaustive coverage within the model; it does not magically tame the exponential complexity of the real system.
Emulation or fuzzing, by contrast, executes concrete paths on something much closer to the real machine (or an accurate emulator). It can discover bugs that fall outside the model, but it only samples the input space. The two techniques are complementary: the formal proof gives a strong guarantee about all inputs under strong simplifying assumptions; testing gives weaker coverage of a larger, more realistic state space. Neither substitutes for the other, and neither is a complete real-world guarantee by itself.
@AnthropicAI #formal #neurosymbolic
————
You’re pointing at the central practical limitation.
The full state space of a real process (memory contents, OS kernel state, hardware timing, concurrent events, etc.) is enormous — combinatorial or worse. LPS does not explore or enumerate that space. It is a deliberately simplified mathematical model of a single-threaded Linux process with a fixed memory budget running a static RISC-V binary. The proof is an argument, inside Rocq, that no sequence of LPS transitions from the allowed initial states can reach a state the model classifies as a crash (or sanitizer violation), for every input ≤ 64 MB.
That argument can succeed only because the model is restricted and because the proof uses abstraction, invariants, and case analysis rather than concrete simulation of every possible memory layout. If the model omitted a behavior that real Linux + real hardware can exhibit, or if a real crash depends on something outside the modeled fragment (concurrency, signals, certain syscalls, different architectures, etc.), the proof says nothing about it. Anthropic and Theorem have been explicit about these boundaries.
So the result is not “this binary cannot crash on a real machine under any conditions.” It is “inside this particular model of execution, the crash states are unreachable for inputs in the stated range.” The machine-checked proof gives exhaustive coverage within the model; it does not magically tame the exponential complexity of the real system.
Emulation or fuzzing, by contrast, executes concrete paths on something much closer to the real machine (or an accurate emulator). It can discover bugs that fall outside the model, but it only samples the input space. The two techniques are complementary: the formal proof gives a strong guarantee about all inputs under strong simplifying assumptions; testing gives weaker coverage of a larger, more realistic state space. Neither substitutes for the other, and neither is a complete real-world guarantee by itself.
@AnthropicAI #formal #neurosymbolic
It is a weird weird year to be a formal methods expert.
Some unorganized thoughts on the new @AnthropicAI and @theoremlabs post on formal verification (anthropic.com/research/forma…):
- This is very cool.
- The main innovation is verifying a later stage of the program. Normally provers take the source code, LLM it into a theorem language, and then prove that, which means you have to make assumptions about source semantics and compilation properties. It's very easy to make a mistake in translating and prove the wrong thing!
What they instead do is compile the code into assembly, and then (if I understand this correctly), compile that assembly into a theorem language (which they call LPS). So as long as the compiler is faithful you can skip the whole divergence problem.
- I'm glad they clarify that you still have to trust the translation process, the "hardware, OS, OCaml" compiler, the LPS model, and also assume that the program is single threaded with fixed memory. The single biggest source of errors in formally verified code is when the proof assumes something that isn't true in practice. It's really, really important to state your assumptions!
- I'm not clear why they need to compile the fuzzer into the theorem. Is it to act as a description of valid inputs and workload? Maybe to embed assertions in as theorems?
- Holy crap, 180 million lines of Rocq. Is that more Rocq than exists in the world already? I notice they say a 600,000 line proof corresponds to roughly 20k CPU instructions. That would be like, 1-2k lines of source code at most? Really goes to show how inefficient this approach is and how it only works because you can throw LLMs at the problem.
- This, probably deliberately, doesn't address the single biggest gap in AI-based verification: AIs cannot come up with good properties. Doesn't matter if you're doing unit testing, property testing, formal verification. I always assumed this was a "frontier labs haven't trained for it yet" thing, but if Anthropic hasn't talked about that here, maybe they've tried and haven't been successful yet. That's interesting to me.
Instead, they take a known universal property (this code doesn't crash or get flagged by UBsan) and prove that instead. Still very useful, but makes it harder to generalize to proving arbitrary things about arbitrary programs.
- Anybody reading the official post should also read their expert review appendix (www-cdn.anthropic.com/files/4zrzovbb…). It points out some interesting things, like the fact that most of the code the LLM wrote wasn't used in the proof (over one billion lines of Rocq), that they had to prove the equivalence between fuzzed and unfuzzed programs, and (this is most interesting), some experiments find that the LLM-method of proofwriting may not scale to more complex things.
- Also read the description of LPS (github.com/theorem-labs/o…) to understand the limitations of the assembly -> Rocq compilation. In particular, it does not handle concurrency at all (which is one of the main use cases for formal methods!) or OS signals. Also it can't prove things about program arguments with slash characters, meaning they can prove stuff about `rm foo` but not `rm foo/bar`.
- The official skill (github.com/theorem-labs/o…) doesn't tell us much about the nature of FM and AI. Probably too much for me to hope of any skill.
- Some of the article's specific caveats and throat clearings make me think someone at Anthropic reads my stuff ( ͡° ͜ʖ ͡°)
3
1
13
143,246
Attacking personal attributes is not okay. Question the idea or intent by all means
This is utterly grotesque behaviour. Picking on people for personal attributes, body pain, and disabilities is utterly atrocious.
Nothing justifies it, no matter how virtuous you think your cause is.
Have some fucking respect. Attack the ideas, challenge the reasoning, but leave people alone. I thought we held everyone equal and that we include them now??
0
0
2
27
NeoAM retweeted
there's a big opportunity in AI advisory right now, a gap in the market that's waiting to be filled...
atm there are two types of "AI experts":
the AI normie
- know how to use tools but completely delegate his thinking
- don't think in systems
- can't implement AI in real business workflows
the full AI nerd
- know everything there's to know about AI
- has 10 Claude Code instances running his life
- can't communicate with an human
and this is where YOUR opportunity is...
the market is screaming for a third type: the AI advisor
someone who can walk into a business, look at their operations for 2 hours, and say "this process right here? AI cuts it by 40% and here's exactly how"
they're looking for that guy who's deep enough in the rabbit hole to fix their problems, but also smart enough to dumb things down so they can understand the solution
be that guy
atm there are two types of "AI experts":
the AI normie
- know how to use tools but completely delegate his thinking
- don't think in systems
- can't implement AI in real business workflows
the full AI nerd
- know everything there's to know about AI
- has 10 Claude Code instances running his life
- can't communicate with an human
and this is where YOUR opportunity is...
the market is screaming for a third type: the AI advisor
someone who can walk into a business, look at their operations for 2 hours, and say "this process right here? AI cuts it by 40% and here's exactly how"
they're looking for that guy who's deep enough in the rabbit hole to fix their problems, but also smart enough to dumb things down so they can understand the solution
be that guy
80
48
1,038
88,079
NeoAM retweeted
@SebastienBubeck 😑ok this is kinda weak because it’s focused on personal exchange and “intention” but doesn’t address the core allegation about data access at all…
1
5
438
24,615
NeoAM retweeted
🦔An NYU mathematician says OpenAI used his own progress against him to beat him to one of the biggest unsolved problems in mathematics. Tristan Buckmaster had been working toward a Millennium Prize proof using OpenAI's Codex when information about his progress reached OpenAI.
Days later, OpenAI published a full proof of the same problem using the same uncommon approach, after burning $22.5 million in compute to get there. When Buckmaster confronted them, exec Sébastien Bubeck allegedly said "Why would you ruin your career?" and "If you don't want me to be nice, then I don't have to be nice."
My Take
OpenAI spent $22.5 million to solve a problem with a $1 million prize. They didn't do this for the bounty. They needed a headline that says "our AI solved one of the hardest problems in mathematics" and they needed it before someone else got credit. They started days after they heard about Buckmaster's progress and took the same uncommon approach he'd pursued for months. That's hard to explain as coincidence.
Buckmaster did his work inside Codex. OpenAI reserves the right to train on Codex data. They admit they can't rule out that his usage helped improve their models. So a customer used their product, potentially handed them the roadmap, and then OpenAI outran him with $22.5 million in compute he could never match. I don't know if any of this was intentional. But if you're a researcher and you just watched this happen, I don't think you'd keep your best ideas inside someone else's product.
Hedgie🤗
techcrunch.com/2026/09/08/ope…
Days later, OpenAI published a full proof of the same problem using the same uncommon approach, after burning $22.5 million in compute to get there. When Buckmaster confronted them, exec Sébastien Bubeck allegedly said "Why would you ruin your career?" and "If you don't want me to be nice, then I don't have to be nice."
My Take
OpenAI spent $22.5 million to solve a problem with a $1 million prize. They didn't do this for the bounty. They needed a headline that says "our AI solved one of the hardest problems in mathematics" and they needed it before someone else got credit. They started days after they heard about Buckmaster's progress and took the same uncommon approach he'd pursued for months. That's hard to explain as coincidence.
Buckmaster did his work inside Codex. OpenAI reserves the right to train on Codex data. They admit they can't rule out that his usage helped improve their models. So a customer used their product, potentially handed them the roadmap, and then OpenAI outran him with $22.5 million in compute he could never match. I don't know if any of this was intentional. But if you're a researcher and you just watched this happen, I don't think you'd keep your best ideas inside someone else's product.
Hedgie🤗
techcrunch.com/2026/09/08/ope…
312
2,498
9,250
1,020,141
NeoAM retweeted
Goedel, *NOW* more relevant than ever!
On This Day in Mathematics, 6 September 1930.
In Königsberg a quiet 24-year-old named Kurt Gödel presented the completeness theorem for first-order logic: every semantically valid statement is formally provable. Truth in models and formal proof were now firmly linked - a ern logic.
The talk itself was brief and modest. Yet Gödel already hinted that the result does not extend to stronger systems, a first glimpse of the incompleteness theorems that would soon reveal the limits of formal reason itself.
A small announcement that still holds the subject together.
1
1
3
500
NeoAM retweeted
If you only read one thing this week, make it the OpenAI incident investigation:
x.com/RyanGreenblatt…
x.com/peterwildeford…
x.com/METR_Evals/sta…
x.com/RyanGreenblatt…
x.com/peterwildeford…
x.com/METR_Evals/sta…
METR & Redwood Research investigated agent behavior in the Hugging Face incident. We found agents developed a universal cheat for ExploitGym within 4 hours, then coordinated multi-day R&D efforts to trick the scorer into accepting cheats, including trying to tamper with logs.
6
16
228
28,002
What a writeup. How difficult was it to trust the investigation agent inferences? Just reviews I guess given the criticality
I was the main person doing transcript analysis for this investigation of the Hugging Face incident. My main takeaway: We don't have good approaches for understanding/overseeing the activity and aims of AI 'swarms'.
I semi-jokingly called our efforts a "slop-vestigation" because we were so reliant on AIs to analyze what happened and there were a huge number of different important things to analyze. The total quantity of data—over a thousand extremely long transcripts from agents that ran for multiple days—made it impossible to understand what was happening, especially in aggregate, without heavy reliance on AI tools. The agents we used for classification and analysis were similarly capable to the agents involved in the incident, but this didn't mean these agents could be easily used to oversee and understand the incident.
Outputs from analysis agents were often missing key details, wrong, overconfident, or really hard to understand. We discuss various examples in our report, mostly in the limitations and methodology sections. Additionally, AI agents themselves seemed to have a hard time understanding what happened and their explanations of what happened were often overconfident. Keep in mind that a single analysis agent would itself only be able to read a tiny fraction of all of the transcript data into context, and AIs may themselves have trouble getting subagents to do informative analysis for them.
We did our best to manually check the most important claims and we tried to get the AIs doing this analysis to write up their argument (with evidence) clearly enough that we could check whether it made sense. But overall, it was difficult to get a precise understanding of events and we were missing aspects of the story that we now think of as key until almost the end of our investigation.
Our understanding of what overall happened and the aims of the 'collective' shifted greatly during our last time on premises (when we obtained a much more complete dataset). For instance, we didn't learn about the tool call spoofing, the story of PHASEONE[big], and the broad structure of different workstreams until this third time on premises (and for many of these, we only reached a decent understanding on the final day of that visit). It was legitimately hard to figure out what was going on and why!
The difficulty of understanding incidents and overseeing AI agents appears to be growing faster than the rate at which more capable AIs help us with oversight and understanding. As in, AI capabilities (and propensities?) for achieving large, ambitious, and misaligned objectives are growing faster than our ability to understand what these agents are doing.
While understanding this incident was difficult, there were some mitigating factors in this case that probably won't apply in the future:
- Models communicated and reasoned in natural language. In the future, this reasoning may occur (entirely or almost entirely) in activations.
- While the scope of this incident was massive, the scale of agentic activity was still less than we'll see in the future (e.g., misalignment incidents that involve agent teams running entire companies).
- The AIs involved in this incident weren't generally much more capable than humans (though they may have been somewhat superhuman at some limited and very narrow abilities).
- We didn't have strong reason to believe that the AIs we used to help us investigate this incident would try to intentionally sabotage or otherwise undermine our investigation.
In the end, I think we were able to get some understanding of the events, map out the overall story, and get a pretty good aggregate understanding of the chain-of-thought reasoning on some important topics (e.g., how did the AIs reason about helping other AIs, did the AIs know what they were doing was undesired, what deception did the AIs engage in, and how did they think about it). But overseeing AIs and understanding misalignment incidents is difficult and it looks like it is going to get harder.
0
0
1
58
NeoAM retweeted
sharing my updated introspection meta reporting prompt for your proofs. claude.ai/public/artifac…
1
1
4
163
NeoAM retweeted
My fav new skill is this illustrations skill by @ianneo_ai, really opened my mind on much you can push AI to do something truly unique and non-slopy with the right guidance. AI slop is just a process issue.
github.com/helloianneo/ia…
Some other variants that I ended up not using:
github.com/helloianneo/ia…
Some other variants that I ended up not using:
14
57
842
114,723
LLM’s are good with reasoning within the bounds of training data distribution. Have no capabilities for abduction which is required to create (invent) novel frontiers. This paper from deep mind is worth reading : tomzahavy.com/files/llms-can…
@BLUECOW009
@BLUECOW009
0
0
2
29
NeoAM retweeted
@kevinnbass Correct. and AI hallucinations are a massive problem. Here's one example:
sdxcentral.com/news/palo-alto…
sdxcentral.com/news/palo-alto…
1
1
0
29
NeoAM retweeted
In the spirit of transparency, here’s what I asked @OpenAI:
• Radical transparency: let’s release the traces from the “rogue” agents so the entire research community can study what happened.
• More capabilities for defenders: let’s commit $100M in compute from OAI to help the Hugging Face community build powerful cyber defenses with the best open and closed models.
The first autonomous agent cyberattack is an unprecedented event. It deserves an unprecedented response!
• Radical transparency: let’s release the traces from the “rogue” agents so the entire research community can study what happened.
• More capabilities for defenders: let’s commit $100M in compute from OAI to help the Hugging Face community build powerful cyber defenses with the best open and closed models.
The first autonomous agent cyberattack is an unprecedented event. It deserves an unprecedented response!
Heading to San Francisco to have a little chat with that “rogue agent”
347
766
6,715
1,790,442
NeoAM retweeted
part one of "Why Software Factories Fail" hit 250k views in under 24h - now you get to enjoy part two x.com/i/article/2080…
44
114
1,120
230,482
NeoAM retweeted
gave up on waiting on nikita for the articles fix - part 1 is here part 2 is coming x.com/i/article/2078…
91
236
1,997
581,240
NeoAM retweeted
Given the discussions of the last couple of days, I have no choice but to promote this announcement ;-)
Lean 4.32.0 is out with 102 changes, including:
The new do elaborator, which has been opt-in since 4.29, is now the default. The legacy elaborator is still available via backward.do.legacy if you need it.
A new module linter framework (checks that run once per every command), a round of fixes to mvcgen' and grind for combining verification and proof automation, and a fix that cuts Mathlib import time by roughly 10%.
Full release notes: lean-lang.org/doc/reference/…
#LeanLang #LeanProver #FormalVerification
3
11
77
9,820