Proven, unproven, not checked: three honest answers

Every finding a scanner reports is a claim about your code. Some claims come with evidence: the scanner followed a value from the request, through two helpers, into a SQL string, and can show every step. Others are a pattern that looked suspicious. Others are questions the scanner raised but could not answer from the source at all.

Most scan output presents all three the same way: a rule, a line and a severity. The reader has to work out which kind each row is, usually by opening the file and tracing the code by hand. Multiply that by a few hundred rows and it becomes the reason teams stop reading the results.

Vulkro gives every finding one of three labels instead. Proven, unproven or not checked. This post explains what each one means, what changed in how they drive severity, and why an empty proof never means the code is safe.

Why the label matters

The cost of a false positive is not the minute it takes to dismiss one row. It is trust. In a 2013 ICSE study, Johnson, Song, Murphy-Hill and Bowdidge interviewed 20 developers about why they did or did not use static analysis. All of them saw value in it, yet false positives and the way warnings were presented came up as barriers to use.

The engineers who built static analysis at Google reached the same conclusion from operating it at scale. In "Lessons from Building Static Analysis Tools at Google" (Communications of the ACM, 2018), Sadowski and colleagues define an "effective false positive" as an issue developers took no positive action on, whatever the tool's own view of it. Checks shown in code review had to stay under 10% effective false positives. They also describe an earlier code-review integration that was discontinued in part because effective false positives made developers lose confidence in the tool.

OWASP's page on source code analysis tools lists "High numbers of false positives" among the weaknesses of the category, next to another one that is the heart of this post: it is difficult to "prove" that an identified issue is an actual vulnerability.

So the useful question is not only "is this a real bug?" It is "how much should I believe this row before I open the file?" A label answers that.

The three answers

Every Vulkro finding carries a disposition. On the command line and in JSON they are named admitted, demoted and not-examined. In the console and the docs they read as proven, unproven and not checked.

Proven. The finding is backed by something a machine can check: a traced data flow from source to sink, a verified secret, a matched dependency advisory, or a decisive code shape such as a non-literal format string. This is the tier we stand behind.

Unproven. The pattern matched, but the scanner could not establish the path. Perhaps the value passed through a library it cannot see into, or the query is built in a helper whose inputs it could not resolve. These are real leads, not proof. They are reported, not hidden.

Not checked (not-examined). The finding belongs to a class that source analysis cannot decide offline. Object-level and function-level authorization are the main example: whether a lookup by id is safe depends on a permission class, a global interceptor or a security configuration that may live somewhere the rule did not read. The scanner flags the shape and says plainly that it did not decide it.

What it looks like in code

A proven finding, in Flask:

@app.route("/users")
def users():
    name = request.args["name"]
    cur.execute("SELECT * FROM users WHERE name = '%s'" % name)
    return jsonify(cur.fetchall())

The value goes from request.args straight into the query string in one handler. The trace has two hops and both are visible. That is proof. The fix is a bound parameter:

@app.route("/users")
def users():
    name = request.args["name"]
    cur.execute("SELECT * FROM users WHERE name = %s", (name,))
    return jsonify(cur.fetchall())

An unproven finding looks like this:

@app.route("/report")
def report():
    cur.execute(build_report_query(request.args))
    return jsonify(cur.fetchall())

If build_report_query comes from a package the scanner cannot analyse, there is a raw execute on something derived from the request, and no way to show what happens in between. It may be safe. It may not. The honest answer is "unproven", and a human should look.

A not-checked finding is the classic object lookup:

class InvoiceDetail(APIView):
    def get(self, request, pk):
        return Response(InvoiceSerializer(Invoice.objects.get(pk=pk)).data)

Nothing in these lines ties the invoice to the caller. Whether something elsewhere does (a permission_classes default in settings, a queryset filter in a base class) is not decidable from this view alone, and the finding says so.

What changed in severity

Labels are only useful if they change what you see first. Two releases made that happen.

Earlier, Critical was reserved for findings backed by a proven data flow: a finding that only matched a name or a shape stopped claiming Critical.

Since 0.29.0, the rule is stronger. A Critical or High finding keeps that severity only when it is backed by proof. Unproven rows are still reported, at Medium. The top of the list is therefore made of findings you can act on without re-deriving them, and the rest stay one level down instead of disappearing.

Some practical consequences:

• The summary line shows the full breakdown: how many findings were found, how many are proven, how many unproven and how many not checked.
• vulkro scan --disposition admitted (or demoted, or not-examined) narrows the table to one tier. It is a display filter only. It does not change which findings exist, the exit code or the JSON and SARIF output, where every finding already carries its disposition.
• Findings whose disposition is not-examined never fail a --fail-on gate, at any severity. They stay in the report, and a warning says how many were withheld from the gate.
• --all-confidence shows everything, including low-confidence rows that are hidden from the default view.
• The console leads the findings view with the same breakdown, with one-click filtering to each group.

An empty proof never means safe

The MCP server that AI coding agents use has a prove tool. Given a finding, it returns the hop-by-hop proof chain behind it. When the chain comes back empty, the meaning is precise: no proven data flow was found. It does not mean the code is safe, and the tool description says so in those words, because an agent reading the result needs to be told as clearly as a person does.

The same rule applies to vulkro verify, which checks another tool's SARIF results against Vulkro's own analysis and marks each one proven, not provable (with the reason) or not checked. "Not provable" is a statement about what Vulkro could establish, not a verdict that the other tool was wrong.

Treating "could not prove" as "safe" is how real bugs get closed as false positives. Treating it as "unproven" keeps them in view at a severity that matches what is known.

Why not just drop the unproven rows?

Because a scanner that only reports what it can prove misses real bugs, and some of the most damaging classes (broken access control in particular) are the hardest to prove from source. Dropping them would make the output look cleaner and the application less safe.

The trade we chose is ordering, not deletion. Proof earns the top of the list. Everything else stays reported, labelled with how much we know. If you want the strictest view for a CI gate, filter on the disposition. If you want everything for a review, use --all-confidence.

This is one of three things we try to keep honest, alongside what a scan actually read and who can reach the code. For the opposite question, why nothing was reported at a line, see why did the scanner not flag this.

Where to see it

Run vulkro scan and read the summary line, then try --disposition admitted. The confidence model explains how confidence and disposition differ, the MCP server docs cover prove and verify_sarif, and the taint analysis page explains how a data flow becomes proof. To get set up, start here.