Not really. Cbmc is really cool but it doesn't lead to the kind of high level proof refinement that lets you say things like "this low level code correctly impl

Not really. Cbmc is really cool but it doesn't lead to the kind of high level proof refinement that lets you say things like "this low level code correctly implements the paxos protocol". Cmbc is -useful- and lets you check some important safety properties and it's a great tool. But it's not the state of the art in terms of how extensively you can check things with formal verification. It's closer to the state of the art of what you can do with legacy code. Things like VeRus let you write annotated rust together with proofs that can show higher-level properties such as liveness, mutual exclusion, etc.