Satisfiability Modulo Theories (SMT) problems are akin to mathematical puzzles: given a mix of equations and logical rules, an SMT solver determines whether there exists an assignment of variables that satisfies everything at once. SMT solving underpins high-stakes assurance tasks: for example, proving that a self-driving car cannot steer into an obstacle under modeled operating conditions, and supporting safety checks in domains like avionics, medical devices, and power systems. These problems become increasingly challenging as modern software and systems incorporate machine learning (ML) and artificial intelligence (AI), which introduce large, highly nonlinear mathematical constraints that often exceed the scalability of traditional solvers. To address this gap, the project develops a new solver framework that transfers highly scalable, hardware-accelerated techniques originally created for neural-network verification into general SMT solving. The project’s novelties are the fundamental re-architecting of traditional SMT solving procedures around a new concept called linear bound propagation, which effectively handles large SMT problems with nonlinear arithmetic and enables massive parallel computation. The project's impacts are an open-source, high-performance reasoning engine that strengthens safety and reliability across software and cyber-physical domains where nonlinear constraints and rigorous safety requirements are central, including next-generation AI-enabled systems, thereby fostering public trust in autonomous technologies. Technically, the project advances formal verification for nonlinear real arithmetic (NRA) SMT through three synergistic thrusts. Thrust I builds a new NRA decision procedure grounded in linear bound propagation, introducing novel methods to efficiently account for correlations among constraints, infer bounds even when variables are only implicitly constrained, and tighten relaxations through computation-graph optimizations and cro