Proof, Not Promises

AI is making bugs cheap to find. Confidence built on effort and track record won’t survive it.

Browse the websites of companies selling industrial software to OEMs, and the claims about robustness and code quality start to sound familiar. Paraphrased:

“Developed to rigorous coding standards.”

“Industry proven. Deployed worldwide.”

“Peer reviewed for robustness and reliability.”

Wonderful. What can you prove about your code?

None of these claims answer that. Coding standards and peer review describe effort. Testing and years in the field are sampling: they show that nobody has found a problem in the inputs tried so far. Only a proof covers every input, and nothing on that list is one.

That was good enough for decades, and rigor had little to do with it. Finding bugs took rare expertise and months of work, so attackers spent that effort where the return was highest. Sampling was enough. Your code only had to be harder to break than the next target.

AI is taking that cost away. When looking is cheap, every target gets looked at. Being harder than the next one stops protecting you, and “nobody has found a problem yet” ceases to mean anything.

This post is also about our own code. We used AI to audit our protocol libraries and found a remotely triggerable panic we’d shipped for more than five years. We fixed more than the bug, because patching bugs piecemeal was always a losing strategy. AI has made it undeniable.

The Economic Shift

In Anthropic’s Firefox audit, Claude found a use-after-free in twenty minutes. Someone still has to understand it, review a fix, test it, ship a release, and get that release onto deployed devices. In industrial systems, re-certification and field-maintenance windows can stretch that process into months or years.

Now let the model find another twenty.

Defenders can run the same tools. AI helps write the patches too. But each one still needs review, testing, and deployment, and a model can’t shorten a utility’s maintenance window. As discovery gets cheaper, the bottleneck moves to getting fixes into service.

Then why not run the latest models before you ship? Do, if you can. In our experience, the most capable consumer models now refuse to hunt for vulnerabilities, even in your own code. Vendors reserve that for verified-access programs, and not every company or open-source project can get in. Even with access, a pre-release audit is still sampling, with today’s model. At some point you have to ship, and what you ship stays fixed while the tools keep improving. A clean report is only as good as the model that produced it, and that model won’t be the best one for long.

The Reports Keep Coming

The public issue trackers of C and C++ libraries that parse network input show what this looks like for maintainers.

The tables compare public reports of memory-related bugs this year with the average over the previous five years. Each year covers the same dates: January 1 through October 23.

Industrial communication libraries

Widely used libraries

Counted by keywords in issue titles using GitHub’s issue search on October 23, 2026. These are reports filed in public, so projects that handle security reports privately receive more than they show here. We left out libexpat and tcpdump, which take none publicly.

In the widely used libraries, more people are finding bugs: OpenSSL heard from 25 different reporters this year, Mosquitto from 11. In the industrial stacks, the jump came from a handful of people, and that is the more unsettling number. One account filed 27 of the 50 reports across these five stacks this year, in five different projects.

It no longer takes a research team to sweep an industry’s open-source protocol stacks. It takes one person with a model.

The industrial stacks jumped hardest, and that fits who has been looking. curl and OpenSSL have paid maintainers, funded external audits (curl alone had three by 2024), years of free continuous fuzzing and enormous scrutiny. Most industrial protocol stacks have had far less, so when finding bugs got cheap, there was more left to find.

Maintainers are coping as best they can. OpENer received 15 reports this year after at most one a year before, mostly remote out-of-bounds reads and buffer overflows in its request parsing, and every one is still open. bacnet-stack received 10 and has closed every one, which is what heroic maintenance looks like, and it is still a treadmill: each fix closes one bug and leaves the class in place for the next report. That is not a criticism of any of these maintainers, many of whom have done this work in public for a decade or more. It is what the economics above predict: reports now arrive faster than most can fix them.

Many maintainers are overwhelmed. In June 2026, curl and uriparser announced pauses in vulnerability reporting; libexpat said it would not accept reports until August:

If you are throwing AI or fuzzing or security research at libexpat these days please hit the pause button.

The libexpat maintainers, issue #1277

And hiding the source doesn’t help. Open-source code drowns first because it is legible, not because it is worse. Closed firmware can be obtained from update packages, field tools, and flash dumps, and a bug in a shipped binary is there whether anyone can read the source or not. Obscurity only ever meant nobody has paid the discovery cost yet, and that cost is exactly what AI collapses. Models now drive decompilers like Ghidra and IDA directly. Source code is no longer a prerequisite for this kind of analysis.

From Slop to Surgical

Not long ago, AI bug reports were mostly noise. Through late 2025 and into early 2026, maintainers got a steady stream of reports like this composite, with the names filed off:

## 🔍 Executive Summary (of a bug report)

Here's the thing: a remote, unauthenticated attacker can trigger a heap
out-of-bounds read in `parse_widget()` with a single crafted frame. This is
not a theoretical concern. It is a real, reachable, and robust primitive.

## 🧠 Root Cause

The load-bearing assumption is that `len` was validated upstream. It wasn't.
Crucially, the parser and the getter disagree about the same bytes, and
that disagreement is doing a lot of heavy lifting and it's worth being
honest about why.

## 💥 Inflated Impact

- Remote denial of service (crash)
- Potential information disclosure
- Plausibly, full compromise of the electric grid

## ⚖️ CVSS Self-Assessment

10.0 (Critical). Possibly 11.

## 🔁 Reproduction (Validated, Trust Me)

1. Build with `-fsanitize=address`
2. Run the bundled example server
3. `python3 poc.py --target 127.0.0.1`

Now picture opening your issue tracker on a Monday to six of those, and having to disprove each one: a function that doesn’t exist, a length checked two lines up, a proof of concept that only crashes the reporter’s own harness. In 2025, curl’s maintainers were among the loudest critics of these reports. They cost hours and fixed little.

Then the reports got good. This month, curl’s Daniel Stenberg wrote:

Since spring 2026 the slop reports are practically gone.

Ignoring real vulnerabilities because they were found by AI does not make users safe and secure.

Daniel Stenberg, “ignore the slop”

Today’s reports are short and surgical: the function, the missing check, an input that reaches it, and a sanitizer trace that reproduces on the first try. No grid compromise, no CVSS 11.

The noise is gone. The bugs are real, and now they're yours to fix.

Sampling Is Not Proof

Many of these projects weren’t short on testing. libiec61850, open62541 and Mosquitto are all in OSS-Fuzz, Google’s continuous fuzzing service, and their reports jumped anyway.

Fuzzing is sampling too: it tries some fraction of the possible inputs and reports the bugs it hits. So are unit tests and property tests, and so is an AI audit, which explores the code differently and finds bugs that fuzzing missed. Sampling is valuable: it found the bugs in the tables above, and it found ours. But none of it is exhaustive, so a clean run never proves that no bugs remain.

A proof holds for every possible input, not just the ones someone tried. That sounds exotic, but most programmers rely on proofs every day. A type checker proves that every call passes and returns the types it promised. If that doesn’t sound like much, you haven’t shipped enough JavaScript. Rust’s compiler proves that safe code is memory-safe: no use-after-free, no double free, no data races, no out-of-bounds read or write. A lint can prove that a function is never called, or that nothing in a crate calls unwrap. These differ in scope, not in kind.

The difference shows up when code changes. Break a proven property and the build fails immediately. Break code that is only sampled, and you may never know.

None of this is an argument against fuzzing. Keep fuzzing, keep your tests, and run the audits. But sampling alone is no longer sufficient. When anyone can sample your code, what sets you apart is what you can prove.

Being the maintainer of a critical open-source C or C++ project is the least enviable job in software right now.

Not because you are doing anything wrong, but because the language gives you so little to prove things with. The compiler proves almost nothing about memory, and the proof tools that do exist for C take specialist effort that doesn’t scale to everyday development. So you sample, you fix, and you wait for the next report.

Our Turn

We build DNP3 and Modbus libraries in Rust, and everything above applies to us too. So we ran these tools on our own code.

In October 2026, through Anthropic’s Cyber Verification Program, we pointed Mythos 5.1 at the core of our DNP3 library, about 34,000 lines of Rust excluding tests, and asked what a hostile peer could do with arbitrary bytes. We did the same for rodbus, our Modbus library.

It found no memory-safety bugs in either library. The language held up its end.

In rodbus, it found no panics either. In DNP3, it found a way to crash the outstation with a single request. To see how, you need to know about a small paradox in the DNP3 standard.

A Paradox in the Standard

DNP3 operates breakers and other outputs with a two-step select-before-operate: the master sends a SELECT naming the controls, the outstation answers, and the master then sends an OPERATE with the same controls. Three parts of the standard collide here.

1. The response must echo the request. SELECT and OPERATE responses must return the same objects in the same order.

2. The response is two bytes bigger. Its header includes two status bytes that the request doesn’t have.

3. 2048 bytes is the common limit. The standard guarantees that masters can accept responses this large. In practice, devices, including our library’s defaults, use 2048 bytes for both receiving and sending.

Put them together. A master sends a 2047- or 2048-byte control request, which the outstation can receive. The standard requires an echo, and the echo is 2049 or 2050 bytes, too big to send.

The standard requires an echo. The buffer requires arithmetic. They disagree by two bytes.

The standard doesn’t say what to do with a request you can never answer. There is only one correct response: refuse it before doing anything else. Nothing operates, and the master gets an error instead of an echo.

A Corner Case Deferred for Five Years

Our first implementation of controls, in December 2020, punted on this case. When an OPERATE had no matching SELECT, the outstation handled the request, threw away the error, and sent the master whatever part of the echo fit:

let _ = controls.respond_with_status(&mut cursor, CommandStatus::NoSelect);

We knew it wasn’t right. It was one of those cases you mean to come back to: the truncated echo broke the standard, but no real master fills a request to the brim with controls, and anyone who can send controls can already operate the breakers. So we moved on, and never came back.

Two months later, a conformance fix needed the response-building code to return a status. The expedient change was to unwrap the write result. That was safe where an OPERATE matched a SELECT: the same objects had already fit in the SELECT’s echo. But the let _ = didn’t say why it was there. Nothing in the code said the error was reachable, so the change went into the two branches without a matching SELECT as well:

- let _ = controls.respond_with_status(&mut cursor, status);
+ controls.respond_with_status(&mut cursor, status).unwrap();

The shortcut we meant to revisit had become a remote panic.

From then on, any master could send an OPERATE without a matching SELECT, sized so its echo didn’t fit, and the outstation panicked. It needed one request, in the default configuration. Nobody went back to it for more than five years. Every release before 1.8.0 is affected, and 1.8.0 fixes it. The advisory has the details.

It survived five years of field use, our unit tests, the DNP3 conformance test procedures we run in CI, and our own fuzzing. None of them sent a request of exactly the wrong size. It did not survive one AI audit.

The fuzzing deserves a closer look. Our coverage-guided fuzzing targeted the parsers, and this isn’t a parser bug: the request parses fine, and the panic comes later, while building the response. A coverage-guided harness around the whole outstation would still struggle. The input has to be a valid OPERATE with no SELECT before it, carry about 2,000 bytes of well-formed controls with every object count matching its contents, and land within two bytes of the maximum fragment size. Coverage guidance doesn’t help: a 2,040-byte OPERATE covers the same code as a 2,048-byte one until the final write, so nothing rewards a fuzzer for growing the request toward the edge. Aegis, our generational fuzzer, drives the whole outstation and builds valid requests by design, but none of its test cases filled a control request to the brim. It does now.

An AI audit comes at it from the other direction: start at the unwrap, ask when the write can fail, and work back to the arithmetic. A fuzzer searches forward from inputs. This bug was easier to find by reasoning backward from the code.

In a memory-safe language, a panic like this is a denial of service, not code execution, a far better worst case than the C bugs above. You might object that an attacker who can send controls can already operate the breakers, so a crash adds nothing. You’d be right about that attacker. But in OT, availability comes first. NIST’s guide to OT security puts safety and keeping the process running ahead of the confidentiality and integrity that IT puts first, and its summary of the difference is blunt: “even momentary downtime may be unacceptable.” An outstation that stops answering is the failure that matters, whoever sent the request that crashed it. We disclosed it as a vulnerability.

That is why we treat secure software and reliable software as one goal. A proof that the parser can’t panic holds for every input, whether it came from an attacker, a buggy master or a test tool pointed at the wrong port.

Eliminate the Class

The obvious response is to fix that unwrap, ship a patch, and move on. That is how the software industry has always dealt with bugs, one at a time, and most vendors would have stopped there. One more bucket over the side. It loses for the reason in the first section. This model found one reachable unwrap, and the models just keep improving.

And finding a bug doesn’t make the fix simple. Sometimes the problem is baked into the architecture, and fixing it means disturbing code that otherwise works. Congratulations: the model found one bug, and your patch is an opportunity to introduce three more.

So we fixed the bug. The outstation now refuses any control request whose echo won’t fit, before it executes anything. Nothing operates, and the response carries no objects and IIN2.2 (parameter error), the standard’s own signal for a request it can’t process:

if !Self::control_response_fits(sol, &controls) {
    return sol.empty(parameter_error(seq));
}

We could have stopped there. Instead, we made the whole class impossible to write in both of our libraries. We did it in three layers. Each one is a proof; they differ in what they cover.

Layer 1: Memory Safety

This one we already had. Both libraries’ core crates forbid unsafe code, and the compiler enforces it. That rules out out-of-bounds writes, use-after-free, and the rest of the memory-corruption class in our code. It does not rule out panics: an out-of-bounds index in safe Rust is caught by a runtime check and becomes a panic. Rust turns remote code execution into denial of service. It doesn’t make the denial of service go away.

Layer 2: Banned Patterns

Each library’s root module bans common sources of panics and silent misbehavior. CI fails on any violation anywhere in the crate, so a passing build proves none of them are there, apart from the exceptions below. An excerpt from the DNP3 library:

#![deny(
    clippy::unwrap_used,
    clippy::let_underscore_untyped,
    clippy::indexing_slicing,
    clippy::arithmetic_side_effects,
    // ...and 26 more
)]

An exception needs a narrow #[expect] with a stated reason, and our policy permits one only where no input can trigger the failure:

#[expect(
    clippy::indexing_slicing,
    reason = "a u8 index is always within the 256-entry table"
)]

With these lints in place, both shortcuts would have failed CI, one for the silent let _ = and one for the unwrap. We could still have deferred the corner case, but we would have had to document why we were ignoring the error. The next developer would have seen an unfinished decision. Replacing it with a crash would have required a separate justification for why the error could never happen.

Most banned patterns have a non-panicking counterpart in Rust’s standard library, and the lint forces you to pick one. Take integer overflow. There is no single right answer:

let seq = seq.wrapping_add(1);        // a sequence number wraps
let count = count.saturating_add(1);  // a counter stops at its maximum
let end = start.checked_add(len)      // an untrusted length is an error
    .ok_or(Error::Overflow)?;

Plain addition does make a decision, silently, and a different one depending on the build. By default it panics in debug builds and wraps in release, and one profile setting makes it panic in release too. The named methods behave the same in every build. They look pedantic, even a little alien, but they say exactly what the code does and remove the footgun entirely. Indexing works the same way: the code has to say what happens when an index is out of range.

The compiler can insist on an answer. It can’t insist on a good one. We could still write code that operates the controls without sending a response. That still takes engineering judgment and review.

Layer 3: No-Panic Proofs

Layer 2 is also a prerequisite for this one. A no-panic proof passes only if the optimizer can remove every path to a panic. Sometimes it can, such as an unwrap on a value it can see, or an index right after a bounds check. But a proof that rests on that is fragile. Refactor the caller, change what gets inlined, or upgrade the compiler, and the optimizer may stop seeing what it saw before. Then correct code fails the check. And it never sees through a value that only exists at run time. Banning the panicking forms outright is the path of least resistance, and it makes the proof sturdier, because it leaves the optimizer far less to prove. Lints only cover our own code, though. They can’t see panics inside the standard library or a dependency, such as a slice method that panics on a bad length. So for the code that decodes bytes received from the network, we prove the absence of panics at link time.

The technique is no-panic. Each function on the decode path carries an attribute that is active only in the proof build:

#[cfg_attr(all(test, dnp3_no_panic), no_panic::no_panic)]
pub(crate) fn parse(options: ParseOptions, fragment: &'a [u8]) -> Result<Self, HeaderParseError>

In that build, each such function is compiled so that a panic escaping it leaves a reference to a symbol that doesn’t exist, and the optimizer removes that reference only if it proves that no path to a panic exists. A test harness feeds the functions input read at run time, so the optimizer can’t specialize them for known values. It hands every result to std::hint::black_box, which keeps the optimizer from deleting a call as dead code and taking its panics with it. If the test binary links, those functions cannot panic, for any input. If it doesn’t, the linker names the function that can. The check fails closed: it never certifies a function that can panic.

The proofs cover the DNP3 link, transport, and application layers: decoding, the encoders, and the outstation’s READ and unsolicited responses. Each check also covers everything the function calls, including the standard library.

This isn’t a toy parser chosen because it was easy to prove. The DNP3 application parser alone is about 4,300 lines of decoding code. It handles variable-length data, packed bits, multiple numeric formats, and timestamps whose meaning depends on earlier data in the same message. We checked the checker: in each DNP3 layer, we planted panics that only specific input could reach, and each one failed the link.

We know what happens when implementations get this wrong. In 2013, Chris Sistrunk and I fuzzed DNP3 implementations in Project Robus. The resulting advisory list runs to 32 entries. Parsing this protocol safely has never been a trivial problem.

The parser is zero-copy and zero-allocation: it borrows the fragment buffer and decodes values as the caller pulls them. The no-panic proof enforces the second half for free. Every heap allocation has a failure path, and whether that path panics or aborts is decided at link time, so the optimizer must keep it. Code that passes the check can’t allocate. Other pull parsers can use the same design: checked lengths, fallible reads, and views into the input. The protocol can be complicated without making every parsing step difficult to verify.

The bug the audit found wasn’t in the code that is now proven to be panic-free. It was in the outstation’s handling of a request the parser had already decoded, which is outside the proof even today. That is the case for layers rather than any single tool: the proof covers the code that touches raw bytes, and the lints do the best they can with the rest of it. Neither alone would have been enough.

What It Cost

Before the hardening, today’s lints would have flagged 192 panic-capable sites across the two libraries:

Each one needed a decision about what to do instead of panicking. AI agents wrote most of the changes; a second model and I reviewed each one. It was still work. AI made it a lot less work.

The proof only works on code the optimizer can follow. Our parser was already in the right shape: a non-allocating pull parser over borrowed bytes, so proving it didn’t take a rewrite. The outstation’s READ path was harder. It walks its point database with BTreeMap::range, whose iterator relies on an unwrap guarded by the tree’s own invariants. No input can reach it, but the optimizer can’t reliably prove that, so we excluded the walk rather than give up the map’s fast seek. Once BTreeMap’s cursor API is stable, we expect to close that gap. More broadly, we expect the standard library to become friendlier to proofs like this one. A Rust Foundation-backed effort to verify it is underway, and BTreeMap’s internals are on its list.

The guarantee applies to one build: release mode, link-time optimization, a pinned compiler, and the default unwinding panics that the check relies on. Remove the optimization or upgrade the compiler, and unchanged code can fail the check. CI catches that. Debug builds have extra overflow checks, which is another reason we ban unchecked arithmetic.

The DNP3 and Modbus security pages list what is covered, what isn’t, and how to run the checks yourself.

What We Can’t Prove Yet

We also found ways for a peer to waste our servers’ time. Open a connection and never finish the handshake. Stop reading. Sit there. Neither library handled all of this as well as it could have.

In different ways, these connections could hold a server or a client longer than they should. We fixed or bounded the worst of them in DNP3 1.8.0 and rodbus 1.6.0, and each library’s Security page lists the limits that remain. But they were found the old way, by a sampler, because “a session can’t be starved” and “a server always gets back to accepting connections” are properties about time and liveness, and the tools we use today don’t prove them.

We haven’t eliminated every kind of bug. We’ve eliminated specific classes, and the job is to keep expanding that list.

The Work Gets Cheaper

AI also changes what it costs to obtain these guarantees, and that is the other side of the squeeze. The first side made going without them more expensive. This one makes them cheaper to get.

Our hardening showed it. AI agents wrote most of the changes to our 192 sites, and they did well because every requirement was one a checker could verify. Ask a model to “make this code safer” and you get its opinion. Deny unwrap and require the no-panic check to link, and you give it a target, and the checker tells it, and you, whether it hit it. Knowing what to ask for is the hard part.

You might expect AI to favor languages with fewer rules to satisfy. In April, before Mythos and before the reports above, I’d used that spring’s consumer models to find auth bypasses in our own backend, and wrote:

When finding an auth bypass drops from a six-figure pentest to one AI session, compile-time guarantees stop being a developer experience preference and start becoming a security control.

Six months later, the strongest evidence comes from the companies building the models. OpenAI rewrote its Codex CLI in Rust, GitHub ported the Copilot runtime from TypeScript to Rust using Copilot, and Bun, the runtime Claude Code ships on, was rewritten from Zig to Rust, mostly by Claude, in eleven days. Bun’s team put it plainly: “Compiler errors are a better feedback loop than a style guide.” When a model does the work of satisfying the rules, the rules become a bargain.

AI makes stronger guarantees cheaper to obtain and more expensive to do without.

Where to Focus

Many teams sit on a large, working C or C++ codebase they can’t discard. They don’t have to. Start with the code an attacker gets to feed: network messages, uploaded files, firmware updates. A two-thousand-line parser on a network port is a better first target than a million lines of internal computation, and it can be replaced behind the same interface. Firefox’s Oxidation effort did exactly that, one component at a time, its MP4 metadata parser among them.

We did the same within Rust. We didn’t prove the whole stack panic-free. We proved the code that touches raw bytes, put lints over the rest, and will keep pushing the proven boundary inward as the tools allow.

What the Job Becomes

A better model can find a bug your last audit missed. It can’t find an out-of-bounds write where the language rules it out, or trigger a panic on a path you’ve established cannot panic. Those guarantees keep their value as the tools improve.

The next model is coming, and it may help us prove much more than the absence of panics. While I was finishing this post, Anthropic and Theorem turned OSS-Fuzz harnesses into specifications and had AI prove them: 239 entry points across 123 libraries, libexpat among them, each proven never to crash on any input under 64 MB. The harnesses that sampled inputs became statements about all of them.

Mathematicians are catching up to us on one front and ahead of us on the next. The disruption reached software first, and plenty of engineers have been saying “welcome to the club.” But they are already living with the consequence we are about to meet: proof checkers now verify AI-written proofs that experts are, in one account, “still working to digest.” Engineers have it easier in one way and harder in another. Easier, because we don’t always want to follow the proof. Our job is intractable without trusting abstractions. Nobody reads the borrow checker’s reasoning; they trust that a program that compiles is memory-safe. We understand our no-panic check the same way, at the level of the idea, dead code elimination, and trust the optimizer with the details. Harder, because a proof is only as useful as the property it proves. Someone has to choose properties worth having, judge whether a tool can plausibly establish them, and read what it actually established.

A proof of the wrong property is just a promise with better paperwork. Our own bug shows why. The code we wrote in 2020 never panicked: it sent a truncated echo, and a no-panic proof would have certified it. The property that mattered, refusing a request you can’t answer before acting on it, took someone who knew the protocol to state. As AI writes more of the proofs, that becomes the job: deciding what has to be true, and under what assumptions.

Dave Kiss recently gave a eulogy for the software engineer, casket and all. He buried the headphones, the notebook and the keyboard: the flow state, the hand-drawn design, the code you typed yourself. The grief is real, and so is the loss. Then he opened the lid back up. What survives, he argued, is the part where “you write down what done looks like before anything gets built.” Write it precisely enough, and a machine can now prove it. I’ll miss parts of the old job. But we’re about to be able to prove things we never could, and I can’t wait to see what we ask for.