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" or "will it ever deadlock", etc. It's still perfectly possible for the code to do all of those things; it's just known that, as of the moment they did this analysis, none of those low-level problems will 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.