GitHub Next introduces PDD Kit: using mathematical proofs to verify that AI-generated code meets specifications

On November 4, 2026, GitHub Next introduced the workings of the Proof-Driven Development Kit (PDD Kit), which it is developing jointly with Microsoft Research, along with an example of its application to login processing. PDD Kit organizes requirements into specifications that can be machine-verified through dialogue with developers, and uses mathematical proofs to confirm that code generated by AI agents satisfies those specifications. It is currently a research prototype targeting Rust code, and its availability is limited to a restricted research preview [1].

PDD Kit - GitHub Next

How we can secure 50% of the world's software.

Traditionally, formal methods have been mostly used for safety-critical systems like operating systems, hypervisors, and databases. We're extending this to formally and empirically verify code correctness and security for full-stack web apps, one of the most common types of applications*, using the Proof-Driven Development Kit (PDD Kit).

Coding agents now write code faster than anyone can review effectively. PDD Kit turns what the developer meant into a Verus specification. It then proves the AI-generated code meets that spec for every input.

Researchers @alexlavaee, @MatthaiP39719, @Mappletons, and @k_cieslak break down Proof-Driven Development x Chopin in the blog here: https://t.co/EwhqTx2OjT

*44.4% of respondents work as full-stack (27.3%), back-end (13.5%), or front-end (3.6%) developers. Stack Overflow Developer Survey 2026, n = 25,767.— GitHub Next (@GitHubNext) November 4, 2026

GitHub Next cites as a challenge the fact that as the volume of code generated by AI agents increases, it becomes difficult for humans to review every line. It also points out that if an agent misunderstands a requirement, that misunderstanding enters both the code and the tests, and the code may pass the tests without behaving as intended. With PDD Kit, humans decide the behavior they want from the software and review whether that content is reflected in the specification.

A comparison of development flows presented by GitHub Next. The upper row shows the flow in which humans review code implemented by an agent. The lower row shows the development flow using PDD Kit. Humans confirm requirements and proof assumptions at the planning stage, and the agent creates the implementation and proofs. Verus, a verification tool for Rust, checks the proofs. The width of each block is schematic and is not a measured value of work time (from the GitHub Next article).

Turning ambiguous requirements into specifications through dialogue with developers

PDD Kit runs inside Chopin, a web app developed by GitHub Next. Chopin is installed on one's own PC or server and operated from a browser [2]. It allows direct editing of development plan documents shared by a team, and also lets users ask AI agents via chat to investigate or revise documents.

PDD Kit reads existing code during this planning process, asking developers questions while explaining what the processing does. Based on the answers, it organizes the behavior the developer wants into a document. Of that, the parts that can be expressed as machine-verifiable conditions are written out as specifications that can be handled by Verus, a verification tool for Rust [3].

On PDD Kit's official page, this specification-building flow is explained using the login processing of "Pet Store," a web app built in Rust, as an example. When login succeeds, this app issues a token that records the account's identifying information and its role, such as customer or administrator. For this processing, the developer gave PDD Kit the requirements "issue a token only when the password is correct" and "issue an administrator token only to administrator accounts."

Under the condition "issue a token only when the password is correct," a token must not be issued for an incorrect password. However, an implementation that rejects all logins and never issues any token would also satisfy this condition. So PDD Kit asked, before implementation began, "Do you also require that a token always be issued when the password is correct?"

The developer also required that a token be issued when the password is correct. However, even if the password is correct, the DB lookup or the signing of the token may fail. Therefore, in the final specification, it was decided that if these processes fail, a server error may be returned instead of a token.

In this way, eight conditions were incorporated into the login processing specification [4]. For example, one condition is that the account used for password verification matches the account indicated by the token. This condition makes it possible to catch bugs where, despite authenticating with one's own password, another person's token is issued.

A screen from the official page's interactive explanation (partial). On the left, users can toggle whether the login request includes an email address or username, whether the account is registered, whether the password is correct, and whether the DB lookup or signing process fails. Users can check the login result and which of the eight specification conditions applies, and the corresponding condition is highlighted on the right. The "Plant a bug" tab also lets users see the relationship between example bugs and the conditions that catch them.

In actual specification work, PDD Kit explains the processing flow with diagrams to help developers review the specification. The specification written for Verus is also annotated with English comments explaining each condition. Developers confirm whether the requirements are expressed as intended and approve the specification.

The agent generates proofs, and Verus checks them

The coding agent generates an implementation based on the approved specification and also creates proofs showing that the implementation satisfies the specification. Verus checks these proofs, verifying whether the conditions hold for all inputs covered by the specification under the defined assumptions. This kind of formal verification differs from testing, which runs code on individual inputs and observes the results.

However, if the specification's conditions are too loose, even code that contradicts the intent will pass verification. So PDD Kit deliberately introduces, one at a time, bugs that violate each condition of the specification into a working copy of the code. It confirms that Verus detects each bug as a violation of the intended condition.

Processing outside the scope of proofs is confirmed by testing

In this login processing, separate libraries are used for the DB lookup, password verification via bcrypt, time retrieval, token signing, and so on. However, the processing inside these libraries is not itself included in the scope of this proof. Therefore, the correctness of the login processing is proven on the assumption that each of these processes behaves as the specification assumes.

Regarding such proof assumptions, PDD Kit explains to developers at the planning stage before implementation the conditions that each process is assumed to satisfy. It also shows which guarantees are lost if those conditions do not hold, and asks for approval for each process. At the same time, it plans tests that confirm each assumed condition.

Even for processing covered by proofs, the guarantees are limited to the scope written in the specification. In this specification, it guarantees that when the login processing returns a response, the result satisfies the conditions. It does not guarantee that the processing always completes or how long it takes to respond.

Review the verification results, merge, and continue verifying after changes

A review LLM compares the plan, specification, and verification results, and checks whether it can confirm, through proofs or tests, that the implementation satisfies each requirement. If any requirement cannot be confirmed by either proofs or tests, it asks the coding agent to address it. If the specification itself is contradictory, it cannot be resolved by fixing the implementation alone, so PDD Kit asks the developer to make a judgment.

Once the proof checks and tests pass, PDD Kit creates a pull request containing the implementation, proofs, and tests. It also describes what was proven, the assumptions about processing excluded from the proofs, the test results, and the scope of the guarantees. Developers review the content against the desired behavior and merge it. After merging, Verus verification and tests are also integrated into continuous integration (CI), confirming that the same specification is satisfied with every code change.

This case is limited to the login processing of a single app. GitHub Next says that creating proofs still takes effort, and is exploring whether the approach can be applied to a broader scope.

The review LLM compares the plan, specification, and verification results, and checks whether it can confirm, through proofs or tests, that the implementation satisfies each requirement. If any requirement cannot be confirmed by either proofs or tests, it asks the coding agent to address it. If the specification itself is contradictory, it cannot be resolved by fixing the implementation alone, so PDD Kit asks the developer to make a judgment.

Once the proof checks and tests pass, PDD Kit creates a pull request containing the implementation, proofs, and tests. It also describes what was proven, the assumptions about processing excluded from the proofs, the test results, and the scope of the guarantees. Developers review the content against the desired behavior and merge it. After merging, Verus verification and tests are also integrated into continuous integration (CI), confirming that the same specification is satisfied with every code change.

This case is limited to the login processing of a single app. GitHub Next says that creating proofs still takes effort, and is exploring whether the approach can be applied to a broader scope.