Fast Lane is a traffic racer with one promise attached to it:

Every row of traffic is proved passable before it is dealt.

Meaning a crash is always something you did, never something the road did to you. It sounds like a small claim. It took five wrong versions of the proof before it was true, and the striking thing in hindsight is that the road generator was never the thing at fault. Every failure was in what we were asking it to guarantee, or in the simulation we used to check.

Here they are in the order we hit them, because the order is the lesson.

1. Too strict: the proof and the physics disagreed

The collision check worked in fractional lane position — the car is somewhere between lane 2 and lane 3 while it is changing lanes. The fairness proof reasoned in whole lanes.

Cars are 0.62 lane-widths wide. So a car halfway between two lanes sits 0.5 from each and therefore overlaps both. Every lane change was double jeopardy, and the proof could not see it, because in the proof's world the car was in exactly one lane at a time.

The proof and the physics have to agree in both directions. This is the direction everyone checks.

2. Too generous — and this one hides

The other direction is the dangerous one.

We committed a lane change at laneT >= 0.5, halfway through the tween. That meant a lane change actually took effect in LANE_TIME / 2, while the fairness proof was budgeting a full LANE_TIME for it.

Now look at what that does. It does not break fairness. The car is faster than the proof assumes, so every row the proof certified as passable is still passable, with time to spare. Nothing fails. No test goes red. The claim in the title of the game remains technically true.

What it does is make the game unloseable. Every autopilot we tested drove 22 kilometres without a scratch — including one deliberately written to be terrible, ignoring traffic until it was 10 metres away.

A bug that makes your guarantee more true than intended survives scrutiny, because everything you are checking still passes. The fix was to commit at laneT >= 1 and refuse input mid-tween, so every lane index the proof reasons about is a genuine integer and the step count is exact.

3 and 4. A history-carrying invariant is a guarantee-shaped variable

Twice we built the proof around a "frontier": the set of lanes the player could possibly be in by the time this row arrives, carried forward row to row.

The union version proved that some lane in that set has a gap. Useless — the player is in exactly one lane, not in the union of several. A gap in a lane they cannot be in is not a gap.

The intersection version demanded a gap in every lane the player might be in. That is sound, but it collapses: after a few rows the reachable set spreads to all five lanes, and no single free lane is within two steps of both lane 0 and lane 4. Nothing satisfies it, so nothing is generated.

The tell was in the failure data, and it is worth recognising: every seed died at the same speed. Bad luck scatters. A systematic threshold does not. When your failures cluster that tightly, you are looking at a constraint, not at variance.

The replacement carries no history at all:

For every lane L, some free lane lies within steps of L.

Stronger than the union version, trivially satisfiable unlike the intersection version, and — this is the point — it cannot drift, because there is no accumulated state for it to drift in. An invariant that carries history is a variable wearing a guarantee's clothes.

5. Check the geometry before you blame the logic

Three genuinely correct rewrites of the proof all still failed. We kept looking at the logic.

The problem was two constants. CAR_LEN was 9 and ROW_GAP_MIN was 19. That leaves one metre of clear road between the end of one collision window and the start of the next — 0.016 seconds at top speed. The check was budgeting gap / speed, roughly 0.3 seconds, for the manoeuvre.

Two corrections came out of that. Budget the space between the windows, GAP − 2·CAR_LEN, not the raw gap. And evaluate it at worst-case speed, not at the speed when the row was placed — the car keeps accelerating after placement, so placement-time speed always overestimates how much time the player will have.

Three correct rewrites failed because of arithmetic in the constants. Check the geometry first; it is cheaper than rewriting the logic.

The bonus mistake: an over-active driver proves nothing

To test the guarantee we wrote autopilots. The sophisticated ones repositioned after every row, moving toward a lane that would also suit the row after the next one. They died at 55 metres per second.

The dumb one — hold your lane until a row forces you to move — ran to the speed cap without incident.

Movement is not free. Every optional lane change spends budget that a later forced change needs. A busy driver dying tells you nothing about the road; it tells you the driver was busy. We spent rounds investigating a generator that was never at fault.

So: drive the proof with the least clever strategy the guarantee justifies. And separate the two claims so they can fail independently — Fast Lane has __proveGenerator, which examines the road with no car in it at all, and __proveRun, which puts a driver on it. If both are one function you cannot tell which claim broke.

And the one that nearly ended it before it began

The very first proof run reported a clean pass: 30 seeds, 120 rows each, no failures.

It had not simulated a single metre. step() begins with if (started), and nothing in the harness had started the game. The suite ran, checked its assertions against a stationary car on an empty road, and reported green.

A flag like started turns a proof vacuous without turning it red. It is the same shape as a test that silently skips because no qualifying case appeared — which is a trap we have hit in this codebase before, from a completely different direction. A green suite that examined nothing looks exactly like a green suite that examined everything.

What fair should actually feel like

Proved-fair must not mean unloseable — mistake #2 is exactly what happens when it does. So difficulty gets measured with a reaction-distance ladder: drivers that only look ahead a fixed number of metres.

  • A careless driver reacting at 12 metres: 30 crashes out of 30 seeds
  • An attentive driver reacting at 22 metres: 0 crashes out of 30

That gap is the game. The road is always passable; whether you pass it is about whether you are looking far enough ahead. Which is, more or less, the thing driving is about.

Play it free in your browser, no account, no install: Fast Lane · how to play

More of ours in the same genre: Turbo Rush · Summit Rider · Drift Arena