AlphaProof Code (deepmind.google)

It's that, yes.

They didn't prove that the code has no bugs; they proved that none of the current bugs (known or unknown) are security-breaking bugs, per their formalized security model.

> First, our researchers collaborated with a mix of models to translate Signal’s security goals into formal mathematical specifications, with human experts reviewing every one. From there, agents powered by Gemini Carbon did the proofs, generating over six million lines of Lean, a computer language that mathematically proves the accuracy of code.

The generated Lean code here is just being checked against the "formal mathematical specifications of Signal's security goals", not checked for the low-level properties you might care about as a programmer, e.g. "will it ever leak memory" or "will it ever crash", etc. And in fact, the code is not even being checked for the reachability of non-security-violating protocol failure states, e.g. "could the protocol ever deadlock such that neither side can send messages any more".

It's still perfectly possible for the code to have all of these problems. It's now just known that, as of the moment they did this analysis, none of those low-level problems, as far as they exist in the codebase, can cause a security-model violation.

Or, to put that another way: the system has been proven to "fail safe" in all its current failure modes, per their specific definition of safety (which is basically "keeping to the security guarantees Signal markets itself to users as having".)

Software doesn't exist in a platonic state like formal mathematics, which at least can be consistent with all other results. Software interacts with the real world and "bugs" can be any number of security weaknesses like emitting useful timing signatures, buffer overflows that depend on the compiler used, weaknesses on certain hardware, etc.

It is great that Google has formalized code to some degree and for software that MUST be hardened, this may be valuable. It may be generally useful, but we need to get a feel for the gaps that inevitably will persist.

Real software needs mind blowingly complex specifications and while it's now fairly easy to get an AI generated proof that your code follows the spec, there's not much to help you with bugs in the spec.

AI will happily change the spec for you so the code verifies though, but that doesn't solve the trust issue.

Truly a trusting trust scenario.

They all don't trust each other.

It's going to take way more than throwing a more advanced LLM at the problem to make any progress.

At least in domains that are "important" (and perhaps everyone thinks their business/API is important?), I'd want this.

For example - Stripe. If I'm using the stripe API, I want it to be guaranteed to work exactly as documented in all scenarios, given that money is at stake?

Getting the Stripe API written in Lean is a different challenge, of course.

Most software verification is proved "for all possible inputs", e.g. the system maintains some invariant regardless of which sequence of actions is taken. Those inputs could be from a user interacting with the software, or they could be API calls made to our library, etc. There's no reason you couldn't model an AI agent's choices in a similar way: i.e. prove that the desired invariants hold, for all possible sequences of actions the AI component might choose.

That might be straightforward, if the AI agent is constrained to pick from a simple set of domain-specific actions. In contrast, we can't say much about a system involving an AI agent with a full Bash shell.

> What scenarios does it make sense to have a lean proof from the start?

It's usually much easier to verify software that was written and structured with that in mind; rather than trying to reason about some arbitrary blob of code after-the-fact. So, if you do want to prove stuff, it should very much be in there from the start.

We need proof systems that are designed to work with our programming languages- working with the code so it more likely represents reality. I like verus with Rust and I have a skill for using it: https://github.com/gregwebs/skills-sdlc/blob/main/skills/rus...

My current workflow is i have a coordinating agent, and then a bunch of long running sessions that are specialized (CS theory, Kernel, Surface, Lowering/Backend, Corpus, Docs, etc). I only talk to the coordinator, they only accept tasks from the coordinator, but they can ask each other questions. None of them do their own coding, they assign coding tasks to agents/workflows. The main purpose of that is to stop it from blowing out context windows. Each has a million tokens of long term context and their own memory/claude.md etc, and they don't waste it by writing code directly. All work is assigned via github issues and answered with PRs. The coordinator mostly just keeps big picture goals in mind and manages PRs, etc..

I've currently got a fully formally verified borrow calculus and effect algebra, with a formally verified guarantee of memory safety and that all programs either continue (don't get wedged, no deadlocks), or they terminate with the heap empty. The only thing _not_ formally verified is the lowering to LLVM.

The language is mature to the point that I have real programs in it...

The extra velocity has meant we move considerably faster than the product team, so a lot of that extra dev capacity has been channeled into improving our tests, verifications and automated review processes - so hardly anything is slipping through the gaps.

This is the opposite of what I expected when we started working this way. One of the concerns we as a team raised was that it would lead to more bugs and lower quality but after 6 months the opposite appears to be true

Use s real password with the signal account thing.