> They took a non-trivial piece of human-written code that has had bugs in the past, formally verified the whole library, and found zero bugs?

Well, if it's SSH then I sure hope it has no LLM-discoverable bugs.