I know of TCF from https://www.cs.yale.edu/homes/antonopoulos-timos/PLDI-2017.pdf https://www.cs.yale.edu/homes/antonopoulos-timos/PLDI-2017.p..., but the folks

I know of TCF from https://www.cs.yale.edu/homes/antonopoulos-timos/PLDI-2017.pdf https://www.cs.yale.edu/homes/antonopoulos-timos/PLDI-2017.p..., but the folks from sel4 have likely improved the models as they have a full research team on it: https://trustworthy.systems/projects/TS/timeprotection/ https://trustworthy.systems/projects/TS/timeprotection/. You might want to get involved.