RT DF A1 Sanchez-Stern, Alex. T1 Hybrid-Neural Synthesis of Machine Checkable Software Correctness Proofs