Bignum Arithmetic by AWS

Did they build it to handle customer invoicing?

These are assembly implementations of arbitrary precision integer arithmetic with correctness proofs in hol light.