Ryan James Spencer retweeted
CVE-2026-69420: Computers are vulnerable to denial-of-service by being shot with a gun
4
7
136
2,016
“The Party thanks you for your 8 tonnes, citizen. The Five-Year Plan demands the ice caps.”
Explore new estimates for all countries for 2025, measured in total, per capita, and historical terms: ourworldindata.org/explorers/co2
Other sources & data:
globalcarbonbudget.org
ourworldindata.org/electric-car-s…
ourworldindata.org/grapher/co2-la…
0
0
0
43
It’s amazing to see how everyone is converging towards determinism, formal verification, stronger guarantees, especially in terms of reaping what’s pragmatic about it.
But I’m also hearing “what if models get so good we don’t need that?”
Another word for verification is “inspection” and I reckon we might see less inspection earlier in the pipeline, but would we really lose inspection entirely?
But I’m also hearing “what if models get so good we don’t need that?”
Another word for verification is “inspection” and I reckon we might see less inspection earlier in the pipeline, but would we really lose inspection entirely?
2
0
3
133
Maybe it’s just fanciful thinking on the part of the ai-pilled but I’m dubious we’d stop caring about the outcomes eventually. And if the outcomes matter so does finding issues anywhere in the “pipeline” before they show up.
1
0
0
19
Anycase, I’m writing another book.
formalenough.com
And I’m disappointed I didn’t call it “formulenuff”
formalenough.com
And I’m disappointed I didn’t call it “formulenuff”
0
0
2
14
Ryan James Spencer retweeted
Lovely explanation of statecharts.
What is a "statechart"? State machines, but better.
Another hand-written 2-minute read ⬇️ x.com/i/article/2116…
4
12
204
19,448
Ryan James Spencer retweeted
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 ( ͡° ͜ʖ ͡°)
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 ( ͡° ͜ʖ ͡°)
38
125
852
199,728
Heat is turning up.
New on our Frontier Red Team blog: using Claude to formally verify software at large scale.
Formal verification can prove that code is free of certain bugs, but historically it has only been feasible for small codebases (or required a lot of expert time).
With AI models, however, this is beginning to change. In collaboration with @theoremlabs, we used Claude to prove security properties in over one hundred real-world open-source libraries over the span of a few weeks.
Read our research in full here: anthropic.com/research/forma…
0
0
0
36
Ryan James Spencer retweeted
I put together a minimalistic pure-Rust, CPU-only implementation of the recent LFM2.5-8B-A1B language model from @liquidai that you can directly link into your Rust projects😎
github.com/maximecb/bebelm
github.com/maximecb/bebelm
6
12
183
14,810
Ryan James Spencer retweeted
what’s everyone’s favorite PL paper published so far this year
3
4
58
3,994
Ryan James Spencer retweeted
You may have already heard, but the core SQLite team is working on Vec1 — native vector search (ANN) in SQLite.
It supports Euclidean (L2) and cosine distances, and uses SIMD for fast vector operations.
Vec1 is already feature-complete. The only things left are improving test e optimizations.
sqlite.org/vec1
It supports Euclidean (L2) and cosine distances, and uses SIMD for fast vector operations.
Vec1 is already feature-complete. The only things left are improving test e optimizations.
sqlite.org/vec1
8
57
610
27,886
Ryan James Spencer retweeted
I just released mold 3.0.0! This is the first Rust version of mold, rewritten from C++ with performance on par with 2.42.1. The goal of mold 3.x is to close the remaining GNU ld compatibility gaps and make mold the default linker in Linux distros. github.com/rui314/mold/re…
42
214
1,434
72,455
