#13: Rod Chapman – It's Either Automated or It's Wrong

<p>Rod Chapman explains his recent verification of TweetNACL using SPARK/ADA. We discuss how every aspect of his proofs are automated, how the correctness proofs actually enabled better performance after compilation, and higher confidence in some otherwise risky-seeming optimizations.</p><p>Watch all our episodes on the <a href="https://youtu.be/98_egT5VGCY" target="_blank">Building Better Systems youtube channel</a>.</p><p>Joey Dodds: <a href="https://galois.com/team/joey-dodds/" target="_blank">https://galois.com/team/joey-dodds/ </a></p><p>Shpat Morina: <a href="https://galois.com/team/shpat-morina/" target="_blank">https://galois.com/team/shpat-morina/  </a></p><p>Rod Chapman: <a href="https://www.linkedin.com/in/rod-chapman-7b60266">linkedin.com/in/rod-chapman-7b60266</a></p><p>Galois, Inc.: <a href="https://www.youtube.com/redirect?event=video_description&redir_token=QUFFLUhqbnVzaUtCYnpWTjhZTDhqaHBJa0R0TDU1Y2VHUXxBQ3Jtc0trQVVFSHFDYTM5TUpPbXZraHN1VU0zWFRfZ2ZNTHRPWWZJeThwLVFZQy0wemphLTlhVU5xajV5VUhPQmFHUk1ocFRUM1hXcjNGZGtzRk41RDlDLXpDSEpxWlVUcHlNaEhqYVVuSHQ5MkJsZDhLSzBmRQ&q=https%3A%2F%2Fgalois.com%2F" target="_blank">https://galois.com/</a> </p><p>Contact us: <a href="mailto:podcasts@galois.com">podcast@galois.com</a></p>