Different proof tools inhabit different areas on the "specification to implementation" spectrum (problem/solution). Since it's possibly to perfectly implement a

Different proof tools inhabit different areas on the "specification to implementation" spectrum (problem/solution). Since it's possibly to perfectly implement a bad specification, proving a specification valid has value, even if it isn't formally proving your implementation of that spec.