Open Source Summit North America 2026 and Embedded Linux Conference brought together the open source community in Minneapolis from May 18–20, 2026.
According to the event report, the event welcomed 1,231 attendees from 524 organizations, with 68% of attendees in technical positions. The program included 210 conference talks selected from 977 talks submitted, reflecting strong interest and participation across the open source ecosystem.
For the ELISA Project community, the event was an important opportunity to continue the conversation around safety-critical software, open source safety standards, regulatory compliance, requirements traceability, verification, software supply chains, and safety engineering.
The Safety-Critical Software Track highlighted practical work across several domains, including aerospace, embedded systems, medical devices, robotics, avionics, automotive, and industrial systems. Sessions explored how open source communities are addressing the technical, process, and compliance needs of safety-critical systems.
Over the next few weeks, we will highlight selected session recordings from the track and share key takeaways with the community.
Session Spotlight: Modernizing Software Verification
This week, we are highlighting Modernizing Software Verification by Craig Christianson, United States Air Force.
Craig opened the session by discussing the difference between “software craftsmanship” and “software engineering,” using the analogy of building structures to explain why safety-critical software needs more than trial, error, and confidence. When software can affect whether people are protected or put at risk, stronger assurance practices are needed.
The session shared real-world examples of software in safety-critical contexts, including systems where software can help protect lives and systems where failure or compromise could create serious risk. Craig also discussed the compliance challenges faced by software engineers working on safety-critical software, including the rigorous and time-consuming nature of assurance and certification processes.
A key part of the talk focused on software assurance and the role of traceability across requirements, specifications, design, implementation, and maintenance. Craig explained how traditional assurance often depends on systematic evaluation, testing, reviews, and evidence, while formal verification uses mathematical models and proofs to reason about system behavior.
The session then explored how automated reasoning can help improve formal methods by making proofs machine-checkable, repeatable, reusable, and less dependent on manual human reasoning. Craig introduced automated reasoning tools and semantics, and showed how these approaches can help reduce errors in logical reasoning.
Craig also discussed the seL4 microkernel as an example of a system supported by formal verification. The talk explained how a small trusted computing base, strong isolation, and publicly available proofs can support higher assurance, while also noting that formal methods still rely on clearly stated assumptions.
The session concluded with a practical demonstration project built for seL4 using the Microkit build system. Craig walked through a Raspberry Pi example, showing how protection domains, mapped device registers, notifications, and hardware interrupts can be used to build a simple system while reasoning more carefully about separation and system behavior.
As open source continues to expand into regulated and safety-critical domains, this talk highlighted why modern verification methods matter. Formal methods and automated reasoning are not a replacement for all testing, but they can help strengthen assurance, improve traceability, reduce certain classes of errors, and support safer systems over time.
Watch the session recording here.
Stay tuned for more Safety-Critical Software Track session highlights from Open Source Summit North America 2026. Check the playlist here.
