Yu Feng (Veridise) on formal verification - https://www.youtube.com/watch?v=av7Wq742GIA

Zcash bug write up - https://electriccoin.co/blog/zcash-counterfeiting-vulnerability-successfully-remediated/

Soundness

Completeness