This is the first I’ve seen “ghost code,” though I admit that I generally don’t work with High Assurance systems or in Ada/Spark (often). Seems like a neat, if somewhat cumbersome idea.