And I suspect that cross section of people writing C code you want to verify with formal verification folks is not particularly big.

Perhaps not, but C is still used in a lot of critical systems. Things like this for proving properties of some core of your program can be very helpful.