2 papers
cs.SE2026
Agent-Driven Verification of Memory Safety for liblzma Decoder Components with VST
Prokhor Shlyakhtun, Alexander Gryzlov, Vladimir Kukharenko +5
We report on the verification of memory safety for decoder components of liblzma, the compression library underlying xz-utils: the LZMA2 state machine, the LZMA1 decoder it control…
cs.AI2026
FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified?
Nikil Ravi, Kexing Ying, Vasilii Nesterov +5
We present FormalProofBench, a private benchmark designed to evaluate whether AI models can produce formally verified mathematical proofs at the graduate level. Each task pairs a n…