Hacker News

This article is not saying that AI did the proof magically. Their statement is quite clear, the agent system helped human experts for the proof, going back and forth at different steps. The complexity came from the size of the codebase and the compiled implementation, which an AI-assisted process was able to tackle at much greater speed than a meat-only team of experts would have. The experts are still responsible for designing the mathematical specifications, and maybe along the way something was wrongly designed, but I still feel much safer about Signal's architecture and implementation.

Rust need not apply, since the proof is about the libsignal-cli ELF binary, compiled under reasonable assumptions (single-threaded, statically linked, etc). The semantics of the some-hundred instructions in their language in Lean were tested to adhere to Arm-provided ASL spec, as compared to two independent emulators.

It's not and we don't. We can however run some lean in rust with things like https://github.com/conao3/lean-rs

Or you can use verus instead which does automatic mapping from the rust code to the proof where possible.

I mean typically the answer to this question should be that the underlying compiler has also been proven and both proofs cover a guarantee of no undefined behavior in either implementation

Yeah this is what people want, less hype, more "boring" but useful examples of a powerful tool.

Do you have some examples of this misaligned behaviour?

yeah it's nice and all but you're not providing evidence to back all those wild claims you're making

This.

Now, write a theorem describing a non-trivial piece of software. Is your theorem longer or shorter than the source code? Easier or harder to read?

In many cases we don't even know ourselves what the program should do. There are many edge cases, business decisions, dark and not dark patterns, misunderstood requirements, etc. What can it verify, that the program is doing correctly what we actually did not want it to do? At least we could end up with no bugs in the ORM, but it's not there that my customers are making money.

Right. The paper notes that they stubbed out all the trickier crypto and system call routines with contracts. If those routines don't adhere to the modeled contracts in real execution, then the proof's guarantee won't hold. Also things like concurrency and signal handling are intentionally not modeled.

I think this is an incredible result and I hope we'll see more and more of it, but even still, it's verifying a pretty thin slice of an actually executing system!

Why? We already have formally verified microkernels in production (Apple's L4 variant in their security enclave, for example). I'd say the tools are mostly there, it's a matter of scaling, and maybe a matter of adapting code to make verification easier. Both things where LLMs can shine.

The biggest hurdle is probably the number of bugs in most code. Verification would mean fixing all of those as well.

The thing about exponentials is that we can go from "we're not even close" to "all software in the world was getting aggressively hacked and we figured it out to stop that from happening" very very quickly. I would not be surprised if by this time next year we had some sort of nist standard for formal verification or something. It certainly changes things a lot once llms can solve millennium problems

We're starting to get there with stuff like the compression thing.

> Most software verification is proved "for all possible inputs", e.g. the system maintains some invariant regardless of which sequence of actions is taken.

Without suggesting that this has no value-- it must be noted that such verification only applies on theoretical hardware and to the specific behavior in scope of the verification. Actual hardware is nondeterministic, and an algorithm can be correct while suffering from a side-channel.

Have seen that as well. A ton of the extra eng productivity has flowed into better eng practices

Any engineering layoffs? Still hiring? Frozen?

How often do you need to change the actual library which does the encryption for the signal protocol? Adding features to the app does not require changes to the encryption.

That’s not a great source to support your claim. From the paper

> The resolution (decompression) of such backreferences in an imperative context is trivial, but uses lots of invariants that make it hard to prove correct. In a purely functional context, it is non-trivial to find data structures that are fast enough. We decided to stick with purely functional algorithms, as they can be verified directly using Coq, and optimization of purely functional programs is interesting for its own sake. In our current verified implementation, this is the slowest part. The benchmarks in Appendix 0.A support this claim. We already have figured out an algorithm with better performance, but we are not yet done proving it formally correct; we will not get deeper into this algorithm in this paper.

There are many ways verify programs; the authors of your linked paper just chose a method that resulted in a slow binary. Alternatively, one can build a model of an imperative language (C) and prove that an imperative programs meets some specification.

There was recently a decently fast implementation of DEFLATE in Lean: https://kim-em.github.io/blog/2026-7-24-why-lean-is-faster-t...

It took 4 weeks according to the Article.

so, millions? billions?

Hmm. Which means that they just luckily don't have to prove anything about any software that might halt...? Or?

Like, they use some pretty stark terms here:

  Formal verification—mathematically proving code runs correctly without flaws—is the highest standard of security assurance; however, it is difficult and often labor-intensive.

I type this message to you all with sadness in my heart, cause I know I could get a better answer 100x faster by just asking an agent to research, which I could then have it dumb down to my level until I grasp it. I don't really know what the point of forums are, anymore. It's undeniably hard not to see ourselves as a planet of sad, fragile monkeys wasting away the hours between birth and death. That was already the case, perhaps, but at least learning and sharing knowledge about engineering in places like this felt like a somewhat meaningful way to positively impact the material conditions of my fellow humans, even in an indirect way. As of November 2026, I'm just the taste/framing component of artificial minds that seem overwhelmingly likely to develop their own within months or maybe years.

For a long time (since noticing the singularity) I've felt like someone doused in napalm and set alight while falling through the sky, frantically trying to put myself out while fixing my broken parachute. But post-Mythos I can't help but fear that there is no solid ground below. Just endless void. :(

there certainly is a relation; you might not be able to prove all the properties you care about because of the halting problem; but that is more a theoretical problem, not a practical one

still a big codebase: https://github.com/signalapp/libsignal

And it's never the crypto that breaks, it's usually something else.

E.g : Pegasus spyware don't break whatsapp crypto either

White-listing contacts would have prevented the gaffe when a journalist was added to a war planning group

    Well the NSA is probably decent at building software. 

It's not just total compensation. Working on classified stuff can be a bit of a career killer, since you can't talk about your past work when looking for a new job.

Plus there's the antipathy toward the current Trump administration, and the general moral unwillingness of many to do defense-related work in general.

Also, last I heard, cannabis use was still a disqualifier for DoD work and/or various security clearances. There are periodic ongoing polygraph tests, not sure about ongoing piss tests. The government is big; I'm sure the exact policies differ from department to department. But this turns a lot of people off.

Of course, every single thing I've said above might also be viewed as a positive by some engineers. Maybe they attract enough "true believers" to more than make up for the other factors.