Dans un programme informatique, des fonctionalités de base sont parfois implémentées par des opérations bit-à-bit, par exemple à cause d'un besoin d'être proche de l'architecture matérielle sous-jacente, ou bien pour des questions d'efficacité, aussi bien en temps de calcul qu'en place mémoire. Si l'on cherche à spécifier formellement le comportement attendu d'un tel programme, il est souhaitable que la spécification se place à un niveau plus abstrait que celui des bits. Prouver formellement qu'un programme bas niveau est conforme à une spécification de plus haut niveau est un défi, à cause de l'écart important entre les niveaux d'abstraction en jeu. Notre approche pour résoudre ce défi consiste à concevoir une théorie formelle des vecteurs de bits, qui d'une part permet à un utilisateur d'écrire des spécifications proches d'un niveau de conception humain (ou bien disons, mathématique), et d'autre part peut se connecter aux procédures de décision et aux outils sachant traiter les vecteurs de bits, comme ceux qui sont développés dans le cadre SMT (Satisfia-bility Modulo Theory). Cette approche est implémentée dans le cadre de l’environnement généraliste Why3 pour la preuve déprogramme, ainsi que dans l’environnement SPARK pour le développement de codes critiques en Ada, qui utilise Why3 en interne. Nous présentons plusieurs études de cas afin de valider notre approche.