Yes, making a mistake when writing down the C semantics is definitely possible. The point of the work announced here is to get rid of that risk, so that the pro

Yes, making a mistake when writing down the C semantics is definitely possible. The point of the work announced here is to get rid of that risk, so that the proof only relies on the semantics of the RiscV instructions (and the C semantics become an intermediate thing which are proven rather than trusted). It's still possible that they made a mistake when writing down the RiscV semantics, but machine code is much simpler than C so the risk is smaller.