It doesn't seem like a completely different thing to generate specifications and formally verified programs for those specifications (though I'm not familiar with how those are done today).