When trying to get kani to work one often has to do small changes to a file. Kani recompiles all crates all over again even when only one file changed. Including proc macros, so if there's some technical reason why the code can't be reused for conversion to CBMC at least proc macros should be reusable.