GoKawiilProofcraft completes formal proof for dynamic seL4 domain scheduling
Proofcraft has implemented and formally verified a new domain scheduling API for the seL4 microkernel, removing the requirement for a single fixed, compiled-in schedule to maintain information flow security proofs. The API lets systems load semi-static domain schedules that can change across runtime phases, such as longer time slices during boot and shorter ones during normal operation. This capability is now included and proven in seL4 15.0.0.