Coq used to have a why3 tactic:
http://why3.lri.fr/doc-0.82/manual011.html
It was removed here:
https://gitlab.inria.fr/why3/why3/commit/76504523dde683fb6f8b3f34dd8a385b69e72b3b
Are there any plans to bring it back and/or perhaps integrate it with smtcoq or coq_hammer?
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?