Do you use Copilot on a language equipped with refinement or dependent types, and use said types to constrain generation of entire functions, in a single step,

Do you use Copilot on a language equipped with refinement or dependent types, and use said types to constrain generation of entire functions, in a single step, that are also formally verified?