1 - 3 September | Vancouver, Canada BC View More Details & Registration The schedule is subject to change, so please check back before the event for the most up-to-date information.
Please note that all session times are listed below in Pacific Daylight Time (PDT), UTC-7.
Sign up or log in to add sessions to your schedule and sync them to your phone or calendar.
The Collins Aerospace INSPECTA project (part of the DARPA PROVERS program) aims to provide a model-based development tool chain for seL4 with integrated formal methods. The High Assurance Modeling and Rapid engineering for embedded systems (HAMR) framework, whose development is led by researchers at Kansas State University, is a key part of the INSPECTA tool chain. HAMR supports modelbased development for seL4 via modeling in SysMLv2, code generation to C and Rust, and deployment to seL4 using Microkit and CAmKeS. Key themes of HAMR include component-based development, multiuse formal behavior contracts integrated across models and code that can be used for formal verification, automated testing, and run-time monitoring, and integration with the Collins INSPECTA assurance case framework. On the INSPECTA project, HAMR is being applied to increase the cyber-resiliency of several autonomy platforms, including the Collins Aerospace Rapid Edge mission system.
At the 2025 seL4 summit, I gave an overview of HAMR framework, with an emphasis on its new capabilities for SysMLv2 modeling, Rust code and contract generation, and integration of the Microkit framework for configuring seL4. That talk focused on specification and verification of individual components using component contracts. In this talk, I describe two new layers of capabilities that significantly improve the effectiveness and speed at which seL4-based systems can be developed using HAMR.
First, to improve support for reasoning about component integration and system level reasoning, HAMR model and code generation has been extended to support auto-generation of multiple forms of run-time monitoring including run-time checking of component contracts, system contracts, and checking of Mission Time Temporal Logic specifications using R2U2 framework. Several aspects of this work leverage new capabilities for “user-land” static scheduling of HAMR components (Microkit protection domains) recently added by UNSW to Microkit.
Second, I give an overview of an emerging agent-based engineering framework for HAMR that supports automated development of HAMR models, contracts, component application code, testing and verification, assurance, and reporting tasks. Several INSPECTA teams are collaborating on building out these capabilities. Our team’s contributions have included (a) integration of Model-Context-Protocol (MCP) support for a variety of HAMR modeling, coding, contract verification, and testing capabilities, (b) specification of HAMR process/workflow steps that agents follow to develop HAMR-based systems on seL4, (c) agent skills that support workflow steps, and (d) specification of human/agents interaction points to support design, property-specification and validation, and audits. I summarize my views of the benefits of model-based development and seL4 in the context of agentic development of high-assurance systems, and I describe how KSU contributions are integrating into the broader INSPECTA work on agentdevelopment. I present outcomes of experiments that we have carried out with this framework including the direction and interaction with the system monitoring capabilities listed above as applied to the INSPECTA Open Platform autonomy reference examples.
HAMR is available under an open-source license, and the project website includes an example repository and collection of videos, tutorials, and classroom lecture materials (also suited for workforce training).
