Most verification is undecidable, lots of it is pspace complete. That doesn’t mean very much in practice since those are worst case bounds. People regularly solve problems that are undecidable for all practical instances that they care about.