> doesn't mean when the algorithm gets actually implemented in C, it still maps to TLA+ as proven.

So true, but you know what would be amazing and useful? A TLA+ spec transpiler that emits fuzzing code. That would probably be easier to make than TLA+ spec transpiler that emits C.