Midspiral

As LLMs become more capable of writing code, the programmer's role shifts from implementation to describing intent. Two major open questions emerge in AI programming: 1) How do we know AI-generated code is correct, not just plausible? 2) How do we know the code accurately captures the programmer's intent? Our recent work addresses the first question by adding formal verification to the AI code generation loop — forcing the AI to mathematically prove its code is correct. But the second question remains: does the proved specification capture the intent? Claimcheck closes the gap between “the code is guaranteed correct” and “the code makes the intended guarantees.” We use the Claude API to conduct round-trip informalization: it translates formal language to English without knowledge of the initial input. It then compares the intent to the guarantee to ensure they match. On 108 comparisons, it got 96.3% correct in 2 API calls per run batched per file.