  We present an elegant, generic and extensive formalization of Gr\"obner bases
in Isabelle/HOL. The formalization covers all of the essentials of the theory
(polynomial reduction, S-polynomials, Buchberger's algorithm, Buchberger's
criteria for avoiding useless pairs), but also includes more advanced features
like reduced Gr\"obner bases. Particular highlights are the first-time
formalization of Faug\`ere's matrix-based $F_4$ algorithm and the fact that the
entire theory is formulated for modules and submodules rather than rings and
ideals. All formalized algorithms can be translated into executable code
operating on concrete data structures, enabling the certified computation of
(reduced) Gr\"obner bases and syzygy modules.
