[seL4] Optimizations?

Easier to keep the generator simple and let the compiler do the optimisations it already understands.

Based on things like the experiences of Tahoe LAFS with compiler optimizations vs. security - let alone plain bugs - I am scared if anybody uses any optimizations at all, especially for serious business. I have not researched the position se4L takes on this. Are the proofs about the before-optimization code, or do they consider the after-optimization assembly output?

thanks.