This research introduces Marmaragan, a tool that enables formal verification of LLM-generated code using the SPARK framework for Ada, addressing a critical gap in AI code reliability.

• Leverages formal verification to mathematically prove correctness of AI-generated code
• Automatically generates SPARK annotations for existing programs
• Provides a systematic approach to verify code produced by Large Language Models
• Creates a bridge between cutting-edge AI capabilities and mission-critical software engineering requirements

This innovation is particularly valuable for high-integrity systems where code failures can have severe consequences, offering a pathway to safely adopt AI coding assistants in security-sensitive applications.

Verifying LLM-Generated Code in the Context of Software Verification with Ada/SPARK