[Animats]

Well, here's the code that Go uses to do elliptic curve encryption:

https://github.com/golang/crypto/blob/master/curve25519/squa...

It's in assembler, with no comments. It's from Bernstein's code, via Supercop, and is not original to the Go team.

A recent effort to formally verify that code, out of Taiwan, Japan, and the Netherlands, found one bug not previously detected by testing.

http://delivery.acm.org/10.1145/2670000/2660370/p299-chen.pd...

This stuff is really hard to get right.

[Khao]

Your second link gives me an error.

[Animats]

Here it is without the ACM paywall:

https://cryptojedi.org/papers/verify25519-20140428.pdf