AI code generation that comes with formal correctness proofs

LLM-generated code offers no correctness guarantees, forcing developers to review and test it manually — often erasing the productivity benefit. Viverra addresses this by prompting an LLM to produce C code alongside candidate assertions about safety and correctness, then verifying those assertions using a portfolio of bounded model checkers in a compositional, best-effort fashion. Tested across 18 programming tasks, the system efficiently produces code with verified annotations. A user study with over 400 participants confirmed that the verified assertions tangibly improved code comprehension, making the tool relevant to any practitioner relying on AI coding assistants.