A real run shows you one path. To ask about all of them, you first need to say what would count as wrong on any of them.
Invariant
Something that must always be true, at every moment, whatever happens: a balance never goes below zero, a refunded order never ships, the shares always add up to the bill. It is a plain sentence first and code second.
You can say an invariant without reading the code, which makes it the part of the job you can do and an agent can't guess. It is also what every check from here up needs: a tool can try every order of events only if something says which outcomes are wrong.
“Write three invariants for refunds in docs/invariants.md, in plain English first: total refunded never exceeds the amount paid, a refunded order never moves to shipped, and every refund row points at a real payment. Add a fast-check property for each, and show each one failing on a copy you have broken on purpose.”