Synthesis and Verification of Neural Control Barrier Functions for Safe Reinforcement Learning with Guarantees