I've been looking at model checkers and program proof assistants on and off since FDR and Isabelle/HOL and the like, and there were similar tools going back another decade before that. If you're verifying part of an ASIC or a crypto protocol or something similar they're fine (if extraordinarily painful to use), but for anything else they've been bypassed by AI. I'm not saying that as an AI fan but because by the time you get your PhD and then spend another five years learning how to use the tool and mark up the code and hope you got the markup right and after another six months of what feels like trying to make a string go in a certain direction by pushing it and the tool finally finds a nonexploitable buffer overflow in a function that's never called you realise you could have done the same thing with $2 in AI tokens. It's the program verification technology of the future, and always will be, while "claude, find places where this code does things it shouldn't" is right now and doesn't require a PhD to use.