Presented at ASE on October 15, this March 23 paper prepares helper lemmas from annotated programs, then adapts or proves more during proof search. The Rocq/AutoRocq implementation uses Frama-C/WP conditions. Evaluation includes modules from larger systems; it does not certify those entire systems.
LemmaNet brings source context into proof search
Presented at ASE on October 15, this March 23 paper prepares helper lemmas from annotated programs, then adapts or proves more during proof search.
3 sources · 1 min read
Link to noteOriginally published 16 October 2026. Reporting, forecasts, prices, odds and event availability reflect the original edition.
Sources & further reading
- Paper arxiv.org
- Implementation github.com
- Conference entry conf.researchr.org