Verified computing is a newly developed methodology to estimate all errors in numerical computing and provide mathematically rigorous results. Recently, there have been several newly developed verified computing methods to give guaranteed eigenvalue estimation for differential operators. In this talk, I will explain basic concepts about verified computing and give a survey on guaranteed eigenvalue estimation methods. Particularly, the newly developed verified eigenvalue estimation method based on finite element method (FEM) will be introduced in detail. Such a method has been successfully applied to various differential operators, for example, the Laplace, the Biharmonic, the Stokes, the Steklov operators. Also, applications of the guaranteed eigenvalue estimation in mathematical proof will be introduced. As an example, I will show the latest result on solution existence proof about the Navier-Stokes equation in 3D space.