The following paper provides an overview of the Collins Aerospace INSPECTA Project (DARPA PROVERS). This presents the most recent overview of how HAMR is being applied in defense industry research.

• David Hardin, Isaac Amundson, Junaid Babar, Darren Cofer, Saqib Hasan, Karl Hoech, Jason Belt, John Hatcliff, Robby, Stefan Hallerstede. “Automated SysML v2 System Model to Memory-Safe Language Code Generation for Avionics Applications”. 44th Digital Avionics Systems Conference (DASC 2025), September 2025. (pdf)

Journal paper on HAMR’s component property-based testing framework for Slang (safety-critical subset of Scala), in which a variety of forms of testing infrastructure is generated as part of HAMR code generation. This framework takes model-level behavior specifications written in HAMR’s GUMBO contract language and auto-generates (a) eXecutable versions of GUMBO contracts (GUMBOX contracts) that serve as unit test oracles to accompany auto-generated component application code, and (b) random value generators to shove values into every component input ports and automatically test component application code against GUMBOX oracles. The paper also discusses cloud-based infrastructure for running tests in a distributed fashion.