Implementing AES and DES in ACL2 Warren A. Hunt, Jr. This talk will summarize implementing AES and DES in ACL2. Both implementations have been compared to reference implementations, and in the very few cases checked, produce the same results as specified by their respective standards-based definitions. Possibly, more interesting is the fact that both definitions are guard verified -- and, in one case, the guard verification of a helper function produces a guard goal that exceed five megabytes to print.