Efficient methods for verified solutions of optimization problems and non-linear systems of equations. SONIC is a new rigorous nonlinear solver and constrained optimizer based on interval computations. Having been developed primarily to support the parametrically robust design of dynamic systems, SONIC can also be used to solve nonlinear problems arising in other application areas. Since its high-level solvers can be coupled with several different basic interval libraries, it can achieve optimized performance while maintaining a high degree of portability. This work focuses on presenting new efficient methods for the verified solution of nonlinear systems of equations and a set of sophisticated advancements of known techniques: optimal linear programming preconditioners, extended Newton method, hybrid Newton method with probation approach, and a hybrid subdivision scheme. The efficient handling of non-total functions in SONIC allows for solving nonlinear problems which arise in chemical process engineering, while established solvers fail in these cases. In addition to the serial code, efficient parallel versions for shared and distributed memory architectures are available.