At what point is that mantra pushed by a state to keep their holes active in existing crypto libraries?

Maybe it should be "never roll out your own crypto without independent review and verification as well as thorough testing" .

We had to sign a 'contract', promising never to implement our own crypto!

That's dumb. It gives the impression the cryptographic library developers are grown in the lab or something.

Guess what, cryptographic library developers go the same schools as the rest of us. That's there's some sort of development that's somehow out of reach for "regular" devs is elitist and counterproductive.

It means there's a generation of graduates that don't do systems programming or anything where security is important.

Schools are dodging the important societal responsibility of teaching students how one designs and implements software that really, really needs to be correct.

Are most crypto libraries verified? I'm not sure they are!

The main ones certainly are nowadays. With some regularity, our customers ask us to verify some of the software or dependencies they're using, and this sometimes includes cryptographic libraries. We would then check the parts which the customer actually uses, so not all of openssl for example, but in general yes this is being looked at. These fixes are always upstreamed, by the way, although it's up to the customer whether they want to handle it themselves or whether we do the responsible disclosure process.

What tools do you use for verification? We don’t have many verified compilers yet so even if you verify the code how do you verify it’s compiled correctly?

For all I know I've got 5G implanted, how am I to verify that? Obviously the implant will make whatever measurements I do return the wrong results.

Gotta trust something, we decided we mainly trust the OS download and the repository keys that came with it.

Anyway we seem to have been talking about different kinds of verification, like checking that what Joan Daemen and Vincent Rijmen wrote is really what your CPU is executing versus verifying that implementations of a trusted algorithm aren't broken. We're not in the conspiracy theory or incident response business, so unless someone comes with something that sounds like we should forward them to incident response, the former is not what we do.

Formal verification is a thing people do - and I think that’s what most people think from ‘verified’. They aren’t conspiracy theorists they’re proving things like that your C implementation code is defined and matches what you think you’ve written, since that’s where these errors creep in.

you can do those things under the assumption "the compiler is correct". That still very much counts as formal verification.

So you're going to a school (which I assume you've paid for), to learn about cryptography - only to be told "don't ever bother"?

Of course at some point some people will have to implement crypto.

But I think a good way to think about it is this: This shouldn't be on top of your list when you learn crypto. Before you even think about rolling your own crypto you should break other people's crypto. That'll help you to gain deeper insights in how the whole thing works.

(Disclaimer: I broke other people's crypto, I wrote papers about it. I still never tried to roll my own crypto.)

That's how it always felt for me, yeah.

At peak, and in multiple independent courses, the teacher would step through a well-made AES key schedule visualization while none of us are (even planning on) doing the heavy math studies necessary to design a successor to or find vulnerabilities in something like AES. Most of us would be software engineers, sysadmins, or perhaps a handful of us might go into security fields like forensics or pentesting. The internals of AES are completely irrelevant. A curiosity maybe, but not something to be quizzed on. Then I went to do my master's and the teacher started about caesar ciphers...

All formal cryptography-for-non-cryptographers education I've ever had was completely useless (I was in tertiary education in the Netherlands between 2010 and 2018, in case anyone is wondering how dated this is).

The concept of authenticated encryption was mentioned in passing I think, though in one course I had to prompt the teacher to mention that as what you would want to be doing, but got far less attention or practice than doing things like a Caesar cipher or AES key schedule by hand.

Merely knowing that you have to look for the keyword authenticated encryption (when you want to do encryption for some reason) would already be enough in my opinion, from there you can find good answers. Or for secure connections, keyword searches should include something about key distribution/verification and, if you want to use something configurable like TLS, also configuration choices like enforcing allowed protocol versions. Which versions those are, that changes over time and there is little point memorizing it. You should just know that you should look into this when you need it.