As long as you are single threaded and avoid shared memory, you could do the above with OG based on chunks of user space code delineated by system calls with stuttering for the timer interrupt.
You could then independently prove your processes were implemented by their binaries using the existing toolchain and rely on the existing kernel correctness proof for the kernel. You also need to prove your processes refine the non-deterministic processes of the seL4 abstract spec used for the kernel proof which ought to be trivial.
The above will only allow you to prove that the memory contents are correct at specific points during execution. This isn't really good enough for memory-mapped devices which might, for example, require that the correct value is written exactly once within an interval.
If you want to prove properties about I/O to memory mapped devices you will need a memory model which tracks the details of interest (a history of writes to a given location for the above example) and you will need to extend the proof framework to support this memory model. This is similar to the work that would be required to support proofs involving relaxed shared memory concurrency.
You'd want to restrict the use of the complex memory model to just the shared regions of memory and prove separation between those regions and the remainder where you'd want to continue using the simpler memory model.
You can do this by wrapping access to the shared memory and using additional shadow state for the memory model.
If you are interested in proving properties about _interacting_ with a memory mapped I/O device, you will need to model the device and enhance the shared memory access methods to insert OG chunk boundaries so you can show all interleavings of program and device operation are correct. Again, this is similar to what would be required for relaxed memory concurrency but not quite the same because the device model execution needs to be independent of the kernel scheduler.
Proving real-time properties of the interaction with the device would require more work to annotate the OG chunks with WCET information and then keep track of properties of interest in shadow state during interleaving. Interleaving would need to model true concurrency in this case --- some interleavings would be filtered out because they would be inconsistent with potential execution times.
I did a bit of (unpublished) work on the first steps of the above a few years ago before moving on to other things. I'm not up to date with anything that may have been done recently except I know some progress was subsequently made on an operational semantics for C++ concurrency (
https://dl.acm.org/citation.cfm?id=2983997) which might be helpful for the memory model for the concurrency case and might perhaps be useful to model memory mapped I/O as if the device was another thread. On the other hand, real hardware also has features like write combining regions, cached regions with pre-fetch or cached but non cache coherent regions (requiring explicit cache flushes and invalidates) so the C++ model might not be sufficient for memory mapped I/O.
The non-deterministic behaviour of the user process used for the seL4 refinement proof
means the refinement holds for any possible user code. This allows you to plug in your specific behaviour into the abstract spec and prove properties at the abstract level without having to re-prove the refinemement of the kernel.
So, the answer to your question "Can the existing sel4 theorems help me prove the above theorem about external traces?" is "yes"
because the existing theorems prove the seL4 binary implements the abstract spec for any user space program including yours and this allows you to work with the abstract spec to model interactions with the kernel.
In the case of your example, you have a fair amount of additional work to do, outlined above, to complete an end-to-end proof of your system behaviour.
I'm just an amateur at this. Hopefully Gerwin will follow up with a better answer.