[flagged]
I had a dig and found that ssh had in fact been done 9 years ago, tho it doesn't seem to have made it to a distribution: it's an offshoot of the CryptoVerif project[1] (which is, maybe unsurprisingly, under the umbrella of the same Prosecco team at Inria who worked on Project Everest). In 2015 Bruno Blanchet and David Cadé wrote a paper "From Computationally-Proved Protocol Specifications to Implementations and Application to SSH"[2] which describes using CryptoVerif to generate an implementation of SSH from the spec; the code is in the CryptoVerif tarball, but someone's helpfully put that up on github if you want a look[3]
The eye opening bits in the paper (given the claims of tinyssh to be small at The bad news would be that it's not very performant: 30MB/s compared to 90MB/s for openssh on the same hardware, in the paper. Since HACL is from the same stable and was designed to perform well as well as be verified, it might be worth dusting off and seeing if this could be made more usable. The implementation probably has value even if just as a test oracle.
[1]: https://bblanche.gitlabpages.inria.fr/CryptoVerif/
[2]: https://bblanche.gitlabpages.inria.fr/publications/CadeBlanc...
[3]: https://github.com/mgrabovsky/cryptoverif/tree/master/implem... the official implementation appears to be here now https://gitlab.inria.fr/bblanche/CryptoVerif/-/tree/master/c...