Comment by NohatCoder

"A specification that can be implemented using formal methods". That is just source code. If the specification can completely define arbitrary programs it is necessarily Turing complete on its own, and as such prone to the same type of bugs as any other program.