As I have studied Linux internals, eBPF, and kernel-level observability, I have become increasingly interested in a practical question: how can developers write eBPF programs more clearly and reliably without obscuring what the kernel will execute? That question led me to begin building Solnix, an experimental language for structured, verifier-conscious eBPF development.
Why the verifier matters
eBPF allows sandboxed programs to run in the Linux kernel for observability, networking, tracing, and security. Before a program can be loaded, however, the kernel verifier must establish that its execution satisfies safety requirements. This is an essential protection, not an incidental obstacle.
In practice, developers must make details such as nullable pointers, memory bounds, map lookup failures, and loop limits evident to the verifier. The verifier is responsible for rejecting unsafe programs, while the developer is responsible for expressing the program in a form whose safety can be established.
A language shaped by safety requirements
Solnix explores whether a smaller language can make these requirements more visible during development. Its design emphasizes explicit memory access, guarded pointer use, checked map lookups, and predictable control flow. The intention is not to eliminate the verifier or promise that a program is automatically safe. Instead, the language aims to make common safety obligations easier to express and review before the final verification step.
C remains a capable and important language in the eBPF ecosystem. Solnix is not intended to replace C or its established tooling. It is an experiment in a more constrained programming model, where verifier requirements can influence the language design from the outset.
Compiler architecture
Solnix is implemented in Rust, but it is not a Rust-based source language. The compiler currently processes Solnix source through lexical and syntactic analysis, semantic and safety analysis, and code generation. It emits C, which Clang then compiles into an eBPF object. That object is still subject to the Linux kernel verifier.
This C backend keeps the early toolchain comparatively transparent: generated code can be inspected, there is no large hidden runtime, and the resulting program follows the familiar eBPF verification path. The compiler is an additional layer of assistance, not a substitute for the kernel's safety boundary.
Working within eBPF constraints
eBPF programs operate under deliberate limits, including a bounded stack, restricted memory operations, and requirements for loops and termination. These constraints encourage developers to ask whether a pointer is valid, an access is bounded, a loop can finish, and register values are understood. Solnix treats these questions as part of the programming model rather than concerns to postpone until loading.
An experimental project
Solnix remains an experimental preview and is not recommended for production or security-critical deployment. Generated output should be reviewed, and experiments should be conducted on non-production systems. Areas for continued work include diagnostics, safety analysis, additional program types, map abstractions, testing, and developer tooling.
Building the project is also a way for me to study compiler design, Linux internals, Rust, C, Clang, and kernel security as parts of one connected system. The work is ongoing, and documenting its limitations and design decisions is part of that process.
Continuing the investigation
The question behind Solnix remains open: can a programming language make verifier-friendly eBPF development more natural while preserving transparency? I do not yet know how far the approach can go. For now, the project is a practical way to investigate that question, one compiler diagnostic and verifier result at a time.