Been looking into L4’s specifications again for reasons, and the thing that looks odd to me is that while there’s certainly lots more hype around it in recent years, the most recent API spec I could find is x.2 r7 from the pre-hype era.
And yes, it’s been vibrant. There’s a paper from 2016 (again 3 years old!) describing what worked and what didn’t, and how various L4 implementations evolved their design (thankfully pointed out by one of its owners last year), but apparently no attempt to formalize any of that stuff.
Is that because L4 is now an industrial workhorse instead of an academic exercise?