I wasn't fully appreciating the difference between the MPU and MMU in relation to seL4. If the R5's can't be supported then that simplifies the decision space somewhat. Guess I'll evaluate the RTOSes before throwing my hands in the air and rolling my own design. 

You  could run eChronos. It’s an RTOS with a (partial) verification  story that supports the  MPU: https://ts.data61.csiro.au/projects/TS/echronos/

Gernot