Feel like “translating the proof into your end product” is a bit of a “draw the rest of the owl”

You assume lean can express more than it can.

Unlike Postgres, the average product isn't written in C or C++, so it's probably better. People (even the Rust fans) underestimate how many footguns are everywhere in C and C++. Even the best developers write security bugs not infrequently.

And the average product is solving much easier problems (in terms of low-level programming, which is where the worst bugs tend to be) than a high-performance database.

The average software product is worse. Lots worse.

And half the software products are worse than that.

Any organisation that said "let's move fast and break things" is now busy finding out what's actually broken.

Most likely pretty bad. It's not all that difficult to sweet talk Fable into doing a security review of a code base. I've pointed it at a few of the major open source projects in the main tech stack I work with and it found dozens of bugs in each. Many were fairly minor, and some of the more significant issues relied on fairly narrow attack vectors (for example, a compromised DB server being used to attack a web server). But this was just a single search pass, literally a few lines of prompt and an hour's worth of agent time.

Postgres is old but a lot of its features are new. You can't really say it's mature software, as much as it has changed over its lifetime.

Truly mature software doesn't get used, because people see low activity on github and assume it's "dead" or see no new features in years and assume that it's stagnating.