Formally verifying agent-written full-stack web apps with PDD Kit

Proof-Driven Development (PDD) Kit is a tool that makes formal software verification more accessible for everyday software development. It helps turn the developer's intent into a formal specification, then proves that the generated code meets that specification for all possible inputs. When a proof can't reach certain inputs, PDD Kit falls back to tests to ensure correctness.

Traditionally, formal methods were reserved for specialized software development, requiring experts in complex languages and lengthy proof development processes. However, recent advancements in coding agents have made it more practical for these agents to assist in generating formal proofs from well-defined specifications. PDD Kit leverages these advancements to help teams write formal specifications and proofs more efficiently.

PDD Kit operates within GitHub Next's Chopin, a real-time, collaborative planning environment where developers and AI agents can work together in a shared document. The process consists of two main parts. First, team members review the intended functionality using plain language. PDD Kit then guides the review, asking relevant questions, explaining code snippets, and recording the answers in an intent artifact. This artifact bridges the gap between the user's intent and the formal specification or tests.

Next, PDD Kit automatically generates formal specifications for the parts of the intent that can be formalized and informal specifications for the rest, which must be trusted for now. It also generates proofs that the code adheres to these specifications, along with high-quality tests for the informal specifications. The results in PDD Kit indicate which kind of verification is responsible for each result: formal verification, which is a mathematical proof that the code satisfies its specification for every possible input, or empirical verification, which involves running the code and observing its behavior.

While formal verification provides stronger assurance for specified properties, empirical verification covers inputs that proofs may not reach, such as third-party cryptography libraries or user interfaces. A passing test only shows that the code works for the inputs it was tested on, so PDD Kit labels these as evidence rather than proofs.

This dual approach to verification ensures a comprehensive validation of the code, addressing both the obvious and the hidden issues that can arise as AI agents generate increasingly large amounts of code.