Comment by Sniffnoy

I think the thing that you're missing here is that the "malicicous program" being discussed here isn't malicious from the usual point of view of what "malicious" means. It's truly functionally identical to the original program -- it returns the same outputs on the same inputs, there isn't some secret input that makes it do something wrong.

Despite that, it's nonetheless "malicious" in that, with the modifications made to it, FS can be made to "prove" false things about it. So you can "prove" that M(x)=y, even though when you actually run M(x), you find that you don't get y.