Comment by hashxyz

I don’t see how the distinction makes any sense when the Verus project you linked requires you to write correctness specs. It sounded like intrinsic techniques were preferred because they would not require you to write and maintain a separate spec, but this is not the case.