C and formal verification is an awesome combination. I tried cmbc on some toy programs, it it fully automatically proved memory safety and all assertions. But for larger programs one has to split up with a contract-like facility.

Can you tell us more how you use cbmc with macros? I am also exploring this.

I also wonder what feature from C++ you miss in C?