En utilisant en particulier les propriétés de finitude de la monodromie locale $p$-adique des équations différentielles nous démontrons un théorème d'image directe pour les complexes $p$-adiques constructibles étendant le le Théorème de finitude de la cohomologie de de Rham $p$-adique d’une variété affine. Nous en déduisons la formule $p$-adique des traces sur les corps finis et la rationalité des fonctions $L$ des complexes constructibles munis d'une structure de Frobenius. Cette formule des traces contient comme cas particuliers toutes les formules de trace connues auparavant. Le Théorème de Finitude réduit la formule des traces au cas de la droite affine exactement comme pour la formule des traces de Grothendieck dans le cas $\ell$-adique.