The starting-point of my talk is a project at AWS to develop a 
library of verified cryptographic arithmetic primitives
(https://github.com/awslabs/s2n-bignum). This project
was the motivation both for foundational work on the formalization
of mathematics and for the development of specialized proof automation
including "generic" decision procedures for bitvectors. I'll discuss
a few selected highlights of this work.