  Reliably determining system trajectories is essential in many analysis and
control design approaches. To this end, an initial value problem has to be
usually solved via numerical algorithms which rely on a certain software
realization. Because software realizations can be error-prone, proof assistants
may be used to verify the underlying mathematical concepts and corresponding
algorithms. In this work we present a computer-certified formalization of the
solution of the initial value problem of ordinary differential equations. The
concepts are performed in the framework of constructive analysis and the proofs
are written in the \texttt{Minlog} proof system. We show the extraction of a
program, which solves an ODE numerically and provide some possible optimization
regarding the efficiency. Finally, we provide numerical experiments to
demonstrate how programs of a certain high level of abstraction can be obtained
efficiently. The presented concepts may also be viewed as a part of preliminary
work for the development of formalized nonlinear control theory, hence offering
the possibility of computer-assisted controller design and program extraction
for the controller implementation.
