While the word problem for monoids is undecidable in general, having a decision procedure for some finitely presented monoid of interest has numerous applications. This paper presents a toolbox for the Rocq proof assistant that can be used to verify the decidability of the word problem for a given monoid and, in some cases, to produce the corresponding decision procedure. As this verification can be computationally intensive, the toolbox heavily relies on proofs by reflection guided by an external oracle. This approach has been successfully used on several large monoids from the literature, as well as on a database of one million 1-relation monoids. The huge size of this database forced some unusual considerations upon the Rocq formalization, so that its formal proof could be checked in a reasonable amount of time.