Neuro-Symbolic Proof Generation for Scaling Systems Software Verification

Baoding He, Zenan Li, Wei Sun +4

Formal verification via interactive theorem proving is increasingly used to ensure the correctness of critical systems, yet constructing large proof scripts remains highly manual a…