> there is an abundance of other theorem provers that can model C very closely

Can you list some/all of them please? Would be helpful to others here.