HN

Comments (38)

• Menu

  wbeckler
  I think the royal combo is Lean 4/TLA+/etc. plus AI plus a deterministic generator. For large systems formal method assertions need to be compressed down to a human comprehensible size. This can happen when the assertions are confirming the accuracy of a model and its attached code generators. The generator can generate proofs of the generated code and a human only needs to ensure that the generator provably generates the correct mass scale assertions.This is how formal methods can constrain AI for large systems.We're doing this at the Open Markets Initiative, where we've generated millions of lines of Lean 4, TLA+, and Rocq that ensure that our open source electronic trading protocol code is accurate. We didn't expect it but the Lean prover did identify some incorrect steps. https://github.com/Open-Markets-Initiative
• Menu

  chamomeal
  What do people think of property based testing? I’ve set up a few property based tests and it feels almost like formal verification.I know it’s not the same thing, but PBT’s can catch all sorts of absolutely crazy bugs that I never would think to check for. Stateful stuff, cross-service stuff. My only gripe with PBTs has always been the tedious setup, but LLMs solve that.I haven’t seen much discussion around PBTs lately, but you get a ton of bang for your buck in the LLM age
• Menu

  PandaRider
  > ... But we expect, in the next few months and years, people will focus way more on the specifications, on the models, on the properties you want the software to have.Does anyone have resources on learning modelling for formal verification? (Does not have to be in Lean)
• Menu

  beecasthurlbow
  If you use agents to generate formal verification, how do you tell if the properties that are verified are the correct ones?
• fspeech
  Currently the foundation theories in mathlib are built with the assumption that formal proofs are expensive. Concepts are fragmented to share as much proof as possible. With LLM the assumption is no longer correct. Concepts and proofs should be built to fit human thinking as much as possible and proofs can be ported by LLMs between theories. Lean would ensure that the translation is correct.
• Menu

  westurner
  Examples of comparing the results of Lean and e.g. Rust as is described in the video?I have symbolic error terms in Lean that I guess can be sampled and compared to Monte Carlo analysis? But I already had sampling-based analysis, that's why I had to do all of this (double-slit experiment and gravity with GrC(2,4)) in Lean 4.What would it take to combine Lean and one or more Rust TLA+ implementations? How does an agent plan and implement this and what are the advantages and disadvantages?"Comparison of Isabelle/HOL, Lean, HOL4, and Agda: A Tale of Four Theorem Provers" (2026) but not Rocq? https://news.ycombinator.com/item?id=50043202
• Menu

  jdw64
  While learning and applying formal verification in the context of using AI agents, what I feel is that sometimes it's hard to express my own thoughts as formal verification. But more than that, I doubt whether formal verification being done correctly actually solves the phenomenon of AI spinning in circles on a specific task.For example, I want to eat chicken, so I try formally verifying "chicken dish," and every time GPT or Claude starts digging into the origin of the sauce in the chicken dish or the breed of the chicken. Then the chicken dish never gets finished and never makes it to dinner, and instead I gain deep knowledge about the origin of chickens.Of course, I know that formal verification has liveness — meaning that there must be progress in the work is also part of formal verification — but the AI judges that learning the origin of the chicken counts as progress too. Yet it ends up doing work that it actually shouldn't be doing.Personally, while organizing these AI anti-patterns, I feel that when you formally verify one condition, verification of another condition gets weakened, and within that phenomenon I sense the AI spinning in circles again. In the end, I end up going through the process of reading and merging everything one by one myself, and I want to know whether this is something only I experience.
• meirwolf1289
  [flagged]
• aaron695
  [dead]
• tug2024
  [dead]
• Menu

  logir22
  [flagged]
• mentalgear
  ... somewhat disappointed the guy is now associated with AWS. I guess I was hoping for a non-profit organization.
• shevy-java
  I noticed a problem in the "AI is our future!" crowd.What they do, does not really interest me. With that I mean it is nice that they can solve many problems as-is, and that will probably become more important - but I am just not interested in looking at AI project. It is totally meaningless to me.In the past, when you, say, have a project written by a real human author on github, this could be interesting. With AI generated projects, I just don't have the slightest interest in "connecting". I also don't think to be the only one; you notice this on youtube too. Some people no longer have an interest in AI-generated videos and avoid them. I am curious when the AI hype phase will go down; right now it seems to not come down but I think it eventually will.
• zujkas
  Nobody verifies it because there isn't a ZFS axiom system for software development and you first need a spec to prove anything-Then perhaps fix Lean's type system, which isn't really understood and has holes.Can these AI-monied people shut up for a single hour?