There is a way. You have to meticulously prove operations down to machine code to not have externally observable side effects.
You can weaken the condition by excluding, say, timing effects or cacheline effects. (Say hello to Spectre)
This means you get to prove bounded access and data race freedom on any piece of memory safe code touches. Likewise prove bounded access for all unsafe code and correct cpu flag and state handling.
It it's not as bad as it seems - you can use the machine code prover designed for seL4 as a good starting point.
You can weaken the condition by excluding, say, timing effects or cacheline effects. (Say hello to Spectre)
This means you get to prove bounded access and data race freedom on any piece of memory safe code touches. Likewise prove bounded access for all unsafe code and correct cpu flag and state handling.
It it's not as bad as it seems - you can use the machine code prover designed for seL4 as a good starting point.