Many applications in image processing, control systems and other areas, have very well understood mathematical models. Optimization problems, in particular, are a class of (implicit) models which is particularly useful. When faced with the task to develop such an application, a software engineer aware of best practices might use a computer algebra system to compute some problem-specific quantities which are then put into a simulation environment (such as Matlab), and ultimately translated to code. Such a process requires the development of multiple versions of the mathematical model, often by hand, in tools with widely varying levels of formalism, which are generally susceptible to soundness problems. Moreover, it may be very difficult to decide whether the various models are in fact equivalent. Through an extended example of a multidimensional Newton’s Method, we demonstrate how computer algebra and theorem proving systems can be used to largely automate this process. We compute problem-specific quantities, including higher-order ones, verify their correctness, and automatically generate code which is verifiably correct. The process combines untrusted components with trusted ones so that failure in an untrusted component is always detected.