Last week, I was able to visit the University of Bristol CyberSecurity CDT and Cryptography groups to give a long-overdue seminar about SPARKNaCl. The talk goes into the motivation for development SPARKNaCl in the first place, the formal verification of the code, and the subsequent performance optimization work. The CDT staff were able to record the seminar and it’s now available here.