> This isn't easy, and I know the problem space is larger, but does anyone ever do this for software? Typically the state space is simply too large to be pract

> This isn't easy, and I know the problem space is larger, but does anyone ever do this for software? Typically the state space is simply too large to be practical. It is, admittedly, how a lot of verified software is done (because there are so few verified compilers), though often then the source-code to assembly correspondence is verified manually, which limits possible optimisations.