181–186 of 186 posts
In other words, the code was proven correct according to spec by LEAN. Which is exactly what LEAN claims to do.
claude making a statement that sounds impressive but it is actually the first codebase it has ever analyzed. "This is genuinely one of the most memory-safe codebases I've analyzed."
It is definitely not the first codebase an extensively RL-trained Claude has ever analyzed. How do you think it got so good?
claude making a statement that sounds impressive but it is actually the first codebase it has ever analyzed. "This is genuinely one of the most memory-safe codebases I've analyzed."
It is definitely not the first codebase an extensively RL-trained Claude has ever analyzed. How do you think it got so good?
Earlier quoted context omitted.
It is definitely not the first codebase an extensively RL-trained Claude has ever analyzed. How do you think it got so good?
Meaning it has no episodic memory of any of those analyses that it has done.
The spec-completeness problem here is the same one that bites distributed systems verification: the proof holds inside an operating envelope (no adversarial inputs, trusted runtime, bounded sizes), and the interesting failures live at the boundary. TLA+ has the same property - you can prove liveness under a fairness assumption the deployment silently violates, and nothing in the proof tells you when reality drifted o…
As someone who has discovered a bug in a CPU that was previously unknown to our chip vendor, I would like to point out that the rabbit hole is deep. On the other hand, I've discovered thousands of bugs that weren't hardware bugs, and dozens of bugs due to people not having read hardware errata documents, so just formally modeling what we can model will absurdly reduce the bug quantity.
Earlier quoted context omitted.
A missing specification in the proof of lean-zip, a lean component, is a real problem to the philosophy and practice of software verification. To illustrate, let's say you want to verify a "Hello world" program. You'd think a verification involves checking that it outputs "Hello, world!". However, if a contractor or AI hands you a binary, what do you need to verify? You will need to verify that it does exactly print…
> A missing specification in the proof of lean-zip, a lean component, is a real problem to the philosophy and practice of software verification. Every time someone makes this point, I feel obliged to point out that all alternatives to software verification have this exact same problem, AND many, many more.