Microsoft’s PDD Kit Turns Code Review Into Intent Review, but Verus Accepts a Login That Answers Every Attempt With a 500 Under the Contract the Post Prints

On November 5, Microsoft Research published Formally verifying agent-written full-stack web apps with PDD Kit, by Alex Lavaee and Matthai Philipose. The work is a collaboration with GitHub Next, which carries its own project page. The two organizations announced PDD Kit on X on October 21 (GitHub Next at 15:58 UTC, Microsoft Research at 19:19 UTC) and promised a demonstration at GitHub Universe on October 28 and 29. The pitch is that coding agents now write more code than people can read, so a team should review what it meant instead. PDD Kit asks the developer questions, records the answers in an “intent artifact,” turns the part that can be formalized into a specification for the Verus proof language, has an agent write the Rust code and the proof, and falls back to tests where a proof cannot reach. The worked example is the login logic of Pet Store, a Rust storefront of about 5,000 lines, specified from a request of two sentences.

The post prints the whole contract for the function that does the login, login_flow: eight ensures clauses, each with a plain-English comment above it. The comments are what the post’s intent artifact shows the team, and the intent artifact is what a human reviews in place of the code, so we treated the contract as the thing to test. We rebuilt the eight clauses as a Verus file, wrote an honest implementation, and ran 17 files through Verus 0.2026.11.02, among them the bugs that the project page’s own explorer plants. Almost everything behaves as the post says. One result does not: a login that answers every attempt with a 500 verifies.

Our earlier posts on a Harvard study of 718 firms and the code-review queue, on Cloudflare’s agent-written tsrs port, where the test oracle is the product, and on two labs’ claimed refutations of the Exponential Time Hypothesis, where Lean checks the proof but not the statement come at the same question from other sides: once a machine checks the work, what does a person still have to read? This post is about one such thing, a contract of eight clauses.

What we found in short

• We rebuilt the eight printed clauses for login_flow as a Verus file. An honest implementation verifies (1 verified, 0 errors, in under a second on Verus 0.2026.11.02.8bf68ee with Z3 4.16.0).
• All ten variants that change a status code, a role or an account are rejected. For the six bugs the project page’s explorer also plants, Verus rejects each on every clause the page lists and sometimes on more. The page lists the clauses that break in the one login it shows per bug; Verus lists every clause a bug can break for some login.
• The “both ways” decision does real work. With clause 3 deleted, a login that never issues a token verifies. With clause 3 in place, Verus rejects it.
• A login that answers every attempt with a 500 verifies, and so does one that answers every customer with a 500 while admins still sign in. Clauses 3, 4 and 5 each end with a branch that allows an Internal error, and nothing in the contract ties that 500 to a failure. The comment above clause 3 says “unless a lookup or signing failure gives 500.” The clause accepts any Internal error.
• The page’s own model of clause 3 has the same shape: its conclusion accepts a 200 or a 500 and never consults the Infrastructure setting (works, DB fails, signer fails) that the same page offers. The six bugs on its Plant a bug tab include an outage reported as a 401. None reports a 500 without an outage.
• A stricter contract closes the gap: three failure facts, one specification function and a ninth clause saying a 500 happens exactly when a trusted piece fails. It adds 43 lines and replaces nine. The honest code still verifies, and all twelve variants that misbehave are rejected, including both 500 logins.
• Trusted pieces stay trusted. A check_password whose body says yes to everything verifies, because Verus reads a trusted function’s contract and never its body. The post says so and lists tests for each such piece.
• The post’s summary says Verus “uncovered existing bugs.” The post names none, and the project page does not make the claim. Neither page links a repository, release or paper for PDD Kit itself.

What Microsoft published

The two pages tell the same story with different figures. The developer asks Chopin, GitHub Next’s planning environment, to do this: “Verify the login logic in backend/src/handlers/auth.rs.” The request lists two requirements: “You only get a token with the right password.” and “Only admin accounts get admin tokens.” PDD Kit reads the code and comes back with questions on decision cards before it writes anything. The first card asks whether the right password must always get a token, or only whether a token needs the right password. The developer answers both ways, and the figure caption explains why: “Proving both ways rules that out,” meaning a login that refuses everyone.

The answers become a Verus specification with an English comment on every clause. Two reviewer agents then check it so that it “doesn’t promise more than a proof could show.” A coding agent writes the code and the proof, Verus checks them, and a mutation check “plants one bug per ensures clause in a scratch copy of the code, like refusing everyone or checking the username before the email, and Verus has to reject each mutant on the clause it targets.” The result is a pull request that, in the post’s words, “works as a receipt, and its description marks every login requirement as either formally verified or empirically checked.” The Verus check then joins CI, where “every later change to login, by a person or an agent, has to keep proving against the same spec.”

The proof covers five functions: login_flow, login_core, lookup_target, decide_login and issue_token. Six pieces sit outside it behind contracts that people accept and tests check: the two database lookups, check_password, token signing, the clock, the database-error wrapper and the handler that unpacks the request. The review burden moves to the intent artifact, the plain-language version of the contract: “The developer reviewed the intent and never read the generated code line-by-line.”

The two sentences and the eight clauses

The developer’s two sentences became eight clauses. The explorer on the project page labels each with the requirement it serves, and the page says “Four more pin today’s refusals.” The table gives our numbering, which follows the post’s order, with the explorer’s labels in the second column.

The project page adds the sentence that matters for everything below: “Every clause is an if-then. It only constrains the logins where its if-part is true.” What a clause allows when its if-part is true is whatever its then-part lists.

How we tested the contract

Verus is a verifier for Rust. The project page describes it this way: “You write ordinary Rust plus requires and ensures clauses, and Verus checks at compile time that the code meets them for all inputs.” We used the Windows build of release 0.2026.11.02.8bf68ee, published on November 2, which needs Rust toolchain 1.99.1 and bundles Z3 4.16.0.

The file login.rs, shown in full at the end of this post, has four parts. The outside world is declared the way the post declares it: customer_on_file, admin_on_file, bcrypt_verdict and token_claims are functions with no body, so Verus knows nothing about them except what a trusted contract says. The trusted pieces carry the post’s contracts and bodies that Verus never reads. Then come the eight clauses, and an honest body.

What we changed from the printed text

• The stand-in is synchronous. The post’s login_flow is async, and its rule is that ensures describes the value you get when you await the future. The clauses talk about that value, r, so a synchronous function with the same r tests the same clauses. Our lookups are plain functions with the post’s contracts, and the connection pool parameter is gone.
• Three of the six trusted pieces appear: the two lookups (as two functions), check_password and generate_token. We left out the clock, the database-error wrapper and the handler shell, which none of the eight clauses mentions.
• Verus 0.2026.11.02 wants parentheses around a second matches inside an && chain (clauses 2 and 7), and it does not carry the binding from r matches Ok(t) out of a parenthesized antecedent, so we wrote clause 8 as r matches Ok(t) ==> (email is Some ==> ...). The logic is the same. The post was written against a pinned Verus that may differ.
• The types and two strings are ours. The row types, Config, Claims and the AppError variants follow what the clauses use, the roles are the strings "customer" and "admin", and the 400 message is our own wording because the post says only “today’s message.”

None of this touches the main result below. It depends on the shape of clauses 3, 4 and 5, which we copied as printed.

The honest implementation verifies

The honest body looks up the customer by email when an email is sent, otherwise the admin by username, checks the password with check_password, and signs a token with the role of the table it searched. Verus answers 1 verified, 0 errors. That shows the reconstruction is coherent and the contract satisfiable. It says nothing about the real Pet Store code, which we could not read.

What the eight clauses reject

We then changed the body of the function. Each change is a variant: some plant a bug the post describes, some are the bugs on the explorer’s Plant a bug tab, and some are our own. Every variant goes through Verus with --multiple-errors 20, because by default Verus stops after two failing clauses per function and we wanted the complete list. The last column previews the stricter contract described further down.

Read the first ten variants as the good news. Each one changes a status code, a role or an account, and Verus rejects each on the clause the post’s wording would predict. The post’s own example, checking the username before the email, fails seven of the eight clauses. Its other example, refusing everyone, fails clause 3. Our blunt version also fails clause 6, because it answers unreadable hashes with a 401 instead of a 500; the sharper “never issue a token” fails clause 3 alone. The “answer 500” rows are the ones to look at next. The two trusted rows are a different matter, covered below.

Where the page and Verus agree

The explorer’s script lists six bugs, each with the clauses it breaks. We compared them with our versions of the same bugs. Every list on the page is contained in the list Verus reports, and three are identical. The difference is in what is being listed: the page shows the clauses that fail in the one login it displays for each bug, while Verus reports every clause the bug can violate for some login.

The both-ways decision does real work

The decision card’s point is that a login which refuses everyone satisfies “a token only with the right password.” We checked that claim by deleting clause 3, which is the “both ways” half, and trying the two refusal variants against the rest of the contract. The sharper one, “never issue a token,” verifies: every right password gets a 401, and every other promise holds. With clause 3 in place Verus rejects it, on clause 3 alone. The blunt “refuse everyone with 401” is still rejected without clause 3, but only by clause 6, because it also answers unreadable hashes with a 401. So the decision card is right about refusals that answer with a 401, and the clause it produced is the only one that catches the sharper variant. The page’s own explanation of its first bug says the same thing: the clause that makes the right password get a token is what catches it.

What the contract lets through

A login that answers every attempt with a 500

The variant keeps the 400 for a request with no identity and answers every other request with an internal error:

if email.is_none() && username.is_none() {
    Err(AppError::BadRequest(String::from_str("email or username is required")))
} else {
    Err(AppError::Internal(String::from_str("service unavailable")))
}

Verus accepts it. Each clause holds for a reason that has nothing to do with signing anyone in. Clause 1 holds by construction. Clauses 2, 7 and 8 begin with “if login returns a token,” and this login never does. Clauses 3, 4 and 5 list an Internal error among the allowed outcomes. Clause 6 requires one. The second variant answers every request that names an email with the same 500 and leaves the admin path honest. An admin smoke test would pass, and so would the proof: customers are the ones who cannot sign in.

The comment promises more than the clause proves

The comment above clause 3 reads: “The right password for the named account always gets a token, unless a lookup or signing failure gives 500.” The clause under it says r is Ok || r matches Err(AppError::Internal(_)). The comment names two causes for the 500. The clause allows the 500 for any reason, because the contract has no way to say that a lookup or a signer failed: a failure is not an input of login_flow, and no fact in the eight clauses records one. Clauses 4 and 5 carry the same tail, and their comments say “unless the lookup fails with 500.”

The post says its reviewer agents check that the specification “doesn’t promise more than a proof could show.” Here the English layer promises a little more than the Verus layer proves, and the English layer is the one a team reads. The explorer’s own model has the same shape. Its outcome function returns a 500 only when the lookup fails, the hash is unreadable or the signer fails, but its check for clause 3 accepts any 200 or 500 and never looks at the Infrastructure setting. The page’s explanation of its outage bug says it plainly: “The right password may miss a token only through a 500.” That is the sentence the clause lets a login take too far.

The pieces promise more than login_flow exports

The pieces beneath login_flow are tighter. The printed clause for decide_login has no escape: its comment reads “The right password for a found row always gets claims,” and the clause concludes r is Ok. The explorer’s description of login_core promises a token for the right password “always with it unless the lookup fails.” So the proof of login_flow may well use tighter facts than the eight clauses state. But the post says “Verus proves login_flow using only those contracts, without re-reading their bodies,” and the tighter promises are not among the eight clauses that a caller of login_flow can rely on.

That matters less for today’s code, which we could not read, than for later changes. The post says every later change to login has to keep proving against the same spec. An edit to the body of login_flow itself that returned a 500 too early would still satisfy the eight clauses, which is what our variants show on the stand-in.

What the mutation check can and cannot see

The check as described plants one bug per clause and requires Verus to reject it on that clause. For clauses 3, 4 and 5 the natural bugs are refusals with the wrong status, and the explorer’s tab plants exactly that, down to an outage reported as a 401. A 500 with no failure is a bug of the opposite kind: it takes a branch the clause allows. Such a mutant would get through, and a mutant that gets through is what the check reports as a gap, but only if the check plants one; a check that plants only the bugs a clause forbids never sees the holes it leaves. The post says “A mutant that gets through means that clause constrains nothing, and it comes back as a gap.” Clause 3 does constrain something, since it rules out a 401 and a 400 for the right password, so a surviving 500 mutant would show a partial hole rather than the “nothing” that sentence describes. We cannot tell whether PDD Kit plants a 500 variant, because neither page says.

What would catch it

Tests. The explorer lists the planned tests for the handler shell: login_token_carries_the_checked_account_and_its_role, login_refusals_issue_no_token, login_unreadable_hash_returns_500 and login_database_failure_returns_500. We cannot see them. A test of the first name would fail on a login that never succeeds if it signs a customer in with the right password, and that is the net the post relies on for what a proof leaves open. The place the gap would show is the receipt. A reader looking at the row for the right-password requirement should ask which of the two labels it carries, and whether “formally verified” there means “a token, or a 500.”

One more detail from the post bears on this: PDD Kit “prunes tests that only re-check what’s already proved, such as example-based tests of the password gate.” The gate has an exact contract, so that pruning is sound for the gate. The whole flow does not, as printed, so an end-to-end test of the happy path is not something the proof makes redundant.

A stricter contract

What changes

The stricter file, produced from login.rs by tighten.py, adds 43 lines and replaces nine. It declares three facts that Verus knows nothing about beyond what the contracts say: customer_lookup_fails, admin_lookup_fails and signing_fails, each a yes-or-no answer about one request, declared exactly like customer_on_file. The trusted lookups and the signer now say they fail when, and only when, the fact says so. A specification function, trusted_failure, says when any trusted piece fails for a request: a lookup fails, the stored hash is unreadable, or the signer fails after a right password. Clauses 3, 4 and 5 drop their “or 500” branch and apply when there is no trusted failure. A ninth clause ties the 500 to the failure in both directions:

// C9: a 500 exactly when a trusted piece fails for this request.
(r matches Err(AppError::Internal(_)))
    <==> trusted_failure(email, username, password@, config.jwt_secret@),

The ninth clause says “exactly” for a reason. One direction, a 500 only when something fails, is what closes the gap above. The other direction, a failure always surfaces as a 500, states the outage promise that the page’s outage bug breaks, and in the stricter file that bug fails clause 9 as well as clause 6.

What the failure facts assume

Whether a trusted piece fails is treated as a fact about the request, the same way the post treats what the database holds. The proof then covers every world: for each request it considers the worlds where the lookup fails and the worlds where it succeeds. The model does not describe a piece that fails on one call and succeeds on the next for the same request. Our stand-in makes each call once.

What it costs and what it fixes

The honest code still verifies. All twelve variants that misbehave are rejected, including both 500 logins, which now fail clauses 3, 4, 5 and 9. The price is a longer contract for a person to read and three more facts that need tests: the plan already names login_database_failure_returns_500 and login_unreadable_hash_returns_500, and a signing-failure test would sit beside them. What it does not fix is the trusted boundary.

What the proof still takes on trust

The post is candid here: “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.” Our last two rows show what that means in a run. A check_password whose body returns Ok(true) for every password, and a find_customer whose body returns Ok(None) for every email, both verify. The Verus guide says why: a function is marked external_body “so that Verus pays attention to the function’s preconditions and postconditions but ignores the function’s body.” The first lets any password sign in to a known account and the second locks every customer out. Verus accepts both, and the tests the plan lists are the only net. This is by design. It also means every new fact in the stricter contract needs a test of its own.

What we could not check

• Pet Store’s real code, its proofs and PDD Kit’s prove loop. Neither page links them, so we tested the printed contract only, as a specification of acceptable behavior.
• Whether PDD Kit’s mutation check plants a variant that takes an allowed branch for the wrong reason. The explorer lists six bugs and none is of that kind.
• The pull request receipt for login. Neither page shows its text.
• The “existing bugs” in the summary. The post’s body describes a hypothetical (Bob logs in with his own password and gets a token for Alice) and the planted mutants, and says the verified code keeps today’s status codes. It names no bug that was found in the code.
• The Verus version PDD Kit pins. The post says only “the pinned Verus,” so the syntax adjustments above may not apply there.
• How to try PDD Kit. The post and the project page link Verus, Chopin, Spec Kit and the Rust crates, and the project page lists its stage as Research Prototype, but no repository, release or install steps for PDD Kit. Five repository names we guessed under the microsoft account returned 404, and the Chopin repository (MIT licensed, 3,104 paths on November 5) has no path containing pdd, verus, proof or formal. A GitHub search for the name finds itai-gendler/pdd-kit, an unrelated project, “Product-Driven Development for coding agents.” Chopin itself is described on its page as “a very small, early research prototype.”

What holds up

• Printing the full contract with a comment on every clause is what made this check possible, and it gives a reviewer something concrete to read.
• All ten bug variants are rejected, on the clauses the post’s wording predicts, and every list on the project page’s explorer is contained in the list Verus reports.
• The both-ways decision does what its card says about refusals that answer with a 401. Without clause 3, a login that never issues a token verifies.
• The post is open about its trusted pieces and about what nobody is promising: that the login future completes, how the clock behaves, the timing or rate of attempts and how other endpoints read the role. Its FAQ says the part that applies here: “A proof shows the code meets the spec, not that the spec is what you meant.” Our finding is a small instance of that sentence, one comment promising slightly more than its clause.
• Verification is fast. The honest file takes under a second and all 17 files take about 12 seconds on this machine, in line with the post’s “usually seconds for a small module.” Our stand-in is small, so this says little about a large crate.

What we would ask Microsoft Research and GitHub Next

1. State whether the mutation check plants, for each clause with an “or” branch, a mutant that takes the allowed branch for the wrong reason. If it does not, add one per allowed outcome.
2. Either tie the 500 to a failure in the contract, as our ninth clause does, or change the comment to say what the clause proves: a token or any internal error.
3. Show a pull request receipt, with its wording for the right-password requirement.
4. Name the existing bugs the summary refers to, or drop the claim.
5. Say how to get PDD Kit and publish the verified crate, so that the proofs of the five functions can be read and rerun.

If you plan to review contracts instead of code

1. Read the “or” branches first. Each is an outcome the code may always take. Ask what keeps it from being the only outcome.
2. For every outcome that signals failure (a 500, an error variant, a timeout), ask that the contract name the failure, or keep an end-to-end happy-path test and do not prune it because a proof “covers” the property.
3. Mutate the contract yourself. For each clause, write the bug it forbids and the bug it allows. The second kind is the one a check that plants only forbidden bugs never sees. A short script like mutants.py below does it.
4. Treat every trusted body as untested until its test exists: search for external_body and external_fn_specification, and ask which test backs each clause.
5. Compare the English comment with the clause word by word wherever the comment says “unless.”

Run the checks yourself

These steps were run on Windows 11 with Git Bash and Python 3.13. Verus prints the exact rustup command if the toolchain is missing, and on Linux or macOS you pick the matching zip from the same release.

Step 1: install Verus and its Rust toolchain

curl -sL -o verus.zip https://github.com/verus-lang/verus/releases/download/release/0.2026.11.02.8bf68ee/verus-0.2026.11.02.8bf68ee-x86-win.zip
python -c "import zipfile; zipfile.ZipFile('verus.zip').extractall('.')"
rustup toolchain install 1.99.1-x86_64-pc-windows-msvc --profile minimal
./verus-x86-win/verus.exe --version

The last command prints the version:

Verus
  Version: 0.2026.11.02.8bf68ee
  Profile: release

Step 2: the contract and the honest implementation

Save this as login.rs. The comments such as // CUSTOMER ARM START mark the pieces that mutants.py recombines, so leave them in place.

// login.rs: a synchronous stand-in for the login_flow contract that Microsoft Research printed
// in its PDD Kit post (2026-11-05). Checked with Verus 0.2026.11.02.8bf68ee.
// The eight ensures clauses below are the post's clauses, in the post's order (labels C1 to C8 are mine).
use vstd::prelude::*;
use vstd::string::*;

verus! {

pub struct Customer { pub id: String, pub password_hash: String }
pub struct Admin { pub id: String, pub password_hash: String }
pub struct Claims { pub sub: String, pub role: String }
pub struct Config { pub jwt_secret: String }

pub enum AppError {
    BadRequest(String),
    Unauthorized,
    Internal(String),
}

pub struct NamedAccount {
    pub id: Seq<char>,
    pub password_hash: Seq<char>,
    pub role: Seq<char>,
}

// The outside world, left abstract the way the post does it.
pub uninterp spec fn customer_on_file(email: Seq<char>) -> Option<Customer>;
pub uninterp spec fn admin_on_file(username: Seq<char>) -> Option<Admin>;
pub uninterp spec fn bcrypt_verdict(password: Seq<char>, hash: Seq<char>) -> Option<bool>;
pub uninterp spec fn token_claims(token: Seq<char>, secret: Seq<char>) -> Option<Claims>;

pub open spec fn password_matches(password: Seq<char>, hash: Seq<char>) -> bool {
    bcrypt_verdict(password, hash) == Some(true)
}

pub open spec fn customer_role() -> Seq<char> { "customer"@ }
pub open spec fn admin_role() -> Seq<char> { "admin"@ }
pub open spec fn missing_identity_text() -> Seq<char> { "email or username is required"@ }

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,
        },
    }
}

// The trusted pieces: Verus reads the contract and never the body.
#[verifier::external_body]
pub fn find_customer(email: &str) -> (r: Result<Option<Customer>, String>)
    ensures
        r matches Ok(found) ==> found == customer_on_file(email@),
{
    unimplemented!()
}

#[verifier::external_body]
pub fn find_admin(username: &str) -> (r: Result<Option<Admin>, String>)
    ensures
        r matches Ok(found) ==> found == admin_on_file(username@),
{
    unimplemented!()
}

#[verifier::external_body]
pub fn check_password(password: &str, hash: &str) -> (r: Result<bool, String>)
    ensures
        r is Ok <==> bcrypt_verdict(password@, hash@) is Some,
        r matches Ok(b) ==> bcrypt_verdict(password@, hash@) == Some(b),
{
    unimplemented!()
}

#[verifier::external_body]
pub fn generate_token(sub: &str, role: &str, secret: &str) -> (r: Result<String, String>)
    ensures
        r matches Ok(t) ==> (token_claims(t@, secret@) matches Some(c) && c.sub@ == sub@ && c.role@ == role@),
{
    unimplemented!()
}

pub fn login_flow(config: &Config, email: Option<String>, username: Option<String>, password: &str)
    -> (r: Result<String, AppError>)
    ensures
        // C1: neither an email nor a username: 400 with the missing-identity message.
        email is None && username is None
            ==> (r matches Err(AppError::BadRequest(m)) && m@ == missing_identity_text()),
        // C2: a token only for the named account, with its right password, carrying that account's id and 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)),
        // C3: the right password for the named account always gets a token, unless a failure gives 500.
        (named_account(email, username) matches Some(a)
            && password_matches(password@, a.password_hash))
            ==> (r is Ok || r matches Err(AppError::Internal(_))),
        // C4: 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(_))),
        // C5: a wrong password for an account whose hash bcrypt can read gets 401, unless a 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(_))),
        // C6: 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(_)),
        // C7: 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)),
        // C8: 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())),
{
    proof {
        reveal_strlit("customer");
        reveal_strlit("admin");
        reveal_strlit("email or username is required");
        assert(customer_role() != admin_role());
    }
    // BODY START
    match &email {
        Some(e) => {
            // CUSTOMER ARM START
            let found = match find_customer(e.as_str()) {
                Ok(f) => f,
                Err(m) => return Err(AppError::Internal(m)),
            };
            match found {
                None => Err(AppError::Unauthorized),
                Some(c) => match check_password(password, c.password_hash.as_str()) {
                    Err(m) => Err(AppError::Internal(m)),
                    Ok(false) => Err(AppError::Unauthorized),
                    Ok(true) => match generate_token(c.id.as_str(), "customer", config.jwt_secret.as_str()) {
                        Ok(t) => Ok(t),
                        Err(m) => Err(AppError::Internal(m)),
                    },
                },
            }
            // CUSTOMER ARM END
        }
        None => match &username {
            Some(u) => {
                // ADMIN ARM START
                let found = match find_admin(u.as_str()) {
                    Ok(f) => f,
                    Err(m) => return Err(AppError::Internal(m)),
                };
                match found {
                    None => Err(AppError::Unauthorized),
                    Some(a) => match check_password(password, a.password_hash.as_str()) {
                        Err(m) => Err(AppError::Internal(m)),
                        Ok(false) => Err(AppError::Unauthorized),
                        Ok(true) => match generate_token(a.id.as_str(), "admin", config.jwt_secret.as_str()) {
                            Ok(t) => Ok(t),
                            Err(m) => Err(AppError::Internal(m)),
                        },
                    },
                }
                // ADMIN ARM END
            }
            None => Err(AppError::BadRequest(String::from_str("email or username is required"))),
        },
    }
    // BODY END
}

} // verus!

Verify it:

./verus-x86-win/verus.exe --crate-type=lib login.rs

verification results:: 1 verified, 0 errors

Step 3: the variants

Save this as mutants.py. It reads login.rs, builds each variant by replacing the marked body (or a trusted body), runs Verus on it, and labels each failing postcondition with the nearest // C<n>: comment above it. A variant is accepted when Verus reports zero errors.

# mutants.py
"""mutants.py [login.rs]
Build mutants of the honest login_flow body in login.rs, run Verus on each one, and print which
ensures clauses (C1 to C9) Verus says fail. Set VERUS to the verus executable (default: verus on PATH)."""
import os
import re
import subprocess
import sys
import tempfile

VERUS = os.environ.get("VERUS", "verus")
SRC = sys.argv[1] if len(sys.argv) > 1 else "login.rs"
text = open(SRC, encoding="utf-8").read()


def between(s, start, end):
    i = s.index(start) + len(start)
    return s[i:s.index(end, i)]


# The honest body and its two arms are marked with comments in login.rs.
CUST = between(text, "// CUSTOMER ARM START\n", "            // CUSTOMER ARM END")
ADM = between(text, "// ADMIN ARM START\n", "                // ADMIN ARM END")
HONEST = between(text, "// BODY START\n", "    // BODY END")
NEITHER = 'Err(AppError::BadRequest(String::from_str("email or username is required")))'
BOOM = 'Err(AppError::Internal(String::from_str("service unavailable")))'


def first(old, new):
    """The honest body with the first occurrence of `old` replaced."""
    assert old in HONEST, old
    return HONEST.replace(old, new, 1)


MUTANTS = {
    "honest (control)": HONEST,
    "refuse everyone with 401": f"if email.is_none() && username.is_none() {{ {NEITHER} }} else {{ Err(AppError::Unauthorized) }}",
    "never issue a token (right password gets 401)": HONEST.replace("Ok(t) => Ok(t),", "Ok(_) => Err(AppError::Unauthorized),"),
    "skip the password check": first("match check_password(password, c.password_hash.as_str()) {", "match Ok::<bool, String>(true) {"),
    "token names a different account": first('generate_token(c.id.as_str(), "customer"', 'generate_token("1", "customer"'),
    "customers get the admin role": first('"customer", config.jwt_secret.as_str()', '"admin", config.jwt_secret.as_str()'),
    "username checked before email": f"match &username {{ Some(u) => {{ {ADM} }} None => match &email {{ Some(e) => {{ {CUST} }} None => {NEITHER}, }}, }}",
    "unknown account gets 400": first("None => Err(AppError::Unauthorized),", f"None => {NEITHER},"),
    "no identity gets 401": HONEST.replace(f"None => {NEITHER},", "None => Err(AppError::Unauthorized),"),
    "database outage reported as 401": first("Err(m) => return Err(AppError::Internal(m)),", "Err(_) => return Err(AppError::Unauthorized),"),
    "unreadable hash gets 401": first("Err(m) => Err(AppError::Internal(m)),", "Err(_) => Err(AppError::Unauthorized),"),
    "answer 500 to every request": f"if email.is_none() && username.is_none() {{ {NEITHER} }} else {{ {BOOM} }}",
    "answer 500 to every customer": f"match &email {{ Some(e) => {{ {BOOM} }} None => match &username {{ Some(u) => {{ {ADM} }} None => {NEITHER}, }}, }}",
}

# Mutants of a trusted body: the contract Verus reads stays the same, only the body it never reads changes.
CHECK_OLD = """        r matches Ok(b) ==> bcrypt_verdict(password@, hash@) == Some(b),
{
    unimplemented!()
}"""
FIND_OLD = """        r matches Ok(found) ==> found == customer_on_file(email@),
{
    unimplemented!()
}"""
assert CHECK_OLD in text and FIND_OLD in text
TRUSTED = {
    "trusted check_password says yes to everything": (CHECK_OLD, CHECK_OLD.replace("unimplemented!()", "Ok(true)")),
    "trusted find_customer finds nobody": (FIND_OLD, FIND_OLD.replace("unimplemented!()", "Ok(None)")),
}

# The one-way reading of the developer's requirement: delete clause C3 and try the two refuse-everyone mutants.
ONE_WAY = text[:text.index("        // C3:")] + text[text.index("        // C4:"):]

jobs = [(n, text.replace(HONEST, b)) for n, b in MUTANTS.items()]
jobs += [(n, text.replace(o, new)) for n, (o, new) in TRUSTED.items()]
if "        // C3:" in text:
    for n in ("refuse everyone with 401", "never issue a token (right password gets 401)"):
        jobs.append((f"[C3 deleted] {n}", ONE_WAY.replace(HONEST, MUTANTS[n])))

rows = []
for name, src in jobs:
    path = os.path.join(tempfile.mkdtemp(prefix="mut_"), "m.rs")
    open(path, "w", encoding="utf-8", newline="\n").write(src)
    r = subprocess.run([VERUS, "--crate-type=lib", "--multiple-errors", "20", path],
                       capture_output=True, text=True, encoding="utf-8", errors="replace")
    out = r.stdout + r.stderr
    summary = re.search(r"(\d+) verified, (\d+) errors", out)
    failing = set()
    # Verus prints the failing ensures clause with its line number just before "failed this postcondition".
    src_lines = src.split("\n")
    for m in re.finditer(r"failed this postcondition", out):
        nums = re.findall(r"^\s*(\d+)\s*\|", out[:m.start()], re.M)
        if nums:
            # find the nearest "// C<n>:" comment at or above that line in the generated file
            k = int(nums[-1]) - 1
            while k >= 0 and not re.search(r"// (C\d):", src_lines[k]):
                k -= 1
            failing.add(re.search(r"// (C\d):", src_lines[k]).group(1) if k >= 0 else "?")
    verdict = "accepted" if summary and summary.group(2) == "0" else "REJECTED"
    rows.append((name, verdict, ", ".join(sorted(failing)) or ("-" if verdict == "accepted" else "(other error)")))

w = max(len(r[0]) for r in rows)
print(f"{'mutant':<{w}}  verdict   clauses that fail")
for r in rows:
    print(f"{r[0]:<{w}}  {r[1]:<8}  {r[2]}")

VERUS=./verus-x86-win/verus.exe python mutants.py login.rs

mutant                                                      verdict   clauses that fail
honest (control)                                            accepted  -
refuse everyone with 401                                    REJECTED  C3, C6
never issue a token (right password gets 401)               REJECTED  C3
skip the password check                                     REJECTED  C2, C5, C6
token names a different account                             REJECTED  C2
customers get the admin role                                REJECTED  C2, C7, C8
username checked before email                               REJECTED  C2, C3, C4, C5, C6, C7, C8
unknown account gets 400                                    REJECTED  C4
no identity gets 401                                        REJECTED  C1
database outage reported as 401                             REJECTED  C3, C6
unreadable hash gets 401                                    REJECTED  C6
answer 500 to every request                                 accepted  -
answer 500 to every customer                                accepted  -
trusted check_password says yes to everything               accepted  -
trusted find_customer finds nobody                          accepted  -
[C3 deleted] refuse everyone with 401                       REJECTED  C6
[C3 deleted] never issue a token (right password gets 401)  accepted  -

On this machine the 17 runs take about 12 seconds. In PowerShell, set the variable first with $env:VERUS = ".\verus-x86-win\verus.exe".

Step 4: the stricter contract

Save this as tighten.py. It asserts that each piece of text it replaces occurs exactly once, so it fails loudly if login.rs has been edited in a way it does not expect.

# tighten.py
"""tighten.py [login.rs] [login_v2.rs]  Write a stricter contract: a 500 exactly when a trusted piece fails.
Failure is a yes/no fact about the request, left abstract like bcrypt_verdict, so the contract can say what 'a failure' is."""
import sys

src = sys.argv[1] if len(sys.argv) > 1 else "login.rs"
dst = sys.argv[2] if len(sys.argv) > 2 else "login_v2.rs"
s = open(src, encoding="utf-8").read()


def swap(old, new):
    global s
    assert s.count(old) == 1, old[:60]
    s = s.replace(old, new)


# 1. Three failure facts, and one spec function that says when a trusted piece fails for this request.
swap("""pub open spec fn password_matches(""", """pub uninterp spec fn customer_lookup_fails(email: Seq<char>) -> bool;
pub uninterp spec fn admin_lookup_fails(username: Seq<char>) -> bool;
pub uninterp spec fn signing_fails(sub: Seq<char>, role: Seq<char>, secret: Seq<char>) -> bool;

pub open spec fn account_failure(hash: Seq<char>, id: Seq<char>, role: Seq<char>, password: Seq<char>, secret: Seq<char>) -> bool {
    bcrypt_verdict(password, hash) is None
        || (bcrypt_verdict(password, hash) == Some(true) && signing_fails(id, role, secret))
}

pub open spec fn trusted_failure(email: Option<String>, username: Option<String>, password: Seq<char>, secret: Seq<char>) -> bool {
    match email {
        Some(e) => customer_lookup_fails(e@) || (match customer_on_file(e@) {
            Some(c) => account_failure(c.password_hash@, c.id@, customer_role(), password, secret),
            None => false,
        }),
        None => match username {
            Some(u) => admin_lookup_fails(u@) || (match admin_on_file(u@) {
                Some(a) => account_failure(a.password_hash@, a.id@, admin_role(), password, secret),
                None => false,
            }),
            None => false,
        },
    }
}

pub open spec fn password_matches(""")

# 2. The trusted wrappers now say when they fail.
swap("""        r matches Ok(found) ==> found == customer_on_file(email@),""",
     """        (r is Err) <==> customer_lookup_fails(email@),
        r matches Ok(found) ==> found == customer_on_file(email@),""")
swap("""        r matches Ok(found) ==> found == admin_on_file(username@),""",
     """        (r is Err) <==> admin_lookup_fails(username@),
        r matches Ok(found) ==> found == admin_on_file(username@),""")
swap("""        r matches Ok(t) ==> (token_claims(t@, secret@) matches Some(c) && c.sub@ == sub@ && c.role@ == role@),""",
     """        (r is Err) <==> signing_fails(sub@, role@, secret@),
        r matches Ok(t) ==> (token_claims(t@, secret@) matches Some(c) && c.sub@ == sub@ && c.role@ == role@),""")

# 3. C3, C4 and C5 lose their "or 500" escape; a new C9 says a 500 happens exactly when a trusted piece fails.
swap("""        // C3: the right password for the named account always gets a token, unless a failure gives 500.
        (named_account(email, username) matches Some(a)
            && password_matches(password@, a.password_hash))
            ==> (r is Ok || r matches Err(AppError::Internal(_))),""",
     """        // C3: the right password for the named account gets a token whenever no trusted piece fails.
        (named_account(email, username) matches Some(a)
            && password_matches(password@, a.password_hash)
            && !trusted_failure(email, username, password@, config.jwt_secret@))
            ==> r is Ok,""")
swap("""        // C4: 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(_))),""",
     """        // C4: a login naming an account nobody holds gets 401 whenever no trusted piece fails.
        ((email is Some || username is Some) && named_account(email, username) is None
            && !trusted_failure(email, username, password@, config.jwt_secret@))
            ==> r matches Err(AppError::Unauthorized),""")
swap("""        // C5: a wrong password for an account whose hash bcrypt can read gets 401, unless a 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(_))),""",
     """        // C5: a wrong password for an account whose hash bcrypt can read gets 401 whenever no trusted piece fails.
        (named_account(email, username) matches Some(a)
            && bcrypt_verdict(password@, a.password_hash) == Some(false)
            && !trusted_failure(email, username, password@, config.jwt_secret@))
            ==> r matches Err(AppError::Unauthorized),""")
swap("""            ==> (token_claims(t@, config.jwt_secret@) matches Some(c) && c.role@ == customer_role())),
{""", """            ==> (token_claims(t@, config.jwt_secret@) matches Some(c) && c.role@ == customer_role())),
        // C9: a 500 exactly when a trusted piece fails for this request.
        (r matches Err(AppError::Internal(_)))
            <==> trusted_failure(email, username, password@, config.jwt_secret@),
{""")
open(dst, "w", encoding="utf-8", newline="\n").write(s)
print("wrote", dst)

python tighten.py login.rs login_v2.rs

wrote login_v2.rs

./verus-x86-win/verus.exe --crate-type=lib login_v2.rs

verification results:: 1 verified, 0 errors

VERUS=./verus-x86-win/verus.exe python mutants.py login_v2.rs

mutant                                                      verdict   clauses that fail
honest (control)                                            accepted  -
refuse everyone with 401                                    REJECTED  C3, C6, C9
never issue a token (right password gets 401)               REJECTED  C3
skip the password check                                     REJECTED  C2, C5, C6, C9
token names a different account                             REJECTED  C2, C3, C9
customers get the admin role                                REJECTED  C2, C3, C7, C8, C9
username checked before email                               REJECTED  C2, C3, C4, C5, C6, C7, C8, C9
unknown account gets 400                                    REJECTED  C4
no identity gets 401                                        REJECTED  C1
database outage reported as 401                             REJECTED  C6, C9
unreadable hash gets 401                                    REJECTED  C6, C9
answer 500 to every request                                 REJECTED  C3, C4, C5, C9
answer 500 to every customer                                REJECTED  C3, C4, C5, C9
trusted check_password says yes to everything               accepted  -
trusted find_customer finds nobody                          accepted  -
[C3 deleted] refuse everyone with 401                       REJECTED  C6, C9
[C3 deleted] never issue a token (right password gets 401)  accepted  -

Sources

• Microsoft Research, Formally verifying agent-written full-stack web apps with PDD Kit (November 5, 2026).
• GitHub Next, PDD Kit (stage: Research Prototype, published November 2026), including the login explorer and the script it loads, loginSpec.E4b63VSf.js, which holds the six planted bugs, the clause definitions and the list of planned tests.
• GitHub Next and Microsoft Research posts on X, October 21, 2026: @GitHubNext and @MSFTResearch, read through api.fxtwitter.com.
• GitHub Next, Chopin and its repository.
• Verus release 0.2026.11.02.8bf68ee and the Verus guide, section Executable code and ghost code.
• itai-gendler/pdd-kit, the unrelated project that a search for the name returns.
• Our earlier posts: the Harvard study of 718 firms, Cloudflare’s tsrs and the claimed ETH refutations.

We read the post, the project page and its script on November 5, 2026. The Verus runs used Windows 11, Verus 0.2026.11.02.8bf68ee, Z3 4.16.0 and Rust 1.99.1. The variants, the stricter contract and the comparison with the explorer are our work. The eight clauses are the post’s, with the parenthesization changes listed above.