The extraction from Coq is not verified itself, but produces proofs for the correctness of each single extracted program semi-automatically. The frameworks builds on the Coq plugin Template Coq. It eliminates the non-computational parts of the Coq program and produces a term in L and the corresponding correctness statement, which in turn can be verified using several provided automation tactics.
Using the framework, one can focus on the interesting parts of developments in L, because the task of programming is taken care of. We use the framework to develop a formalization of Computability theory as a case study.