Check out the tooling from the seL4 project. I'm aware they used intermediate levels between raw C and the proof assistant, but I don't see why that should be p

Check out the tooling from the seL4 project. I'm aware they used intermediate levels between raw C and the proof assistant, but I don't see why that should be prohibitive.