📄 Paper accepted @ the Post-AI Formal Methods Workshop @ AAAI 2026! 🎉
Image credit: P-AI-FM-26 WorkshopI’m excited to share that our paper on PyVeritas has been accepted to the Post-AI Formal Methods Workshop @ AAAI 2026! 📄
TL;DR: Python → LLM transpiles to C → bounded model checking (CBMC) + MaxSAT-based fault localisation (CFaults) → source-level mapping back to Python.
What’s PyVeritas?
A framework that leverages Large Language Models to transpile Python into C, then applies bounded model checking and MaxSAT-based fault localisation on the generated code.
This brings assertion-based verification and interpretable bug diagnosis to small yet non-trivial Python programs!
On two Python benchmarks, LLM-based transpilation achieved up to 80–90% accuracy with some models, enabling an effective verification workflow.
