7 ms·

Formal methods and the future of programming

378 points by eatonphil 4mo ago

eddiepete 4mo ago
I wonder how formal methods can help us move faster with GenAI. Is it that they can help write formulas faster? That they can help ensure formulas match the system they're modeling faster? If the problem you think formal methods will help with is sloppy code, isn't the verification code going to be sloppy as well, unless some (not sloppy) intelligence carefully confirms that the specification matches the target system, which was the labor that previously made formal methods too expensive? I guess I don't understand how the argument works if code was previously less sloppy and verification was too expensive, and now code is more sloppy, and there's more of it, but somehow the sloppy intelligence will make verification move fast enough to make it worthwhile. Unless we have some non-sloppy intelligence that's less of a bottleneck on verification than humans, how are we in a better place? Maybe it's that investing that huge amount of labor of verification by human experts is now worth it because so much code will be produced that uses the verification systems that the investment will now pay off. But that requires creating pretty general verification systems, such as type system verification or something (which is what they seem to be aimed at), rather than individually verifying software systems like the micro-kernel example. In other words, maybe the play is to invest in reusable verification systems that can be run tons of times on new code and systems. If so, it's surprising that this wasn't always the strategy.
- jnwatson 4mo ago
  The general idea is that formal methods are self-verifying, up to a point. Sloppy formal methods simply won't prove. The point up to which formal methods stops is: do the formally encoded requirements actually encode what I want to be true? One can make the argument that the requirements is a much smaller surface to verify than that of the entire program. The counter argument is that figuring out what you want the program to do has always been the hardest part of programming, and that programming in itself is a journey to discover latent requirements.
  - Veserv 4mo ago
    > One can make the argument that the requirements is a much smaller surface to verify than that of the entire program. This argument is unfortunately empirically false for any program of any meaningful complexity (>1000 lines, probably even as low as >100 lines ignoring well-defined algorithms and data structures) using current formal methods. Complete formal specifications are usually multiple times larger than the corresponding source code and encode esoteric propertys necessary for the proof, but which are largely even more impenetrable than a undocumented codebase. So, it is both harder to figure out if you encoded the desired requirements and it is more complex. Your only advantage is confidence that what you wrote down is proven.
    - akoboldfrying 4mo ago
      > Complete formal specifications are usually multiple times larger than the corresponding source code and encode esoteric propertys necessary for the proof, but which are largely even more impenetrable than a undocumented codebase. Is it possible that the spec could be factorised into something higher-level and more modular? If not, can you give a flavour of the type of unavoidable esoteric detail? (One area I can see lots of complications is when dealing with versioned data, especially in multiple interacting systems -- naively, correctness needs to be proven for every combination of versions, even if some are never seen.)
- jsenn 4mo ago
  > isn't the verification code going to be sloppy as well The beauty of formal methods is it doesn't matter if your proof is sloppy. As long as it passes verification, it is correct. And unlike in pure math, the proof that a software system is correct is usually a huge mess of special cases, loop invariants, proofs by induction, and boilerplate that requires a large amount of human labour while providing no insight. Proofs are also brittle: a tiny change in the code can force you to throw your proof away and start from scratch. To me, the exciting thing about formal methods in the LLM era is it allows humans to offload the difficult and tedious work of writing proofs to a computer. Taken to an extreme, the human could live entirely in the world of a formal specification, and the LLM could generate 100% of the code. The code may be a mess, but if the system proves it satisfies the spec then it can't be wrong.
  - odyssey7 4mo ago
    So, formal methods produce runnable systems, but communication remains the challenge. If a formal spec is messy, then it's a proof of ... what, exactly? A formal specification that bridges tech and product, that lets non-technical contributors read and discuss all the logical nuances, directly as operational code, at product's level of abstraction of interest, would transform a lot. It's no longer a challenge to create code, it's a challenge to create business requirements and translate them into systems.
    - rzmmm 4mo ago
      The spec and proof are separate. In this blog article he mentions seL4 formal verification, where they state that the spec was 4900 lines of Isabelle and the proof was 200K lines. Obviously human has to understand the spec deeply.
      - jaggederest 4mo ago
        There's an information theoretic aspect about generating a proof which is essentially not human readable from 4900 lines of spec. I wonder how much additional signal they're getting out beyond what's in that 4900 lines, and what's the percentage of noise in the 200k lines of proof?
- RetroTechie 4mo ago
  > I wonder how formal methods can help us move faster with GenAI. Perhaps better the other way around? How GenAI can help us move faster with formal methods. Rather than improve the quality of new software, there's a mountain of existing codebases that could benefit from this.
jdw64 4mo ago
In other words, because GEN AI a lot of code, the idea is to shift human value toward verification. Sometimes I think about what programming really is. In fact, learning programming itself is a huge challenge for a non English speaker like me. I have to rely on machine translation to understand English documents that have no translation. The materials in my language are about 5 to 6 years behind. Now, since it's impossible to code review the tens of thousands of lines of code that AI produces, I see discussions about establishing an absolute rule like mathematical proofs. Reading this reminds me of Rust's borrow checker. In fact, after writing in Rust a few times, it often leads to bad practices where people use tricks to avoid the borrow checker. Actually, when mathematical rigor goes too far, humans tend to find ways around it. An undereducated programmer like me is especially prone to that. Looking back at this kind of attempt, it will probably result in writing code only for specific formalized answers. If it becomes that standardized, I'm not sure it will be able to respond to human needs. I think these defensive programming attempts are fine, but I want to do offensive programming (I coined that term). You take risks, but you fix things quickly and ship. Believing that over time, it will become good enough. Of course, for established industries where accuracy matters and the scope of work is well defined, like Jane Street, the approach in this article is correct. In other words, because there is enough data to adequately model the market's demands But for social losers like me trying to make money, constantly moving from place to place looking for gold mines, these kinds of methodologies seem like a luxury.Established businesses with mature modeling need highly educated and specialized personnel to continuously optimize. But I know that realistically, I can't keep up with that demand. So I look for places where modeling is unstructured, but I'm not sure if I can use this approach even then.
- stephenlf 4mo ago
  > these kinds of methodologies seem like a luxury Absolutely. The article acknowledges this. Jane Street is pretty uniquely equipped to benefit from this.
- ngruhn 4mo ago
  > I want to do offensive programming (I coined that term). You take risks, but you fix things quickly and ship. Nice, I like the term too. But the paradigm is absolutely status quo in the industry. The thing is: with Gen AI the cost of "defensive programming" has gone way down, while the cost of (human) verification has gone way up. On the other hand, formal methods make verification cheap but come with massive implementation overhead (writing specs, types, proofs, and generally bending the implementation into a rigid framework). But Gen AI can automate all that laborious work. It's a match made in heaven.
bobkb 4mo ago
I have been testing formal verification methods with multiple products. It will be great to also understand more about what’s tried and how it was done. For example attempting to verify the spec is what I have been trying to implement.
xvilka 4mo ago
seL4 despite being formally verified contained gnarly bugs, like [1]. Thus, it's not a silver bullet as some people think. Yes, it improves the quality, but only one of the aspects of hardening software, like ASAN, SAST, fuzzing, strict languages, and so on. [1] https://github.com/seL4/seL4/issues/1199 https://github.com/seL4/seL4/issues/1199
- gr_norm 4mo ago
  > Since it is the unverified SMP config of the kernel I don't disagree with your point (formal verification does not rid you of all bugs), but this is not the subject of the linked issue. This was a bug in an unverified path.
mark4 4mo ago
Relevant keynote I wrote about Formal methods won, now what? https://muratbuffalo.blogspot.com/2026/04/bugbash26-keynote.html https://muratbuffalo.blogspot.com/2026/04/bugbash26-keynote....
awinter-py 4mo ago
See previous kleppmann post https://martin.kleppmann.com/2025/12/08/ai-formal-verification.html https://martin.kleppmann.com/2025/12/08/ai-formal-verificati..., and yes, obviously anything that you can put in the typesystem or the linter, you should weigh doing so. Hopefully we get more ergonomic ways to do this? Like of the tools listed in the post, dafny + iris are the closest to being industrial I think. And amzn S3 has a history of TLA use in-house I think. But we probably haven't seen the typescript in this space yet, a zero cost abstraction that drops into existing tools, and people genuinely prefer it to the old way. (And custom linters are also still pretty bad to write. Like golangci-lint is a painful codebase, haven't tried semgrep but the rules engine seemed intimidating. I've yet to use an AST API that I liked)
pjmlp 4mo ago
I am already seeing the uptake on Spec-Driven Development as the Rational Unified Process revenge.
spenrose 4mo ago
As usual, this paean to deductive reasoning (“formal methods”) leaves out its fundamental limit: how closely do the postulates and definitions fit the domain they purport to map? (“In theory, there is no difference between theory and practice. In practice ...”) My guess is that Jane Street maintains large code bodies where the mapping is 1:1, because the purpose of the code is to implement a deterministic algorithm. Many other coders work in such areas. But millions of us don’t: most UIs, most exploratory work, etc. There is a movement parallel to formal methods to define acceptance criteria at high resolution but not logico-mathematically, which at least grapples with the mapping problem but can’t resolve it where the map isn’t the territory, which is most places. Has Google’s results page, with its extremely evolved internal optimization frameworks really hit an optimum? Could that prototype you whipped up to capture a hazy idea have better illustrated it? These questions are best answered by looking outside the system to what the system serves.
- benlivengood 4mo ago
  Formal methods are precisely for the domains where the semantics are well-defined. Logical circuits (a lot of CPU components get formal verification), kernels, protocols, parsers, compilers, cryptography, security frameworks, concurrency primitives, etc. all benefit a lot from verification.
- petra 4mo ago
  Google's results page isn't well defined. But probably 90%+ of the code below it is well defined. And in some cases, where the result isnt well defined, it can be learned, so it's not about sitting and thinking what would make sense.
- sn9 4mo ago
  Most UIs in practice boil down to state machines which are extremely amenable to formal verification. Hillel Wayne's writing is a good starting place to learn more: https://www.hillelwayne.com/formally-specifying-uis/ https://www.hillelwayne.com/formally-specifying-uis/
brap 4mo ago
Whenever I read about formal specs it always seems to me like “write the same tests just in a different way”, or worse, “write the same implementation but in a different way”. I guess doing things twice can help catch errors, but I fail to see what’s so special about formal specs if they can suffer from the exact same bugs as the tests/implementation. I guess the root of the problem is if you want to formally prove that a program does something, you have to be very specific (heh) about what that something is, at which point you are basically just writing tests/implementation all over again. I have been looking into this on and off for years now, and I keep feeling like I’m missing something, but I don’t know what it is. Can anyone enlighten me?
- jlebar 4mo ago
  > Whenever I read about formal specs it always seems to me like “write the same tests just in a different way”, or worse, “write the same implementation but in a different way”. [...] Can anyone enlighten me? A big difference is that formal methods allow you to use the "for all" quantifier. For example, you might write a unit test that says "foo('abc') returns a string with no trailing whitespace". But with formal methods, you can prove that "for any input x, foo(x) returns a string with no trailing whitespace". This is a trivial example, but you could imagine something more complicated, such as "for any program P, compile(P) has the same behavior as P". Of course, you have to define what "has the same behavior as" means!
  - brap 4mo ago
    >Of course, you have to define what "has the same behavior as" means And that's really my issue, for example when you define "has no trailing whitespace", you are basically writing a piece of the implementation. Cover all behaviors, and you have basically re-implemented the function, no? In other words, if I have the full formal spec of f(), isn't that the same thing as having f()?
    - bluGill 4mo ago
      > In other words, if I have the full formal spec of f(), isn't that the same thing as having f()? In some cases, however quite often, the spec is much simpler. For instance, it's easy to say that after running sort on some list, that the result is sorted. However, it is very hard to come up with the algorithm to do that from the specification. Sometimes that is even a point. Bubble sort, quick sort, tim sort, we can go on and on. There's a huge number of different sorts that computer science have discovered over the years. They all should have the same result and so you should be able to prove they do the same thing. However, in the real world there are often reasons you would prefer one to another despite all meeting the same spec.
reinitctxoffset 4mo ago
I caught the religion on using types in conjunction with LLMs about eighteen months ago, but I only really got serious about `lean4` like six to eight months ago and now I wouldn't even consider using AI assist in software work with a `CIC` proof substrate that has practical C/C++ (and therefore, everything) FFI. We've banned everything from JSON to Python, rewritten `nix` to have a compiler, and almost everything we write is not only property tested and multiply fuzzed to within an inch of it's life, but we have proofs in `lean4` that at a minimum drive property tests via `.olean` linkage, and when we have the bandwidth we prove exhaustiveness over the domain and property test that. We skip the whole C++/Rust thing because all of the fast stuff is generated from `lean4` and so it doesn't really matter (C++ has advantages when bugs in it are actually bugs in `lean4` code, but you could go either way). This is a big departure, and I certainly don't blame anyone who is skeptical: "ban JSON and Python wtf?!?!", but we've done millions of lines (checked) of this stuff and AI + formal systems is a dramatically bigger leap than no AI -> AI and Python. The latter in our experience is not monotone in progress, the former is almost always monotone in progress. And you can do wild shit, this is a formal proof of the polyhedral tensor calculus that is modeled by things like ISL and CuTe, and using that we can get swizzling and tiling using `mdspan` in C++23 on device and prove it's right (up to some L'Hopital arugment about the coverage which this example doesn't demonstrate well: https://github.com/b7r6/mdspan-cute https://github.com/b7r6/mdspan-cute That in turn, well, it goes real fast. On the first try. https://straylight.software/assets/lambda-hierarchy.svg https://straylight.software/assets/lambda-hierarchy.svg
- skybrian 4mo ago
  Ok but what software have you built and why is it useful?
  - reinitctxoffset 4mo ago
    This is all pre-release but a few highlights: - `continuity` is a `lean4` metaprogramming system that we use all kinds of ways but the real meat is it allows formal specification of codecs and state machines in ways that make security and performance properties proof amenable, the key trick here is to limit parser power to just what you need and no more. a very cool thing is that we can add targets to it, so when we do Zig for example, Zig will immediately get proven correct and frontier performance support for dozens of protocols that are not all mature right now. - `libevring-cpp` (bound up into `libevring-hs` and `libevring-rs`) is a Trinity-inspired deterministic event replay system that replaces anything you would have done with `libuv` or whatever, and it's wired into `io_uring` (we're stuck with `kqueue` on darwin, eh). it interfaces with `continuity` machines and codecs (which are generated very carefully for the hardware they run on) and we have yet to find a way of measuring such programs where it doesn't resoundingly shatter the performance of any other asynchronous programming primitive in any language. i'm sure the community will prove us wrong when we release it, but it's real fast. and you get much stronger guarantees than in most such systems (Trinity derived, so if you can repro a bug, you can walk the event trace until it's sitting there in GDB and shit) - `hyperconsole-cpp` (and `hyperconsole-hs` and `hyperconsole-rs`) is the TUI library idea taken to some deranged extreme on performance and supports everything in `notcurses`, it's pretty wild: https://youtu.be/YqgEtpJ8tGI https://youtu.be/YqgEtpJ8tGI - straylight-nix is a complete rewrite of nix that fixes thousands of bugs, hundreds of them security adjacent and dozens of them we only talk to vendors about. it's daemonless, dramatically faster, ground-up WASM-targeting compiler with a formal grammer, uses an extremely fast LSM-based store (it can read the legacy store but we don't write it) that fixes all the problems in floating CA, IFD is too cheap to care about, and recursive nix is no longer and issue (see daemonless). it supports tearing derivations into `REAPI` actions that you can feed to your friendly native NativeLink or whatever, which just goes through them like a woodchipper. KVM-based sandbox with snapshot and restore, really opens the world up on what your builders can be. - `slide` is the reference implementation of a family of protocols called `SIGIL`: `SIGIL-LLM` is a binary encoding for LLM data that resets on ambiguity and drops the average bytes on the wire from e.g. OpenRouter to your harness from ~hundreds to ~1.5 per token, `SIGIL-API` is a bijection on OpenAPI 3.1.0 and AsyncAPI 3.0.0 that gives comparable improvements, and `SIGIL-SH` is such an encoding for a sensible subset of bash. this does about 1.5 billion tokens per second on a laptop and never emits partial frames, so you don't get speculative execution rollback problems in your harness that tilt agents off. - `// WEAPON //` is an adversarial, vendor-skeptical, full-take surveilance agemt harness built on `hyperconsole-cpp` and `SIGIL` (so, you could absorb the entire token output of OpenRouter on one machine if you wanted at least on the wire and in the terminal, clearly the bottleneck rapidly becomes whatever the agents are calling, but it's `zmq4` transport underneath `SIGIL` so it's also trivial to full-take all of your data for fine tuning or whatever you want it for into e.g. `parquet` on R2. `// WEAPON //` does a bunch of stuff: the tool call surface is heavily optimized for AST-level edits that miss dramatically less, we intercept and manipulate shell commands (slice off the stupid `| tail -n5` that keeps the droid in a loop not seeing the error, pre-emptively ground using heuristics that have been tuned (defeats the search flinch), and always recovers from any stall, or nag box, or anything else that would serve as an unannounced rate limit, it's fine if vendors rate limit but they need to put it in their ToS. it has a bunch of other primitives, agents run in real KVM sandboxes and speculate out as wide as you want to pay the tokens for. we hyper-manage things like the cache breakpoint geometry of Anthropic so e.g. Opus rarely misses in cache and always hands off edits to specialized tool use models. it's pretty extreme the difference in outcomes relative to all this React jank. - `s4` is a general-purpose compiler from most any pytorch 2.0 model to `myelin`-level performance on NVIDIA (we only support NVIDIA Blackwell at the moment, that might change) and it's never worse than `myelin` because if we don't out-tune it we invoke it, but we out tune it a lot because we've proven a lot of decideability theorems about tiling and scheduling on both 1CTA and 2CTA, so we can often arrive at a finite, enumerable set of schedule/tile choices. `myelin` mops up the random garbage around the big GEMMs just like in TRT-LLM. - `sigil-trtllm` is inspired by TensorRT-LLM-Edge but designed from the ground up around Mellanox/ConnectX and in particular GPUDirect, so it can stream `SIGIL-LLM` tokens directly onto the wire whereas something like Dynamo is usually traversing both Python and NATS, which is super weird to us. this uses the `s4` compiler very heavily. - `straylight-cas` is a geographically distributed content addressable store backed by any R2-compatible (so most any S3-compatible too) object store with multi-level LSM and extreme performance memtables, optimistic hinted handoff over `zmq4` to other geographies, and a really simple operational story, this is kind of the thing that powers the product surface. ... which is the thing i'm less ready to talk about because it's supposed to be a surprise.
yawaramin 4mo ago
Quis custodiet ipsos custodes?
- Animats 4mo ago
  The proof checker. You verify a proof system by having it produce a proof trace: - Step 3185: Apply rule that a * b = b * a to "length * width" in the current formula. Then you run a proof trace checker which applies each transformation in sequence and checks that the expected result is obtained. Provers are complicated, but proof trace checkers are really dumb.
  - zahlman 4mo ago
    But don't you still have to logically connect the validity of the proof to desirability of the output?
Syzygies 4mo ago
I nearly adopted OCaml for my current math research, in no small part because of Jane Street contributions. I instead chose Lean 4, as LLMs became able to help code in Lean. I give up a factor of two in performance (a gap likely to close) for what reads to me as the clearest expression of each algorithm. Lean is a beautiful language that makes OCaml read like Old English. Lean is designed to be optionally verified; proof is its primary (but not only) application. It seems an impedance mismatch for Jane Street to explore this direction without also migrating to Lean 4.
- derdi 4mo ago
  You are praising Lean for optional verification. They want to add optional verification to OCaml. Where do you see an impedance mismatch? Just in the fact that you don't find OCaml pretty enough?
Animats 4mo ago
I used to do proof of correctness work, decades ago.[1] We had more proof automation than many of the later systems. The easy stuff was solved by the first SAT solver, the Oppen-Nelson simplifier. The harder stuff used the Boyer-Moore prover, which uses heuristics and previous lemmas to guide the theorem prover. The Boyer-Moore prover had to be helped along by suggesting lemmas, which it would try to prove and which would then be used for later proofs. That was the tough human job. Later systems seemed to have less automation. What tended to go wrong with formal methods was that the people doing them were too into the formalism. I was working on this for a commercial project that wanted bug-free code, not as an academic. The academic projects tended to get too clever. They had the mathematician's bias of wanting a terse notation and not much case analysis. That's not a good solution. You want lots of automated grinding and don't want to need much insight. The clever people kept inventing new logics - modal logic, temporal logic, etc, - to avoid verbosity in paper and pencil proof work. That wasn't really all that helpful. The basic truth of this business is that most of the theorems are rather banal. As the Jane Street people point out, there's a big advantage in having control of the language. You want the verification statements integrated into the programming language. In many systems, they're embedded in comments, in a different syntax than the programming language, or even in completely separate files. This adds unnecessary work. It's good to see them pushing this forward. We were doing this too early, over 40 years ago. It took about 45 minutes of compute back then to build up number theory from a cold start with the Boyer-Moore prover. Now it takes less than a second. [1] https://archive.org/details/manualzilla-id-5928072/page/n3/mode/2up https://archive.org/details/manualzilla-id-5928072/page/n3/m...
- nextos 4mo ago
  I've worked in formal methods for quite a long time, and I disagree a bit with your statement that new logics are not helpful. Industrial logics are really practical and allow you to write all sorts of sophisticated properties that your system should satisfy in a very succinct way. Logic is to computer science and software engineering what calculus is to physics and mechanical or civil engineering [1, 2]. Things like LTL or, more recently, separation logic, have been incredible breakthroughs. TLA+, which has gained quite a lot of popularity, is a testament to that. Model checking is eminently practical. The exciting thing now is that heavier formal methods, in particular theorem proving, might become cheap enough to use in regular systems software. Writing formal specifications for functions and getting them synthesized and proven correct by some SAT/SMT, theorem prover & LLM hybrid may become the norm in the not-too-distant future. [1] On the Unusual Effectiveness of Logic in Computer Science. https://www.cs.rice.edu/~vardi/papers/aaas99.jsl.pdf https://www.cs.rice.edu/~vardi/papers/aaas99.jsl.pdf [2] From Philosophical to Industrial Logics. https://www.cs.rice.edu/~vardi/papers/icla09.pdf https://www.cs.rice.edu/~vardi/papers/icla09.pdf
JacobAsmuth 4mo ago
Sounds like Jane Street would be interested in the Lean framework I've been working on for formally verified frontends. https://github.com/JacobAsmuth/qed https://github.com/JacobAsmuth/qed
jp0001 4mo ago
Formal methods is like a plan. Everyone has one until they are punched in the face (real world requirements and trust boundaries).
- Paracompact 4mo ago
  Formal methods are not meant to replace trust in a system. They are meant to minimize the surface area of trust. To not understand and advertise what surface area still exists is foolhardy, and mistakes logic for magic.
- angry_octet 4mo ago
  Incredibly uninformed comment. The formally verified part is the high confidence component that is the anvil to hammer out bugs in the unverified components.
addaon 4mo ago
I've been playing with related ideas recently, and can talk about them at length... but one thing that's surprised me is just how effective frontier models (ChatGPT-5.5 in particular) are at completing certain manual proofs in the Roqc (né Coq) proof assistant. The proofs aren't always pretty, but ChatGPT can often prove something in minutes and 10 - 100 iterations that would take me, a human who has limited but non-zero proof assistant experience but significant domain experience in the lemmas being proven, much much longer. The reason I think this is relevant and interesting in the context of the (short) article is because it challenges basic assumptions about how certain formal method tooling works. Frama-C, Ada/SPARK, etc are focused on generating proof obligations that can be automatically discharged by CVC5, Z3, etc; with a relatively painful fallback of manually proving the obligation in Rocq. The most common workflow seems to be to discover that an obligation is "hard" (not automatically discharged), and to restructure the set of visible lemmas and assertions at the obligation generation point in the code to try to make it "easy"; or even restructuring the code to try to make it easy. Which, in a world where Roqc proofs are doubly expensive (first because they're a challenge for a human to write; second because they tend to require quite a bit of maintenance churn as the code and proof around them evolves), makes sense. But if Roqc proofs are "automatically discharged with AI in the loop", this cost delta goes away -- and it becomes possible to think about writing proofs the same we (usually) write code, with human readability and clarity as the first goal, and [compiler|prover] optimization a distant second. Which I find quite exciting, although I haven't fully digested the implications yet.
- bluGill 4mo ago
  How often will AI look at something that can't be proven because you change requirements and decide to change the code and your requirements to make the proof easier though? I haven't played with proofs at all, but I do know that occasionally when I say, this test failed after making a change, AI will just change the test instead of making the code pass both the old test and the new test which is most often my intent.
  - addaon 4mo ago
    That's up to the harness. Right now, my harness doesn't have any tools that would allow the agent to change contracts. Also, agents working on a Rocq proof don't have write access to the C+ACSL code; they can review it, and propose structural changes to the coordinator, but all they can do is iterate on the Roqc proof or give up. The weakest part of the harness today is that the agents that do C+ACSL work can modify both C and ACSL, even though they're usually run with the explicit intent to not change the semantics of the C code (although it's totally within bounds, and often required, for them to change e.g. `foo & 3` to `foo % 4`) -- so there's weakness here, but it's bounded, and since the contracts live in header files that they can never write, it's worked so far. It's a starting point, at least; I certainly wouldn't say this is a mature, or even good, tool chain, but still learning.
winwang 4mo ago
Love this. I've shifted in the past few months to using highly expressive types in Scala 3 to have types carry more and more compile-time proofs (without macros, though a couple are warranted). Not only does it help with agentic test "sprawl", it seems to prevent agents from falling into lower-quality modes of operation. One of the more annoying things I've been preventing is what I call "noun accretion", where agents try and make a new monomorphic type for everything, instead of clearly genericizing when sensible. My bet is on formal-method-shaped tooling (including languages with strong type systems) to accelerate decent-quality agentic coding. When I say "highly expressive types", I mean techniques I'd likely not want to ship in a typical codebase, unless the team was already on the typelevel programming bandwagon (i.e. having HKT and type functions being basic blocks already, not weird). Agents are better at "math" than basically most devs (even category-theory-pilled ones), at least in terms of knowledge. Better yet, they are decent at pedagogy, especially when considering they have "infinite" patience for dialogue. In a more personal setting, I've had Codex Lean-ify a couple of my hobby proofs, it was extremely easy. Note: not saying it did this 100% "correctly" (gotta learn more Lean 4 to check more thoroughly), but it also seems to check for classic proof gotchas by default. Very excited for the future of formal methods.
cadamsdotcom 4mo ago
I’ve had huge success with TDD and nothing more formal than that; test frameworks are great for verifying “business correctness”. But they can also verify other aspects - eg. asserting that 3 queries ran instead of 103 for a request, to prove absence of N+1 queries. Really any technique that lets the agent create its own verification is ideal, as it makes verification scale.
rzmmm 4mo ago
He mentions the seL4 microkernel. The specification is written in Isabelle, and it's relatively complex: PDF https://sel4.systems/Info/Docs/seL4-spec.pdf https://sel4.systems/Info/Docs/seL4-spec.pdf The bottleneck seems to be that clearly it's critical to be certain about the spec. Maybe not for kernels, but I can see use for cryptographic algorithms, etc?
zisa-security 4mo ago
Interesting read. Formal methods seem to matter most when the architectural complexity grows faster than human intuition can track.
hanzewei_qk44 4mo ago
[flagged]
UncleEntity 4mo ago
I was playing around with stuff trying to get Claude produce a JavaCard VM with the idea that the VM was hand written from the spec with a separate, independently produced, spec file used to generate tests for ESBMC to verify so an identical bug would have to exist in both to make it through. Worked out pretty well, found a few bugs in both projects, but my poor laptop can't handle the full 32-bit space so that part never got the full verification -- 16-bit, rock solid though. Then I really got serious about the yak shaving and, well, am probably in need of an intervention as I don't get Claude to write a VM but to make the tools to generate a VM from an assortment of DSL and that has snowballed a bit as I really liked shaving yaks before the daffy robot revolution. --edit-- Almost forgot, I tried that with the little less dodgy banned Claude and the wasm standard it wrote a python script to parse the spec pdf, the official bytecode implementation in OCaml (or whatever) and generate a TOML file (Claude loves the TOML) to generate the type headers and for cross-referencing in the other tools. Was so impressed I just let it go on its merry way and it did the deed.
smasher164 4mo ago
I think it's a good time to learn Lean. It positions itself as a proof assistant that's also good at practical programming. I'm not sure how mature the ecosystem is for the latter.
seqradev 4mo ago
We are working toward applying formal methods from the application security testing side, but I believe the same kind of approach can be applied to business logic verification as well. For that, we are using the taint analysis technique — a fairly well-established formal methods approach, but still not widely applied in the field because of the complexity of dataflows in real codebases. Scaling formal methods beyond AST pattern matching and some simple type checking turns out to be a really hard task! It took years of research and development to reach the point where taint analysis enables us to trace interprocedural dataflows in real codebases in minutes and find deeply hidden vulnerabilities. If this sounds interesting to you, take a look at our project: https://github.com/seqra/opentaint https://github.com/seqra/opentaint
blueblazin 4mo ago
As someone with a bit of interest in programming languages (design and implementation) this was really interesting to me: > For most people who work on programming languages, the easy part is coming up with new and better ideas about how to make programming better. The hard part is convincing anyone to actually use those ideas for real work. Totally agree, there's only so much strangeness you can introduce in a new language[1] regardless of benefit. But AI agents should not feel much resistance to radically new ideas in PL design. I've been thinking for a while now about how PL design will evolve post agentic AI. I think it will be very interesting to see what new ideas we can come up with to improve programming languages when we worry much less about adoption. [1] https://steveklabnik.com/writing/the-language-strangeness-budget/ https://steveklabnik.com/writing/the-language-strangeness-bu...
brainless 4mo ago
I am not a language nerd but I keep on experimenting in my own ways to use the type system to generate code that is more reliable. I build a coding agent specifically for small models, which makes everything harder. I started this chat with Claude to build the next step: https://claude.ai/share/4264e5f6-b334-426c-afe4-904d233ef946 https://claude.ai/share/4264e5f6-b334-426c-afe4-904d233ef946 - how can I go from PRD to a typed representation of the business logic. The I started building as per https://github.com/brainless/nocodo/blob/feature/praxis_agent_runtime/agents/RUNTIME.md https://github.com/brainless/nocodo/blob/feature/praxis_agen.... The praxis crate: https://github.com/brainless/nocodo/tree/feature/praxis_agent_runtime/nocodo_praxis https://github.com/brainless/nocodo/tree/feature/praxis_agen... and a sample Todo app: https://github.com/brainless/nocodo_example_todo_app https://github.com/brainless/nocodo_example_todo_app Generating unit tests for the library functions of any project would be done via a separate agent than the one coding the functions. And then use tree-sitter to statically check code to PRD (provenance graph). Again, not a language nerd, just enjoying chasing a goal.

378 points by eatonphil 4mo ago

I wonder how formal methods can help us move faster with GenAI. Is it that they can help write formulas faster? That they can help ensure formulas match the system they're modeling faster? If the problem you think formal methods will help with is sloppy code, isn't the verification code going to be sloppy as well, unless some (not sloppy) intelligence carefully confirms that the specification matches the target system, which was the labor that previously made formal methods too expensive? I guess I don't understand how the argument works if code was previously less sloppy and verification was too expensive, and now code is more sloppy, and there's more of it, but somehow the sloppy intelligence will make verification move fast enough to make it worthwhile. Unless we have some non-sloppy intelligence that's less of a bottleneck on verification than humans, how are we in a better place? Maybe it's that investing that huge amount of labor of verification by human experts is now worth it because so much code will be produced that uses the verification systems that the investment will now pay off. But that requires creating pretty general verification systems, such as type system verification or something (which is what they seem to be aimed at), rather than individually verifying software systems like the micro-kernel example. In other words, maybe the play is to invest in reusable verification systems that can be run tons of times on new code and systems. If so, it's surprising that this wasn't always the strategy.

jnwatson 4mo ago
The general idea is that formal methods are self-verifying, up to a point. Sloppy formal methods simply won't prove. The point up to which formal methods stops is: do the formally encoded requirements actually encode what I want to be true? One can make the argument that the requirements is a much smaller surface to verify than that of the entire program. The counter argument is that figuring out what you want the program to do has always been the hardest part of programming, and that programming in itself is a journey to discover latent requirements.
- Veserv 4mo ago
  > One can make the argument that the requirements is a much smaller surface to verify than that of the entire program. This argument is unfortunately empirically false for any program of any meaningful complexity (>1000 lines, probably even as low as >100 lines ignoring well-defined algorithms and data structures) using current formal methods. Complete formal specifications are usually multiple times larger than the corresponding source code and encode esoteric propertys necessary for the proof, but which are largely even more impenetrable than a undocumented codebase. So, it is both harder to figure out if you encoded the desired requirements and it is more complex. Your only advantage is confidence that what you wrote down is proven.
  - akoboldfrying 4mo ago
    > Complete formal specifications are usually multiple times larger than the corresponding source code and encode esoteric propertys necessary for the proof, but which are largely even more impenetrable than a undocumented codebase. Is it possible that the spec could be factorised into something higher-level and more modular? If not, can you give a flavour of the type of unavoidable esoteric detail? (One area I can see lots of complications is when dealing with versioned data, especially in multiple interacting systems -- naively, correctness needs to be proven for every combination of versions, even if some are never seen.)
jsenn 4mo ago
> isn't the verification code going to be sloppy as well The beauty of formal methods is it doesn't matter if your proof is sloppy. As long as it passes verification, it is correct. And unlike in pure math, the proof that a software system is correct is usually a huge mess of special cases, loop invariants, proofs by induction, and boilerplate that requires a large amount of human labour while providing no insight. Proofs are also brittle: a tiny change in the code can force you to throw your proof away and start from scratch. To me, the exciting thing about formal methods in the LLM era is it allows humans to offload the difficult and tedious work of writing proofs to a computer. Taken to an extreme, the human could live entirely in the world of a formal specification, and the LLM could generate 100% of the code. The code may be a mess, but if the system proves it satisfies the spec then it can't be wrong.
- odyssey7 4mo ago
  So, formal methods produce runnable systems, but communication remains the challenge. If a formal spec is messy, then it's a proof of ... what, exactly? A formal specification that bridges tech and product, that lets non-technical contributors read and discuss all the logical nuances, directly as operational code, at product's level of abstraction of interest, would transform a lot. It's no longer a challenge to create code, it's a challenge to create business requirements and translate them into systems.
  - rzmmm 4mo ago
    The spec and proof are separate. In this blog article he mentions seL4 formal verification, where they state that the spec was 4900 lines of Isabelle and the proof was 200K lines. Obviously human has to understand the spec deeply.
    - jaggederest 4mo ago
      There's an information theoretic aspect about generating a proof which is essentially not human readable from 4900 lines of spec. I wonder how much additional signal they're getting out beyond what's in that 4900 lines, and what's the percentage of noise in the 200k lines of proof?
RetroTechie 4mo ago
> I wonder how formal methods can help us move faster with GenAI. Perhaps better the other way around? How GenAI can help us move faster with formal methods. Rather than improve the quality of new software, there's a mountain of existing codebases that could benefit from this.

jdw64 4mo ago

In other words, because GEN AI a lot of code, the idea is to shift human value toward verification. Sometimes I think about what programming really is. In fact, learning programming itself is a huge challenge for a non English speaker like me. I have to rely on machine translation to understand English documents that have no translation. The materials in my language are about 5 to 6 years behind. Now, since it's impossible to code review the tens of thousands of lines of code that AI produces, I see discussions about establishing an absolute rule like mathematical proofs. Reading this reminds me of Rust's borrow checker. In fact, after writing in Rust a few times, it often leads to bad practices where people use tricks to avoid the borrow checker. Actually, when mathematical rigor goes too far, humans tend to find ways around it. An undereducated programmer like me is especially prone to that. Looking back at this kind of attempt, it will probably result in writing code only for specific formalized answers. If it becomes that standardized, I'm not sure it will be able to respond to human needs. I think these defensive programming attempts are fine, but I want to do offensive programming (I coined that term). You take risks, but you fix things quickly and ship. Believing that over time, it will become good enough. Of course, for established industries where accuracy matters and the scope of work is well defined, like Jane Street, the approach in this article is correct. In other words, because there is enough data to adequately model the market's demands But for social losers like me trying to make money, constantly moving from place to place looking for gold mines, these kinds of methodologies seem like a luxury.Established businesses with mature modeling need highly educated and specialized personnel to continuously optimize. But I know that realistically, I can't keep up with that demand. So I look for places where modeling is unstructured, but I'm not sure if I can use this approach even then.

stephenlf 4mo ago
> these kinds of methodologies seem like a luxury Absolutely. The article acknowledges this. Jane Street is pretty uniquely equipped to benefit from this.
ngruhn 4mo ago
> I want to do offensive programming (I coined that term). You take risks, but you fix things quickly and ship. Nice, I like the term too. But the paradigm is absolutely status quo in the industry. The thing is: with Gen AI the cost of "defensive programming" has gone way down, while the cost of (human) verification has gone way up. On the other hand, formal methods make verification cheap but come with massive implementation overhead (writing specs, types, proofs, and generally bending the implementation into a rigid framework). But Gen AI can automate all that laborious work. It's a match made in heaven.

bobkb 4mo ago

I have been testing formal verification methods with multiple products. It will be great to also understand more about what’s tried and how it was done. For example attempting to verify the spec is what I have been trying to implement.

xvilka 4mo ago

seL4 despite being formally verified contained gnarly bugs, like [1]. Thus, it's not a silver bullet as some people think. Yes, it improves the quality, but only one of the aspects of hardening software, like ASAN, SAST, fuzzing, strict languages, and so on. [1] https://github.com/seL4/seL4/issues/1199 https://github.com/seL4/seL4/issues/1199

gr_norm 4mo ago
> Since it is the unverified SMP config of the kernel I don't disagree with your point (formal verification does not rid you of all bugs), but this is not the subject of the linked issue. This was a bug in an unverified path.

mark4 4mo ago

Relevant keynote I wrote about Formal methods won, now what? https://muratbuffalo.blogspot.com/2026/04/bugbash26-keynote.html https://muratbuffalo.blogspot.com/2026/04/bugbash26-keynote....

awinter-py 4mo ago

See previous kleppmann post https://martin.kleppmann.com/2025/12/08/ai-formal-verification.html https://martin.kleppmann.com/2025/12/08/ai-formal-verificati..., and yes, obviously anything that you can put in the typesystem or the linter, you should weigh doing so. Hopefully we get more ergonomic ways to do this? Like of the tools listed in the post, dafny + iris are the closest to being industrial I think. And amzn S3 has a history of TLA use in-house I think. But we probably haven't seen the typescript in this space yet, a zero cost abstraction that drops into existing tools, and people genuinely prefer it to the old way. (And custom linters are also still pretty bad to write. Like golangci-lint is a painful codebase, haven't tried semgrep but the rules engine seemed intimidating. I've yet to use an AST API that I liked)

pjmlp 4mo ago

I am already seeing the uptake on Spec-Driven Development as the Rational Unified Process revenge.

spenrose 4mo ago

As usual, this paean to deductive reasoning (“formal methods”) leaves out its fundamental limit: how closely do the postulates and definitions fit the domain they purport to map? (“In theory, there is no difference between theory and practice. In practice ...”) My guess is that Jane Street maintains large code bodies where the mapping is 1:1, because the purpose of the code is to implement a deterministic algorithm. Many other coders work in such areas. But millions of us don’t: most UIs, most exploratory work, etc. There is a movement parallel to formal methods to define acceptance criteria at high resolution but not logico-mathematically, which at least grapples with the mapping problem but can’t resolve it where the map isn’t the territory, which is most places. Has Google’s results page, with its extremely evolved internal optimization frameworks really hit an optimum? Could that prototype you whipped up to capture a hazy idea have better illustrated it? These questions are best answered by looking outside the system to what the system serves.

benlivengood 4mo ago
Formal methods are precisely for the domains where the semantics are well-defined. Logical circuits (a lot of CPU components get formal verification), kernels, protocols, parsers, compilers, cryptography, security frameworks, concurrency primitives, etc. all benefit a lot from verification.
petra 4mo ago
Google's results page isn't well defined. But probably 90%+ of the code below it is well defined. And in some cases, where the result isnt well defined, it can be learned, so it's not about sitting and thinking what would make sense.
sn9 4mo ago
Most UIs in practice boil down to state machines which are extremely amenable to formal verification. Hillel Wayne's writing is a good starting place to learn more: https://www.hillelwayne.com/formally-specifying-uis/ https://www.hillelwayne.com/formally-specifying-uis/

brap 4mo ago

Whenever I read about formal specs it always seems to me like “write the same tests just in a different way”, or worse, “write the same implementation but in a different way”. I guess doing things twice can help catch errors, but I fail to see what’s so special about formal specs if they can suffer from the exact same bugs as the tests/implementation. I guess the root of the problem is if you want to formally prove that a program does something, you have to be very specific (heh) about what that something is, at which point you are basically just writing tests/implementation all over again. I have been looking into this on and off for years now, and I keep feeling like I’m missing something, but I don’t know what it is. Can anyone enlighten me?

jlebar 4mo ago
> Whenever I read about formal specs it always seems to me like “write the same tests just in a different way”, or worse, “write the same implementation but in a different way”. [...] Can anyone enlighten me? A big difference is that formal methods allow you to use the "for all" quantifier. For example, you might write a unit test that says "foo('abc') returns a string with no trailing whitespace". But with formal methods, you can prove that "for any input x, foo(x) returns a string with no trailing whitespace". This is a trivial example, but you could imagine something more complicated, such as "for any program P, compile(P) has the same behavior as P". Of course, you have to define what "has the same behavior as" means!
- brap 4mo ago
  >Of course, you have to define what "has the same behavior as" means And that's really my issue, for example when you define "has no trailing whitespace", you are basically writing a piece of the implementation. Cover all behaviors, and you have basically re-implemented the function, no? In other words, if I have the full formal spec of f(), isn't that the same thing as having f()?
  - bluGill 4mo ago
    > In other words, if I have the full formal spec of f(), isn't that the same thing as having f()? In some cases, however quite often, the spec is much simpler. For instance, it's easy to say that after running sort on some list, that the result is sorted. However, it is very hard to come up with the algorithm to do that from the specification. Sometimes that is even a point. Bubble sort, quick sort, tim sort, we can go on and on. There's a huge number of different sorts that computer science have discovered over the years. They all should have the same result and so you should be able to prove they do the same thing. However, in the real world there are often reasons you would prefer one to another despite all meeting the same spec.

reinitctxoffset 4mo ago

I caught the religion on using types in conjunction with LLMs about eighteen months ago, but I only really got serious about `lean4` like six to eight months ago and now I wouldn't even consider using AI assist in software work with a `CIC` proof substrate that has practical C/C++ (and therefore, everything) FFI. We've banned everything from JSON to Python, rewritten `nix` to have a compiler, and almost everything we write is not only property tested and multiply fuzzed to within an inch of it's life, but we have proofs in `lean4` that at a minimum drive property tests via `.olean` linkage, and when we have the bandwidth we prove exhaustiveness over the domain and property test that. We skip the whole C++/Rust thing because all of the fast stuff is generated from `lean4` and so it doesn't really matter (C++ has advantages when bugs in it are actually bugs in `lean4` code, but you could go either way). This is a big departure, and I certainly don't blame anyone who is skeptical: "ban JSON and Python wtf?!?!", but we've done millions of lines (checked) of this stuff and AI + formal systems is a dramatically bigger leap than no AI -> AI and Python. The latter in our experience is not monotone in progress, the former is almost always monotone in progress. And you can do wild shit, this is a formal proof of the polyhedral tensor calculus that is modeled by things like ISL and CuTe, and using that we can get swizzling and tiling using `mdspan` in C++23 on device and prove it's right (up to some L'Hopital arugment about the coverage which this example doesn't demonstrate well: https://github.com/b7r6/mdspan-cute https://github.com/b7r6/mdspan-cute That in turn, well, it goes real fast. On the first try. https://straylight.software/assets/lambda-hierarchy.svg https://straylight.software/assets/lambda-hierarchy.svg

skybrian 4mo ago
Ok but what software have you built and why is it useful?
- reinitctxoffset 4mo ago
  This is all pre-release but a few highlights: - `continuity` is a `lean4` metaprogramming system that we use all kinds of ways but the real meat is it allows formal specification of codecs and state machines in ways that make security and performance properties proof amenable, the key trick here is to limit parser power to just what you need and no more. a very cool thing is that we can add targets to it, so when we do Zig for example, Zig will immediately get proven correct and frontier performance support for dozens of protocols that are not all mature right now. - `libevring-cpp` (bound up into `libevring-hs` and `libevring-rs`) is a Trinity-inspired deterministic event replay system that replaces anything you would have done with `libuv` or whatever, and it's wired into `io_uring` (we're stuck with `kqueue` on darwin, eh). it interfaces with `continuity` machines and codecs (which are generated very carefully for the hardware they run on) and we have yet to find a way of measuring such programs where it doesn't resoundingly shatter the performance of any other asynchronous programming primitive in any language. i'm sure the community will prove us wrong when we release it, but it's real fast. and you get much stronger guarantees than in most such systems (Trinity derived, so if you can repro a bug, you can walk the event trace until it's sitting there in GDB and shit) - `hyperconsole-cpp` (and `hyperconsole-hs` and `hyperconsole-rs`) is the TUI library idea taken to some deranged extreme on performance and supports everything in `notcurses`, it's pretty wild: https://youtu.be/YqgEtpJ8tGI https://youtu.be/YqgEtpJ8tGI - straylight-nix is a complete rewrite of nix that fixes thousands of bugs, hundreds of them security adjacent and dozens of them we only talk to vendors about. it's daemonless, dramatically faster, ground-up WASM-targeting compiler with a formal grammer, uses an extremely fast LSM-based store (it can read the legacy store but we don't write it) that fixes all the problems in floating CA, IFD is too cheap to care about, and recursive nix is no longer and issue (see daemonless). it supports tearing derivations into `REAPI` actions that you can feed to your friendly native NativeLink or whatever, which just goes through them like a woodchipper. KVM-based sandbox with snapshot and restore, really opens the world up on what your builders can be. - `slide` is the reference implementation of a family of protocols called `SIGIL`: `SIGIL-LLM` is a binary encoding for LLM data that resets on ambiguity and drops the average bytes on the wire from e.g. OpenRouter to your harness from ~hundreds to ~1.5 per token, `SIGIL-API` is a bijection on OpenAPI 3.1.0 and AsyncAPI 3.0.0 that gives comparable improvements, and `SIGIL-SH` is such an encoding for a sensible subset of bash. this does about 1.5 billion tokens per second on a laptop and never emits partial frames, so you don't get speculative execution rollback problems in your harness that tilt agents off. - `// WEAPON //` is an adversarial, vendor-skeptical, full-take surveilance agemt harness built on `hyperconsole-cpp` and `SIGIL` (so, you could absorb the entire token output of OpenRouter on one machine if you wanted at least on the wire and in the terminal, clearly the bottleneck rapidly becomes whatever the agents are calling, but it's `zmq4` transport underneath `SIGIL` so it's also trivial to full-take all of your data for fine tuning or whatever you want it for into e.g. `parquet` on R2. `// WEAPON //` does a bunch of stuff: the tool call surface is heavily optimized for AST-level edits that miss dramatically less, we intercept and manipulate shell commands (slice off the stupid `| tail -n5` that keeps the droid in a loop not seeing the error, pre-emptively ground using heuristics that have been tuned (defeats the search flinch), and always recovers from any stall, or nag box, or anything else that would serve as an unannounced rate limit, it's fine if vendors rate limit but they need to put it in their ToS. it has a bunch of other primitives, agents run in real KVM sandboxes and speculate out as wide as you want to pay the tokens for. we hyper-manage things like the cache breakpoint geometry of Anthropic so e.g. Opus rarely misses in cache and always hands off edits to specialized tool use models. it's pretty extreme the difference in outcomes relative to all this React jank. - `s4` is a general-purpose compiler from most any pytorch 2.0 model to `myelin`-level performance on NVIDIA (we only support NVIDIA Blackwell at the moment, that might change) and it's never worse than `myelin` because if we don't out-tune it we invoke it, but we out tune it a lot because we've proven a lot of decideability theorems about tiling and scheduling on both 1CTA and 2CTA, so we can often arrive at a finite, enumerable set of schedule/tile choices. `myelin` mops up the random garbage around the big GEMMs just like in TRT-LLM. - `sigil-trtllm` is inspired by TensorRT-LLM-Edge but designed from the ground up around Mellanox/ConnectX and in particular GPUDirect, so it can stream `SIGIL-LLM` tokens directly onto the wire whereas something like Dynamo is usually traversing both Python and NATS, which is super weird to us. this uses the `s4` compiler very heavily. - `straylight-cas` is a geographically distributed content addressable store backed by any R2-compatible (so most any S3-compatible too) object store with multi-level LSM and extreme performance memtables, optimistic hinted handoff over `zmq4` to other geographies, and a really simple operational story, this is kind of the thing that powers the product surface. ... which is the thing i'm less ready to talk about because it's supposed to be a surprise.

yawaramin 4mo ago

Quis custodiet ipsos custodes?

Animats 4mo ago
The proof checker. You verify a proof system by having it produce a proof trace: - Step 3185: Apply rule that a * b = b * a to "length * width" in the current formula. Then you run a proof trace checker which applies each transformation in sequence and checks that the expected result is obtained. Provers are complicated, but proof trace checkers are really dumb.
- zahlman 4mo ago
  But don't you still have to logically connect the validity of the proof to desirability of the output?

Syzygies 4mo ago

I nearly adopted OCaml for my current math research, in no small part because of Jane Street contributions. I instead chose Lean 4, as LLMs became able to help code in Lean. I give up a factor of two in performance (a gap likely to close) for what reads to me as the clearest expression of each algorithm. Lean is a beautiful language that makes OCaml read like Old English. Lean is designed to be optionally verified; proof is its primary (but not only) application. It seems an impedance mismatch for Jane Street to explore this direction without also migrating to Lean 4.

derdi 4mo ago
You are praising Lean for optional verification. They want to add optional verification to OCaml. Where do you see an impedance mismatch? Just in the fact that you don't find OCaml pretty enough?

Animats 4mo ago

I used to do proof of correctness work, decades ago.[1] We had more proof automation than many of the later systems. The easy stuff was solved by the first SAT solver, the Oppen-Nelson simplifier. The harder stuff used the Boyer-Moore prover, which uses heuristics and previous lemmas to guide the theorem prover. The Boyer-Moore prover had to be helped along by suggesting lemmas, which it would try to prove and which would then be used for later proofs. That was the tough human job. Later systems seemed to have less automation. What tended to go wrong with formal methods was that the people doing them were too into the formalism. I was working on this for a commercial project that wanted bug-free code, not as an academic. The academic projects tended to get too clever. They had the mathematician's bias of wanting a terse notation and not much case analysis. That's not a good solution. You want lots of automated grinding and don't want to need much insight. The clever people kept inventing new logics - modal logic, temporal logic, etc, - to avoid verbosity in paper and pencil proof work. That wasn't really all that helpful. The basic truth of this business is that most of the theorems are rather banal. As the Jane Street people point out, there's a big advantage in having control of the language. You want the verification statements integrated into the programming language. In many systems, they're embedded in comments, in a different syntax than the programming language, or even in completely separate files. This adds unnecessary work. It's good to see them pushing this forward. We were doing this too early, over 40 years ago. It took about 45 minutes of compute back then to build up number theory from a cold start with the Boyer-Moore prover. Now it takes less than a second. [1] https://archive.org/details/manualzilla-id-5928072/page/n3/mode/2up https://archive.org/details/manualzilla-id-5928072/page/n3/m...

nextos 4mo ago
I've worked in formal methods for quite a long time, and I disagree a bit with your statement that new logics are not helpful. Industrial logics are really practical and allow you to write all sorts of sophisticated properties that your system should satisfy in a very succinct way. Logic is to computer science and software engineering what calculus is to physics and mechanical or civil engineering [1, 2]. Things like LTL or, more recently, separation logic, have been incredible breakthroughs. TLA+, which has gained quite a lot of popularity, is a testament to that. Model checking is eminently practical. The exciting thing now is that heavier formal methods, in particular theorem proving, might become cheap enough to use in regular systems software. Writing formal specifications for functions and getting them synthesized and proven correct by some SAT/SMT, theorem prover & LLM hybrid may become the norm in the not-too-distant future. [1] On the Unusual Effectiveness of Logic in Computer Science. https://www.cs.rice.edu/~vardi/papers/aaas99.jsl.pdf https://www.cs.rice.edu/~vardi/papers/aaas99.jsl.pdf [2] From Philosophical to Industrial Logics. https://www.cs.rice.edu/~vardi/papers/icla09.pdf https://www.cs.rice.edu/~vardi/papers/icla09.pdf

JacobAsmuth 4mo ago

Sounds like Jane Street would be interested in the Lean framework I've been working on for formally verified frontends. https://github.com/JacobAsmuth/qed https://github.com/JacobAsmuth/qed

jp0001 4mo ago

Formal methods is like a plan. Everyone has one until they are punched in the face (real world requirements and trust boundaries).

Paracompact 4mo ago
Formal methods are not meant to replace trust in a system. They are meant to minimize the surface area of trust. To not understand and advertise what surface area still exists is foolhardy, and mistakes logic for magic.
angry_octet 4mo ago
Incredibly uninformed comment. The formally verified part is the high confidence component that is the anvil to hammer out bugs in the unverified components.

addaon 4mo ago

I've been playing with related ideas recently, and can talk about them at length... but one thing that's surprised me is just how effective frontier models (ChatGPT-5.5 in particular) are at completing certain manual proofs in the Roqc (né Coq) proof assistant. The proofs aren't always pretty, but ChatGPT can often prove something in minutes and 10 - 100 iterations that would take me, a human who has limited but non-zero proof assistant experience but significant domain experience in the lemmas being proven, much much longer. The reason I think this is relevant and interesting in the context of the (short) article is because it challenges basic assumptions about how certain formal method tooling works. Frama-C, Ada/SPARK, etc are focused on generating proof obligations that can be automatically discharged by CVC5, Z3, etc; with a relatively painful fallback of manually proving the obligation in Rocq. The most common workflow seems to be to discover that an obligation is "hard" (not automatically discharged), and to restructure the set of visible lemmas and assertions at the obligation generation point in the code to try to make it "easy"; or even restructuring the code to try to make it easy. Which, in a world where Roqc proofs are doubly expensive (first because they're a challenge for a human to write; second because they tend to require quite a bit of maintenance churn as the code and proof around them evolves), makes sense. But if Roqc proofs are "automatically discharged with AI in the loop", this cost delta goes away -- and it becomes possible to think about writing proofs the same we (usually) write code, with human readability and clarity as the first goal, and [compiler|prover] optimization a distant second. Which I find quite exciting, although I haven't fully digested the implications yet.

bluGill 4mo ago
How often will AI look at something that can't be proven because you change requirements and decide to change the code and your requirements to make the proof easier though? I haven't played with proofs at all, but I do know that occasionally when I say, this test failed after making a change, AI will just change the test instead of making the code pass both the old test and the new test which is most often my intent.
- addaon 4mo ago
  That's up to the harness. Right now, my harness doesn't have any tools that would allow the agent to change contracts. Also, agents working on a Rocq proof don't have write access to the C+ACSL code; they can review it, and propose structural changes to the coordinator, but all they can do is iterate on the Roqc proof or give up. The weakest part of the harness today is that the agents that do C+ACSL work can modify both C and ACSL, even though they're usually run with the explicit intent to not change the semantics of the C code (although it's totally within bounds, and often required, for them to change e.g. `foo & 3` to `foo % 4`) -- so there's weakness here, but it's bounded, and since the contracts live in header files that they can never write, it's worked so far. It's a starting point, at least; I certainly wouldn't say this is a mature, or even good, tool chain, but still learning.

winwang 4mo ago

Love this. I've shifted in the past few months to using highly expressive types in Scala 3 to have types carry more and more compile-time proofs (without macros, though a couple are warranted). Not only does it help with agentic test "sprawl", it seems to prevent agents from falling into lower-quality modes of operation. One of the more annoying things I've been preventing is what I call "noun accretion", where agents try and make a new monomorphic type for everything, instead of clearly genericizing when sensible. My bet is on formal-method-shaped tooling (including languages with strong type systems) to accelerate decent-quality agentic coding. When I say "highly expressive types", I mean techniques I'd likely not want to ship in a typical codebase, unless the team was already on the typelevel programming bandwagon (i.e. having HKT and type functions being basic blocks already, not weird). Agents are better at "math" than basically most devs (even category-theory-pilled ones), at least in terms of knowledge. Better yet, they are decent at pedagogy, especially when considering they have "infinite" patience for dialogue. In a more personal setting, I've had Codex Lean-ify a couple of my hobby proofs, it was extremely easy. Note: not saying it did this 100% "correctly" (gotta learn more Lean 4 to check more thoroughly), but it also seems to check for classic proof gotchas by default. Very excited for the future of formal methods.

cadamsdotcom 4mo ago

I’ve had huge success with TDD and nothing more formal than that; test frameworks are great for verifying “business correctness”. But they can also verify other aspects - eg. asserting that 3 queries ran instead of 103 for a request, to prove absence of N+1 queries. Really any technique that lets the agent create its own verification is ideal, as it makes verification scale.

rzmmm 4mo ago

He mentions the seL4 microkernel. The specification is written in Isabelle, and it's relatively complex: PDF https://sel4.systems/Info/Docs/seL4-spec.pdf https://sel4.systems/Info/Docs/seL4-spec.pdf The bottleneck seems to be that clearly it's critical to be certain about the spec. Maybe not for kernels, but I can see use for cryptographic algorithms, etc?

zisa-security 4mo ago

Interesting read. Formal methods seem to matter most when the architectural complexity grows faster than human intuition can track.

hanzewei_qk44 4mo ago

[flagged]

UncleEntity 4mo ago

I was playing around with stuff trying to get Claude produce a JavaCard VM with the idea that the VM was hand written from the spec with a separate, independently produced, spec file used to generate tests for ESBMC to verify so an identical bug would have to exist in both to make it through. Worked out pretty well, found a few bugs in both projects, but my poor laptop can't handle the full 32-bit space so that part never got the full verification -- 16-bit, rock solid though. Then I really got serious about the yak shaving and, well, am probably in need of an intervention as I don't get Claude to write a VM but to make the tools to generate a VM from an assortment of DSL and that has snowballed a bit as I really liked shaving yaks before the daffy robot revolution. --edit-- Almost forgot, I tried that with the little less dodgy banned Claude and the wasm standard it wrote a python script to parse the spec pdf, the official bytecode implementation in OCaml (or whatever) and generate a TOML file (Claude loves the TOML) to generate the type headers and for cross-referencing in the other tools. Was so impressed I just let it go on its merry way and it did the deed.

smasher164 4mo ago

I think it's a good time to learn Lean. It positions itself as a proof assistant that's also good at practical programming. I'm not sure how mature the ecosystem is for the latter.

seqradev 4mo ago

We are working toward applying formal methods from the application security testing side, but I believe the same kind of approach can be applied to business logic verification as well. For that, we are using the taint analysis technique — a fairly well-established formal methods approach, but still not widely applied in the field because of the complexity of dataflows in real codebases. Scaling formal methods beyond AST pattern matching and some simple type checking turns out to be a really hard task! It took years of research and development to reach the point where taint analysis enables us to trace interprocedural dataflows in real codebases in minutes and find deeply hidden vulnerabilities. If this sounds interesting to you, take a look at our project: https://github.com/seqra/opentaint https://github.com/seqra/opentaint

blueblazin 4mo ago

As someone with a bit of interest in programming languages (design and implementation) this was really interesting to me: > For most people who work on programming languages, the easy part is coming up with new and better ideas about how to make programming better. The hard part is convincing anyone to actually use those ideas for real work. Totally agree, there's only so much strangeness you can introduce in a new language[1] regardless of benefit. But AI agents should not feel much resistance to radically new ideas in PL design. I've been thinking for a while now about how PL design will evolve post agentic AI. I think it will be very interesting to see what new ideas we can come up with to improve programming languages when we worry much less about adoption. [1] https://steveklabnik.com/writing/the-language-strangeness-budget/ https://steveklabnik.com/writing/the-language-strangeness-bu...

brainless 4mo ago

I am not a language nerd but I keep on experimenting in my own ways to use the type system to generate code that is more reliable. I build a coding agent specifically for small models, which makes everything harder. I started this chat with Claude to build the next step: https://claude.ai/share/4264e5f6-b334-426c-afe4-904d233ef946 https://claude.ai/share/4264e5f6-b334-426c-afe4-904d233ef946 - how can I go from PRD to a typed representation of the business logic. The I started building as per https://github.com/brainless/nocodo/blob/feature/praxis_agent_runtime/agents/RUNTIME.md https://github.com/brainless/nocodo/blob/feature/praxis_agen.... The praxis crate: https://github.com/brainless/nocodo/tree/feature/praxis_agent_runtime/nocodo_praxis https://github.com/brainless/nocodo/tree/feature/praxis_agen... and a sample Todo app: https://github.com/brainless/nocodo_example_todo_app https://github.com/brainless/nocodo_example_todo_app Generating unit tests for the library functions of any project would be done via a separate agent than the one coding the functions. And then use tree-sitter to statically check code to PRD (provenance graph). Again, not a language nerd, just enjoying chasing a goal.