Peter Schwabe, Benoît Viguier, Timmy Weerwag, Freek Wiedijk. A Coq proof of the correctness of X25519 in TweetNaCl. IACR Cryptology ePrint Archive, 2021:428, 2021. [doi]
@article{SchwabeVWW21,
title = {A Coq proof of the correctness of X25519 in TweetNaCl},
author = {Peter Schwabe and Benoît Viguier and Timmy Weerwag and Freek Wiedijk},
year = {2021},
url = {https://eprint.iacr.org/2021/428},
researchr = {https://researchr.org/publication/SchwabeVWW21},
cites = {0},
citedby = {0},
journal = {IACR Cryptology ePrint Archive},
volume = {2021},
pages = {428},
}