Why source only, and what that means for proof
Bakakuk never executes the target. That rules some proofs out and makes the rest cheaper and safer. Here is the line between what a cited line can prove and what it cannot.
The rule
The target is never run. No build, no container, no fuzzing, no model-written harness. Bakakuk reads.
That is a deliberate boundary. Running a target means running whatever is in the repository, and running model-written code means trusting a sandbox. Reading needs neither.
What a cited line can prove
- A check that is missing: the comparison that rejects a shorter array but not a longer one.
- A check that is wrong: the comparison done on one normalisation of the input and the action done on another.
- A sink an input reaches: the path from a request field to a shell, a query, a template, a file path, with every transform on the way shown.
- A guarantee a fix added in one place and not in its sibling.
For these, the proof is the cited lines plus a reproduction a human runs by hand: a request, a function call, or a unit test dropped into the repository. The report writes that test out in full.
What it cannot prove
- Races that depend on scheduling.
- Behaviour that depends on runtime configuration the repository does not pin.
- Memory corruption that depends on allocator state.
These are not dropped. They become a Candidate: the mechanism holds on the cited lines, the confidence is calibrated by a final high-effort review, and the report says exactly what a human must check to confirm it.
What it costs
Because nothing is built or run, a scan is network time and model time. The last full scan read 1.2 million lines and cost under a dollar on a laptop-class machine. The cap is set up front, in minutes or in dollars, and the scan stops when it hits it.