Bitvector est une bibliothèque dédiée à la gestion efficace de vecteurs de bits dans l'environnement Rocq. Elle permet d'optimiser les opérations sur des structures de données binaires tout en s'appuyant sur des tableaux primitifs et des entiers natifs. Principalement utilisée pour des développements formels en logique et en mathématiques, elle facilite la vérification de preuves et l'implémentation d'algorithmes fiables.