I don't know, but given that AWS has 1000s if note millions of servers that may have idle cycles, it makes sense to use them for automatic theorem proving. And there is no existing ITP or even SMT solver that was specifically designed for efficient use of so much parallelism.
AWS certainly hired a lot of senior STM and ITP guys, such as John Harrison.
