◼️ coq-of-noir

coq-of-noir is a formal verification tool for Noir programs. With it you can ensure that Noir programs are totally bug-free and secure, assuming a correct specification!

It works by converting Noir programs to the 🐓 Coq proof assistant in a shallow embedding, after the monomorphization phase of the Noir compiler which removes that generics and the traits.

To secure your Noir application to highest possible standard of safety, 📧 contact us!