Ce projet est la bibliothèque standard du Rocq Prover, un assistant de preuve interactif. Il propose un langage formel pour écrire des définitions mathématiques, des algorithmes exécutables et des théorèmes, accompagnés d'un environnement pour développer des preuves vérifiées par machine. La bibliothèque standardise et organise les modules essentiels pour les utilisateurs et développeurs, favorisant ainsi la rigueur et la réutilisabilité dans les travaux de preuve formelle.