Neurosymbolic C++ Verification in Rocq

Lennart Beringer, Jasper Haag, Rodolphe Lepigre, Gregory Malecha, Rayan Soban, Ehtesham Zahoor

Neurosymbolic capabilities have revolutionized the entire software development process, from requirements engineering and code development to testing and maintenence. In this talk, we will present our work integrating agentic techniques into the Brick C++ verification platform. Our approach combines algorithmic reasoning techniques, e.g. concurrent separation logic with sophisticated automation, proof search strategies, etc., with higher-level insights and probabilistic inference provided by LLMs. Our experience demonstrates that combining these technologies enables scalable reasoning for real-world programs.

rocq c++ program verification separation logic brick templates skylabs-ai

paper conference link slides

@inproceedings{malecha2026-neurosymbolic,
  title={Neurosymbolic {C++} {V}erification in {R}ocq},
  author="Lennart Beringer and Jasper Haag and Rodolphe Lepigre and Gregory Malecha and Rayan Soban and Ehtesham Zahoor",
  booktitle={High Confidence Software and Systems Conference (HCSS) 2026},
  location={Annapolis, MD},
  year="2026",
  month="May",
  day=12
}