HN

Need help?
<- Back
AlphaProof Code

AlphaProof Code

ilreb

Comments (49)

  • nicou
    Nice to see this actually being done. I thought it was a very interesting idea when I read Martin Kleppmann's post about it a while back: https://martin.kleppmann.com/2025/12/08/ai-formal-verificati...
  • thibsrn
    Great, what a great use case for AI. I feel like Google has been the cleanest of the big players in terms of useful contributions and control of their AI systems. This new proof agent doesn't seem to challenge the spec though, just the implementation, if I've understood correctly.I wonder how this agent is different than a classic coding agent, in the end it seems to work the same way, iterating over a codebase while writing Lean or Rocq code and running it.
  • Mizza
    I'm expecting that very soon, perhaps in the next two or three years, it will seem mad that we ever ran _any_ unverified software on our systems, like how it now seems mad we used Telnet or plaintext HTTP.
  • 0o777
    Do I understand correctly that they verified the entire libsignal Rust library and not just a human-written spec of the Signal protocol?Also I noticed something in the libsignal protocol:>attest: Functionality for remote attestation of SGX enclaves and server-side HSMshttps://github.com/signalapp/libsignalHow trusted are Intel's (SGX) and AMD's hardware level security features?Cloudflare runs their edge network in random ISP datacenters and in shady jurisdictions and promise AMD's TSME is enough to keep things secure.
  • fercircularbuf
    Awesome. I remember thinking last year that software is about to get a lot more buggy now that people are offloading more to AI, but tools like this give me hope that perhaps the future of software actually looks a lot more safe.
  • sim04ful
    Curious question, in this case for verification they ported the software into a formal mathematical model. Why can't software development start from the other end instead ? Start with a formal model with the properties you want, then translate it into software.
  • beernet
    >> AlphaProof Code is a multi-LLM agentic framework that splits the work of formal verification the way a research team wouldNot sure if this is precise. At least it sounds somewhat odd. I think what they really wanted to say here is "multi-agent system" (which usually, but not necessarily, implies the use of multiple LLMs).
  • hoppp
    This is the way. I have been working on similar.Since code is cheap there is no excuse to not have verification everywhere.
  • hmokiguess
  • throwaway198846
    I hope it will be possible to verify CPUs soon as well. Of course that is much harder because they are not open source and physical and you need to simulate physics to verify them fully.
  • anon
    undefined
  • xrisk
    wonder how many dollars were spent on this
  • nurumaik
    Now pls do telegram to settle "telegram shouldn't have invented their own crypto" debate once and for all
  • whattheheckheck
    "human experts work with AI to decide what to prove"Why can't ai do this too? Is this the fundamental limit of ai?
  • whattheheckheck
    How do you prove the lean code represents what the code its proving?
  • yread
    They thank Sundar Pichai. I guess it makes sense but at the same time...
  • paganel
    I'm not at all versed in this "formal proofing" thing, but without diving all that much into it how does this handle the halting problem (and the related problems that in the end all point to said halting problem)?
  • p-e-w
    It’s nothing short of amazing that a huge codebase like Signal’s is apparently not only secure in a practical sense, but secure even in a strict formal sense. The people who wrote the Signal code must be engineers of the highest caliber.
  • Computer0
    I'm pleased to read Signal looks good to our robot mindlords.
  • anon
    undefined