LLMs are making formal software verification feasible at a much larger scale
anthropic.com
anthropic.com
So far, I've proven that about 12% of the code behaves the same when executed single-threaded. That works out to roughly 70k lines of C code. This has found very minor differences in behavior, such as how floating-point operations across platforms can produce different results.
I'm working on figuring out how to scale this up, but I don't see any fundamental limitation that would prevent this from scaling up further.
I tried giving Astra a shot. Since it scores better on math, I thought it might do better at writing Lean. I forgot the exact details, but that didn't end up being the case. I think it wasn't thinking holistically enough and tended to rabbit hole itself more
Right now my consortium is Opus 5.5, Grok 4.7 and Muse Wonder. These three are different enough that their insights are very complementary. Once a plan is detailed enough, any decent model can execute on it successfully, but I personally like Grok’s ability to stick to the plan. (And no 5-hour quota!)
Of course, it should go without saying that my comment was a genuine, good-faith account of my real world experience with these models. Not that a public reputation seems to count for much these days, but for what it's worth I have over 25 years of public involvement in the tech sector, and I'm posting under my real name and real identity.
It's also worth noting that, living in an unfavourable time zone relative to most HN activity, I'm rarely here to offer the opening opinions in a discussion. More often I'm arriving 12 hours into a conversation, where everything I'd want to say has already been said. I end up contributing only where I think a different perspective is missing. Naturally, that means my comment history will disproportionately reflect the rare instances where my opinions buck the prevailing HN orthodoxy.
If you disagree with a particular claim I've made, by all means challenge it on its merits. That could be the basis of a much more interesting conversation than this fatuous one.
I mean, we all know what we are talking about here, so please go ahead and do make your case
However, the comment I did reply to seemed to think that just because you ran a forum that you would be unlikely to be biased. This is like obviously false, if anything you have major internet brain where you spend enough time on the internet where you come up with a whole complex about how you are contributing the uncommon opinion the site needs to hear or whatever, when it's just the same dreck from the rest of the internet sprinkled in here when it hasn't been posted enough by someone else. That is not directly "I used Grok and thought it was good at x" but, like, it's clear that it's something that is at the periphery of a whole network of positions you hold that are aligned this way.
I don't necessarily think this is bad and in fact I think most people on the internet at least basically post in this way but I do think it's important to be aware of it at least. I'm not sure you are. I can tell you more or less where my slop opinions come from and I don't think it would be accurate in any capacity to describe them as bucking "the prevailing HN orthodoxy". I, uh, think you should probably describe your comments differently.
How do you verify this compiler is correct? To do that, I think you at least need a formal semantics for both C and Rust in Lean, both sound like Herculean efforts
I haven't yet. My main goal has been to find as many bugs as possible. While bugs could still slip through because my compiler is incorrect, I'm still finding a good number, so I think it's worth it.
Edit: I don't do this often, but why is my question being downvoted? Is this question not allowed?
"Aeneas currently functionalizes a subset of safe Rust, and we are in the process of extending the functional model with reasoning based on separation logic to support unsafe code and concurrent code."
If we're doing Ancient Athens, then Platonic Methexis probably fits better.
pgrust is incredible btw
I tried several approaches to support both C and Rust. I tried using LLVM bytecode, but that ended up being way too low-level. The proofs ended up being gargantuan.
I also tried converting CBMC's intermediate representation, "GOTO Programs" to Lean. This seemed worth a shot because CMBC supports C and Kani adds support for Rust. Unfortunately, Kani's Rust-to-GOTO conversion caused a massive blow-up in code size.
What I ended up doing was converting both GOTO Programs and MIR (Rust's IR) to my own custom IR. The IR is low-level enough to convert both languages, but high-level enough to keep the code relatively concise. I then run simplification passes over the IR and compile it to Lean.
https://news.ycombinator.com/item?id=50205816 seems to differ
In general, the spec must be human readable, and I believe to achieve that we must do away with SQL. Putting aside the thousands of pages of SQL standard, even the core subset has a gnarly semantics due to issues like nulls.
A simpler semantics is one of the main motivations behind Prela [1], and despite its simplicity, we now know it’s powerful enough to express thousands of queries in the wild [2], as well as run doom [3].
Eh. Carthago delenda est? Why?
Like, SQL was around before I was born, and barring the immanence of the Machine God (and potentially even then), will be around long after I die (unless civilisation collapses, I guess).
Like, what the literal fuck?
Usually I would agree with you but when porting code the source code is the spec.
Dude, this is a database.
Concurrency is the source of all the hard stuff in databases.
Databases without concurrency are super-trivial.
I don't see any fundamental limitation that would prevent this from scaling up further.
The fact that you've dodged all the hard stuff is a pretty fundamental limitation.
so either you verify the whole thing or basically you didnt verify anything.
remember what verification is for. its great your query parser is functionally correct but verification is meant to prove something.
say you have a car. and its got safety requirements. those need to be verified. But now they say we've verified its safe only for the rear seat passengers. or, only the engine block is verified itll keep running safely.. it completely negates what is being done if its not done completely to the entire car.
and then ofc another driver just prangs into you anyway with their uncerified car, or suddenly the unverified road (OS) turns into a sinkhole and all ur verification still goes out the window..
there are limits already to verification if done properly and skipping the hard/important parts is really a big issue... u might aswell not do it.
(i do respect that there is a road to fully verified, u wont slap out those 9 million lines in one go. but saying you're winning halfway through the race.... nope)
If you use a language like Java, you have to start with a multi threading aware design concept first or the retrofit is going to be painful and probably will never happen.
Multi threading in classical programming languages with mutable aliasing by default requires global program analysis to check if it is safe or not. Rust restricts the programs to what can be reasoned locally.
They're using LLMs. The economics of this sort of retrofit has changed considerably with LLMs.
Databases and operating systems are inherently concurrent. They deal with concurrency sources outside the process running the Rust code. Because of this, they don't get the magical shared-xor-mutable => deterministic-concurrency benefit that Rust is famous for.
And, frankly, if you tried to make SQL/ACID shared-xor-mutable you'd completely cripple it. Databases are inherently concurrent.
To me, it makes sense that we start being more rigid in how we specify so we don't ever need to look at the code generated by LLMs.
There's no such thing as "formal verification except for minor floating point differences" ... I would think this is one of the first things to pin down before continuing to anything else?
Or do you calculate bounds or something?
What is the solution here? I'm assuming you're running into some lib function in C that has a different order of operations than the similar one in Rust, or something?
I invested a ton of my life and my entire life savings into this transition. Now Im being screamed at everyday to go be an electrician because Anthropic claims they're going to solve the halting problem in some round about way, they dont even have to do what they claim. They just have to convince 20% of industry that they will, and guys like me will never get a chance to work long enough to retire.
I really don't think they'll suceeed, but if they do, Im going to be homeless coding from the public library because im not starting over again.
Be sure to distinguish between "jobs" and "good jobs" (that are enough to survive and even prosper on). Jobs that pay pittances can be created til the cows come home.
The fact that some of those jobs would have paid 3-5x the median wage in 2021 isn’t a scathing indictment of AI, even if it’s inconvenient for the slice of the world who could have made 4x the median wage and now only makes double it.
I find it unrealistic anyway, that market will be saturated so fast, it won't make a difference for you or me, in the grand scheme of things.
I feel like a good chunk of my skills that I honed over decades as a software engineer are obsolete: programming, debugging, navigating code. But there are other skills and especially experiences that, at least with the current level of tools, allow me to do much more than someone who doesn't have them: knowing what computers can and cannot do, or only inefficiently; distributed systems; deployment; CI/CD pipelines.
I have been having a different exp with it. Those are even more important. These things are creating some wild code. Then sticking to its guns in some cases and just rewriting the same bug over and over.
Just this week I literally showed the thing where it was breaking. I wanted it to trace where the error was coming from. Instead it immediately wrote guard code and patted itself on the back. Not a bad idea but does not give me the reason of why something was broken. As where it broke is just part of the problem. Turns out I had a data issue. Guarding the error was the wrong plan in what I was looking for. The user needed his data fixed. Without tracing and debugging I am pretty sure AI would not have found it. Not without me prompting even more. It had twisted itself silly trying to make the error good instead of root cause. Took me an hour or so before I realized it was doing that.
Trust by verify. These things make all sorts of assumptions unless you are very accurate in your prompts.
1. Are you using the latest frontier models? I know that feeling: "These things are creating some wild code. Then sticking to its guns in some cases and just rewriting the same bug over and over." But that was a few months ago. With Opus 5.5, it's gone.
2. For debugging, I give Claude read-only access to the prod DB, and it has access to logs and traces (Signoz in our case). With this, it has amazing debugging skills. Orders of magnitude faster than myself, and it has yet to fail finding the cause of an issue.
Even though opus 5.5 is like a goddamn genius, and I don't really even feel like I need to check the code, I still absolutely could not imagine a PM taking over most of my tasks. Not even close
They WILL fire some people.
But the entire substrate of corporate america depends on empire building.
People need people.
AI will never fully replace people because PEOPLE literally can't replace people.
Therefore, people will always be needed.
Be likeable. Learn to kiss ass. Be competent. Be aggressive.
You will be fine.
It's like Bezos talking about how we're going to have 3 day work weeks while he makes his employees piss in a bottle.
Software doesn't have this scarcity dynamic. People will use LLMs to build better sounder foundations (as rust is 'better' than c) and code quality will improve as we migrate to them. You won't get screwed on your rust++ license though to the point you have to piss in bottles.
Time is finite. People’s problems that can be solved by software is also finite. There’s diminishing returns in improving software. Rewriting bash in rust, and then testing the result would barely help anyone. Also the real world (where inputs come from) is messy. You can have the perfect mechanism (memory safety), but that grain of sand (corrupted or unexpected data) can still make it behave erratically (wrong result).
A while back a knowledgeable man was a philosopher, and they could all easily talk to each other and understand. As time went we split up - we have philosophy doctors in various fields who have very little to talk about.
This happened again when the term “engineer” fractured (even before software engineering). Software engineering itself fractured, too.
And it’s happening again now.
The bonus here is that you can cut in at the prose spec stage and change it to whatever you need, as well as being able to target it at specific technical choices at the last couple of steps.
Where I've seen this work really well is with privilege escalation management, where you do actually want to be careful about the states the system can get into, and the APIs available for managing privileges in a system might be super specific to that system. But I can imagine the workflow being quite a useful one any time you've got anything state-machine flavoured.
They say “ While this is an enormous volume of proof code, virtually none of it needs to be manually reviewed. The Rocq proof checker ensures that the spec is correctly satisfied by the proof. As a result, the only artifacts that a developer needs to trust are: The formal models of RISC-V and of Linux processes;
The exact theorem statements that were proved;
The Rocq proof checker itself.”
What are the formal models of RISCV and Linux? I’m guessing they allow translation of RISCV code directly into Rocq proofs?
I’d love to see more info about their workflow of code -> proof. Or even an open source tool
It is also interesting how the LLM optimists are leaning on tools like Rocq and Lean to save them from the mess of uncertainty and confusion. These are tools created by people who understood their code and worked with deeply with type theory etc. People can keep thinking they can get away with making products from vibes, but down in the infrastructure they still have to depend on people thinking and building carefully.
It is hypocritical to campaign for "nobody will look at code anymore" while depending on the hard work of people who carefully look at code.
Likely, a proliferation of experimental languages all somewhat akin to Typescript for SQL with significantly more nuanced operators to tersely capture the same outcomes as imperative languages.
They’ll compile down to be able to run performantly for game development or even for the Linux kernel (as if Linus would ever agree lol) but also they’ll be able to run on distributed execution engines with effectively a shared memory space, etc.
Allows for significantly more terse artifacts. Lower chance of hallucination, fewer output tokens, fewer thinking loop iterations and concise enough for humans to review (for domains that need it).
On top of that, additional theorem like syntax to drastically limit the ability of functions, etc. likely some sort of higher level effect system for verification. Used for many things like “constant time compilation for crypto functions”, and also “ensure acid compliance” for writes and reads in a local context, and things like “ensure only once delivery” for functions on a distributed execution engine.
At which point every program will be formally verified by default. You could think of it as AdaErlangSQL+++
Which, if that were really possible, would be pretty good evidence of AGI. Or, at least, the end of 6-7 figure software engineer salaries. Conversely, I think it's a pipe dream. Writing a compiler that actually works well across such a broad range of hugely complex behaviors would itself be absurdly complex.
PD: inform7 can run on an RaspPi B+ or 25 year old PC's like nothing, and i6 down to 30 year old ones. The ZMachine adventures themselves, from any 16 bit computer and up.
I think Rust's success in the AI space shows how useful formal proofs are, as Rust provides something very similar to that. Both because it helps with the understanding of LLMs, as well as with trusting the LLMs are not violating any basic properties (like please no nasal demons if the user sends a buffer larger than the allowed amount).
Now imagine what AMD64 machine can do with 2GB of RAM (minimum baseline for legacy, maybe some C2D computer) today.
Very few developers look at the underlying “source code” that this SQL compiles into. Very few people even read the “source code” that tsc outputs.
The reality is the lowest level checkpoint worth looking at and understanding is the highest possible abstraction layer which preserves 100% of the needed precision and flexibility that the product being built requires.
Also, you’d just use something like sscache or just .o files to speed up compilation. It’d be unusual to store compiler MIR/LIR in git.
I think the important part will be figuring out what we need from the higher level language that achieves 100% of the precision and flexibility of Rust for the product being built.
Only because there’s a group of people that do understand database theory and know how to write a proper implementation and they have a track records of doing so. Themselves relies on compilers maintainers and OS developers, and this goes on down to the semiconductors where people do study how electricity interact with the materials.
Every layers of the tower of abstractions have people that understand the current layers, knows the safe semantics of the layer below, and can provide a safe foundation for the layer above.
Since when? Rust just has an ML-like type system, and seemingly many have met that for the first time with Rust, even though it has decadeS of history, and multiple production languages running it just fine (ocaml, scala, etc).
Formal proofs are way way above an ML type system. Like how do you encode mathematical statements in Rust's type system? What about statements about program semantics, like program A is equivalent to program B <- in formal verification THAt is the type of an expression, and the implementation of it is the proof.
Of course the Rust language doesn't give you tools to prove that the program is bug-free or such. The proofs only extend to a basic set of properties, but there is a proof system in Rust.
As for other ML languages, they aren't really C/C++ competitors performance wise, Rust is.
https://aws.amazon.com/blogs/storage/how-automated-reasoning...
I was mostly referring to accuracy when I said "good" above, in the sense that they should reflect the actual behaviour of the language they describe.
/s
So, in a near future most people will prefer to have both in order to avoid syntax issues/errors.
You'd think performance would be easy to achieve because you'd just write clear, high-level declarative facts and LLM + good optimiser + proof certification system will get you there in terms of performance. But you'll be surprised that relational/declarative specification gives you so much behaviour 'for free' that choosing what to actually compute from those relations is a very deliberate choice. It starts to look like finding an imperative-like path of demand through the relations. It seems that you get exactly the same problems but one level up.
Linus doesn't have to care, MirageOS already exists for OCaml, and I'm pretty sure there's something like MirageOS for Rust...
We need “a declarative language flexible enough to do what the product requires”
I’m generally cautious/sceptical about the current LLM hype, but if that did ever happen and it worked to a useful degree, it might truly be a significant advance. I’m not saying that just because of the LLMs themselves, though.
To reach that point, we would first need to overcome the classic problems in this area:
1. How can you specify the required behaviour for a system in precise detail without ending up with a specification language that is essentially another programming language with similar complexity to the ones we use today?
2. How do you solve the sufficiently smart compiler problem so that producing reasonably efficient and reliable implementations of those declarative specifications is not only viable but expected?
And then, if you still need someone (let’s call them a “developer”) to carefully specify the required behaviour of the system in detail, and you also know how to reliably generate a good implementation of a specification, how much value is left for LLMs to add in this picture?
Maybe LLMs really could be trained to reliably produce good implementations in that scenario? Never say never, but it seems more likely to me that we would develop deterministic algorithms for doing so. That’s already a very hard problem that a lot of smart people have explored, but if a solution could be found, most likely it would be strictly better than relying on LLMs in this part of the process.
Maybe there would still be a role for LLMs to convert natural language problem statements into specifications? Maybe for systems that don’t really matter, that would be enough and a big time saver. However, I’m sceptical about how much time it would be likely to save for systems that did need to work, where you would still need careful design and review of all the detailed specifications by developers anyway.
Maybe LLMs would end up in a similar role to the scaffolding tools that are popular in some ecosystems today, where you feed in some basic choices and the tool then produces a first pass at the files and code you might need, which you take as a starting point for the real work but without wasting so much time on boilerplate? That seems realistic and useful, but it’s a relatively small part of what would then be the overall development process.
In short, I would love for the existence of LLMs/agents to push us towards those better programming languages and tool chains, but if that did ever happen, I wonder how much benefit LLMs/agents could still offer once developers had the more powerful languages and tools available and could work at a “higher level of abstraction” themselves.
I think the best bet is to let a hundred developers play at it for a bit. There will be a lot of bespoke domain specific declarative languages. They will over time learn from each other to be better and better.
Experiments like GoogleSql’s pipe syntax https://docs.cloud.google.com/bigtable/docs/reference/sql/pi... getting pushed even further and further. That’s where I’d put my money. Cloudflare might be another candidate for building such a programming language for the distributed compute and memory “machine”.
(Also once we are there) I think there will be even better questions: What does programming CRDTs like a blockchain that reconcile across Mars and Earth look like? and in that way, LLMs will constantly be useful helpers to explore the state/latent space.
Granted this isn't usable for all kinds of problems, however plenty of enterprise CRUD software can be easily tackled with such agentic runtimes.
People love to make such claims, but the actual CRUD part of enterprise system, while it’s the primary interface, isn’t the actual value of that enterprise and most enterprise code I’ve seen rely already on frameworks to take care of the technicalities. Most of my time has been taken by what should happen when you do one the CRUD actions. The specs of that can be quite complicated to gather, easy to build, and difficult to verify.
That is left for microservices, aka MCP tools, being called from such agentic runtimes.
We had RAD tools like Access and we still have Excel. Even if they do lack some capability, you can do implement most of the core ideas of whatever features you’re trying to prototype. Actual coding is then to translate that to another platform and solve some accidental complexity.
Those core ideas are what’s valuable and they do not change often over the lifetime of a business. If the software has a good architecture, maintenance cost can be quite low.
For example, instead of coding a whole microservice in e.g. Go, Java, C# whatever, you use such a platform.
The API endpoints are defined, and then you connect a bunch of prompts, everything that previously required special kind of nodes (conditions, db access, calling into micro services,...) are now all the same kind of Agent node, where what you want to perform is described in plain English.
Maybe this other tool provides a better overview,
https://learn.microsoft.com/en-us/microsoft-copilot-studio/f...
I think for now the answer to adaerlangsql+++ is just Rust - but its semantics have always been about human usability.
Humans have this thing where we can only keep 7 things at once and have to juggle our context, but recall seems much more broad than model contexts.
If we were to start designing a language and toolkit based around LLM context sizes, limitations and quirks - how would that look?
Also terseness and operators are one thing, but what if it’s the other way around - English words etc - can have a much bigger vocabulary of things that can be done but can easily be generated on the fly.
For a new LLM language realistically you would need to probably either write or convert a shit ton of software to it first if you are to train an adequate model on top of it …
And also what about “IDEs” for agents? So far they are clumsily using human tools - just looking Claude string along bash loops and greps to try to eek out meaning form code _it itself had written a week ago_ is frankly frustrating.
There must be a better way and some rich agent specific tooling for code exploration and verification.
Anthropic stance has always been “yeah we tested them all, grep is better” but I still am not convinced - just by the fact that it constantly fails one or two attempts before “figuring it out” yeah it’s fast anyway but it could be _faster_ and could allow the agent to “think” in code space more and not have to validate itself at every minute step …
What I want tho would be Rust+Akka for example. There has to be a distributed execution mechanism that is as seamless as Java’s GC. Then the distributed execution mechanism needs to evolve to also be as light weight and “zero cost” while being seamless like Rust’s compile time memory management.
That is what low code/no code enterprise tools have pivoted to.
Check Boomi, Workato, Optimizely Opal, Sitecore AI, PowerPlatform.
This is why you see my comments regarding the way AI based coding is going to, I have already tasted the future in such tools, and even if they have issues today, they will eventually be ironed out.
This result is exactly the opposite. They're verifying at the machine code level, which is totally imperative.
However just like the uptake in SaaS, iPaaS, serverless, managed cloud environments, this means way smaller teams will be needed, and everyone that doesn't get to press buttons at the software factory, will need to find another occupation.
Some mathematicians have observed a similar pattern in the recent LLM proof drops, leading them to suggest that LLMs will hit a wall in mathematical capability just beyond the convex hull of human mathematics. The sort of proofs done in formal verification are a pretty interesting litmus test for LLM reasoning since the systems considered aren't necessarily on distribution (compare with math where the "systems" and structures worked with, and proofs about them, make appearances in thousands of individual books) so the advantages in broad domain knowledge pretrained LLMs have over humans doesn't really buy you much. IMO this observation from Anthropic/Theorem lends more credibility to the convex hull hypothesis.
[0] https://www-cdn.anthropic.com/files/4zrzovbb/website/6867ead...
Yeah agents need to step up their programming game in general. They write too verbose code and are happy with duplicating code. This works up until the code is so big that they can't process the code base effectively.
If I had to guess, if you train agents to write better proofs (better modularized, etc), they will get better at programming in general. Or at very least, better at writing Haskell, since so many theorem provers are just sufficiently powerful functional programming languages. And if you get better at writing Haskell, you probably get a little better at writing Rust too. That's why I think this skill probably generalizes a lot.
So maybe training agents to do math will get them, like, use Creusot [0] or flux [1] or Aenas [2] to write proofs on their Rust code, and even when they don't, they will probably write code in ways that are more amenable for reasoning
How does this compare with the verified crypto from project Everest that is used in Firefox? (Fstar / related to miTLS)
Are you proving more / more interesting things? Do they also have pain when dealing with richer type level stuff like length indexed lists?
I think LLMs have demonstrated tons of generalization already, but I concede that being good at theorem provers don't automatically translate into being good at other forms of programming and vice versa. But the labs should probably focus on generalizing rather than optimizing for each subfield of programming individually.
Also as an aside, I meant that the use of theorem provers for proving theorems is just programming, that is, Lean, Rocq etc. are programming languages. They are functional programming languages and they invoke Curry-Howard as a reason for them to work, like, at all. And that's why their reasoning is essentially intuitionistic
This was to be expected, llms are trained on a very large corpus of data, they 'look' like creative from our point of view, as humans don't have that much knowledge, so, if the LLM proposes something that a human does not know, it looks like creative. But they stay neural networks after all, so very good in interpolation, very bad at extrapolation. Building new knowledge is extrapolation if it's truly outside the convex hull how the dataset.
I usually write code and ideas that are at the border of the convex hull, I haven't seen yet an llm being able to propose a really innovative solution. All the time they reuse building blocks that are already there. And I really tried pushing by making them creating proofs.
If I have an insight on some problem and I ask for the proof for it, it will usually be able to generate the proof, but that proof is never creative, and often it will use novel ideas only if I explain the novel idea. It will not come up with it alone. (And sometimes it's very hard to even explain the ideas, as it tends to return to knew waters)
Its only a data point, but I haven't seen a paper that handle this issue yet, and I don't expect them to magically become good at extrapolation due to the theory behind neural networks.
EDIT: typo
Saying that is like saying everything is about combination because well, it is even the creative stuff if you are pedantic.
The wibbily wobbly dna of humans is how we keep recombining things into new shit. Comp sci absolutely has deep creativity in it.
There is absolutely no DNA recombination during a thought process.
It’s well known that many people think all art is merely copy of a copy, so I’d be curious what field you’re thinking about
For instance, the transition of music from the 1950s to the Beatles, then to Nirvana, hip-hop, and beyond. Before Beatles, there wasn't such thing as Beatles. Before Nirvana, there wasn't anything that sounded like that. Of course you can point out underground bands doing something like that around that era, but stray way back in time to like 1940s and chances of hearing something like Nirvana are near zero.
True art is not easy to make. It is, rather, difficult. If you lower the difficulty to make art, then it is not already a piece of art. It is just another product down the line of plenty of copy cats. Art involves risk taking that AIs I don't think are capable of producing. Art is a medium to express human emotions, and the inherent concept here is that it will end up being consumed by another human being, and it has value because you know that another human being was on the other side of the table making it. Even if you do something you consider art for yourself with an AI, the human being on the other side was, well... you. You prompted it and you guided it. I don't believe people in general would be contempt with an endless stream of autonomous AI generated stuff (if they invent such loop) because it would not only be generic, repetitive and predictable at some point, but also the fact that you know its AI it destroys the whole vibe. Same as if you get an email and you don't know if it was an AI or human behind it. If it was a human being, great, you feel a connection there. If it was AI, well... that sucks to no end, and I guess that is for a very good reason.
Although I'm using art here as the argument for creativity, I believe there may be something analogous to scientific leaps and discoveries. To my understanding, people who seem to be fairly successful in uncover the truths of the universe via science also happen to be pretty good when it comes to some artistic endeavors, even if its only about consuming and appreciating art and not necessarily creating it. So, there might be some link in creativity there. I'm open to be wrong, of course. Creativity is about risk taking and pushing the edges, not re-iterating upon what's been already there.
What if van Gogh turned out in hindsight to actually not have had “subjective experience”? Would this diminish his art? It now no longer “true”?
I love that “convex hull” analogy. LLMs can certainly serve as a channel for knowledge transfer. They can help spread knowledge and know-how throughout society, enabling breakthroughs that were simply held back by practical limitations (e.g. lack of money, time, or expertise). Personally, I think LLM is more valuable as a tool for democratizing knowledge than as artificial intelligence.
> The most striking feature of agent proofs is that they are verbose, repeatedly spelling out details about the program’s execution: specifying the contents of CPU registers, explicitly writing out integer conversions, explicitly spelling out that many different addresses are all distinct from one another, writing out the exact contents of stack addresses, explicitly considering every possible branch in a function, etc.
> To be sure, these details are important to precisely reason about the execution of code. However, human proof engineers would have immediately introduced abstractions to factor out these types of repetitive specifications.
- - -
This matches my experience when I look at the tests LLMs write to check their own work when I’ve given them a task. The tests are almost universally terrible because they hard code everything in the most brittle way possible. They are nearly useless for regression tests because if I change anything about the source, even in non material ways, the tests all break in stupid ways that aren’t checking any important properties.
If I have the LLM make the then it also has to rewrite all the tests in a new episode of brittle concrete hyper-literal tests. The concept of a regression suite is non-existent.
It’s probably just as well. Having the implementer write the verification is generally a bad idea with people, maybe the problem of carrying over assumptions and blind spots and misconceptions applies to LLMs as well.
One might say it’s operator error, and I’m underspecifying things, but if I have to go to such elaborate lengths to get it to do what I need, I’ll just implement it myself.
Nobody (sane) does that.
Lots of people have the implementer write the tests. But this only seems like a bad thing because of an unfortunate terminology collision:
- Microsoft culture: tests are adversarial verification.
- Google culture: tests are executable documentation.
Both of these things are important. It's really unfortunate we call both of them "tests".
At Microsoft, (verification) tests are written by a different engineer than the one who wrote the code under test. VLSI/Hardware works like this too.
At Google, (documentation) tests are written by the person who wrote the code, because it's their job to document it, and because the point of documentation-tests is to make sure other people who modify your code don't break it.
This is not just plausible but in fact the most likely result.
We already have plenty of evidence of this phenomenon in programming. LLMs are awesome for working on human-written or at least human-reviewed codebases.
But when you set them loose without a human around to force them to refactor their code into something that fits in meatbag-brain-sized contexts, they drift into the ghastly nightmare of the Anthropocene (go ahead, take a look at the leaked source code for Claude Code). They can handle this for a while, especially if you're doubling your model's weight count every four months.
But when you stop doing that, they choke on their own spaghetti.
It's like Feynman said about teaching -- great theoretical physicists need to re-explain the basics to students from time to time in order to force them to come up with not just the correct physical laws, but the simplest version of those laws. Take away that constraint -- IAS or LLM -- and eventually it all goes wrong.
I mean, even just that would prove to be a very productive workhorse - potentially being able to automate away almost every white collar job.
The elusive 100%-coverage formal spec that covers every intended and unintended input, the interests of every stakeholder, and every possible user behavior? In the vibecoding era? No, the page has the decency to acknowledge this doesn't exist.
In the end, they settle on finding crashes with a conventional fuzzer, fixing crashes, and then... writing a formal proof that the crash is fixed? That seems... pretty pointless? Am I missing something here?
> Proving that a fuzz test has no more crashes to find is more significant than it sounds. It’s common for fuzz tests in real-world code to test for violations of meaningful high-level properties, such as encode-decode roundtripping, idempotence, algebraic laws, differential testing, self-consistency, or equivalence to reference implementations. For example, a fuzz test for the LZO compression algorithm asserts that if you compress an input, then decompress it, the result is the same as the original. If the property does not hold, the program crashes—so proving the test never crashes is equivalent to proving the property itself.
However, you're correct that this is not formal verification in the sense of a correctness proof against a full specification validated to capture what the program is intended to do. Pretty impressive though.
Translating your program to Rocq is vastly easier than to write a proof for a binary.
What they did is tried to prove that the conventional fuzzer won't find crashes. Where they found counterexamples, they fixed the bug and tried again.
In essence, a fuzzer takes random samples out of a space of possible inputs that could crash. They proved that nothing in the space of possible inputs could crash.
This is a strictly more powerful result than a fuzzer could give you.
Verification: Code does what it says.
Validation: Code does what Specifications say.
Specifications: Were hopefully correctly modeled to the Problem.
In IEEE terms:
> Verification: "Are we building the product right?" > Validation: "Are we building the right product?")
You can write mathematically flawless code that highly efficiently solves the wrong problem.
---
While I think formal verification is the future (essential for cybersecurity), it's not a silver bullet for the other 2 items, which are way more ambiguous. I think however they can all iterate on each other and improve the project overall, but it still depends on competent steering
If you have had experiences with good approaches for verification Validation & Specification framework, do let us know about them.
Isn't this the exact opposite of what "formal verification" means? First sentence on Wikipedia [1]: "Formal verification is the act of proving or disproving the correctness of a system with respect to a certain formal specification or property."
In formal verification, "the specification" means the encoded claims that will be proved, i.e., the lemmas and theorems to which the proofs directly correspond. When we use proof assistant languages (e.g., Rocq, Lean) to accomplish the verification, this means the specification is given as a type.
I think this is not what the parent comment had meant by "specification"; it seemed to me that they meant that word to refer to the human-accessible document that states what the program ought to do.
The translation of an informal (human-readable) specification into a formal specification is not always straightforward, often due to issues on either (or both) end(s) of the process. You can write Rocq code that type-checks and thus "is verified" in the sense that the type-checked code conforms to the formal specification, but if the claims you proved are not what you had intended to claim, then that verification is not very helpful.
So that is where the parent comment introduces "validation" to mean (in my words) the process of ensuring that your formal specification matches the informal specification, such that any formal verification that occurs is useful and meaningful.
Verification: code does what the specifications say
Validation: specifications describe something we wanted to build
Specifications don't need to be lower-level. They also compose nicely. Ie you can figure out how to formally specify a 'this doesn't crash' requirement once, and then re-use it on all your projects.
I.e. a field in a government form for residence permit might validate if the date entered is between the applicant's arrival date and three months later. And screw the applicant who wanted to apply for the permit before they landed in the country (this is a not invented example).
Also, since I worked in "software validation", I feel like it's important to note that the dictionary definition is different from practice. For the most part, the task of validation is the one that should culminate in the testers OK'ing the shipment of the product. Typically, testers, as well as the rest of the company involved in the shipping, are painfully aware that the product doesn't meet the customer's requirements (or any formal or informal requirements). It is simply declared "valid" because the potential damage is assessed to be manageable. I.e. a product may as well be declared "valid" while having a list of "known defects".
> independent verification & validation (IV&V)
> A comprehensive review, analysis, and testing, (software and/or hardware) performed by an objective third party to confirm (i.e., verify) that the requirements are correctly defined, and to confirm (i.e., validate) that the system correctly implements the required functionality and security requirements.
In my experience it's more common to use "verify" for the lower-level "conforms to specs" and "validate" for the higher level "are the specs right" but in other areas it might be different.
In other fields (I'm more familiar with medicine), there are "bibles" that serve as a medium or the source of common language between professionals. If you are talking about radiology, then you open Basic Radiology by Chen, Pope and Ott on the designated page, and read the definition. And you know that another radiologist will do the same, and so you both have the same reference point.
In programming, even the basic stuff like variables, functions, types etc. aren't defined universally. Plenty of local environments will offer conflicting definitions (and often the definitions themselves are internally inconsistent).
Unfortunately, bodies like Wikipedia cannot serve as an authoritative source on such questions because instead they record the current state of events. They can't choose which definition to follow if there's no authority respected by the vast majority of programmers.
AI verification: AI meticulously abuses all available loopholes to deliver answer expected by operator, rather than actually responding to the problem.
Simplest example: proof that `x+1 > x` (borderline impossible)
- Verification: Are we building the product right?
- Validation: Are we building the right product?
My intuition was different. To me verification is a process while validation is that the outcome of that process. As in: to validate the "+" operator, you verify that 1+2=3.
Looking at the Wikipedia article https://en.wikipedia.org/wiki/Verification_and_validation the definitions are not very clear and seem to depend on the context, tough the general idea is that of the LLM answer.
Funnily enough, the https://en.wikipedia.org/wiki/Engineering_validation_test Wikipedia article is introduced with "An engineering verification test (EVT)..."
It seems to be the kind of thing where everyone has a different idea and they are often conflated, making the distinction almost meaningless without context. You can give a precise definition for your project, but it may not apply elsewhere.
Note about using LLMs: I often like to use LLMs to settle these questions. Not because LLMs are flawless, far from it, but because they work by generalizing the content of their training dataset, they should do a pretty good job on extracting consensus. It fact, it is all they do; when a LLM tells the truth, as it is often the case, it is because the consensus is often the truth.
The description was most likely given in a natural language, with many assumptions about the shared objective reality.
Today, we have LLMs, which de facto (but with significant flaws) formalize the interpretation of natural language, as well as the shared objective reality we inhabit. They are becoming closer to the truth than any individual human. (Their construction is a wittgensteinian program of sorts.)
So we can take an LLM with the prompt "Respond according to the following specification:" plus the original specification/requirement, in natural language, itself, as a program A.
Then we can take the written program itself, together with the emulator of the machine it runs on, as a program B.
We can feed both of these into some theorem prover - and formally prove that program A and program B give identical outputs on identical inputs. That's most likely the best we can do, ever.
(Or we can, in theory, develop programs this way, as a solution to the following question: Which program, when run on the given platform, gives provably identical answers to program A? That's a general program synthesis problem.)
I wonder if not having to deal with women as a straight man frees up some part of the brain for more productive uses.
Unfortunately, I love women so I can only be an application programmer.
1. Vision: what we want (our intent)
2. Blueprint: the spec we wrote (our design)
3. Inspection: checking what we built against the blueprint (the proofs)
This research makes the inspection close to perfect. But an inspection only checks the blueprint, not our vision, so a house built from the wrong blueprint can still pass a perfect inspection. The other half is making sure the blueprint matches our intent and stays that way while agents build. I'm working on that, so I think this is complementary:
Now I have it working on a verifier for the bytecode transformations the optimizer uses, also using the static verification approach, to discover them all and ensure they are all valid. This one is seeming to be on track to making it fast enough to work on a real grammar as opposed to the 'academic grammars' the literature typically uses to prove the lemmas. Claude seems to be fighting this and has been working on the same refactor for over a week now so, we'll see...
https://martin.kleppmann.com/2025/12/08/ai-formal-verificati...
All of human knowledge, experience, distilled down to idempotent instructions and code for specific tasks, functions, situations is fully testable against a near infinite amount of fuzz and attacks.
We do not question the strength of steel if properly treated.
Code is no different. We will enter the point where code is finally trusted as a carabiner and rope for the life of a climber.
Preferably, I wouldn’t trust my life to a calculating device running on AA batteries while dangling from a rope.
We also have fully redundant systems. The elevator for example required Otis to do this fantastic demonstration 150 years ago and now we don't think twice about it.
Do you know how elevators work now? Their safety mechanisms? Planes are 10x more likely to cause death.
There's something called safety regulation. An installed elevator is very likely to have passed all the verification necessary for it to clear the safety bar. Same with the other devices you listed.
As for general code, it's mostly based on trust. But I see practices endorsed by the AI providers and trust is very low on my end.
If AI can stress test the code faster, more correctly than humans, the quality and regulation will follow.
That’s fair, including insulin pumps over Bluetooth with known vulnerabilities. Many vulnerabilities might be fixed or formally verified if they are part of the architecture.
> Do you know how elevators work now? Their safety mechanisms? Planes are 10x more likely to cause death.
Both rely on inspections, routine maintenance, procedures, and fail-safe hardware afaik. Just like climbing gear.
Would formally verified software add anything? For example, could it cut the need for inspections or software maintenance? I think neither is going to change.
But what might change is that the specific spelling error on an elevator display is formally verified. It becomes about coziness with impressive amounts of paperwork that only a few people can understand.
Just changing one statement requires new verification, which is why formally verified code currently is not touched but ported verbatim into new projects and “rewrites”. That cost may decrease, which is nice but also not nice: the systems you currently want to formally verify are systems you might not want to alter without high friction in the first place.
I’m hopeful it will produce more robust software, and I’m by no means against it, but I’m skeptical of producing more when we might want to produce less.
I am very curious about this now. Bad software is now free. Stability and security sell better than ever.
It's absolutely cool to see this sort of validation process get cheaper and easier, but it means nothing if no one cares enough to do it. EAL1 certification can be as cheap as a beefy server, but it's not commonly done because effectively no one cares.
As microsoft learned with the zune just because it's cheaper or better at the same price doesn't mean anyone will use it. Culturally, we have to make the effort of verifying code worth it.
I could probably use less stuff in my Claude files tbh. I wonder if that sort of thing is being pushed out. Still, when the marginal cost of running a bunch of stuff in a shell or REPL is 0, it should be the go-to for the LLM, not something it needs reminders to do.
It’s exciting to see how low the barriers to fuzzing and formal proofs and higher verification standards like property based testing has become! It’s just a shame this LLMs are what it took, and even then adoption in the industry is slow.
1. Prove the ASan-instrumented binary doesn't crash
2. Prove the non-instrumented binary doesn't crash
3. Prove the instrumented and non-instrumented binaries have the same behaviour (under a particular model of a Linux process's behaviour)
This is a clever hack for automatically generating a formal spec for an existing program, but the fact that you need ASan in there makes it seem like this is less general than it sounds. Could the agents directly prove that out of bounds memory accesses don't occur on the original binary and skip ASan altogether? It's convenient to let the spec just be "it doesn't crash", and ASan provides a crash when the other bad things you care about happen (i.e. out of bounds memory accesses), but I wonder if modelling the memory accesses directly would simplify things.
But you're right that don't need ASan at all if you've encoded semantically meaningful properties. E.g., if you assert(decompress(compress(x)) == x), proving that you don't crash requires proving that compression round-trips. (Similarly if you have a reference implementation.)
The upshot is that the spec doesn't need to be written in a proof assistant and can instead be encoded as an end-to-end test.
Alloy is a tool I tried to learn many years ago, but I never learned it well enough to use it for formal verification of a complex production system. Credit goes to agentic coding tools for making it a reality.
I feel like these people aren't really experts in the field of testing... Linux is not known for its testing... there's plenty of good things one can say about Linux, but great testing isn't one of those.
Now, things that are well-tested are things that do critical stuff, like avionics, power-plant control, medical equipment, storage... It's software from a different league.
Linux is too big, too dynamic, too distributed between different authors to hope for great testing. And it's OK. I'd rather have more people being able to contribute, not being constrained by the difficulties of the testing than have a very well-tested and borderline useless system.
How do you actually know what the LLM proved is what you want?
I was going through an experiment trying to spec out a simple caching system in Lean. I was getting Gemini to help me run through doing this, step by step. At one point it writes out this statement with a proof to show something, the specifics of which I forget, but it was some simple property of the cache. I stare at it for a while thinking to myself this can't be right, it was some sort of plain tautological statement that didn't really say anything, like saying 1 = 1.
I give it to Opus 5.5 and it basically confirmed my gut feeling that it was useless.
I'd like to rely more on formal verification. I like the idea of starting out with specs in a formal setting and designing software that way. The problem is it's hard to do right, and my point is even with AI, it's hard to do right.
It’s to easy to write an assertion that looks like it checks what you want it to, and gives you a false confidence when it passes, only to figure out after a field failure that it wasn’t checking what you thought at all.
But I’d pay for a commercial set of properties and assertions that had guarantees, and not worry about their complexity. For something standard like cache protocols and bus protocols.
Other cases it needs to be pretty straightforward to grasp by a peer reviewer in minutes, or it’s not worth it.
But when you can hit the sweet spot, a set of easily understood properties (or complex but trusted properties), formal can save massive amounts of time.
We will move into formal verification alongside AI tools, thus generation of executables via translation to 3 GLs is going to be a transition step, just like Assembly coders wary of optimising compilers always wanted to manually check the generated Assembly code.
And yes, many of us will have to search another source of income as an outcome of "progress".
Trying to become even lazier by skipping code reviews and then vibe-coding formal software verification will get you into trouble.
In my experience with software verification, perfect is the enemy of good. My recommendation is to start with a software design you actually understand, and then try to understand how to map your requirements to something you can prove.
So why do people work? For the vast majority of people there are three main incentives:
1. Survival. You need food and shelter. Most people don't own anything so have to do whatever the owners want them to do to meet basic needs,
2. We get satisfaction from helping, pleasing and impressing other people,
3. We get personal satisfaction from doing a good job, being proud of our outputs and learning and honing our skills.
A bad job like factory work or unskilled labour only has incentive 1. Nobody takes pride in how well they've cleaned a toilet, nor does anyone appreciate it. Better jobs get 2 and 3 as well. We generally got all three incentives in abundance.
What we're seeing is the loss of incentive 3 and inevitable eventual loss of 2. Those were what drove us to do more than the bare minimum that's required for 1. That's why we would spend time thinking through things, struggling with problems, learning and bettering ourselves in the process. Now there's no personal satisfaction because an LLM could do it. And we know that there's nothing really stopping other people doing to too, so what we did soon won't even be impressive or help others (although we can cling on to it for a little while maybe).
We have a few options going forward. On a personal level we could try searching for something that gives us the satisfaction we once had, or we could just accept that we'll become wage slaves likes so many others. On a societal level we could all decide to minimise the amount of work we do, given that it's much less enjoyable now.
I see two possible ways forward, not necessarily mutually exclusive.
* Make AI work with languages with reduced complexity. A lot of language complexity exists to make it (surprise!) easier for humans to deal with the language. For example, generics in a language like Java make it easier because they allow the programmer to write many similar programs just once. And because people are prone to make mistakes when working on repetitive code, generics are useful for people. AI, on the other hand, doesn't get tired. It doesn't care if it needs to implement the same template for a different type a dozen more times. So, if we give AI a language without generics, it will be just as happy, but it will eliminate a whole class of potential errors related to eg. up/down-casting of generic collections. Similarly, we could remove "dangerous" tools like infinite loops, or outlaw some system calls, producing less generic / more purpose-built languages (like PostScript!) Perhaps projects like OMeta could see some revival in this light?
* Replace, as much as possible, the work of testers with proofs, but not AI-generated proofs! The formal specification (which is another way to look at the proof, at least its statement) is where the human being needs to provide input to AI. If it's not possible to read the whole generated code, we need a tool more reliable than a test to convince ourselves that the code does what we want. Formal verification, or, even better, tests generated dynamically from formal specification (there's no need for AI to do that, this can be an entirely deterministic process) should be the way for the human to stay in the loop.
"What TLA+ can and can't check" https://news.ycombinator.com/item?id=49909056
"The internet discovers TLA+. Now what?" https://news.ycombinator.com/item?id=49863600
2017: Leslie Lamport: Video course on TLA+ (328 points, 74 comments) https://news.ycombinator.com/item?id=13918648 (219 points, 2018, 17 comments) https://news.ycombinator.com/item?id=16956778
2017: Writing correct lock-free and distributed stateful systems in Rust, with TLA+ (374 points, 94 comments) https://news.ycombinator.com/item?id=14373359
2019: TLA+ model checking made symbolic (197 points, 51 comments) https://news.ycombinator.com/item?id=21662484
2019: Introduction to TLA+ Model Checking in the Command Line (176 points, 44 comments) https://news.ycombinator.com/item?id=18937214
2019: Learn TLA+ (387 points, 92 comments) https://news.ycombinator.com/item?id=19661329 (310 points, 2020, 58 comments) https://news.ycombinator.com/item?id=22393653 (254 points, 2022, 64 comments) https://news.ycombinator.com/item?id=33010645 (350 points, 2022, 75 comments) https://news.ycombinator.com/item?id=31952643
2020: Using TLA+ in the Real World to Understand a Glibc Bug (166 points, 76 comments) https://news.ycombinator.com/item?id=24958504
2026: Hunting a 16-year-old SQLite WAL bug with TLA+ (239 points, 29 comments) https://news.ycombinator.com/item?id=48730953
...
https://hn.algolia.com/?dateRange=all&page=0&prefix=true&que...
Couldn’t it very well be that you proved something that wasn't actually your program?
You can go a step farther and model the instruction set and architecture, and which point you can make proofs about the final binary directly (thereby sidestepping the problem of compiler bugs). At this point, your assumption is just that your physical hardware actually matches your model.
Correct. It can happen, where the actual code, could diverge from a lean representation of it, in a glaring or subtle way.
You can do it backwards. You declare the properties you want the resulting program/function to have, using a proof assistant like Lean, then prove that a program exists that meets those requirements, and the proof assistant spits two things: a confirmation that the proof is valid, and a piece of code that implements the proof, in the form of computer code.
At least that's how the proof assistant Coq would often be used. You still have the challenge of ensuring that you have defined the properties you really want in the first place, but at least it solves the part where you want the code to meet the specification.
For things like programming languages we often have tedious, but slow, semantics that can be directly implemented in a suitable language. Then really all that a compiler or interpreter is is a faster version of those semantics.
If you are able to show correspondence between the fast and the the correct version, then you can toss the correct and slow version without even ever running it and just defer to the provably correct fast version.
Most software is ultimately like this
[1] https://github.com/gregwebs/skills-sdlc/blob/main/skills/rus... [2] https://github.com/gregwebs/skills-sdlc/blob/main/skills/ver...
> This technically also means we have to trust the hardware, OS, OCaml compiler that the Rocq proof checker relies on.
It just so happens Claude and I recently did an independent implementation of OCaml and ruled out malware in the compiler bootstrap via DDC (and also by achieving byte identical outputs).
https://discuss.ocaml.org/t/ocaml-compiler-implemented-in-c-...
So, we can at least rule out "trusting trust" malware in the OCaml part of the stack and up. (Rocq does not have trusting trust concerns since it's implemented in OCaml and C)
Imagine having a formal spec for reality!
"Quantity has a quality all its own."
OpenAI wrote some lean that pass the validate, write a math paper that feel plausible, but the paper don't match what's in lean.
Anthropic is now translating programs into Rocq proof. The same can happen.
Don't get me wrong -- this process can help catch some bug. but this is far from a proof
If you need LLM, it is not formal.
Formal software are not LLMs.
LLMs/agents can use formal software.
The limit of formal software is the formal model itself, roughly speaking the binary specification is designed by humans. If the formal model is "wrong", bravo, you have formally proven a "wrong" model...
I think there are more details, but this is the gist of it. However, you need to manually verify that the LLMs produce Lean definitions that actually match your problem statement.
Is formal verification the path forward? Meh... I dont think so. Does it have applications in some areas: yes. But this is just more robust "unit testing".
Anthropic keeps trying to convince you that "one agent" will do the job. It does so with the statement "We built 36 small verification tasks from real OSS-Fuzz code. Opus 5.5 proves half of them with about 40% fewer tokens than Opus 5. We expect this trend to continue as models are trained on long verification tasks."
But this is not the path forward. Robust E2E, durable (can your app go from python to rust with out loosing tests) Simulation/Emulation tests are the way. This is an "in bulk" and "brute force" activity. Go look at TigerBeetle for an example of this in practice. Go look at how oxide is doing testing.
Can a swarm of cheaper agents write these tests more effectively that Anthropics premium products. I assure you that it can.
If you look at OAI's actions (hugging face hack) and anthropic own publication on its version control AI is not a best of breed solution its a brute force hammer at it till you get what you need solution.
I think learning to code will still help with the other things here - its a good first step, even if its now obsolete on a direct level. Like how its useful for mathematicians to be able to calculate by hand even though calculators exist - it gives intuition for how to operate the tools and check results
I wish people would learn a little computer science before making this kind of impossible claim. And I wonder how many people read claims like this and accept them without investigation.
The Turing Halting Problem (THP) invalidates the above claim, on all nontrivial software systems, forever.
The THP (1937) is derived from Gödel's Incompleteness Theorems (1931), and the latter are not a matter of opinion.
For those with limited attention spans, ask yourself this: How does the foolproof program checker check itself?
Pop-sci explanations of the halting problem have probably done incredible damage to formal verification as a whole. Mostly because it makes people with only the most cursory understanding of it go "why bother, it won't work anyway."
No, they aren't -- they are all Turing-complete, look it up. The THP applies to all non-trivial programs, meaning programs that support Peano arithmetic or anything more involved. That limitation certainly applies to all the programs you're describing.
> Pop-sci explanations of the halting problem have probably done incredible damage to formal verification as a whole.
That's pretty funny. It's not every day I hear Alan Turing and Kurt Gödel described as purveyors of "pop-sci".
> Mostly because it makes people with only the most cursory understanding of it go "why bother, it won't work anyway."
I won't try to list all the logical fallacies in your argument. You could do that if you were so inclined.
That means we can't make the claim that a particular program, running in that language, is error-free. I don't get why people find this so hard to understand.
> That would imply you could never know anything about a program.
No, it means we can't make the claim that a program is error-free. That's the simplest statement of the Halting Problem.
When someone applies Lean to verify the correctness of a chain of logic, they must remember than Lean cannot be proven to be error-free, because ... wait for it .. Lean is Turing-complete.
But most real-world programs are maybe not that "expressive" since we don't even want them to be capable of infinite loops (since those would often be denial of service vectors). So you should usually be able to prove that they halt (and presumably other properties as well), especially when you allow agents to rewrite things to pull out invariants that make proofs easier (as they did).
And for cases where getting clean invariants are difficult, I imagine you can just hack it by having some cutoff which trivially ensures things always halt. (Not sure what the equivalent would be for "no bug" proofs, probably rejecting things that are technically valid input per spec but seem unusual?)
I would say, in practice, you are more likely to encounter complexity barrier (we don't know how to decide some NP-hard problem fast enough) to proving things about your program than you're to encounter a true undecidability barrier (Rice theorem).
Although the prover might be smart enough to say, "this function is getting kinda complicated, let me model it as a random variable and see if it's enough". I think LLMs can kinda do it but not sure if your typical theorem provers can (it's on the level of being able to employ probabilistic proof techniques).
Yes, true, they just ignored it and made unsupportable claims. And the Halting Problem cannot be "solved," that is what the Halting Problem says and proves.
Here's the claim:
> Ideally, such techniques could find and patch all bugs, and then provide some proof that there are no more to be found.
The claim "Find and patch all bugs" is false. This is computer science 101. It is not possible. All one can say is that the claims are well-repeated. They aren't supported at all.
See for yourself:
https://github.com/Giancarlos/Culebral
Anyway, my custom (currently paused because I'm taking on a much more ambitious compiler project with Claude... just to push the limits) language can build ASP .NET applications, and a bunch other things. I also took the Rust approach to types, all method signatures must have types defined, type hints are inferred when declaring new values from the value on the right.
I've also had Claude rewrite legacy C# projects with 100k+ lines of code, fully in Rust, long before Opus 5.0. I've spent the last year pushing the limits with Claude, including reimplementing existing software, which people are catching on to now, and I've managed to get rather far in some cases.
So I wouldn't be surprised if yes, Claude can implement Python, mind you, there's Python interpreter coded in Python in what was it? 500 lines of Python? You can build a Python stack machine bytecode interpreter in like 60 ~ 80 lines of Python code.
Would not surprise me if you can trim a C programming language interpreter down in terms of lines of code when you rewrite it in Rust especially when you have access to a much more functional language, not to mention Rust took the best bits out of OCaml it could to make itself very efficient at writing compilers / languages (so they could write their own compiler in Rust...).
I am also having Claude building me a much smaller compiler, which started out in under 500 lines of Python, but as I got more ambitious it had to write more code for my language, it was meant to be a slightly less restrictive Go, the Python basically converts the syntax to C which then compiles anywhere. Havent put that one on GitHub since I'm still tinkering with it.
Right now I'm working on a compiler / runtime for a more complicated language than Python or C and while its "slower" I know that once it's done through this run I'll be able to have it focus on optimizations, especially with rigorous tests that some languages have to test their compilers. I have plans to run back to Culebral, but I have to scratch a bigger itch I've had, people like you who've told me repeatedly that an LLM cannot be used to build a compiler. So here I am, slowly chugging at it, getting decades of developer effort worked through every week.
If I'm wrong, so be it, if I'm right, it'll be fun to release. :)
I looked at a similar project to mine, done by someone for several years now, they're working 100% solo, I'm already where they're at, with several things they don't yet have.
They're often simpler, and whole classes of security vulnerabilities are mitigated by design. My favorite example is SQL injection mitigated by having proper access controls in the DB. Why prove about every SQL statement that it cannot be nefarious, when we can just prove it about the connecting user? The user access carries the intent of what the application program wants to do with the database, in a separate channel, independently of the complexity of the application.
Nothing solidified Sharpee more than “compiling” this manual chapter by chapter.
But even that left gaps. I then designed a true DSL called Chord that compiles to Sharpee and this really ramped up the solidity of Sharpee.
no idea what you are even talking about
My point was made. Use GenAI to write a manual for your DSL and then use GenAI to “compile” every chapter from a dumb context-less state. You can validate your language in a week or two.
Is this end to end verification? Cause this sounds closer to validation than verification.
Did they solve Halting Problem?
And like yes, it does just launder defects to a layer higher, but another way to phrase that in this case (and in many other cases) is that it raises the bar.
Instead of defects being mostly about nonsense minutia (relative to business logic), they are about actual design decisions and their correspondence to reality, i.e. the actual original goal and point of this god forsaken, navel-gazing field.
I didn’t read the whole article, just the appendix. There they talked about having Claude write a python interpreter. Then they had it write a set of properties to test and they vetted the properties against accepted existing python interpreters.
Proving two things are equivalent is a major component of formal.
For everything else, formal is only as good as the properties you specify. A long standing problem. But it’s a problem for all verification. If you write a shitty tests, you get shitty verification.
A key difference I think is that the same skills used for evaluating and reviewing application code apply to reviewing test code. That’s not really true for formal.
Or are they just saying we can use LLMs to generate a piece of code/test that can do formal verification?
People, hide your test suites from the criminals.
If I recall correctly the only news they used to post were new models updates, while now they have expanded their topics, or so I feel.