The work done/supervised by Kristopher Micinski on using HPC hardware (not only GPUs but clusters) for formal methods is really encouraging. I hope we reach a breakthrough of affinity between COTS compute hardware and all kinds of formal methods, as GPUs found theirs with deep learning and subsequent large models.
One possible answer to 'what do we do with all the P100s, V100s, A100s when they're decomissionned from their AI heyday (apart from 'small(er) models'.