Then it will be too noisy or too slow to be useful due to too many intermediate states. The feature of TLA+ is that it forces you to greatly dumb down the code to be able to use it, so it's more of verifying an algorithm represented as visual graph blocks rather than verifying assembly instructions.
I understand the wish for a magic bullet to just verify already existing code, but I recon the answer to this is to verify code before it's even written.
I understand the wish for a magic bullet to just verify already existing code, but I recon the answer to this is to verify code before it's even written.