This paper addresses the challenging task of solving nonlinear optimal control problems, particularly in high-dimensional settings. The authors propose two algorithms for model-based policy iterations: ELM-PI and PINN-PI. ELM-PI formulates the optimization problem as a linear least squares problem, inspired by extreme learning machines (ELM), and is efficient for low-dimensional problems. PINN-PI uses physics-informed neural networks (PINNs) to solve partial differential equations (PDEs) and is better suited for high-dimensional problems. Both algorithms are shown to outperform traditional methods like Galerkin methods. The paper provides theoretical analysis proving convergence of neural approximations to true optimal solutions and employs formal verification techniques to ensure the stability of the resulting controllers. Numerical experiments demonstrate the superior performance of ELM-PI for low-dimensional problems and PINN-PI for high-dimensional problems, highlighting the importance of formal verification in safety-critical applications.This paper addresses the challenging task of solving nonlinear optimal control problems, particularly in high-dimensional settings. The authors propose two algorithms for model-based policy iterations: ELM-PI and PINN-PI. ELM-PI formulates the optimization problem as a linear least squares problem, inspired by extreme learning machines (ELM), and is efficient for low-dimensional problems. PINN-PI uses physics-informed neural networks (PINNs) to solve partial differential equations (PDEs) and is better suited for high-dimensional problems. Both algorithms are shown to outperform traditional methods like Galerkin methods. The paper provides theoretical analysis proving convergence of neural approximations to true optimal solutions and employs formal verification techniques to ensure the stability of the resulting controllers. Numerical experiments demonstrate the superior performance of ELM-PI for low-dimensional problems and PINN-PI for high-dimensional problems, highlighting the importance of formal verification in safety-critical applications.