We propose the Mizar system as a theorem prover capable of verifying generic algebraic algorithms on an appropriate abstract level. The main advantage of the Mizar theorem prover is its special input language that enables textbook-style presentation of proofs, hence proofs in the language of algebra. Using Mizar we were able to give a rigorous machine-assisted correctness proof of a generic version of Brown/Henrici arithmetic in the field of quotients over arbitrary gcd domains. In this talk we give a short introduction into the Mizar language and show how to use the system to verify generic algebraic algorithms. We also deal with proof documentation based on literate programming, claiming that even complex proofs can be presented so that they stay readable and understandable.