Comment by nickpsecurity

There were many prototyoes of certifying compilers and proof-carrying code in academia. The FLINT group by themselves had many. Maybe try building on those.