Archetype provides a specification language for contract invariant and entry point postconditions. It generates the contract in the Why3 language for verification
Coq is an interactive proof assistant. The user sends instructions to the proof engine to build up the proof step by step: apply a theorem to justify a proposition, rewrite a term by another and so on. It is possible to program macros for automation purpose. Proving a program in Coq requires the language semantic in Coq theory (provided by Michocoq for Michelson) used to prove the correctness of the program.Why3 is a plateform dedicated to program verification: it translates the program and specification into SMT problems (called proof obligation) for SMT solvers to solve. When solvers succeed, the verification is automatic. When solvers fail, it is necessary to help them by providing intermediate properties about the program, that they can solve, and that they can use to solve the problem.