The implementation can be formally written and verified, but the specification itself cannot be automatically verified.

That's effectively what a contract is anyway - it's a specification for a 'legal agreement' which is this sort of invisible obligation that is created after it is signed (for instance, the time spent in contract negotiations is usually spent debating what should happen in edge-cases).