This paper presents an algorithm for synthesizing formally verified continuous-time neural Control Barrier Functions (NCBFs) in stochastic environments. The proposed method ensures safety by enforcing Lipschitz bounds on the neural network, its Jacobian, and Hessian terms. The training process is designed to be efficient with only a finite number of data points, ensuring efficacy across the entire state space. The methodology eliminates the need for post hoc verification, making it a complete and practical approach. The effectiveness of the approach is demonstrated through case studies on the inverted pendulum system and obstacle avoidance in autonomous driving, showing larger safe regions compared to baseline methods. The paper also includes a detailed theoretical framework, including problem formulation, loss function construction, and training procedures, along with simulations to validate the approach.This paper presents an algorithm for synthesizing formally verified continuous-time neural Control Barrier Functions (NCBFs) in stochastic environments. The proposed method ensures safety by enforcing Lipschitz bounds on the neural network, its Jacobian, and Hessian terms. The training process is designed to be efficient with only a finite number of data points, ensuring efficacy across the entire state space. The methodology eliminates the need for post hoc verification, making it a complete and practical approach. The effectiveness of the approach is demonstrated through case studies on the inverted pendulum system and obstacle avoidance in autonomous driving, showing larger safe regions compared to baseline methods. The paper also includes a detailed theoretical framework, including problem formulation, loss function construction, and training procedures, along with simulations to validate the approach.