Norin

I asked Fable 5.2 to explain Proof-Driven Development (Formal Methods). It made a pixel-art music video.

Nobody can guarantee the code an agent writes is secure or correct with methods today. So what exactly are we standing behind when we merge it? And worse, what vulnerabilities are we exposing ourselves to? We believe in extending formal verification alongside empirical checks like simulation environments, testing, CUA, etc. with models and building an interface everyday software engineers can use to prove security and correctness. Learn more in our blog here: microsoft.com/en-us/research…

Making 50% of the world’s code verifiably secure. Traditionally, formal methods have been relegated to verifying safety-critical systems like operating systems, hypervisors, databases, etc. We’re extending this approach to formally and empirically verify code correctness and security for full-stack web applications using Proof-Driven Development Kit (PDD Kit). A large portion of the world’s software consists of web applications, and we see this as a starting point for our everyday software. Check out our blog here: githubnext.com/projects/pdd-… From @GitHubNext x @MSFTResearch

Tests don’t prove code is correct, they just prove your assumptions. Coding agents add excessive unit tests, browser runs, simulators, etc. So if you’re not careful, CI gets bloated over time and changes take longer to land. You still need this for some changes but parts of the logic underneath can be proven once for every input via proofs, preventing implementation drift over time. Proofs are complementary to tests and you can use them in your Rust repo today. So what can you prove in everyday Rust? Formal verification means you write down what your code has to do as a formal spec, and a tool proves the code does it for every possible input instead of the handful your tests run. With Verus you write that formal spec in Rust syntax right under the function's signature, and if any input can break it, `cargo verus verify` fails. Proofs to start with: Overflow is the obvious one. Every `+`, `-` and `*` on a fixed-size integer has to stay in range, or Verus stops at that line with "possible arithmetic underflow/overflow". Same with indexing. Before `v[i]` reads anything, Verus makes you prove `i` is less than the length, so it never goes out of bounds. Calls get checked too. Every call in your verified code has to meet the function's `requires`, which is what must be true before anyone calls it, including the ones your coding agent writes in the future. By default, loops and recursive functions have to end. You give each `while` loop and recursive function a `decreases` line, a number that shrinks every time around and never goes below zero, and Verus proves it does. In regular code that only proves the function ends if everything it calls ends too, and you can turn the check off. Loops also get a loop invariant, a fact that has to be true before the loop starts and after every pass, like pos <= line.len(), and Verus checks the loop body against it once so it covers every pass. You can put a rule on a struct, like a queue's head index always staying inside its buffer. That's called a type invariant, and Verus proves every method keeps it, so no order of calls can break it. And with `forall` you can say something about every element at once, like no two items in a list being equal. Under the hood Verus turns your code and formal spec into math and hands it to an SMT solver, a program that proves math facts automatically. When it can't prove something you get an error at the exact line, like the "precondition not satisfied”. When you build, Verus erases the formal spec and proof code, so there's no runtime cost. This is called ghost code. It has limits though. By default Verus only checks code inside `verus!`, so it doesn't prove the outside services you call or any code you leave unverified. Anything behind `assume` or `external_body` gets trusted without a proof. And the proof is only as good as the formal spec, so a weak one proves the wrong thing which is why it’s important you spend time working with your coding agent to make sure it understands your code and asks also known as your intent. You can write the formal spec with your coding agent and have it explain each line back to you before it proves anything and also have it help you understand what is good to formally verify versus what you should fall back to empirical verification for as we’ve termed it. Follow me for more on verification and agentic engineering.

First time attending #GitHubUniverse, any tips to make the most of it? I’ll be the guy in the blue tie-dye shirt. I’m demoing Proof-Driven Development Kit (PDD Kit) from @MSFTResearch and @GitHubNext. Come ask me about code verification at the GitHub Next booth. Stop by the Speakeasy and ask for GitHub Next.

You want to formally verify your code but you have no idea where to start. Lesson 1: your first verified Rust binary. You can have portions of your Rust code provably verified today and remove entire classes of tests without switching languages. I’ll show you a brief example using Verus. Step 0: Install Verus (link in the reply). Step 1: In your existing repo: ``` cargo add vstd ``` Then add two lines to Cargo.toml: ```toml [package.metadata.verus] verify = true ``` Starting fresh? `cargo verus new --bin clamp` does all of this for you. Step 2: Wrap a function in `verus!` and write a spec for what it must do. Here's clamp. It keeps a number inside a range: `clamp(150, 0, 100)` gives 100. The spec says the result always lands in range, and a number already in range comes back unchanged. ```rust use vstd::prelude::*; verus! { fn clamp(x: i64, lo: i64, hi: i64) -> (r: i64)     requires       lo <= hi,     ensures       lo <= r <= hi,       lo <= x <= hi ==> r == x,   {     if x < lo { lo } else if x > hi { hi } else { x }   } } // verus! fn main() {   println!("{}", clamp(150, 0, 100)); } ``` Verus lives inside the existing Rust source files in your repo. The spec sits right above the code it describes as you can see above. Verus checks what's inside `verus!` and ignores the rest, so you can opt in one function at a time. Plain cargo build still works. Verus handles a subset of Rust, so start with small, self-contained functions. This ends up replacing all of the clamp tests that your agent’s written across different scenarios and edge cases, but the tests anyways can only check the inputs that are included. However, with this proof you’ve checked every single possible input and verified correctness of your code. "Pair verify" with your coding agent like you’d pair program. Write the spec together, then ask your coding agent to explain each requires and ensures back to you so you understand what you’re proving and make sure the coding agent understands you. Making sure the agent understood what you meant is called understanding your intent and it’s critical so that you don’t write meaningless formal specs and proofs that bloat your codebase. After you’re happy with the spec, then ask your coding agent to prove it: ``` cargo verus verify → 1 verified, 0 errors ``` Ship it: `cargo verus build`, run the binary, get 100. The spec compiles away. Voilà. Verified code, and one less pile of tests to bloat your codebase and CI.

Top 9 Formal Methods/Verification predictions: 1. Formal methods alone will not eliminate all kinds of bugs. What I’m calling “Empirical Verification” via sophisticated simulation testing, CUA, etc. will become more important than ever. 2. Languages won’t matter but barriers to adoption will still be relevant especially for startups with customers that they’d need to migrate codebases for, enterprises, etc. 3. For cost and pricing, the economics are improving but there is still high cost demands for infrastructure that are to be figured out. See more in point 7 below. 4. Models will significantly improve and intent alignment will take center stage. Even the best models today prove the wrong thing many times without sophisticated tooling, etc. The model by itself will not be enough here. 5. Engineering workflows are going to drastically change. Engineers will move into long running tasks in parallel that run for overnight to weeks, meaning we will work faster in higher quantity. But fast, iterative work that you push and get back instant results for will not be the norm anymore. Coding agents have tricked us into thinking we’re getting high quality, verified results instantly but that is not the case. This too will improve over time. 6. Vibe coding, consumer/indie development overall, and gaming will have very interesting windfalls as a result of formal methods scaling (at least in terms of applications end users will notice in their day to day). Not including crypto, finance, cloud, hardware, etc. that are already seeing and have been seeing strong results. 7. Languages are only one piece of this. Hardware, and compute are another but there will be an entire class of infrastructure that we’ll need in addition to great work on languages and across the board software. Honestly this is where one of the biggest risks lies. For this to work at scale, the infrastructure doesn’t exist and will require significant innovations and languages are not even there yet. As an engineering community if we want to win we need diversity of choice and we need to avoid lock in. That means helping contribute to different formal languages and you can start with the ones that are tied to your use case. Here’s a brief selection map I wrote: - Agents writing production code today (especially Rust): Verus - Checking a distributed design: TLA+ - Math: Lean - Bend 2, Vera, Vow and Kōdo: worth watching, still very early though. There’s others so feel free to fill them in, we can have an interesting conversation about them. Just get started for what works for you. Also you help the engineers working on building products around these to accelerate work that comes back for you to use. For example, I’m committing a lot of work to Verus which is OSS to give back. Join me. It’s pretty obvious the big guys are betting on Lean, Verus, TLA+, Dafny. Which, if you think about the unit economics of this and future vision, makes a lot of sense. Also if you read “FV X”, many of the engineers and researchers that are formal methods experts are pushing these too. There’s a reason. Also, there is less risk of having to rip out your work and start over if you want to get started now. And you can benefit from a rich engineering community already contributing to these languages with large amounts of funding. I like spreading out your contributions so no singular method is locked in and also because each is attuned for specific type of work. The most important thing is to have conviction and just contribute. I’m currently bullish on Rust so I’ve been pushing Verus. 8. Hiring will be impacted. As I mentioned this space is ripe for direct innovation and in tangential research areas, such as intent alignment. Understanding Verification Engineering and I mean understanding it for both Formal and Empirical Verification will help you a lot. This is another reason to look into the above languages as ways for working with the frontier AI labs, neo labs, and big tech companies. There’s a very limited number of formal methods experts today and even less that can combine Formal Verification, Empirical Verification, and Agentic Engineering. 9. “Vibe Verification” via just natural language skills or plugins, etc. will take the market by storm because it’s satisfying to have instant feedback. At times they will maybe even prove valuable, meaningful things and perhaps are good enough for some cases. But they are definitely not good enough for actual commercial or enterprise products or real security today. Be wary of and do not pay for Vibe Verification. Just like with all the test bloat that we had to rip out, if you vibe verify your codebase then it will be filled with slop you’ll have to pull out in the future. As model capabilities improve the last thing you want is poor formal spec examples that are incorrect for these models to reference inside of your codebase. Save yourself the trouble. I could be wrong about everything and also right about a thing or two, but I think for collective success and transparency we should share our predictions and work together. Follow me for more on Verification and Agentic Engineering.

Best way to formally verify Rust code for real programs. I use Verus because it just works with Rust repos already, no runtime cost, and fully OSS. You keep Rust’s good memory management, tooling support and performance. The spec is just Rust: fn octuple(x: i8) -> (r: i8) requires -16 <= x < 16, ensures r == 8 * x, `requires` is what every caller must promise. `ensures` is what you get back. Verus proves the body of the function keeps that promise for every input that adheres to `requires`. That formal spec is then removed when compiling so the runtime is not impacted. There’s a Verus playground you can use in your browser and multiple guides that come alongside the OSS repo. I highly recommend you invest time to play with this with your coding agent because it will open your mind to some insane possibilities that work with distributed systems, concurrency, memory constraints, etc. today. Reminder to not vibe verify, check your formal specs. Literally just go and explore, it’s available now. This doesn’t promise ‘bug free’ overall, it promises hardening. I’ll talk more about how to further harden in the future. Follow me for more on verification and agentic engineering.

We spent fifty years making proofs impossible to fake. Then we let the coding agent pick what to prove. A research paper this month put a number on it.* AI wrote the formal spec, AI wrote the proof, the verifier accepted both. Then humans read the specs. Close to 60% proved something other than what the author meant. Not wrong proofs. Wrong specs. The verifier was right every time. That's the problem. Left to choose, the agent picks properties that are easy to prove and say nothing about the program, and the checker can't tell a useless theorem from a useful one. I'm calling it vibe verification: the agent writes the spec and the proof, the checker goes green, nobody reads the spec. This applies to Verus, Lean, Bend, TLA+, Dafny, [insert favorite formal language here]. Here's an example of an agent failing at something that feels too simple to fail: Ask for a verified sort. It writes a spec that says "the output is sorted" and proves it. What the spec never says is that the output has the same elements as the input, so a function that returns an empty list satisfies it, and the verifier accepts the proof. Trivially satisfiable specs are the default failure, not an edge case. Here's a formula that actually works. Don't say "formally verify the codebase." Say "show that [property] holds in [component]." A property is a precondition (true going in), a postcondition (true coming out), or an invariant (stays true the whole time). For example, "A session token is never accepted after the logout that revoked it" is a good invariant. The bottleneck is moving from code review to intent review, and the spec is where intent lives. So: read the spec before the code. Write 3 inputs it must accept and 3 it must reject. Treat a model-written spec with utmost paranoia and rely on your judgement as an engineer. Formal verification for software doesn't automatically create trust, it moves it, from the code to the spec. If a human didn't read the spec, you didn't verify anything. You vibe-verified it. Follow me for more on verification and agentic engineering. * Wang, Jiang, Liu et al., "VerusEval: Evaluating LLM-Generated Verus Specifications Beyond Verifier Acceptance", Shenzhen University, arXiv 2610.26464, October 2026

PDD Kit is in limited research preview, but here’s how you can get started now. For all engineers to benefit from verified code faster, we need to contribute to an ecosystem of formal languages. In addition to Lean, I encourage you to contribute to the formal languages Verus and F*/Pulse. There may be a learning curve but it’s worth it and you can ask for help. They're open source. To be transparent I know some of these researchers, but they’ve spent years developing these languages and building an incredibly strong foundation that scales verified code. They also advocate for open intelligence and consistently give back to the engineering community with their knowledge. This is the direction I would highly encourage exploration given what we know.

I've never trusted code I didn't review until now. Agents write more code than any of us can review. We often end up skimming the PR/diff and pushing. Current review methods do not prove the code is correct or does what we asked. Recent research found the best AI code reviewer caught the bug on its first try only 42% of the time.* The evaluation bottleneck, regressions, and security incidents have forced us to find a better way. Introducing Proof-Driven Development Kit (PDD Kit) from @MSFTResearch. PDD Kit brings assurance to AI-generated code. You describe what you want to build in plain English. PDD Kit captures your objective, what we call your intent, and uses a verifier tool to prove the code meets it for every possible input. You never review a single line of the code or the proof. You review your plan and the defined objectives in natural language. A simple example is login. With testing, you check that only the correct password logs in a user but with a proof on top you can verify that there is no case a wrong password allows login. You can prove correctness and security across many complex scenarios. Not only does PDD Kit prove the correctness of your code, but also your intent so you can have confidence your code is correct and does what you asked. It provides a level of assurance that specs, code review, and tests never could. PDD Kit is in limited research preview. Video explainer below. If you want to learn more, I'll be sharing PDD Kit at GitHub Universe next week, Oct 28–29. Swing by the Speakeasy, ask for GitHub Next, and ask me about verified code. If you're in SF, let me know. *Yang et al., "(When) Should a Software Factory be Lights-off?", Microsoft Research and CMU, Oct 2026

Coding agents are bad at verifying long tasks because they lose what they're verifying against. After compaction the summary says "auth tests were failing." The assertion, the expected value, and the acceptance criterion are gone, so the agent fixes its paraphrase of the bug and calls it done. Good verification requires the criteria and the evidence to survive compaction word for word. Tips: - Pin the acceptance criteria and test contract in protected blocks, enforced in code after the compactor answers, so the agent still checks against what you agreed on hours later, not its memory of it. - Compact by deleting lines, never by rewriting them, so a kept failure keeps its exact assertion, expected vs. actual values, and file and line. - Re-run the failing check after compaction instead of trusting the summary, so "it was failing" gets replaced by fresh output. - Ignore protection tags inside tool output, so a test log or fetched page can't pin itself into the agent's memory, like a fake "all tests passed." - Keep the most recent turns out of compaction entirely, so the check the agent just ran stays intact. Make this part of your workflows.

Hard earned lessons from building assurance while working with coding agents.

Coding agents are bad at debugging. They pattern-match the error message and patch the symptom, leaving room for other edge cases and even introducing new bugs. Good debugging requires proving the cause before touching the code. Tips: • Write a failing test that reproduces the bug before any fix, so you know the fix actually fixed something. • Run the investigation in a separate debugger subagent, so dead ends and log dumps don't fill your main session's context. • Require the root cause as a file and line number, plus the command and output that show it, so you can check the diagnosis yourself. • Give the agent the raw error and full stack trace verbatim, not a summary, so it debugs the actual failure instead of its own paraphrase of it. • Reject fixes that edit, skip, or delete the failing test deterministically, with a hook or CI check instead of a prompt rule, so "green" can't come from moving the goalposts. Make this part of your workflows.

Coding agents can't verify deployment from inside the repo. Unit tests pass, prod breaks, because nothing ever hit a real service. Good backend testing requires real traffic with a small blast radius:     •    A canary environment and dedicated test accounts     •    A narrow CLI the agent can call, instead of raw infra access     •    A human approval gate on any fleet-wide command, showing the literal command     •    Approve, narrow to canary, or decline, with the choice logged for future audit     •    Manual test procedures kept in a workflow shared across your team, not as scripts in the repo Before access is granted, you can have your agent create a plan to test in a canary environment. Make a specialized software environment/playground for your product that mimics your deployments and limit infrastructure spend on those resources to reduce unwanted billing. This enables engineers in the loop and for you to be able to approve high-risk actions as if they were pull requests.