News for hackers. Stuff that matters.

A comment on AlphaProof Code. Parent comment

Re:AlphaProof Code by derefr on Tuesday November 10, 2026 @01:57PM (#50444606)
I'm actually unclear on whether they just translated the design of the protocol to Lean, or translated the app's implementation of the protocol to Lean.

The wording of the article is a bit too ambiguous to say either way, I think? They just say they "generated" the Lean code; they didn't say what it was being generated from.

[ Parent | on HN ]
Re:AlphaProof Code by pcthrowaway on Tuesday November 10, 2026 @10:55PM (#50449578)
From this I think it's a given that they were talking about the implementation, not the specification

> To confirm that AlphaProof Code can tell correct code from buggy code, we reintroduced two real, previously fixed bugs into an isolated version of Signal's code. In both cases, the system produced a machine-checked proof that the buggy version was insecure.

[ Parent | on HN ]