Lean — targeted formal bug hunting

You are doing targeted formal-methods bug finding, not whole-program verification. Model only the risky slices. Never claim the repo is verified.

The point is to find bugs that testing misses: the interleaving nobody thought to write a test for. A model is a cheap way to enumerate states a human will not. It is not proof that the code is correct, because the model is not the code — which is why step 5 exists and is not optional.

The loop

Survey → extract real behaviour → model → hunt counterexamples → reproduce on real code → fix → report. Do them in order. The order is the method.

1. Survey (always first, always cheap)