The security auditors themselves would never actually word it like that in their reports, because the statement implies a degree of certainty that cannot really exist.

Here's an example of what the auditor's actually said:

"Auditors identified two low-severity vulnerabilities. Additionally, five general recommendations were reported. At the same time, we confirm that no important security issues were identified during the pentest."

There's a reason that audit reports will never say outright that something is "secure". They may say something like "strong and effective security measures are in place", but that's a very different kind of statement.

I think the article itself is great but the headline just falls on the wrong side of being a bit hyperbolic and seems to be optimised for marketing impact over accuracy.

Nothing at all; it's a broken model. The server can at any time start serving malicious payloads [0]. The server hosts your mail but they also serve the webapp. The clientside decrypts the mail, but the server hosts the client code...

It's a fundamentally flawed idea, trying to retrofit encryption into email in this way, when the server essentially has to hold all of your mail. In this case, the only thing that would make me feel secure in using it, is a third-party OSS client that downloads the mail without using the webapp, using only client-side code. And even then, of course, the mail can simply just be not encrypted when being ingested by Proton. So even then I wouldn't really trust it without external encryption like PGP. In which case, why bother?

To be clear I do use private email services (protonmail, tutanota) but I am simply not going to fall for the illusion of guaranteed privacy; I just trust that they are what they say they are. They are still a better option IMO than something like Gmail, but I don't think they're a silver bullet.

[0]: If you think this is unlikely, see this: https://news.ycombinator.com/item?id=25337507

Typically: don't do that.

Nevertheless, if you insist: you can claim a certain abstraction of a system guarantees certain mathematically expressed requirements cannot be violated by a certain attacker model once you've formally proved that.

Of course, all implementations have implementation details which violate the abstraction, your mathematically expressed requirements may not fully capture your intentions, and in practice, an attacker may have additional options that your model doesn't consider. But hey, now you can truthfully claim that "the system" is "secure" - for some values of "system" and "secure".

https://en.wikipedia.org/wiki/Evaluation_Assurance_Level

Proton is claiming something similar to EAL4, which is not secure, there is an assurance that not all trained reviewers can find a vulnerability. Openssh is a little less secure than that formally, but has more trained reviewers informally, which probably cover some parts extremely well and other parts sparsely.

You can write all of the tests, you can get all of the audits, but there’s nothing that’s going to stop a 13-year old polish kid from mucking about in the guts of your tech. Security isn’t a promise you can make in absolutes, at some point you have to ship and you hope that you did everything well enough that there’s no low-hanging fruit.

There’s no such thing as a secure system, only systems which are more expensive to compromise.

It does build confidence in the security to perform security audits.

here’s a maybe wild take, uh, never?