The ELISA Project participated in the Linux Plumbers Conference (LPC) 2025, held December 11–13 at Toranomon Hills Forum in Tokyo (with hybrid remote access). The event brought together developers working in the core areas of Linux for technical discussions and collaboration.
ELISA at the Safe Systems with Linux Microconference
ELISA community members joined kernel developers during the Safe Systems with Linux Microconference to explore how Linux can better support safety-critical and high-integrity systems. The microconference focused on progress around traceability, requirements, testing, and scalable verification to support more dependable kernel development.
Session Highlights:
Aspects of Dependable Linux Systems – Kate Stewart (Linux Foundation), Philipp Ahmann (Etas GmbH (BOSCH))
Kate and Philipp discussed how Linux is increasingly used in safety-critical and regulated industries that rely on dependable and robust software. They explained that these industries follow formal standards for requirements, verification, and change management, but such standards are not well known within the open source kernel community. The session highlighted that while the Linux kernel already contains many good development practices, important artifacts like requirements, tests, and documentation are not yet connected in a structured way. The speakers highlighted the need for shared approaches rather than isolated company efforts to make Linux safer and easier to analyze in complex systems. The speakers encouraged collaboration on improving traceability, clarity, and maintainability to support dependable Linux-based systems.
NVIDIA Approach for Achieving ASIL B Qualified Linux: minimizing expectations from upstream kernel processes -Igor Stoppa (NVIDIA)
In this talk, Igor Stoppa presented NVIDIA’s approach for achieving ASIL-B qualified Linux while minimizing the impact on upstream kernel developers and processes. Unlike traditional safety strategies that require modifying or qualifying large parts of the kernel, NVIDIA proposes mechanisms that isolate and contain safety-relevant components so the wider kernel does not need to be safety-qualified. The approach focuses on reducing dependencies, avoiding burdens on maintainers, and enabling qualification without requiring upstream developers to become safety experts. Igor outlined techniques such as resource partitioning, thread capabilities, and memory pools to ensure verifiable safety behavior without intrusive kernel changes. The goal is to support safety use cases in automotive and robotics while keeping upstream integration feasible and low-friction.
Applying Program Verification to Linux Kernel Code: Challenges, Practices, and Automation – Keisuke Nishimura
In this talk, Keisuke Nishimura presented ongoing work on applying deductive program verification to Linux kernel code, with a focus on the task scheduler. He explained that while the kernel is increasingly gaining specifications, checking that implementations satisfy them still relies heavily on manual effort. Using case studies, he showed how formal verification of scheduler functions can uncover real semantic bugs and increase confidence in functional correctness. The talk also covered practical challenges, such as writing formal specifications, handling loops with invariants, and preparing minimal, verifiable code extracted from large kernel files. Keisuke concluded by outlining automation efforts for code extraction and invariant inference, with the goal of making formal verification a more scalable and practical part of the Linux kernel development process.
Defining and maintaining requirements in the Linux Kernel – Chuck Wolber, Gabriele Paoloni (Red Hat), Kate Stewart (Linux Foundation)
Last year in Vienna the speakers of this talk held a session about “improving kernel design documentation and involving experts”. Following this, the ELISA Architecture working group drafted an initial template for the SW Requirements definition and started documenting the expected behaviour for different functions in the TRACING subsystem.
The work also included reviewing and adopting a framework for formally specifying kernel APIs.
This session aimed to present the latest updates and involve the experts to define the best next steps for having a path to introduce and maintain requirements in the kernel.
The discussion focused on how to document code, show value, address maintainer comments, and link requirements to tests and other verification measures.
KUnit Testing Insufficiencies – Matthew Whitehead (The Boeing Company)
This talk examined the limitations of KUnit when testing small, isolated units of Linux kernel code for high-integrity applications. Matthew Whitehead showed how the current KUnit approach struggles with scalability, system-state dependence, and the lack of built-in mocking or faking needed for low-level testing. Because KUnit tests are built into the kernel, they require full kernel builds, multiple kernels for large test sets, and slow write–execute–observe cycles. He demonstrated how creating isolated tests often requires patches, duplicated code, and extensive setup, which leads to high maintenance costs. The session highlighted the need for unit test capabilities that support out-of-tree compilation, user-space execution, and automatic integration of mocks.
Exploring possibilities for integrating StrictDoc with ELISA’s requirements template approach for the Linux kernel – Tobias Deiminger (Linutronix GmbH)
This talk demonstrated how ELISA’s proposed Linux kernel requirements template could be realized using the StrictDoc model and tooling. Tobias Deiminger showed how StrictDoc can parse requirement templates inlined in Linux source code, merge them with sidecar metadata files, and render traceable documents linking requirements, code, and tests. He highlighted that StrictDoc already fulfills most ELISA needs, including SPDX-REQ tags and structured traceability, while gaps remain around hash-based drift detection. The presentation included a live walkthrough using a demo repository and discussed StrictDoc’s broader model (requirements, design, tests, user stories) compared to ELISA’s current low-level focus. The talk concluded with the proposal that StrictDoc add hash generation and compatibility tweaks, while ELISA could list StrictDoc as a reference tool for kernel developers.
BASIL: Open Source Traceability for Safety-Critical Systems” – Luigi Pellecchia
This talk introduces BASIL – The FuSa Spice, a web-based tool that helps manage traceability for large, fast-evolving projects like the Linux kernel. Luigi Pellecchia explains how safety standards require traceability across requirements, code, tests, documentation, and test results, but these artifacts are spread across many repositories and CI systems (e.g., Linux Test Project, man-pages, CKI, KernelCI). BASIL proposes “traceability as code”: a single configuration file defines which repositories to scan, how to extract work items (requirements, tests, results), and how they relate to each other. From this, BASIL can automatically build and update traceability matrices, integrate data from external test infrastructures, and export results in formats such as SPDX. The session shows how this approach makes traceability and compliance more repeatable, automatable, and sustainable for the Linux kernel ecosystem.
The discussions at LPC 2025 made it clear that building safer and more dependable Linux-based systems is a shared challenge and a shared opportunity. Across all sessions, common themes emerged: improving traceability, defining clearer requirements, strengthening testing practices, and exploring scalable approaches to verification. These conversations reflect exactly what ELISA is working toward: enabling the broader community to confidently use Linux in safety-critical and high-integrity environments.
If you are interested in these topics, we invite you to learn more about the ELISA Project and get involved. Learn more about the ELISA project and working groups.