Engineers ignore your analyzer because undecidability forces it to approximate, so which structural changes buy back precision, and at what cost?

## Why tuning does not help The first instinct when a gate is ignored is to tune it: more analysis time, more context, a better model. Precision does improve that way, and it is worth doing, but it has a ceiling that no budget passes. Whether a program's behaviour has a given nontrivial property has no exact procedure at all, so every version of the tool is approximating, and every version has the same two failure modes available to it. If the team's complaint is 'it is sometimes wrong', no amount of tuning answers the complaint. What answers it is changing what the tool is asked. ## Four escapes, each with a bill 1. **Restrict what may be written.** Define a subset for the component that matters: no dispatch to targets the analysis cannot enumerate, no code loaded at runtime, no unbounded loops in the section under proof. Inside that subset the question can become genuinely decidable, and the tool becomes exact. The bill is expressiveness and a migration, plus the long-term cost of a second dialect that new joiners must learn and that library code will not respect. 2. **Ask the author.** Annotations, contracts, invariants and ownership markings supply the fact the tool could not derive. The analysis stops guessing and starts checking consistency, which is a local, decidable job. The bill is per-site effort, drift as code changes, and a boundary problem: at the edge with unannotated code you are back where you started, and the honest design decides in advance whether the tool *verifies* an annotation or merely *believes* it. 3. **Bound the exploration.** Analyse up to a fixed number of loop unrollings, call depth or steps. Inside the bound the answer is exact and the findings are real. The bill is silence beyond the bound, and the temptation to report that silence as a proof of absence, which it is not. 4. **Change the property.** Replace the behavioural rule with a structural proxy that is exact and conservative — a rule about the shape of the code rather than about what it does. The bill is that the proxy rejects safe code that happens to match the shape, and misses unsafe code that does not. ## Matching a check's authority to its error direction | Check's error direction | What a finding means | Appropriate authority | |---|---|---| | Only speaks with a proof | the finding is real by construction | may block a merge | | Speaks when it cannot rule out | the finding is a hypothesis | advisory, with a review path | | Bounded search, exhibits an input | real, but coverage is limited | may block, but proves nothing on silence | Most failed rollouts get this wrong in one specific way: they put hypotheses behind a blocking gate. The team cannot ship until it disposes of each one, disposal is faster than investigation, and within a quarter the suppression list is the real policy and nobody reads it. The direction of a check should decide its authority, and that decision belongs in the check's own definition rather than in a global severity setting. ## The organisational read Every one of the four escapes spends something an engineer owns: their freedom to write what they like, their time writing assertions, or the coverage they thought they were getting. That makes this a language-and-process decision rather than a tooling purchase, and it is why it lands with a lead. The useful framing in a planning discussion is: *which of these are we willing to pay, on which code?* Almost nobody can pay the language restriction across a whole codebase, and almost everybody can pay it on the small surface that handles money, credentials or data loss. The same is true of annotations. Scoping the escape to the code whose failures actually hurt is the move; applying it uniformly is what makes it fail. ## What to measure - The **survival rate** of each check's findings — what fraction lead to a change. A check whose findings never survive is not a precision problem, it is a check to retire. - The **size and age of the suppression list**, per check. Growth is the leading indicator that a hypothesis is wearing a proof's authority. - The **annotated fraction** of the surfaces you claim to have covered, because a partially annotated boundary gives a guarantee that does not hold. - The **escape-hatch usage** in the restricted subset, which tells you whether the restriction is real or ceremonial. ## The claim to never make Do not promise exactness at the end of the roadmap. You can promise a narrower language on the critical surface, findings that carry proofs, a bounded search that exhibits real inputs, and a suppression path with a name attached. The exact answer to a nontrivial behavioural question is not a thing any budget buys, and a plan that implies otherwise loses credibility on the first counterexample an engineer produces.