Fernanda Graciolli

One of the most powerful uses of AI in software engineering is automation. But true automation with minimal human oversight requires a high degree of trust in the system’s ability to generate correct output. Given that long-running processes anchor the next output to its own prior outputs, an error along the way compounds quickly and may render the entire session or project unusable. We present a “verification-aware” process of programming with AI that embeds various verification methods — with formal verification as the grounding method. This process is flexible enough to accommodate tooling preferences, organization-specific policies, and cost/risk tolerance.

We’ll focus on practical patterns for verification-aware programming inspired by functional programming, how verifier feedback can guide agents to reason about correctness, and how to ensure informal and formal specifications don’t drift. The process and methods result in a considerable decrease in review burden while increasing confidence in output correctness.