Comment by JCattheATM

> I believe this is called model-code gap and there are ways to address it but I haven't found an easy-to-follow approach.

I would say Ada SPARK solves this problem.