[wy1981]

Great find and writeup.

As an aside, this is the type of a problem that I think model checkers can't help with. You can write perfect and complicated TLA+/Lean/FizzBee models and even if somehow these models can generate code for you from your correct models you can still run into bugs like these due to platform/compiler/language issues. But, thankfully, such bugs are rare.

[jraph]

Yep. Model checking is for checking that your design is sound, basically, not at all the implementation.

For the implementation, you can use certified compilers like CompCert [1], but:

- you still have to show your code is correct

- there are still parts of CompCert that are not certified

[1] https://compcert.org/