Riad Wahby discusses a particular zero-knowledge proof called GooSig. Riad is a PhD student at Stanford University who works with Dan Boneh, Christopher Jeffrey, and Joseph Poon using GooSig to enable a privacy-preserving token distribution scheme for the Handshake Naming System. Most of Riad's work is in ZK proofs and verifiable computation.
- GooSig reference code
   https://github.com/kwantam/GooSig
- Handshake's GooSig implementation
   https://github.com/handshake-org/goosig/
- Systemization of Knowledge: Computer-Aided Cryptography
   https://eprint.iacr.org/2019/1393
An overview of current efforts at provable cryptographic software.
- Fiat Crypto
   https://github.com/mit-plv/fiat-crypto
Work out of Adam Chlipala's group at MIT on generating certified
implementations of crypto software. Now used in BoringSSL!
- miTLS
   https://mitls.org/
A certified implementation of TLS. There's also been plenty of work
since then by (some of) the authors on proving security of the TLS 1.3
protocol, e.g.,
   https://www.microsoft.com/en-us/research/publication/implementing-proving-tls-1-3-record-layer/
- HACL*
   https://github.com/project-everest/hacl-star
A formally verified cryptographic library, used in Mozilla's libNSS.