Mmmh, correctness does not mean "it's a nice thing". It just means that something fulfills the specs. Do you know which specs were fed into the prover? The specs could be as weak as - RSA must terminate if fed with the number 42 - x ^ (e * d) = x mod n for all x from 0..(n-1) Hadmut