This repository contains TickTock-a fork of the Tock OS that verifies memory isolation for user space processes. Flux is used for the verification.
You can find the paper here.
The main verification bits can be found under the kernel directory, along with the arch directory. Specifically, allocator.rs contains the memory allocator referenced in the paper. arch/cortex-m/src/mpu.rs contains the MPU implementation for ARMv6m and ARMv7m devices. arch/rv32i/src/pmp.rs contains the MPU implementation for RISC devices.
You can find Lean proofs for SMT solver issues in this repo. Verification of the ARM interrupt handlers and context switching code can be found in this repo.
The original Tock repo can be found here.