Glad you found something fun. If it's L3 for CPU's you mean, then one project of value nobody has done is put in specs for VAMP processor. It was mathematically

Glad you found something fun. If it's L3 for CPU's you mean, then one project of value nobody has done is put in specs for VAMP processor. It was mathematically verified in PVS as part of Verisoft project. They did OS and C subset for it. Adding it to L3 and Myreen et al's toolkit for doing machine code in Isabelle/HOL would let their spec-to-machine-code verifications run on a verified processor. Just throwing that out there for you or anyone interested in lengthening the chain of verification. VAMP doesn't get enough attention. On HW side, someone could do a verified front-end for RISC-V on top of the VAMP components to get a mostly-verified RISC-V. Lots of low-hanging fruit out there.