Evaluating LLM-driven User-Intent Formalization for Verification-Aware
Languages
Evaluating LLM-driven User-Intent Formalization for Verification-Aware
Languages
Verification-aware programming languages such as Dafny and F* provide means to formally specify and prove properties of programs. Although the problem of checking an implementation against a specification can be defined mechanically, there is no algorithmic way of ensuring the correctness of the user-intent formalization for programs -- that a …