Marmaragan is a novel tool that enables formal verification of code produced by large language models through automated generation of SPARK annotations for Ada programs.

• Addresses the critical reliability gap in LLM-generated code through formal verification
• Automates the creation of SPARK annotations, making verification more accessible
• Benchmarks the effectiveness of verification against existing programs
• Bridges advanced AI capabilities with established software engineering practices

This research provides a practical solution for engineering teams looking to leverage LLM code generation while maintaining high reliability standards for critical systems.

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