Practical guide
Track where untrusted values gain authority
A value can be well-formed and still come from someone who must not control a decision. Taint analysis follows influence from an untrusted source toward a sensitive use.
Sources, sinks and sanitizers need concrete meanings
A source is where untrusted data enters; a sink is where its use matters. A sanitizer is an operation that establishes the property needed at that sink. CodeQL documentation distinguishes value-preserving data flow from taint tracking, which can follow derived values as well. A string transformation is not automatically a sanitizer for every use.
Illustrative example: a client-supplied price
Client event: {product_id: "A", quantity: 2, unit_price: 1}
Sensitive use: charge = quantity * unit_price
Trust problem: the client chose the price
The JSON can be valid and the multiplication correct while the transaction violates the pricing rule. A stronger design obtains the authoritative price from a server-controlled catalog and validates the quantity. Sanitizing string syntax or renaming unit_price to validated_price does not establish price authority.
Proof's trust check has a narrower surface
trusted_outputs_from_untrusted_inputs analyzes active FRETish requirements in safety or configured financial scope. It looks for direct client-trusted variable influence through antecedents or declared dependencies into output behavior, without a referenced configured sanitizer. Financial tags and sanitizer names are project policy. This is a requirement-model review signal, not general source-level taint analysis.
proof audit --check trusted_outputs_from_untrusted_inputs --verbose
Its current scope is direct dependencies. It does not infer arbitrary transitive source-code dataflow across a program. An unmodeled path can therefore remain outside this check even when the actual code carries untrusted influence.
Review the alleged trust boundary
Locate the real input, transformation and sensitive operation. Decide whether a server-side recomputation, validation, attestation or explicit risk acceptance supplies the needed guarantee. A sanitizer declaration records a claim that still needs implementation evidence. Test both a valid case and an attacker-controlled value that would change the outcome if the boundary were absent.
Use the right evidence for each path
Combine requirement-level trust declarations with appropriate source analysis and executed tests. A clean model check does not establish that every code path was examined, and a static path finding does not by itself prove an exploitable execution. Retain the concrete path and its assumptions so a reviewer can decide what is actually supported.
Follow the evidence
Find one money- or safety-relevant value and identify who can actually choose it.
Review one trust boundary. Bring the input path and sensitive use so we can assess who controls the value and what implementation evidence supports the claimed validation.