Join the discussion
Write your take first — we'll ask for email only when you're ready to publish.
- Hacker News
- > Aside: verified assembly
This isn't new, it is actually part of how Dafny came to be, another formal verification programming language.
"Safe to the Last Instruction: Automated Verification of a Type-Safe Operating System"
https://www.microsoft.com/en-us/research/publication/safe-to...
However so far hardly anyone in mainstram cared about verified assembly, maybe now with LLMs.
"Programming Language Design and Implementation in the Era of Machine Learning"
by pjmlp - OK so this article is sort of about formal proof automation, but it seems more practically about Zstandard, which I very much enjoyed reading.by jason_s
- Yeah, this is really cool. I'm now deep in the rabbit hole of FSE encoding and ANS & tANS. The last time I poked my head in here, range encoding and arithmetic encoding were the state of the art for fractional entropy representations, but they both sucked. This is a million times better and so simple that I feel like I should have invented it myself.by andrewla
- I'm convinced Math is the canary for what's going to happen to knowledge work. Coding was ahead in harnessing early LLM capability, but Math, given it's pure form, has aleady racing ahead.
The dimensions to notice are: Research speedup, practitioner expertize, labour dynamics, junior entrants, world impact.
In that sense it's a canary, whatever happens to Math, will in order flow to other sciences in-order of purity: Computer science, physics, chem, bio, social sciences.
by anilgulecha - Math is the opposite of a canary because it's possible to generate infinite amounts of synthetic training data for it, unlike almost every other kind of knowledge work where correctness depends on external input.by logicchains
- Proof automation will make things a lot easier. I'm not entirely sure that it's the only thing required, but it's a big part of the thing required.
What's more interesting to me is, how do we prove that the business intent is accurately encoded in the code? This is a different problem. Not "is the logic internally coherent," but "is the logic going to give us what we want?"
And how do we make sure that the logic keeps giving us what we want, iteration after iteration?
I've open source a tool, Drift, for this purpose. So far, biased and anecdotally as its builder, this has been the missing layer. It works because the spec is treated as a duplicate of the code, written and committed in the repo and kept in sync with hashes. The LLM then checks for diffs manually. There are ways to use perplexity here as well. Here is an article about how to get started. https://monarchwadia.medium.com/how-to-make-your-agent-more-...
Doubtless, many more automations will come. We live in very exciting times. It has been a while since a new technology affected every corner of software engineering with such depth of change. This might be unprecedented.
by monarchwadia - > We now have LLMs which, combined with proof irrelevance, promise to be an extremely capable form of proof automation. With sufficient amounts of automation perhaps you don't need to worry about proof engineering nearly so much. You still need to avoid blowing up the type checker but, in my limited tests, LLMs can avoid that. Potentially, LLMs suddenly make dependent-type systems dramatically more practical.
When I've used interactive proof systems like Roq, I'd often kinda code myself into a hole by cutting along the wrong axes and not specifying my problem in a way that's easy to prove. After all, this is just like in math: you really want to cut at a problem the right way to get to the easy proof.
I think people are discounting how important that decision making is. It's not just about whether an LLM can churn through specific proof strategies on a problem, but also about how to pose the problem etc.
I'm not saying LLMs can't help, but I think it's less that "proof engineering is not needed" and more that "when these tools are used in the right way, proof engineering is easier". Because at the end of the day these tools work well when they have the right kind of foundations in the first place
> AWS made LNSym: a semantics and simulator for AArch64. That's cool. Perhaps we could use it to show equivalence between an optimised assembly implementation of some functions, and their Lean counterparts, and then use the assembly code at run-time? Then we could let LLMs rip at optimisation and they couldn't introduce any functional bugs. Verified assembly is well-trodden in crypto implementations, but perhaps now it could be cheap?
Trying to one-shot compcert might be hard! Thinking about it and planning it out might make it easier though...
by rtpg - Yeah computer proof writing involves choosing good abstractions at every turn. LLMs aren't great at that yetby vatsachak
- I'm very bullish on proof automation as well. I'm currently researching AI for algorithm design and using automated theorem provers to get formal guarantees for generated algorithms.
To make a shameless plug, I'm working on a Python package called OpenATP [1] to make it easy to benchmark different models/harnesses for automated theorem proving. It supports running agents in Docker containers or Modal out of the box. If you try it out, I'd love to get your feedback!
I recently wrote about the surprisingly good performance I saw from Grok [2]. On more challenging proofs, Grok doesn't keep up with Opus/Fable and GPT 5.6. I was recently blown away by GPT 5.6 Sol. It's persistence in closing out proofs is unparalleled from what I've seen so far. OpenATP also supports Kimi and Leanstral [3], among others.
[1] https://github.com/henryrobbins/open-atp
- I had a funny experience recently, during a vibe coding bender. This was a few weeks ago when these very impressive new models came out, a whole new class of intelligence and autonomy! So I wanted to see how far I would get, letting the computer handle all the details.
Eventually I did take a look at all the new code, and found that one of the main features had been implemented completely backwards, in a way that was pointless and completely defeated the purpose.
(An LLM also pointed that out, so I guess it must have been a different one which implemented it? I'm trying to get them to sign their names in the commits...)
These new models are very thorough and responsible however, so of course it had written a copious number of tests, and of course all the tests passed! I found this very amusing. It had diligently proven the correctness of the incorrect functionality!*
I've been thinking about how cool it is the AI can assist with writing proofs now, and how we can use this new ability to boost the correctness of our code. It later occurred to me, however, that formal verification would not have helped in this case. It would have just formally verified that the wrong thing was correct!
--
*Yeah I know tests prove the presence of bugs but not their absence. Couldn't think of a better way to phrase that though.
by andai - > An LLM also pointed that out, so I guess it must have been a different one which implemented it?
Or the same one a minute later. LLMs are the software equivalent of Patagonian weather.
by chrisjj - re "An LLM also pointed that out, so I guess it must have been a different one which implemented it?" - no, there is no correlation between whether the same LLM is used and whether it can find errors.
- I had a college professor do the exact same thing in class: he made a fairly subtle mistake formalizing his specification, and thus his proof was perfect but did not solve the actual problem he was trying to address.
He was a mathematician and was convinced that formal methods were the future of software engineering. He also loved handwaving that due to Godel's incompleteness theorem, humans were necessary to introduce creative insights (new axioms) that computers would never be able to do.
I eventually obtained top marks both semesters and left convinced that formal methods are a waste of time in >99% of the cases.
by david-gpu - This is really cool stuff, and I agree the future is likely to look more like this. I was surprised by the last two paragraphs ("Aside: verified assembly") -- my understanding was that this future is basically already here. I believe agl's colleagues at Google have already deployed some auto-mutated verified assembly versions of some crypto routines, based on the Fiat Crypto + CryptOpt work (https://arxiv.org/pdf/2211.10665), both involving Andres Erbsen who I think is currently at Google before starting a professorship soon. I dunno if this work would count as "cheap" (it looks like Fig. 10 unfolds over the course of a day) but spending a day auto-exploring many verified-correct machine code implementations of the same routine to find the fastest one (which you then ship forever) doesn't seem impractically expensive either.
- I have already written it, and I will write it again: dependent types and total functions do not scale. Maintenance is terrible.
Suppose that you have managed to write a non-trivial piece of software with dependent types encoding all sorts of properties everywhere. The actual computation and proof are intermingled. Think of the author's innocent bound-check proof in the zstd decoder, but across the whole program, with more elaborate properties and longer proofs.
Suddenly, you realize that you need to prove a new property of your program. Can you keep your existing work and build on top of it? In general, no, you have to refine every dependent type everywhere by adding a new conjunct expressing a new invariant, and adapt every proof, as the new property is threaded in the existing program.
That is because dependent types (and other staples of naive approaches to proving program properties, like a unique invariant per loop) structure the program along the wrong dimension: they encourage grouping everything that concerns a value ("put this value in a dependent type that encodes everything known about it") or a program point ("write the precondition for this function as a big conjunction mixing all the concerns"), where it works much better, for long-term maintenance, to structure the development along concerns: computational parts of the program, basic functional properties and absence of UB, termination, other functional properties, security, etc., where each layer builds on top of the previous ones without requiring them to change.
That is not to say that dependent types do not have their use. Where they shine is at module boundaries. Consider a library that exposes an opaque type and operations on it. Users of the library can only build and modify values of that type through the library's API. This type should be a dependent type. If it needs to be refined at any point to encode a new invariant, this will have no impact on the library's users, since all they do is pass around values without interpreting them. However, inside the library, I would recommend unpacking/repacking the dependent type at the library's entry points and handling the concerns separately.
- I would say that the value of dependent types in software engineering isn't in proving all code correctness. As a user pointed out in the idris2 Zulip, most programs using dependent types don't have, and shouldn't have, proof of validity for the entire program. Instead, you simply get more correct code by construction, and I think that's the whole point.
I'm currently developing a unikernel in idris2, and the experience is very pleasant (unfortunately, I'm not quite ready to share it yet).
by rafaelRiv - The key is to structure the program so that only a tiny trusted core is verified but the properties extend to untrusted code. For example, the sel4 microkernel is formally proven to not crash (barring hardware), so any program running on it will not crash the entire computer, just itself. Or (only parts of it are formally verified, but) the Rust borrow checker practically guarantees any Rust code without `unsafe` will not produce memory errors; any amount of lines of Rust code, without any proofs themselves, are covered by the relatively tiny trusted core that is the borrow checker.
- > you have to refine every dependent type everywhere by adding a new conjunct expressing a new invariant, and adapt every proof, as the new property is threaded in the existing program.
Having to do this is a sign that the new property depends on implementation details in some way. This can definitely feel like annoying busywork when there is only one reasonable implementation. Of course your sorting algorithm doesn't change the multiplicity of elements in the array, you wouldn't write a bug like that. Of course your sorting algorithm doesn't change the order of elements that are already sorted correctly, you wouldn't write a bug like... except unstable sorting algorithms do that and are widely used for performance reasons. So you do have to check your actual implementation step by step to verify that it really does what you think it must of course be doing. Trying to separate the concerns does not change this.
by yorwba - > they encourage grouping everything that concerns a value ("put this value in a dependent type that encodes everything known about it")
I understood you to be saying "bundling is encouraged", in the sense of
https://leanprover-community.github.io/glossary.html#bundled...
I'm not sure it's encouraged. I agree that it felt natural to define a type like NonNegativeInteger, or a wrapper type like `Sorted(T)` to indicate that that wrapped list is sorted. But I think this is an area of style and aesthetic that is still emerging, far from ossified.
The problem of "threading" new things within existing programs is an important one to address, and it has multiple solutions (context management, dynamic scoping (lol), implicit arguments, type classes). I am curious if the claim of "does not scale" is mitigated by one of those solutions...
by gugagore - It's my own ignorance speaking, but is this as true in math? I could see this being a problem for programs where you have few, if any, real axioms and the axioms themselves change. But if we're talking math, the axioms should be fixed.by prplfsh
- I agree to some extent with your thesis. But also you don't have to encode all the properties of the program in dependent types everywhere. You can have the implementation contain either no proofs or fairly few (e.g., termination and no UB, which can often be automatically discharged), and then separately prove things about it. E.g.
or whatever. That way the function's spec and implementation remain separate and readable. In my limited experience, Lean code usually works more this way rather than having the whole function and its spec in a giant dependently-typed object. For imperative code you can also use Hoare triples and vcgen, but that's currently only partly baked (i.e. proving things is a giant pain).def function_spec bleh blah := math_blargh def function_impl bleh blah := code_blargh theorem function_correct: forall bleh blah, function_impl bleh blah = function_spec bleh blah := by { long proof }Maintenance is still a headache. If you change a small piece of your code, you would then need to change all the proofs that refer to it, and then if the specs also changed then you need to change all proofs that refer to those specs, etc.
by less_less - > dependent types and total functions do not scale.
I'm not convinced that this is much more true than the claim "correct code doesn't scale". If you add to your code in a way depends on a new property for correctness, and the code was not previously written with awareness that the new property was necessary, then you need to check through the rest of your code and make sure that the property is maintained. Formally verifying things is painful because it actually makes you check this.
Instead, we live in a world where we use software that is not completely correct. Browsers have remote code execution vulnerabilities because people who make browsers decided it's more important that javascript can run quickly, and that new standards get implemented, than that we avoid such vulnerabilities at all costs.
by penteract - Strongly agree with the author here. The future will belong to programming languages that natively embed theorem proofers into their type systems so LLMs can forego a lot of testing by just validating the implementations they write against the specs with formal proofs. Writing formal specs is probably the main skill a programmer in the future will need to get work done.
Verus (https://github.com/verus-lang/verus) is a good start for the rust ecosystem, but it's essentially a standalone language today (with custom syntax and type system).
by gz09 - This is the fantasy that has always driven proof systems research. Nobody is going to run software that has never been tested. Would ride a rollercoaster that had never actually been tested before, only "proven" safe? I wouldn't!
So this stuff is always going to be additive and concerned with edge cases, as almost by definition, stuff that isn't edge cases will be found by comprehensive enough testing procedures.
And yet most software doesn't really need to be correct under edge cases, outside of security and data loss issues. People can tolerate a lot of incorrectness in other areas because it's just annoying, not critical.
Security is a case where formal methods could help, but I don't think LLMs will change the industries lack of interest. If anything it'll reduce it even further. Historically security took place in a fog of war. You don't know your enemies capabilities and may not be able to easily match them. But now LLMs are better at finding security bugs than most (all?) humans and ~everyone has access to them, so, from a liability perspective, all you have to do is point a frontier LLM at your codebase and let it fix as many bugs as it can find. Your enemies don't have access to anything better, so once it's done you can tick the box and say security is good enough. Meaning, nobody will fire you if there are still attacks possible.
So in the end I don't see LLMs changing the adoption formal methods.
by mike_hearn - Focus on formal verification is a technique to "harden" an unreliable LLM that produces meaningless slop from arbitrary text into a compiler that produces a correct program from a concise, formal input.
"Writing formal specs" means simply programming, taking a step upward in programming language abstraction level, and whether it's going to be easy remains to be seen.
by HelloNurse - I'm currently writing such a language myself in pure Lean, based on adjoint logic -- as well as graded modes and effects. I started by just trying to formally verify a Rust-like borrow checker and at this point I have a working interpreter and LLVM compiler and a formally verified kernel.
All type checkers are theorem provers, btw, that's just Curry Howard. The question is exactly how expressive they are.
by empath75 - in case anyone's interested i have a vibe coded fork of verus that replaces the verus-the-language side of verus with plain old Lean 4. It's still two languages, but now at least the second language is as mainstream as it gets in the field and has good automation. i haven't finished wiring up the Lean 4 infoview and vs code extensions and LLM skills into it yet, which makes it not as easy to write yet as lean 4 with the IDE bells and whistles.
I'm also playing around with using the lean's compile-to-C tooling to instead compile to rust instead and it's getting more of my focus than the lean-via-verus route right now.
if people are interested, ping me and i can put them up on gh.
by ianhorn - Lean has dependant types. Wouldn't something like Haskell or Idris, that are trying to be general purpose dependantly typed languages--wouldn't they be a better start than versus?
Versus appears to just be a formal verification tool. Perhaps I misunderstand?
You want the formal verification built into the language because the tooling can start to get really crazy good. Agda is the dependantly typed language I've used the most (long ago), and the tooling was interactive in a helpful way I've never experienced with other languages.
You don't want a separate language used to verify a base language, because then everyone ends up having to know two languages. Looking at the history of computing though, I wouldn't be surprised if this happens.
The actual programming language and the verification language can be the same language though, if we want.
by Buttons840 - As a meta-comment on the topic, something I have noticed is that there still exists confusion what it means to use theorem provers for projects -- the other day I read a tweet from Paradigm, a crypto-VC now seemingly AI-pilled. Some LP of theirs had made a Lean 4 formalization of the Ethereum's virtual machine. The tweet said this would have cost like $150k in API tokens ("would have", as in, I guess they get theirs for free), and took a week of inference time for an LLM to produce. I somehow got distracted to actually take a look at the code, which I found rather light on theorems. Nor did the project make use of Batteries or Mathlib which are arguably the one of the strongest motivation for me personally to use Lean4. That is, I generally rather rely on someone else getting the category theory and algebraic structures right, which then leaves me the proof obligation to show the correspondence with whatever toy I'm working on. Here I'm fine to use LLMs for proof search, very similar to how would I use a SMT solver. But what I have found is that the language models have to be really coerced into using these libraries, because otherwise the models much rather overfit and overclaim a solution with a 3 minute inference task rather than attempt to fulfill the proof obligations over 3 hours. And I feel nauseated when I need to convince the LLM (I use Claude) that filling the proof obligation is for "academic exercise" or because I'm coerced into doing so, because otherwise it will come up with reasons of its own why it does not want to do it. Now, this happens under the mental model in which I'm interested in finding equivalences with prior work. Many LLM generated Lean code reads more as if someone was interested whether X can be turned into a Lean 4 program, which is mostly yes, and that in general is a positive thing. But, if you are not interested in refinement types and theorems, why not just choose Haskell? The point is, I strongly sense that unless you have good questions to ask, then that's very evident in these languages. And, this is something the LLM won't help you -- if you don't impose a proof obligation for it, it certainly will not try to go the extra mile to conjure one for you.by Jhsto
- Crypto guys are in the business of grifting magic beans to rubes. They are mostly interested in the aesthetics of these technologies. Using an academic programming language gives these scientific magical vibes and such that make people believe these guys are high tech and know their shit and so on. This is the reason many crypto projects do use Haskell too, it's known as an academic research language that is difficult to use and "if it compiles it works." They come at it from the perspective of "What would sound the best when I try to sell the space money of the future?"by Ampersander