The compiler that hands you the murder weapon

An AI writes most of the code now. So I taught the compiler to do the one thing an AI is worst at — decide whether that code is actually correct — by making it an adversary that hands back the exact input that breaks it.

An AI coding agent's failure mode isn't the syntax error. It's the plausible-but-wrong function: the one that type-checks, reads correctly, passes the happy-path test, and quietly divides by zero when the list is empty. Agents are excellent at writing code that looks right. They are bad — structurally bad — at knowing whether it is right. That's a judgment call, and judgment is exactly what a language model doesn't have.

So don't ask it for judgment. Ask the compiler. I built a feature into machin — the machine-first language I'm building at intrane.fr — that turns the compiler into an adversary. It doesn't lint your code and print a paragraph. It tries to break it, and when it succeeds, it hands you the exact input that does it, plus a program that reproduces it. I call it the Falsifier.

A counterexample beats a lecture

Here's a function an agent might write to sum a list. It has a classic off-by-one:

func sumbad(xs) {
    total := 0
    i := 0
    for i <= len(xs) {          // <= should be <
        total = total + xs[i]
        i = i + 1
    }
    return total
}

It compiles. It runs. On most inputs it even returns the right answer. Run machin falsify on it and you don't get a warning about loop bounds — you get this:

[FALS001] index out of range at `xs[i]` when xs=[]int{}

The exact input. xs=[]int{} — the empty list. The agent doesn't need to reason about why; it needs the case that fails, and iterating on a concrete failing input is the one thing LLMs are genuinely good at. The loop closes mechanically: write → the compiler falsifies → fix → and the counterexample becomes a --repro file — a runnable program that panics at exactly that line, an auto-promotable regression test.

This isn't a toy demo. Pointed at machin's own example programs, the Falsifier immediately found two real latent bugs nobody had noticed: a divmod that divides by zero, and a minmax that indexes xs[0] on an empty slice. Genuine unchecked preconditions, sitting in the repo, surfaced in milliseconds.

Then I let you state your intent

Index-out-of-range and divide-by-zero are bugs the language defines. But the interesting bugs are the ones you define — the postcondition that's supposed to hold and doesn't. So the Falsifier learned design-by-contract. You put declarative clauses on the signature:

func div(a, b) requires b != 0 {
    return a / b
}

func clamp(x, lo, hi) (r)
    requires lo <= hi
    ensures  r >= lo
    ensures  r <= hi {
    ...
}

requires is a precondition: it filters the input domain. An input that violates it is the caller's fault, not a bug here — so requires b != 0 makes the divide-by-zero complaint disappear, because the compiler now knows b == 0 was never yours to handle. ensures is a postcondition over the return value; an input that satisfies every requires but makes an ensures false is a counterexample to your own stated intent. The compiler hunts for the input where your function lies about what it does.

The hard part was teaching it to be honest

A bug-finder that cries wolf is worse than useless — an agent that learns to ignore it is back where it started. So the Falsifier has three honesty rules, and I care about them more than any feature.

It never fails your build. Findings are advisory. The Falsifier is unsound-complete: it finds bugs, it does not prove their absence, so it must never reject a correct program just because it couldn't rule a bug out. It reports; it never gates.

It never cries wolf. A counterexample is reported only when the compiler evaluated a fully-modeled, concrete path all the way to the failure. The instant it touches something it can't model — an opaque call, an unsupported construct — that input is marked inconclusive and silently dropped. It would rather stay quiet than lie. Every finding it reports is a real bug, and the repro proves it.

It never claims a proof it can't back. This is the one most tools get wrong. By default the Falsifier samples inputs — fast, good at finding bugs, but a clean result means only “no bug in the sample”, and it says exactly that. It never prints the word proved it hasn't earned.

And then — carefully — I let it prove things

Once the honesty was airtight, I could add the opposite of falsification. Run machin falsify --prove and it stops sampling and instead enumerates a dense, fully-covered bounded space — every integer in a range, every small list, every combination of booleans and struct fields — and checks the property against all of them. It's a bounded model check by brute exhaustion. No SMT solver, no symbolic engine; just the honest observation that if you try every input in a finite space and none fails, you've proved something.

And it's precise about what. A function over booleans has a finite input space, so --prove enumerates the whole thing and reports proved — an unconditional, total proof. A function over integers can only be exhausted up to a bound, so it reports proved-bounded, always labelled with the exact bound: “no counterexample for any int in [-8, 8].” Never “correct.” And if any input touches a path it can't fully evaluate, or an infinite domain it can't cover, it refuses to say proved at all. It will under-claim before it over-claims, every time.

A nice side effect: dense enumeration is a better bug-finder than sampling. A divide-by-zero that only triggers at x == 7 sails right past a sample of small values — and --prove catches it every time.

The compiler proves its own compiler

All of this — the counterexample search, the contracts, the bounded proofs — is a pass inside the machin compiler. And the machin compiler is written in machin and compiles itself. So the Falsifier is itself written in the machine-first language, and I verified the port the only way that counts: every finding and every verdict from the self-hosted Falsifier is checked byte-for-byte against the reference implementation, across the whole test corpus. machin-in-machin doesn't just compile itself — it falsifies and proves, provably identically.

Why a machine-first language can afford this

Here's the part I keep coming back to. Bounded verification isn't new — model checkers have done it for decades. So why doesn't your language ship it? Because its users are humans, and humans hate the honest output. “Unknown at bound k=8” is a useless sentence to a person. A three-way proved / counterexample / inconclusive verdict feels like the tool weaseling. So mainstream languages bury verification in research tools nobody runs in CI.

But machin's users are agents. An agent loves “inconclusive at bound 8” — it's information, it's actionable, it consumes it as JSON and moves on. It doesn't feel insulted by a counterexample; it feels handed the fix. The exact honesty that makes bounded verification unpalatable to humans is what makes it perfect for machines. This is the same bet as inferring data-race freedom without Send/Sync: designing a language for machines instead of humans doesn't mean less rigor — it means you can finally afford more, because the friction that made rigor unpalatable was always a human tax.

The agent writes the plausible-but-wrong function. The compiler hands back the murder weapon. The agent fixes it and commits the repro. No judgment required from the thing that has none — and, when the space is small enough, a real proof at the end of it.

machin is open source at github.com/javimosch/machin. It’s built by Javier Arancibia — the same engineering that goes into intrane.fr.