Sure, but is it not possible that a hardware acceleration, if not also proven correct, could subtly undermine an otherwise valid software implementation?

I do not assert that this is the case generally, nor particularly here -- I would be quite happy to be wrong about this. But if there's one thing I've taken from my admittedly minor study of crypto is that the most trivial of details can be critically important, and failure to get a detail exactly correct can compromise an entire algorithm and anything built thereupon.

I would love to see hardware acceleration for ed25519, just like there's been hardware acceleration for AES. It could help drive adoption of an algorithm that is less fiddly and easy to get wrong than RSA, and maybe in another 15 years, I'd be able to purchase IT equipment that supports ed25519 and not just hardware accelerated RSA and AES.

Correctness alone is not sufficient. A crypto implementation also has to avoid introducing side channels. He describes how he avoids introducing a timing side channel (can't have any conditional branches that depend on the data) so it seems he took care to get that part right.