> But at least formal methods tools can be applied directly to the specification What makes you think that? For example for C language it has been significant

> But at least formal methods tools can be applied directly to the specification What makes you think that? For example for C language it has been significant effort to translate the specification to something analyzable by tools