A repeatable LLM workflow for finding logic bugs that compilers miss

Every time I ask a model "is there a bug in this file?" I get a confident paragraph back, and no way to tell whether it is right. So I switched to a stricter loop on my own code: the model only proposes concrete findings, and a deterministic tool — compiler warnings, a sanitizer, an assertion — proves or disproves each one. Keeping those two roles apart is the whole trick.

I ran it end to end on a 15-line C file. It took me about 45–60 minutes at an intermediate level, and the bug it surfaced compiles with zero warnings.

What you need before you start

• Linux, macOS, or Windows 11 with WSL2.
• Python 3.10 or newer — python3 --version should print 3.10+.
• Access to an LLM, through a web chat or an API. Model names, limits and pricing move fast, so read your provider's docs before copying any endpoint from a blog post (this one included).
• A C compiler if you want to follow the demo literally: sudo apt install build-essential on Ubuntu, xcode-select --install on macOS.
• A scratch directory such as ~/verify-demo, plus roughly 100 MB of free disk space.

Step 1: Get a baseline from tools that never hallucinate

Start from a file with a deliberate logic bug. The point is not the bug itself — it is knowing exactly what your existing toolchain already catches, because everything it misses is the target for the model.

mkdir -p ~/verify-demo && cd ~/verify-demo
cat > discount.c <<'EOF'
#include <stdio.h>
#include <stdbool.h>

int final_price(int price, bool is_vip, int coupon_pct) {
    int discount = 0;
    if (is_vip) discount += 15;
    discount += coupon_pct;          // bug: nothing caps the combined discount
    return price - price * discount / 100;
}

int main(void) {
    printf("%d\n", final_price(1000, true, 90));
    return 0;
}
EOF
gcc -Wall -Wextra -fsanitize=undefined,address -o discount discount.c && ./discount

The build stays silent: no warnings, no sanitizer reports. The run prints -50. That is the bug — 15% VIP plus a 90% coupon makes 105%, so a price of 1000 turns negative. Sanitizers watch for undefined behavior, not for "a percentage discount should never exceed 100", which is precisely the kind of property the next step is for.

If you see -50 and no warning lines, your baseline is set.

Step 2: Ask for a list, not a review

Free-form feedback is useless here, because there is nothing to check. Save this as prompt.txt and put the format rules after the code you paste in — that ordering matters when the file is long.

You are a formal-verification assistant. Review the code below.
For EACH issue, output exactly:
- ID (L1, L2, ...)
- line number
- class: overflow / boundary / off-by-one / invariant violation / unreachable / other
- severity: high / medium / low
- one line explaining which property is violated
Skip style comments. If a function is correct, say "no issues".
Code:
<paste discount.c here>

An ID, a line number, a class and a severity turn every remark into a checkable claim. That is the difference between a review and a verification workflow: formal verification means proving a property like "the returned price stays between 0 and the input price", and the model's real value is guessing which properties your code breaks.

A web chat works fine for this. If you prefer the API, drop the prompt into a small Python caller:

import os, sys, urllib.request

code = open("discount.c").read()
prompt = open("prompt.txt").read().replace("<paste discount.c here>", code)
body = os.environ["LLM_REQUEST_JSON_TEMPLATE"].replace("{PROMPT}", prompt.replace("\\", "\\\\").replace('"', '\\"'))
req = urllib.request.Request(
    os.environ["LLM_API_URL"],               # your provider's endpoint, see its docs
    data=body.encode(),
    headers={"Content-Type": "application/json",
             "Authorization": "Bearer " + os.environ["LLM_API_KEY"]},
)
print(urllib.request.urlopen(req).read().decode())

A good answer looks like a table of claims, one per line:

L1 | line 7 | invariant violation | high | combined discount can pass 100, so the result goes negative

What you are checking here: at least one finding of class boundary or invariant violation, aimed at the discount += coupon_pct; line, marked high. If you get a paragraph of prose instead, send the prompt again — the model ignored the format block.

If you also want a fix, ask for it in a second message ("rewrite final_price so the total discount is capped at 100 and the result is never negative") and keep it as a separate diff. Never let the model quietly rewrite the whole file.

Step 3: Convert each finding into an executable check

This is the step that separates this workflow from vibes-based code review. Take finding L1, write the violated property as an assertion, and run it:

cat > check.c <<'EOF'
#include <assert.h>
#include <stdbool.h>

int final_price_fixed(int price, bool is_vip, int coupon_pct) {
    int discount = (is_vip ? 15 : 0) + coupon_pct;
    if (discount > 100) discount = 100;
    int result = price - price * discount / 100;
    assert(result >= 0 && result <= price);   // the property the LLM claims is broken
    return result;
}

int main(void) {
    assert(final_price_fixed(1000, true, 90) == 100);
    assert(final_price_fixed(1000, false, 0) == 1000);
    assert(final_price_fixed(0, true, 0) == 0);
    return 0;
}
EOF
gcc -Wall -Wextra -o check check.c && ./check && echo "ALL PROPERTIES HOLD"

Success looks like the single line ALL PROPERTIES HOLD, with echo $? printing 0. If the property still fails, the assertion aborts and tells you the file, line and expression that broke — for example check: check.c:9: final_price_fixed: Assertion 'result >= 0 && result <= price' failed. At that point the finding was real but the fix was wrong, and you know it in one run rather than one code review meeting.

Then repeat the loop — model proposes, you encode the property, a test confirms — for every finding in the list. Small files usually settle in two or three rounds.

Two failure modes I keep hitting

The answer is prose, not a list. Typically the model received the code after a long conversation, or the format block got truncated. Start a fresh chat, put the format rules after the code, and state that the reply must begin with L1 | or with no issues. Check the first line and you immediately know if it worked.

The model reports a bug that does not exist. A classic: it flags "integer overflow in price * discount" while your inputs are tiny and ./check passes. The model is reasoning about every possible input, not about yours. Don't argue with it — narrow the claim: reply that inputs are guaranteed to satisfy 0 <= price <= 10000 and 0 <= coupon_pct <= 100, then ask which findings survive under those bounds. Most of them evaporate, and the ones that stay are usually worth an assertion.

What I take away

• A compiler and a sanitizer tell you what is impossible; a model tells you what is plausible. You need both, in that order.
• The structured output format is not bureaucracy. Without IDs and line numbers there is nothing to verify, and the exercise collapses back into reading suggestions.
• The assertion is where the value lands. An LLM finding is a hypothesis until a test run confirms it — and the assertion stays in your codebase long after the chat is closed.

This article was originally published on AI Release — https://ai-release.org. If walkthroughs like this one are useful to you, the channel at https://t.me/ai_release1 posts them as they come out.