Gradient Sky 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 ( ͡° ͜ʖ ͡°)
36
126
838
196,830
Gradient Sky retweeted
there's something really cool about asking your agent to draw a statechart (hypothetical example in this image), then using the /create-formal-verification-skill you made with pstack to find bugs through something like TLA+. you can both understand your code better and how the and fix issues users would otherwise see
pstack v0.15.27 ships with a new skill /create-formal-verification-skill!
it's still in beta, and similar to /create-verification-skill, this is a meta-skill that creates a new skill and formal verification suite based on the characteristics you want to verify. for example, you machines and systems with concurrency using TLA+, or use kani in rust to check for undefined behavior.
if you're new to formal verification, think of it as mathematically proving properties and invariants (something that must always be true) or "laws" of your system. usually, this means modeling your programs in a separate language like with TLA+ and then running the solver on that spec. newer approaches like with kani and @bendlang take a different approach where there is no separate language: you write kani in rust, and bend in bend (it's also a programming language, and the proofs are written as laws and expressed in its type system).
historically formal verification never reached mainstream status because of the difficulty in modeling and writing proofs. it's quite difficult to model your business requirements and keep them in sync! but i expect that we will see more innovation in formal verification in the future as being able to formally verifiy that the code does what you intended gives your agents superpowers in writing correct software.
in the meantime though, i've been experimenting with modeling our code with TLA+ and have already found several bugs with the skill created by /create-formal-verification-skill.
try it out and let me know how it goes!
233
354
5,267
443,512
Taking inspiration from @RyanSael to visualize Keplerian Orbital Elements
Astra ~1 hour of work
…trument.copper-lark-1870.chatgpt.site
Astra ~1 hour of work
…trument.copper-lark-1870.chatgpt.site
0
0
2
112
Gradient Sky retweeted
The "whiteboard defense:" I should be able to pull you aside at any moment and ask you to explain any customer-facing system you've shipped. You should be able to clearly explain how it works and defend the decisions you made. This is my benchmark for responsible AI usage.
I don't expect line-level familiarity with the code. I don't care if you remember the exact function name or implementation detail. You may not even know it. I don't care.
But if I ask "why did you do X instead of Y?", "what happens if this actor behaves maliciously?", "what data structure did you use here and why?", or "where does this fail?" you should be able to answer confidently.
For PoCs, demos, experiments, whatever: I don't care. Generate 100% of it and understand none of it. Speed over quality every time in those specific scenarios.
But if you're shipping customer-facing work, you can't be shipping things you don't understand at a high level.
I don't expect line-level familiarity with the code. I don't care if you remember the exact function name or implementation detail. You may not even know it. I don't care.
But if I ask "why did you do X instead of Y?", "what happens if this actor behaves maliciously?", "what data structure did you use here and why?", or "where does this fail?" you should be able to answer confidently.
For PoCs, demos, experiments, whatever: I don't care. Generate 100% of it and understand none of it. Speed over quality every time in those specific scenarios.
But if you're shipping customer-facing work, you can't be shipping things you don't understand at a high level.
234
1,019
9,499
489,240
Gradient Sky retweeted
@GeoffreyHuntley Holy crap... the linked talk/not-talk/standup routine from @headinthebox explaining actors is *amazing*: youtube.com/watch?v=7erJ1D…
2
3
5
1,574
Gradient Sky retweeted
A post of ours on vendor lock in and LLMs. We don't like the growing trend of AI companies quietly hiding your data while stripping away your control. We think that's bad for users and bad for the ecosystem. Here's are our thoughts: earendil.com/posts/session-…
39
131
840
160,538
Gradient Sky retweeted
put orwell's 6 rules for writing in your global CLAUDE.md / AGENTS.md
thank me later
it makes codex much more human
thank me later
it makes codex much more human
21
10
637
116,230
My agent-powered workflow is much much deeper: check the code out (the full thing), understand cr intent, what is changing in the new flow, form hypotheses where the change is wrong, send sub-agents to track the whole call chain, collect evidence, prove or refute its real, create reproducible scenarios, then… if it checks… run through critic.
Gaslight agent - I know there’s a big, go find it (adversarial bug hunt). Repeat more iterations if the change is complex…
then… only then have a talk. Plannotator-style discussion is just amazing. You not reading the code, you investigating what’s going on, elbows deep into the PR.
Downside: it’s tens of $$ per CR, so IDK if it makes sense for open source requests from unvetted contributors… but it saved much more in complex debugging, identified latent bugs from old, pre-AI times…
it sees things that got broken by diff, but not present in diff.
It’s a slop menace… you see big PRs coming from your peers, respond with force.
Gaslight agent - I know there’s a big, go find it (adversarial bug hunt). Repeat more iterations if the change is complex…
then… only then have a talk. Plannotator-style discussion is just amazing. You not reading the code, you investigating what’s going on, elbows deep into the PR.
Downside: it’s tens of $$ per CR, so IDK if it makes sense for open source requests from unvetted contributors… but it saved much more in complex debugging, identified latent bugs from old, pre-AI times…
it sees things that got broken by diff, but not present in diff.
It’s a slop menace… you see big PRs coming from your peers, respond with force.
all these static AI PR review tools are pointless no matter how fancy they are
you can tell your robot about a PR, ask it what to look at first and go back and forth with your thoughts until you've processed it all
interactivity is always better
0
0
1
226
Interfaces are alignment structures. A work can happen between well defined interfaces without forcing the whole codebase back into one giant context window. They compress product intent, give the system shape, like a skeleton, and contains ambiguity, like watertight bulkheads in a ship.
End-to-end tests play the complementary role. They define whether the composed system still expresses the intended product behavior, preserve what the system is supposed to mean after the implementation changes. Tests are a model of the product.
It does not mean implementation never matters. Sometimes the implementation is the valuable thing: algorithm design, performance, ranking behavior, concurrency, numerical correctness, security, or domain-specific heuristics. In those cases, you do not hand-wave what’s between the interfaces. You zoom in and focus on that thing.
Apply your skills where the maximum alignment leverage is present.
End-to-end tests play the complementary role. They define whether the composed system still expresses the intended product behavior, preserve what the system is supposed to mean after the implementation changes. Tests are a model of the product.
It does not mean implementation never matters. Sometimes the implementation is the valuable thing: algorithm design, performance, ranking behavior, concurrency, numerical correctness, security, or domain-specific heuristics. In those cases, you do not hand-wave what’s between the interfaces. You zoom in and focus on that thing.
Apply your skills where the maximum alignment leverage is present.
i think where i'm landing is that the code doesn't matter, but the types do
0
0
1
170
The real work was always about alignment between all the participants of the development process. We need to be on the same plane in understanding what is being built and how it is being built. Autonomous loops in the current form are crippled - they have little space for this alignment to happen.
0
0
3
122
Gradient Sky retweeted
3 hours of Warhammer 40k lore on Helsreach narrated by a Black Library narrator? You're welcome!
An honour to collaborate with @40kIndomitus and @LSymphonica to tell a story we're all so passionate about. If you like what you see and would like MORE, please do subscribe to support the channel!
youtu.be/XQ1jlW7hQrA?si…
An honour to collaborate with @40kIndomitus and @LSymphonica to tell a story we're all so passionate about. If you like what you see and would like MORE, please do subscribe to support the channel!
youtu.be/XQ1jlW7hQrA?si…
10
50
351
16,070
Gradient Sky retweeted
LLM Knowledge Bases
Something I'm finding very useful recently: using LLMs to build personal knowledge bases for various topics of research interest. In this way, a large fraction of my recent token throughput is going less into manipulating code, and more into manipulating knowledge (stored as markdown and images). The latest LLMs are quite good at it. So:
Data ingest:
I index source documents (articles, papers, repos, datasets, images, etc.) into a raw/ directory, then I use an LLM to incrementally "compile" a wiki, which is just a collection of .md files in a directory structure. The wiki includes summaries of all the data in raw/, backlinks, and then it categorizes data into concepts, writes articles for them, and links them all. To convert web articles into .md files I like to use the Obsidian Web Clipper extension, and then I also use a hotkey to download all the related images to local so that my LLM can easily reference them.
IDE:
I use Obsidian as the IDE "frontend" where I can view the raw data, the the compiled wiki, and the derived visualizations. Important to note that the LLM writes and maintains all of the data of the wiki, I rarely touch it directly. I've played with a few Obsidian plugins to render and view data in other ways (e.g. Marp for slides).
Q&A:
Where things get interesting is that once your wiki is big enough (e.g. mine on some recent research is ~100 articles and ~400K words), you can ask your LLM agent all kinds of complex questions against the wiki, and it will go off, research the answers, etc. I thought I had to reach for fancy RAG, but the LLM has been pretty good about auto-maintaining index files and brief summaries of all the documents and it reads all the important related data fairly easily at this ~small scale.
Output:
Instead of getting answers in text/terminal, I like to have it render markdown files for me, or slide shows (Marp format), or matplotlib images, all of which I then view again in Obsidian. You can imagine many other visual output formats depending on the query. Often, I end up "filing" the outputs back into the wiki to enhance it for further queries. So my own explorations and queries always "add up" in the knowledge base.
Linting:
I've run some LLM "health checks" over the wiki to e.g. find inconsistent data, impute missing data (with web searchers), find interesting connections for new article candidates, etc., to incrementally clean up the wiki and enhance its overall data integrity. The LLMs are quite good at suggesting further questions to ask and look into.
Extra tools:
I find myself developing additional tools to process the data, e.g. I vibe coded a small and naive search engine over the wiki, which I both use directly (in a web ui), but more often I want to hand it off to an LLM via CLI as a tool for larger queries.
Further explorations:
As the repo grows, the natural desire is to also think about synthetic data generation + finetuning to have your LLM "know" the data in its weights instead of just context windows.
TLDR: raw data from a given number of sources is collected, then compiled by an LLM into a .md wiki, then operated on by various CLIs by the LLM to do Q&A and to incrementally enhance the wiki, and all of it viewable in Obsidian. You rarely ever write or edit the wiki manually, it's the domain of the LLM. I think there is room here for an incredible new product instead of a hacky collection of scripts.
Something I'm finding very useful recently: using LLMs to build personal knowledge bases for various topics of research interest. In this way, a large fraction of my recent token throughput is going less into manipulating code, and more into manipulating knowledge (stored as markdown and images). The latest LLMs are quite good at it. So:
Data ingest:
I index source documents (articles, papers, repos, datasets, images, etc.) into a raw/ directory, then I use an LLM to incrementally "compile" a wiki, which is just a collection of .md files in a directory structure. The wiki includes summaries of all the data in raw/, backlinks, and then it categorizes data into concepts, writes articles for them, and links them all. To convert web articles into .md files I like to use the Obsidian Web Clipper extension, and then I also use a hotkey to download all the related images to local so that my LLM can easily reference them.
IDE:
I use Obsidian as the IDE "frontend" where I can view the raw data, the the compiled wiki, and the derived visualizations. Important to note that the LLM writes and maintains all of the data of the wiki, I rarely touch it directly. I've played with a few Obsidian plugins to render and view data in other ways (e.g. Marp for slides).
Q&A:
Where things get interesting is that once your wiki is big enough (e.g. mine on some recent research is ~100 articles and ~400K words), you can ask your LLM agent all kinds of complex questions against the wiki, and it will go off, research the answers, etc. I thought I had to reach for fancy RAG, but the LLM has been pretty good about auto-maintaining index files and brief summaries of all the documents and it reads all the important related data fairly easily at this ~small scale.
Output:
Instead of getting answers in text/terminal, I like to have it render markdown files for me, or slide shows (Marp format), or matplotlib images, all of which I then view again in Obsidian. You can imagine many other visual output formats depending on the query. Often, I end up "filing" the outputs back into the wiki to enhance it for further queries. So my own explorations and queries always "add up" in the knowledge base.
Linting:
I've run some LLM "health checks" over the wiki to e.g. find inconsistent data, impute missing data (with web searchers), find interesting connections for new article candidates, etc., to incrementally clean up the wiki and enhance its overall data integrity. The LLMs are quite good at suggesting further questions to ask and look into.
Extra tools:
I find myself developing additional tools to process the data, e.g. I vibe coded a small and naive search engine over the wiki, which I both use directly (in a web ui), but more often I want to hand it off to an LLM via CLI as a tool for larger queries.
Further explorations:
As the repo grows, the natural desire is to also think about synthetic data generation + finetuning to have your LLM "know" the data in its weights instead of just context windows.
TLDR: raw data from a given number of sources is collected, then compiled by an LLM into a .md wiki, then operated on by various CLIs by the LLM to do Q&A and to incrementally enhance the wiki, and all of it viewable in Obsidian. You rarely ever write or edit the wiki manually, it's the domain of the LLM. I think there is room here for an incredible new product instead of a hacky collection of scripts.
2,939
7,401
61,033
21,994,838
Gradient Sky retweeted
Episode 10 of Raising An Agent with @sqs and @thorstenball is out!
There's no better summary than this quote:
"We will be killing our editor extension, the Amp VS Code extension. We're going to be killing it. And we're going to be killing it because we think it's no longer the debar is dead. Let's walk through why."
Topics in this episode:
- The new deep mode in Amp
- Balancing developer experience for humans & agents
- Killing the VSCode extension & shift away from traditional editors
- Pi & OpenClaw, two wonderful projects
- Importance of reinventing yourself in AI
Enjoy! And happy hacking!
Timestamps:
01:00 Deep Mode
10:30 Optimizing the codebase for agents
15:00 Feature Preview: which Skills does your team use?
18:00 Balancing DX for humans & agents
21:35 Killing the Amp editor extension
28:00 The future of software and what it means
33:00 You need to stay agile
36:00 Pi & OpenClaw
39:00 Text editors holding companies back
44:00 Is manual context management coming to an end?
49:00 New concept for Threads
50:00 Amp, the business & the art installation
There's no better summary than this quote:
"We will be killing our editor extension, the Amp VS Code extension. We're going to be killing it. And we're going to be killing it because we think it's no longer the debar is dead. Let's walk through why."
Topics in this episode:
- The new deep mode in Amp
- Balancing developer experience for humans & agents
- Killing the VSCode extension & shift away from traditional editors
- Pi & OpenClaw, two wonderful projects
- Importance of reinventing yourself in AI
Enjoy! And happy hacking!
Timestamps:
01:00 Deep Mode
10:30 Optimizing the codebase for agents
15:00 Feature Preview: which Skills does your team use?
18:00 Balancing DX for humans & agents
21:35 Killing the Amp editor extension
28:00 The future of software and what it means
33:00 You need to stay agile
36:00 Pi & OpenClaw
39:00 Text editors holding companies back
44:00 Is manual context management coming to an end?
49:00 New concept for Threads
50:00 Amp, the business & the art installation
39
37
385
312,206
While tinkering with @dexhorthy ‘s RPI (research plan-implement workflows), I followed his ideas to define software engineering in terms of navigation/mapping goals.
LLMs are reasoning computers, and they are very good at navigating abstract spaces. The raw model capability is only half the equation. When you need to move from point A to point B fastest, you can either build a better engine (use opus-4 vs 5 vs 6), or you can draw a better route. The route matters as much as the engine.
RPI is great, but I think it might be even better if we’ll define the abstract spaces so the navigation would be much easier… it’s not specific to software engineering, but I think each domain has the fundamental things below:
Dimensions are the orthogonal axes of a system - independent properties that describe what the system is. They are the intrinsic characteristics of the system itself, existing whether or not anyone examines them. A system has a concurrency model, a cost profile, and a reliability posture regardless of whether anyone has evaluated them. Orthogonality is important - a system can be highly reliable but deeply insecure, or perfectly correct but economically ruinous.
Lenses are Trade-Off Spaces. If dimensions are the platonic space in which a software system exists, lenses are the practical spaces in which engineering decisions are made. Engineers do not think "let me evaluate the Concurrency dimension" - they think "what happens when this system is under load and things start failing?" That question naturally spans Reliability, Performance, Concurrency, Operability, Safety, and Security. It is a trade-off space: choices that improve one dimension within that space often degrade another.
Reasoning is the navigation method. It is a structured process for identifying the delta between a system's current state and its desired state across the dimension space. RPI is a reasoning tool. Ignatius of Loyola built a very similar method centuries ago (12 questions) and it surprisingly aligns almost 1:1 to RPI phases, Rich Hickey’s “how to design” talk. Never in my life I felt philosophy would be one of the most important tools to be efficient.
LLMs are reasoning computers, and they are very good at navigating abstract spaces. The raw model capability is only half the equation. When you need to move from point A to point B fastest, you can either build a better engine (use opus-4 vs 5 vs 6), or you can draw a better route. The route matters as much as the engine.
RPI is great, but I think it might be even better if we’ll define the abstract spaces so the navigation would be much easier… it’s not specific to software engineering, but I think each domain has the fundamental things below:
Dimensions are the orthogonal axes of a system - independent properties that describe what the system is. They are the intrinsic characteristics of the system itself, existing whether or not anyone examines them. A system has a concurrency model, a cost profile, and a reliability posture regardless of whether anyone has evaluated them. Orthogonality is important - a system can be highly reliable but deeply insecure, or perfectly correct but economically ruinous.
Lenses are Trade-Off Spaces. If dimensions are the platonic space in which a software system exists, lenses are the practical spaces in which engineering decisions are made. Engineers do not think "let me evaluate the Concurrency dimension" - they think "what happens when this system is under load and things start failing?" That question naturally spans Reliability, Performance, Concurrency, Operability, Safety, and Security. It is a trade-off space: choices that improve one dimension within that space often degrade another.
Reasoning is the navigation method. It is a structured process for identifying the delta between a system's current state and its desired state across the dimension space. RPI is a reasoning tool. Ignatius of Loyola built a very similar method centuries ago (12 questions) and it surprisingly aligns almost 1:1 to RPI phases, Rich Hickey’s “how to design” talk. Never in my life I felt philosophy would be one of the most important tools to be efficient.
0
0
0
76
Gradient Sky retweeted
Recommended reading.
Building slop machine pipelines that build more slop machine pipelines instead of software actual humans use is not productivity.
If your feelings are hurt, because your 1 minute vibeslop PR got closed, consult a professional.
lucumr.pocoo.org/2026/1/18/agen…
Building slop machine pipelines that build more slop machine pipelines instead of software actual humans use is not productivity.
If your feelings are hurt, because your 1 minute vibeslop PR got closed, consult a professional.
lucumr.pocoo.org/2026/1/18/agen…
11
20
219
15,531
Gradient Sky retweeted
I had a great call with a very well known AI scientist who asked why I take the approach to AI I do, for example “why VHS TV ads?”.
This 1971 MARSHALL MCLUHAN film is a good example of why.
Of course I use 1000s of other high protein sources.
The Ads are a mirror:
This 1971 MARSHALL MCLUHAN film is a good example of why.
Of course I use 1000s of other high protein sources.
The Ads are a mirror:
32
63
371
60,333
