Fascinating article. I've been doing research in this area and I wonder if there was exploration for JinjaThreads - which operate on Jinja (a Java-like language) that does a formal DRF proof guarantee (coincidentally using Isabelle/HOL).

You can read more about this here if you're interested: https://www.isa-afp.org/entries/JinjaThreads.html