Disclamer: This project is still experimental. No support will be provided at this point, and its behaviour is still unstable.
Why3Gospel is a Why3 plugin that enables the parsing of Gospel specifications and their translation into Why3 interfaces. This enables refinement proofs from Why3 contracts to Gospel specifications within Why3.