Often when people mention provably correct software what they mean is software that don't crash and always produces output for correct input. It usually doesn't mean that the output is correct...