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

Building Better Systems - A podcast by Galois, Joey Dodds, Shpat Morina

Categories:

Education Technology

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.