Matrix inversion algorithms are ubiquitous in engineering, computer science, and other disciplines. While formal verification exists for individual inversion methods, a comprehensive verification alongside directly executable algorithms within a theorem prover is lacking for two key methods: inversion via the adjoint matrix (InvAM) and inversion via Gaussian elimination (InvGE). This paper addresses this gap by offering constructive implementations and rigorous formal verifications of both InvAM and InvGE within the Coq proof assistant, thus enabling reliable and ready-to-use computation of matrix inverses directly in the Coq environment.