I was experimenting with approaches and techniques to find miscompilation errors. Not crashes – those are the easy ones. This time — the Ethereum ecosystem. Every codebase there has been audited to death; bug-hunting is desperate, and each find I made was complicated.
So I tried a similar approach on TON, with the latest Tolk compiler. Just for fun. It took about 30 minutes to vibecode a ~500-line script based on hands-on experience. A deterministic and boring script. Only SMT and Python. No LLM in the loop.
Results are interesting. Two hours running. A few ICEs. A couple of real arithmetic miscompiles users can hit. But the best find — the ghost of a 20-year-old JDK bug, alive in the Tolk codebase.
Just look at this example:
const RANGE_LO: int = 1000000000000000;
const RANGE_HI: int = 3000000000000000;
const MID: int = (RANGE_LO + RANGE_HI) >> 1;
// Intended identity: MID > (MID - a) iff a > 0
fun isPositive(a: int): bool {
return MID > (MID - a);
}
Math says
isPositive(-1) == false. Tolk says true. The optimizer cancels MID from the rhs subtraction but forgets the lhs, so the test silently becomes MID > -a:isPositive() PROC:<{ // a
MID PUSHINT
SWAP
NEGATE // -a
GREATER // MID > -a (NOT MID > MID - a)
...
}>FunC compiles the same source correctly with
SUB in place: check it here.(low + high) >> 1 is exactly the midpoint idiom — Bloch's canonical "safe" replacement for JDK-6412541. Twenty years later, the same pattern lives on in a smart-contract compiler.Maybe that's an easter egg as a tribute to a famous bug. But I would prefer boring and well-audited tech with security guarantees over marketing. The compiler isn't bad, just young. Pick the stack that keeps "dudes with Python scripts" out of your threat model.
