After the feedback I received on this quiz from twitter, I added a reset to the design. Since neither Verilog itself, nor the FPGA implementations built with Verilog, have a problem with `initial statements, the “missing reset” wasn’t the reason why the design would never pass a formal check

No, the problem in this design is the assertion,

always @(*)
	assert(counter != 16'd500);

If you run the induction engine with anything less than 500-22 steps, it will just increment the counter from a value the design could never reach up to 500 where the assertion would then fail. This is the reality of induction–when it starts, the registers within your design can have any value that doesn’t violate your assertions or assumptions.

What you need, shown in the answer above, is a more constraining assertion, forcing the counter to stay <= 16'd22. This assertion will now pass, since it doesn’t let the induction engine start in an unreachable state.

This ability of the induction engine to start in the middle of a design, that is to start long after the initial t=0 time step, is both a great advantage and a great curse. It’s an advantage because it allows you to verify designs with extensive timed states within them, such as this SDRAM core that must start with 100uS of idle, in as little as 45 timesteps. It’s a disadvantage because it requires internal assertions–white-box assertions–to force the design into a valid state.