PDD Kit

Major security incidents, widening evaluation bottlenecks, and regressions caused by coding agents have forced us to find better ways to improve software reliability. We started with Chopin, where we argued that the important work in agentic development has moved to planning and review. But a question continued to bug us. If nobody can review every line an agent writes, what exactly are we standing behind when we merge it? Or worse, what are we exposing ourselves to?

A plan in Chopin is the record of what a team decided to build. It’s meant to be the contract you hand the coding agent, but nothing constrains the agent to follow it. And exhaustive line-by-line review can become difficult to scale as agents generate more and more code.

PDD Kit is a collaboration between GitHub Next and Microsoft Research. It shifts review toward what people are essential for: the judgment and decision-making behind what the software should do and what makes it a delight to use. Line-by-line checking and guarantees about correctness fall to a mathematical proof with formal methods, supplemented by tests where a proof isn’t possible.

The Problem with Reviewing Agent Code

Agents are fast and often right, but “often” is a problem when you’re the one merging the code. Four things stick out to us.

1. Plans Aren’t Binding

However good your plan is, the agent doesn’t have to follow it. Usually it gets close, but it might handle a case differently than you described, or skip an edge case you cared about, and nothing flags it. You find out later, when something breaks.

2. Tests Check What Was Built

The agent writes the tests too. Those tests tend to pass for the code it wrote, not the code you meant. CI fills up with lots of low-value tests, coverage looks healthy, and the gap between what you asked for and what shipped stays hidden until a bug report or a nasty edge case shows up. Even good tests only sample a handful of inputs out of an enormous space.

3. Line-by-Line Review Doesn’t Scale

The fallback is a person reading every line of the pull request. That worked when people wrote the code. It gets much harder when an agent ships a whole feature in one sitting, often spanning tens or hundreds of thousands of lines of code. Reviewers end up skimming and approving, and hoping nothing slipped through.

4. Vibe Verification

The obvious fix is to ask a model to prove its code correct using formal methods. On its own, that doesn’t work either. A model that writes its own formal specification, or is tuned to produce proofs, tends to find weak invariants. These are statements that verify but rule out almost nothing. They prove something, just rarely the thing you care about. We call that vibe verification. A green checkmark on the wrong spec is worse than no checkmark, because it looks like assurance.

Why Proof, and Why Now

Formal methods check software with math instead of examples. You write a specification, a precise statement of what the code must do, and a verifier proves the code meets it for every possible input. If the proof goes through, the property holds. If it doesn’t, the verifier shows you where it breaks.

Review asks “does this look right?” A proof answers “is this right?” It covers the inputs your tests miss too. For the properties you specify, that’s stronger assurance than testing alone, especially when line-by-line review isn’t practical.

Proofs used to be too expensive for everyday software. You needed specialists, unfamiliar languages, proofs many times larger than the code, and proofs took years to develop, but two things have changed since. First, recent advances in coding agents have made it increasingly practical for them to help generate formal proofs from well-defined specs. Second, agents can now better help you write those specs in the first place. Put those together and the remaining hard problem is a human one: making sure your intent is aligned with your teammates and agents.

Introducing PDD Kit

PDD Kit is our exploration of Proof-Driven Development (PDD): formal methods for everyday software, not just specialist work. It’s to formal methods roughly what Spec Kit is to Spec-Driven Development. It runs inside Chopin as a planning partner. It reads your code, asks you the questions a careful reviewer would ask, explains the code as it goes, and records your answers in an intent artifact, a document that bridges what you meant and the formal spec. The parts of your intent that can be formalized become a formal specification in Verus, 1 1You write ordinary Rust plus requires and ensures clauses, and Verus checks at compile time that the code meets them for all inputs. a proof language for Rust co-developed by Microsoft Research, Carnegie Mellon University, VMware Research, ETH Zurich, MPI-SWS, UNSW Sydney, the University of Texas at Austin, the University of Michigan, the University of British Columbia, the University of Wisconsin–Madison and the Weizmann Institute of Science. Then it proves the agent’s code meets that specification for every input. The rest, which has to be taken on trust, becomes informal specs that it checks with tests. You don’t need a formal methods background for any of it.

Not everything can be proved, so every result says which kind of verification it rests on:

• Formal verification is a mathematical proof that code satisfies its specification for every possible input, checked by a tool called a verifier, which for PDD Kit today is Verus. Other formal tools you may have heard of include Lean and Dafny, which prove code meets a spec, and TLA+, which checks the design of a system or protocol rather than the code itself.
• Empirical verification checks code by running it and observing what it does. It covers what a proof can’t reach, such as a third-party cryptography library or a user interface, using unit and end-to-end tests, terminal automation, browser agents, and computer-use agents for anything a browser can’t drive. A passing test only shows the code worked on the inputs it tried, so PDD Kit labels it as evidence rather than proof.

Here’s how it went on a real app. To show PDD Kit working with an existing codebase, we built Pet Store, a full-stack web app written in Rust, with an Axum and SQLite backend and a Leptos storefront, about 5,000 lines in all. PDD Kit recommends starting with the most sensitive parts of an app and verifying the rest incrementally, so we picked login. A login bug can hand an attacker a customer’s account or an admin’s controls, so that’s where proof effort pays off first. The same process can verify the functional correctness of the rest of the app, one piece at a time. The whole request was two sentences:

Verify the login logic in backend/src/handlers/auth.rs. Here are my requirements:

1. You only get a token with the right password.
2. Only admin accounts get admin tokens.

We kept it deliberately rough, since capturing what we meant and turning it into something a proof can check is PDD Kit’s job.

PDD Kit came back with questions before writing any code, each one on a decision card. When a question depends on how the code works, the card explains that part first, so you can answer without opening the source. The first card asked something we hadn’t thought to say:

Does “you only get a token with the right password” also mean you always get one with the right password? Those are two different specs. “Only with the right password” rules out the bad case, a wrong password getting a token. But a login that refuses everyone keeps that promise perfectly. “The right password always works” is the half that rules it out. An agent working alone would have picked one without telling us. We picked both ways.

While you talk, PDD Kit keeps a rough work section at the top of the plan up to date, so you can keep track of the important concepts without scrolling back through a long chat to find what was agreed. It includes a diagram of the flow being specified, a spec landscape of what will be proved and what will be trusted, and an intent map that ties each requirement back to your own words:

When a picture helps, PDD Kit draws one. For login, it was a ticket desk with two windows:

That picture carries our whole second requirement. Nothing in the request names a role, so the role comes from which window you walk up to.

Proving the Login Function

Before anything gets built, PDD Kit asks the team to sign off on the plan as a whole. Its first draft proved the decision at the center of login, picking the table and gating on the password, and kept the handler around it trusted and tested. That’s a sensible default, and it’s what PDD Kit recommended, but we wanted more. The handler is where the lookups get awaited and the token gets signed, and that glue is exactly where a refactor can quietly swap two lines. So at intent review we chose to give the login handler its own async spec, so the proof covers that glue too instead of trusting it.

That choice moved almost everything into the proof and left the handler with nothing to do but unpack the request. A new async function, login_flow, carries the contract all the way from the request’s fields to the token or the HTTP error.

Reading the Spec

You might be wondering whether someone now has to read the proof instead of the code. Nobody does, because the coding agent writes the proof and Verus checks every step of it. If Verus accepts the proof, it holds whether or not anyone reads it. The spec is what the proof is held to, so that’s what people review. The intent artifact is its plain-language version, and every clause carries a plain-English comment, so you can review it without knowing Verus. But it helps to know what the proof is a proof of, and this spec is short enough to learn in a few minutes. A Verus spec is Rust with a few extra pieces. The figures from here through the Where Proof Stops section, which covers what a proof can’t reach, are interactive, so hover, click and switch tabs as you read.

Each function in the spec gets an ensures block, a list of statements about its result, r, that must hold for every possible input. Verus checks them when you build, and if any clause could fail for even one input, the build fails and Verus points at that clause.

Each clause reads as an if-then. Here’s the clause for our first requirement, and you can hover over or tap any underlined part to see what it means:

// A token only for the account the login names, with its right password;// it carries that account's id and its table's role.r matches Ok(t) ==> (    named_account(email, username) matches Some(a)    && password_matches(password@, a.password_hash)    && token_claims(t@, config.jwt_secret@) matches Some(c)    && c.sub@ == a.id && c.role@ == a.role),

Notice that a is the same account on every line, which ties the password check to the token. For example, imagine a bug where login checks the password against one account but signs the token for another. Bob logs in with his own, correct password and gets back a token for Alice’s account. Each step looks fine on its own, but this clause catches it, because the password check and the token have to name the same account. That’s the kind of wiring bug a test suite rarely thinks to look for.

Login depends on SQLite, bcrypt and JWTs, and the proof can’t run any of them, so the spec gives each one a name with no body, an uninterpreted function: customer_on_file(email) and admin_on_file(username) for the rows the database holds, bcrypt_verdict(password, hash) for what bcrypt would say, and token_claims(token, secret) for what a token carries. Verus knows nothing about them except what the trusted contracts promise. The proof says “whatever the database holds, login does the right thing with it”. A trusted contract says “the lookup returns what the database holds”. On top of those, named_account(email, username) says which account a login names: the customers row for the email when one is sent, otherwise the admins row for the username, otherwise none. It looks like Rust, but it’s a mathematical definition that never runs and only appears in contracts. Code like this is called ghost code, since the verifier checks it but the compiler erases it from the program.

Here are two of the abstract views, and the definition built on bcrypt’s, straight from the spec:

/// The customers row the database holds for exactly this email, if any, when login looks.
/// Left abstract: only `Customer::find_by_email`'s trusted contract says what it is.
pub uninterp spec fn customer_on_file(email: Seq<char>) -> Option<Customer>;
...
/// What bcrypt says about `password` against a stored `hash`: Some(true) when it is the password
/// the hash was made from, Some(false) when it is not, None when bcrypt cannot read the hash.
/// Left abstract: its meaning is bcrypt's, taken on trust through `check_password`.
pub uninterp spec fn bcrypt_verdict(password: Seq<char>, hash: Seq<char>)
    -> Option<bool>;

/// The password is the right one for the stored hash, by bcrypt's verdict.
pub open spec fn password_matches(password: Seq<char>, hash: Seq<char>) -> bool {
    bcrypt_verdict(password, hash) == Some(true)
}

And here’s named_account. The email-wins rule and “the role comes from the table” are written once, here, and every clause about tokens refers back to it:

/// The account a login names: the customers row for the email when one is sent (role "customer"),
/// otherwise the admins row for the username (role "admin"), otherwise none.
pub open spec fn named_account(email: Option<String>, username: Option<String>)
    -> Option<NamedAccount> {
    match email {
        Some(e) => match customer_on_file(e@) {
            Some(c) => Some(NamedAccount {
                id: c.id@, password_hash: c.password_hash@, role: customer_role() }),
            None => None,
        },
        None => match username {
            Some(u) => match admin_on_file(u@) {
                Some(a) => Some(NamedAccount {
                    id: a.id@, password_hash: a.password_hash@, role: admin_role() }),
                None => None,
            },
            None => None,
        },
    }
}

Our two-sentence request ended up as eight clauses in the ensures block on login_flow:

• “You only get a token with the right password” became: a token only for the account the login names, with its right password, and the token carries that account’s id and its table’s role.
• The “Both ways” decision became: the right password for the named account always gets a token, unless a failed lookup or signing gives a 500.
• “Only admin accounts get admin tokens” became two clauses: the admin role only for an admins row found by username with no email sent, and an email login always gets the customer role.
• Four more pin today’s refusals: 400 with today’s message when neither an email nor a username is sent, 401 for an unknown account, 401 for a wrong password, and 500 for a stored hash bcrypt can’t read. We didn’t ask for these, but PDD Kit kept today’s behavior so the storefront and the existing API tests keep working.

Here’s the whole contract, with its doc comment trimmed. Each clause has the plain-English comment above it that the intent artifact shows you:

/// The whole login, awaited end to end: from the request's fields to the token or the HTTP error.
/// ...
pub async fn login_flow(pool: &sqlx::SqlitePool, config: &Config,
    email: Option<String>, username: Option<String>, password: &str)
    -> (r: Result<String, AppError>)
    ensures
        // Neither an email nor a username: 400 with today's message.
        email is None && username is None
            ==> (r matches Err(AppError::BadRequest(m))
                && m@ == missing_identity_text()),
        // A token only for the account the login names, with its right
        // password; it carries that account's id and its table's role.
        r matches Ok(t) ==> (named_account(email, username) matches Some(a)
            && password_matches(password@, a.password_hash)
            && token_claims(t@, config.jwt_secret@) matches Some(c)
            && c.sub@ == a.id && c.role@ == a.role),
        // The right password for the named account always gets a
        // token, unless a lookup or signing failure gives 500.
        (named_account(email, username) matches Some(a)
            && password_matches(password@, a.password_hash))
            ==> (r is Ok || r matches Err(AppError::Internal(_))),
        // A login naming an account nobody holds gets 401, unless the lookup fails with 500.
        ((email is Some || username is Some) && named_account(email, username) is None)
            ==> (r matches Err(AppError::Unauthorized)
                || r matches Err(AppError::Internal(_))),
        // A wrong password for an account whose hash bcrypt
        // can read gets 401, unless the lookup fails with 500.
        (named_account(email, username) matches Some(a)
            && bcrypt_verdict(password@, a.password_hash) == Some(false))
            ==> (r matches Err(AppError::Unauthorized)
                || r matches Err(AppError::Internal(_))),
        // An account whose stored hash bcrypt cannot read gets 500 and no token.
        (named_account(email, username) matches Some(a)
            && bcrypt_verdict(password@, a.password_hash) is None)
            ==> r matches Err(AppError::Internal(_)),
        // The admin role only for an admins row found by username, with no email sent.
        (r matches Ok(t) && token_claims(t@, config.jwt_secret@) matches Some(c)
            && c.role@ == admin_role())
            ==> (email is None && username matches Some(u)
                && admin_on_file(u@) is Some),
        // An email login's token always carries the customer role.
        (r matches Ok(t) && email is Some)
            ==> (token_claims(t@, config.jwt_secret@) matches Some(c)
                && c.role@ == customer_role()),
{
    unimplemented!()
}

Here’s every way a login can end, and only one path reaches a token:

You can try this yourself in the explorer below. Pick what the request sends, whether the account is on file and which password it uses, and it shows which of the eight clauses apply and what login returns. Then switch to Plant a bug to see which clause catches each mutation.

Most agent interfaces only ask you to make decisions, but PDD Kit also aims to teach you along the way, and it checks that you understood what you’re about to approve. When agents write the code, checking their output at the end isn’t enough. The people who own the code need to stay involved in the decisions and aware of what they’re signing off on, so one of PDD Kit’s cards is a quiz:

login_flow is async because it awaits a database query. Verus can put contracts on async functions, and there’s one rule worth knowing about when each part of the contract applies. Switch between fn and async fn below to compare them:

So the spec promises what you get if login answers, but it doesn’t promise that login answers at all.

The doc comment on login_flow says so in as many words:

/// ... No promise the future completes.
pub async fn login_flow(...) -> (r: Result<String, AppError>)

login_flow stays short because it’s built from smaller proved pieces. lookup_target picks the table. login_core awaits the lookup and calls decide_login, the password gate. issue_token signs the token, or maps a refusal to today’s HTTP error. Each piece has its own contract, and Verus proves login_flow using only those contracts, without re-reading their bodies. Change the body of decide_login and only decide_login gets proved again.

Here’s the smallest piece, whole, and the start and end of the password gate:

pub fn lookup_target(email: Option<String>, username: Option<String>)
    -> (r: Result<LookupTarget, LoginError>)
    ensures
        // An email, when sent, wins: customers are searched for exactly that email.
        email matches Some(e)
            ==> r == Ok::<LookupTarget, LoginError>(LookupTarget::CustomerByEmail(e)),
        // With no email, a username sends the search to admins for exactly that username.
        email is None && username matches Some(u)
            ==> r == Ok::<LookupTarget, LoginError>(LookupTarget::AdminByUsername(u)),
        // With neither, the login is refused for missing an identity.
        email is None && username is None
            ==> r == Err::<LookupTarget, LoginError>(LoginError::MissingIdentity),

pub fn decide_login(target: &LookupTarget, found: Option<AccountRow>, password: &str)
    -> (r: Result<IssuedClaims, LoginError>)
    ensures
        // No row found: refused as Unauthorized, the same answer as a wrong password.
        found is None
            ==> r == Err::<IssuedClaims, LoginError>(LoginError::Unauthorized),
        // Claims come back only for a found row whose stored hash matches the password.
        r is Ok ==> found is Some
            && password_matches(password@, found->Some_0.password_hash@),
        // The right password for a found row always gets claims.
        found matches Some(a) && password_matches(password@, a.password_hash@)
            ==> r is Ok,
        ...
        // An admins-table search gives the role text "admin".
        r matches Ok(c) && target is AdminByUsername ==> c.role@ == admin_role(),
        // A customers-table search gives the role text "customer".
        r matches Ok(c) && target is CustomerByEmail ==> c.role@ == customer_role(),

An Overview of login.rs

Here’s the formal spec the team signed off on, verified/src/login.rs, part by part. It reads top to bottom in four layers: the types Verus needs to know about, an abstract view of the outside world, the trusted contracts that connect that view to real code, and the five contracts the proof has to meet. Pick any part in the list, or step through with the arrows, to see what it does, why it’s there, and the exact lines.

A few things are worth noticing. Every assumption is written down in one place, as a contract with a doc comment that says what rests on it. The spec never simulates SQLite, bcrypt or a JWT. It names what it needs from them and says, in one trusted contract each, how the real code provides it. And the five proved functions have no bodies yet. That’s on purpose, because the contracts come first, the team approves them, and only then does the proof stage write code that has to meet them.

Here are two of the less obvious parts, abridged. external_type_specification introduces a type Verus didn’t define. The pool stays opaque, while a customers row keeps its fields visible:

/// The connection pool, opaque to the proof: only the lookups' contracts say what it returns.
#[verifier::external_type_specification]
#[verifier::external_body]
#[verifier::reject_recursive_types(DB)]
pub struct ExPool<DB: sqlx::Database>(sqlx::Pool<DB>);
...
/// A customers row, with its fields visible to the proof.
#[verifier::external_type_specification]
pub struct ExCustomer(Customer);

And LoginError keeps the decision separate from the HTTP response, which is what lets issue_token pin each refusal to today’s status code:

/// Why a login gets no token.
pub enum LoginError {
    /// Neither an email nor a username was sent: 400 Bad Request.
    MissingIdentity,
    /// No such account, or the password does not match: 401 Unauthorized.
    Unauthorized,
    /// bcrypt could not read the stored hash, with its message: 500 Internal.
    UnreadableHash(String),
    /// The lookup query failed: 500 Internal, with sqlx's message.
    Database(sqlx::Error),
}

Where Proof Stops

There are plenty of things you can’t prove about a program, and login runs into most of them:

• Code the verifier can’t see. bcrypt’s hashing, sqlx’s queries and jsonwebtoken’s signing live in other crates, outside the proof.
• Facts about the outside world. What SQLite holds right now and what time the clock says are inputs to the program, not something its code can establish.
• Whether, and how fast, something finishes. This spec says what you get if login answers. A hung query, or a slow one, breaks nothing in it.
• Anything a person has to judge, like whether an error message helps or a screen makes sense.
• Whatever nobody wrote down. A proof covers its spec and says nothing about requirements outside it.

That’s where empirical verification comes in. PDD Kit spells out the trusted boundary, the trusted computing base (TCB) that the proof assumes behaves as described. It wraps each trusted piece in a small function with an assumed contract, asks you to accept each one on its own, and writes a test for every assumed clause into the plan before any of them exist. For login, that’s six sign-offs. Here’s what two kinds of trusted piece look like in the spec. A lookup keeps its code where it is and gets a contract from the outside with external_fn_specification:

/// Looks up a customer by exact email.
/// Trusted, not proved: the SQL query runs in sqlx, which Verus cannot check.
/// Every customer promise of `login_flow` rests on it.
#[verifier::external_fn_specification]
pub async fn ex_customer_find_by_email(pool: &sqlx::SqlitePool, email: &str)
    -> (r: Result<Option<Customer>, sqlx::Error>)
    ensures
        // When the query succeeds, it returns the customers row on
        // file for exactly this email, or None when there is none.
        r matches Ok(found) ==> found == customer_on_file(email@),
{
    Customer::find_by_email(pool, email).await
}

check_password and the clock are small wrappers marked external_body. Verus uses their ensures clauses and never reads the bodies:

/// Asks bcrypt whether `password` matches the stored `hash`.
/// Trusted, not proved: Verus cannot check bcrypt's hashing,
/// so this wrapper's contract is assumed.
/// Every password promise of `login_flow` rests on it.
#[verifier::external_body]
pub fn check_password(password: &str, hash: &str) -> (r: Result<bool, String>)
    ensures
        // bcrypt answers (Ok) exactly when it can read the stored hash.
        r is Ok <==> bcrypt_verdict(password@, hash@) is Some,
        // Its answer is its verdict: true for the right password, false for any other.
        r matches Ok(b) ==> bcrypt_verdict(password@, hash@) == Some(b),
{
    bcrypt::verify(password, hash).map_err(|e| e.to_string())
}

/// Reads the clock and computes a token's expiry 24 hours ahead.
/// Trusted, not proved: chrono's clock is outside the proof.
/// It panics if the time is out of range, as today's login does;
/// that panic is not promised against.
#[verifier::external_body]
pub fn expiry_from_now() -> (r: Expiry)
    ensures
        // The expiry is exactly 24 hours (86,400 seconds) after the clock reading.
        r.exp as int == r.now as int + 86_400,
{
    ...
}

Click any function in the call tree below to see whether it’s proved or trusted, and for each of the six trusted pieces, what you accept and how it’s tested:

ensures r is Ok <==> bcrypt_verdict(password@, hash@) is Some
ensures r matches Ok(b) ==> bcrypt_verdict(password@, hash@) == Some(b)

Each sign-off is its own decision card. It shows the clauses Verus will take on faith, what you’re accepting, and which promise falls apart if the assumption is wrong:

The plan is just as explicit about what nobody is promising: that the login future ever completes, that an out-of-range clock won’t panic, anything about the timing or rate of attempts, and how other endpoints read the role. Every trusted clause gets a test in the plan’s Empirical verification section, written as Given/When/Then scenarios and marked planned until it runs. Then it records the command’s result and the commit it ran against. A passing test is evidence, not proof, and PDD Kit labels it that way.

Behind the plan, PDD Kit writes the formal spec as Verus contracts. You can read them, and every clause has a plain-English comment above it, but you don’t have to. The intent artifact you reviewed is the human-readable version of the same thing. Before the spec comes back to you, two reviewer agents poke holes in the formal spec derived from the intent artifact: does it match what you asked for, and does it promise more than a proof could show? The refinement runs in the background, taking your feedback as it comes, and iterates until the reviewers agree the spec is sound. That’s still review, and the proof comes next.

From Spec to Merged Code

Signing off on the spec is where the developer’s review ends. Everything after it, the implementation and the proof, is checked by machines. That’s why this page spends its time on the spec and not the proof: the spec is what people review, and the proof only has to match it.

Once the plan matched what we meant, we clicked Build plan. PDD Kit turned the approved spec into a small task graph and started working through it in the background on a development machine:

Each task runs the same loop. A coding agent writes the implementation and the proof, and Verus checks them against the spec. An LLM verifier reads the plan, the spec and the results side by side, looking for gaps: requirements with no proof and no passing check. Gaps go back to the coding agent. A contradiction in the spec itself comes back to the team as a decision. The loop is strict about not moving the goalposts. If an async construct can’t be expressed in the pinned Verus, the task stops and asks rather than switching to a non-async helper or weakening a contract.

A proof is only as good as its spec, so PDD Kit checks the spec too. Its mutation check plants one bug per ensures clause in a scratch copy of the code, like the ones in the Plant a bug tab of the login explorer above, and Verus has to reject each mutant on the clause it targets. A mutant that gets through means that clause constrains nothing, and it comes back as a gap. This is how PDD Kit guards against vibe verification, the specs that verify but rule out almost nothing that we described in the Vibe Verification section.

When the tasks pass, PDD Kit opens pull requests. They add the verified/ crate with login_flow, its pieces, their proofs and the trusted wrappers with their tests, and route the real login handler through login_flow, so the verified logic hardens the production login path, not a copy of it. The pull request works as a receipt, marking every login requirement as formally verified or empirically checked and listing every trusted piece with the test that covers it. A developer reviews that receipt against the intent they already signed off on, instead of reading the generated code line by line, and merges.

Merging is where the proof joins the team’s normal workflow. The Verus check goes into CI next to the empirical tests, so every later change to login, by a person or an agent, has to keep proving against the same spec, and a broken proof fails the build like a failing test. And because a proof covers every input, PDD Kit prunes tests that only re-check what’s already proved, such as example-based tests of the password gate, and keeps the ones that guard the trusted boundary, so CI gets stronger and smaller at the same time.

Here are the headline pieces we’ve built into PDD Kit so far:

• Decision cards that explain the relevant code before asking you to decide anything.
• A rough work section that keeps a long planning session readable, with flow diagrams, a spec landscape, mental-model pictures and an intent map tied to what you said.
• An explicit trusted boundary. Every piece the proof assumes is named, accepted by a person, and given a test.
• Formal specs in Verus, async functions included, generated from the intent you approved, with an English comment on every clause.
• A prove loop. A coding agent writes code and proof, Verus checks them, and an LLM verifier hunts for requirements with no proof and no passing check.
• A mutation check that plants one bug per clause, so no clause can be vacuous.
• Pull requests that work as receipts, stating what was proved, what was trusted, and the limitations.
• CI that runs the Verus check next to the empirical tests, and prunes tests the proof already covers.

There’s a side effect we didn’t expect to like so much. Once reliance on exhaustive line-by-line review goes down, readability stops being the main reason to choose a language. You can pick Rust for speed and safety and optimize as hard as you want, because any change that breaks the spec fails the proof.

What to Expect from PDD Kit

PDD Kit is a research prototype, and it only verifies Rust today since that’s the language Verus works on. Code in other languages can be ported to Rust and checked against the same spec, and non-Rust projects can call verified Rust through bindings. Proofs still take real effort, mostly in producing the proof itself, and a clear spec is what keeps that effort down, which is why so much of PDD Kit is about getting intent right first. We’d start where a bug costs the most, such as login, payments, or permissions, and verify the rest of a codebase one piece at a time.

Pet Store’s login is one piece of one app: a spec anyone can read, a Verus proof that the code matches it, and tests for everything the proof takes on trust. We want to be upfront about the weakest links. The guarantees are only as strong as the six trusted pieces, and two carry most of the weight: check_password for every password promise, and the two lookups for every promise about which account a token names. Tests support them, but nothing proves them. We expect that trusted boundary to shrink significantly over time, so a growing share of the code can be formally verified, and we want to find out how far this scales.

What we’re really changing is what people review. Instead of relying mainly on line-by-line review of agent-generated code, a team reviews what it meant, in plain language, and a proof holds the code to it. The plan was always supposed to be the contract, and now the agent actually has to keep it.