A trace formula for rigid varieties, and motivic Weil generating series for formal schemes

We establish a trace formula for rigid varieties $X$ over a complete discretely valued field, which relates the set of unramified points on $X$ to the Galois action on its \'etale cohomology. We develop a theory of motivic integration for formal schemes of pseudo-finite type over a complete discrete valuation ring $R$, and we introduce the Weil generating series of a regular formal $R$-scheme $\mathfrak{X}$ of pseudo-finite type, via the construction of a Gelfand-Leray form on its generic fiber. Our trace formula yields a cohomological interpretation of this Weil generating series. When $\mathfrak{X}$ is the formal completion of a morphism $f$ from a smooth irreducible variety to the affine line, then its Weil generating series coincides (modulo normalization) with the motivic zeta function of $f$. When $\mathfrak{X}$ is the formal completion of $f$ at a closed point $x$ of the special fiber $f^{-1}(0)$, we obtain the local motivic zeta function of $f$ at $x$. In the latter case, the generic fiber of $\mathfrak{X}$ is the so-called analytic Milnor fiber of $f$ at $x$; we show that it completely determines the formal germ of $f$ at $x$.