Vocal Disclamer: This project is still experimental. No support will be provided at this point, and its interface is still unstable. Vocal is a set of OCaml modules, formally verified using Gospel and various tools (currently, Why3, CFML, Coq).