MirrorCore is a framework for easing the burden of building reflective automation in Coq proof assistant.
ExtLib is an extension to Coq's standard library which embraces new features such as universe polymorphism, primitive projections, and type classes.
Template-Coq is a bare-bones quoting library for Coq. Its syntax is designed to be as close as possible to Coq's internal representation.
VeriDrone is exploring foundational verification of cyber-physical systems such as quadcopters. Check us out!