Hybrid Natural and Formal Language Verifier

Jul 21, 2026 · 1 min read
Hybrid natural-language and formal-language verification
projects

This verifier combines natural-language specifications with formal specifications, allowing users to trade token budget for stronger and more reliable safety assurances.

It is more precise than natural-language specifications while making precise feedback on specification and code correctness easier to obtain than with traditional formal specifications alone.

Source Code

Program Verification Formal Methods Large Language Models
Wenkai Xing
Authors
Wenkai Xing
Ph.D. Student in Electronic Information
I am a Ph.D. student at Peking University and a member of the Programming Languages Lab, advised by Prof. Zhenjiang Hu. My research interests include programming languages, LLM-based program verification, and simplifying agent implementation.