This is very interesting work! Do you have axiomatic semantics for Ivory and Tower, and/or specifications for SMACCMPilot? If so, it might be interesting to show specification preservation from Ivory to the Verified Software Toolchain (I'm just assuming that Ivory targets some C subset compatible with Verifiable C). With the ARM backend of CompCert this would give high assurance right down to the machine code.

In any case, I found your experience report to be very well written and would love to hear more about this project.