Defensive Certification in Coq with ML Type-Safe Oracles ?

Initially promoted by CompCert, the embedding of untrusted Ocaml code into extracted code from Coq – through a skeptical approach – significantly simplifies Coq developments of formally proved software. However, as illustrated by various examples of this paper, such an embedding could be unsound. This paper conjectures sufficient conditions to ensure soundness. And, it illustrates the power of these conditions on the ultra-lightweight certification of an UNSAT-prover: its Coq sources (less than 250 lines) have been developed in around one man·day.