The most dangerous bug is not a crash. It is a failed or denied state that renders as a normal, reassuring value: 0 errors, $0 owed, access granted. A crash tells you something is wrong. A safe-looking value tells you everything is fine while it is not, so nobody looks. Call that gap trust debt, and treat it as a reachability property: is there a path where a non-OK state reaches a render that shows a valid value? If there is, you can prove it.
There is a lot of talk lately about the difference between software that works and software you can trust. Most of it is about product polish, and that is fair. But the sharpest, most dangerous version of the gap is not a confusing dashboard. It is a single value: the screen states a fact, and the fact is fiction. The read failed, the check was skipped, the state was unknown, and none of that reached the surface. What reached the surface was a clean number.
In July our own scanner printed a line we will not forget: this scan cost $38.2223 · balance now $0.0000. To the person reading it, their entire account balance had just evaporated into one scan. It had not. No money was lost. The ledger had billed the scan correctly, in fractions of a cent, and the real balance was untouched at $38.19 the whole time.
The end-of-scan line is just balance_before minus balance_after. The client fetched the after-balance, ignored the HTTP status code, and the helper that reads the JSON returns 0.0 when a field is missing. So the instant that read returned a 401, the after-balance parsed to zero, and the line rendered balance now $0.0000 with a cost equal to the entire prior balance. The before-read had already been guarded to return a sentinel on a non-200; only the after-read had not. One unguarded read, and a failed request wore the costume of a real, alarming number.
The fix was not cleverer math. It was to fail loud: on a non-200, the client now prints "could not read your balance back, your scan was billed normally, run redmirror balance" instead of inventing a figure. The tell-tale we wrote down for the class: if a reported cost is exactly the prior balance, it is not a cost, it is X minus 0. The server is the source of truth about money; the client is only a renderer, and a renderer must never turn a failed read into a confident fact.
A crash is a signal. It stops the line, it shows up in the logs, it makes someone look. A failed state that renders as a normal value is the absence of a signal: it says "fine" and everyone moves on. Our case pointed in the alarming direction, which is actually the lucky one, because alarming gets reported. The deadly direction is reassuring. 0 vulnerabilities found when the scan errored out. no PII detected when the detector threw. access: denied to the attacker that was actually allowed. These read as good news, and good news gets believed and shipped. This is failing open, and it is exactly the failure mode you least want in code that guards money, access, or safety.
It is almost always a default for the missing case that happens to be a valid, benign value. The exceptional path and the happy path quietly converge on the same output:
0 for an absent or malformed field.try/catch that swallows the error and returns an empty list or null.|| 0, a ?? false, an optional chain that collapses undefined into a clean default.Each is one line that looks tidy and defensive. Each lets an error, a timeout, or a denial arrive at the screen indistinguishable from a real, successful result. AI-written code is especially prone to it, because "return a sensible default" is the most probable, most agreeable-looking thing to generate, and the model has no way to know that 0 and "we could not find out" are different claims.
The reason this is our territory: every instance of it reduces to one sentence about a state the system should never present. A value is shown as fact only when the state that produced it was OK. Unavailable is never rendered as zero. Denied is never rendered as allowed. Once the rule is written as an invariant, catching the bug is a search over the reachable states, not a matter of taste.
invariant: shown_balance_reflects_a_successful_read (render only when status == OK) REFUTED 1. <init> after_read.status = 401 // key revoked mid-scan 2. parse missing "balance" balance_after = 0.0 // default for an absent field 3. render end-of-scan line "balance now $0.0000" // a failed read shown as a real number
Either a path like that exists in your code or it does not. If it does, RedMirror hands it back as a sequence you can rerun; if it does not, you get a bounded proof there is no such path. You cannot eyeball your way to "no failed read ever reaches a render as a valid value," but you can prove it.
The engineering rule is old and simple: fail closed, not open, and never let "unknown" share a representation with a real value. Distinguish 0 from "we do not know." Guard every read by its status before you use the result. Make the exceptional path render an exceptional value, loudly. And then, because these bugs are invisible by construction, prove there is no path where the exceptional and the normal collapse into the same output. That last step is what RedMirror does: it runs inside your coding agent, on your machine, and turns "this looks fine" into a proof that it is, or a path showing it is not.
The honest scope, as always: this catches reachable correctness, fail-safe, and state bugs, the kind that render clean and pass every test. It is not a secrets scanner or a dependency checker; pair it with those. But the class in this post, the broken state that shows a safe value, is exactly the kind of thing you cannot see and can prove, and that is the whole reason to prove it.
A crash is a signal: it tells you something went wrong and stops you from trusting the result. A failed state that renders as a normal value is silence: it tells you everything is fine when it is not, so nobody investigates. The reassuring direction is the dangerous one, because 0 errors or access granted reads as good news and gets believed.
A default for the missing or failed case that happens to be a valid, benign value. A parse that returns 0 for an absent field, a catch that returns an empty list, a null that collapses to false, a read that ignores its status code. The default is the bug: it lets an error, a timeout, or a denial arrive at the screen wearing the costume of a real, successful answer.
The gap between what your product shows and what actually happened. Unavailable rendered as zero, denied rendered as allowed, error rendered as success. It is quieter than technical debt because nothing looks broken, and in software that handles money, access, or safety it can hurt you before technical debt does.
State the rule as an invariant, for example a value is only shown as fact when the state that produced it was OK, then search the reachable states for a path where a failed or denied state reaches that render. RedMirror returns a concrete, replayable path or a bounded proof there is none. It is the model proposing where the rule should hold and a compiled kernel proving or refuting it.
RedMirror runs inside your coding agent and proves whether a failed or denied state can reach the screen as a valid value, with a replayable path or a bounded proof there is none. Start with anything that renders money, access, or a security result.
Get RedMirror Read: the invisible authorization bugs