We present recent progress on the formalization of exact real computation within a dependent type theory and its implementation as the Coq library cAERN. A key feature of cAERN is the extraction of certified Haskell programs for exact real computation from proofs in the system. The extracted programs can be used to compute rigorous numerical approximations with arbitrary precision. We introduce the main aspects of the formalization and present some recent extensions, specifically focusing on the problem of solving initial value problems for systems of first-order ordinary differential equations.