Coq used to have a why3 tactic:
It was removed here:

Are there any plans to bring it back and/or perhaps integrate it with smtcoq or coq_hammer?

1 Like

I didn’t hear anything, neither developer is on Discourse so I am unsure about their plans, but I think that Why3 may not be so interesting as it doesn’t produce proof witnesses; and you want them.

It is pretty easy to stumble upon unsoundness when going back/forward to STM solvers and CiC, not to speak of the bugs the solvers themselves have.

Easycrypt uses why3 as a backend. I know it’s not perfect, but it seems somewhat suboptimal to have three such translations. Also, the proof reconstruction might be a somewhat orthogonal issue to the translation, don’t you think?