Thanks for the kind words! You might find our more recent Haskell Symposium paper of interest if you're interested in semantics (this is also a good reminder f

Thanks for the kind words! You might find our more recent Haskell Symposium paper of interest if you're interested in semantics (this is also a good reminder for us to update the webpage with a link): https://www.cs.indiana.edu/~lepike/pubs/ivory.pdf https://www.cs.indiana.edu/~lepike/pubs/ivory.pdf Essentially, we built an Isabelle/HOL model of a Core Ivory language, and then used those semantics to prove type safety through the usual progress and preservation. We don't have specifications of the higher-level properties of SMACCMPilot at the Ivory/Tower level. Instead our partners at Rockwell Collins are developing AADL specification and analysis tools to prove system-level properties at the architecture level.