I haven't worked with L4, but have worked with other microkernels.
There are parallels between secure kernels and real-time kernels. If you randomly build a system on top of a real-time kernel, you don't have a real-time system. If you randomly build a system on top of a secure kernel, you don't have a secure system.
However, if you want to build a real-time system, and understand what that requires, you will use a real-time kernel (assuming you have use for a kernel).
If you use a verified kernel (or any component for that matter) and accidentally break the requirements for the security proofs, then you weren't going to be successful building a secure system anyways, because you aren't doing enough systems security analysis. If you are going to do the security analysis, the pre-existing analysis of your kernel is something you can re-use, and your analysis will include evidence that you have met the requirements for reusing that analysis.
Similarly in real-time systems if you use a real-time kernel but don't do some sort of time-based analysis (e.g. rate monotonoic analysis), you won't end up with a real-time system. However, those sorts of analyses are not possible with a kernel that lacks proper real-time features.
There are parallels between secure kernels and real-time kernels. If you randomly build a system on top of a real-time kernel, you don't have a real-time system. If you randomly build a system on top of a secure kernel, you don't have a secure system.
However, if you want to build a real-time system, and understand what that requires, you will use a real-time kernel (assuming you have use for a kernel).
If you use a verified kernel (or any component for that matter) and accidentally break the requirements for the security proofs, then you weren't going to be successful building a secure system anyways, because you aren't doing enough systems security analysis. If you are going to do the security analysis, the pre-existing analysis of your kernel is something you can re-use, and your analysis will include evidence that you have met the requirements for reusing that analysis.
Similarly in real-time systems if you use a real-time kernel but don't do some sort of time-based analysis (e.g. rate monotonoic analysis), you won't end up with a real-time system. However, those sorts of analyses are not possible with a kernel that lacks proper real-time features.