Get Started

Solnix is a verifier-safe language for writing Linux kernel programs targeting eBPF. It compiles to eBPF object files while enforcing explicit safety rules required by the kernel verifier.

Project status

Solnix is currently in preview. The compiler supports a core language focused on verifier-safe control flow, map access, and tracepoint programs.

Who is Solnix for?

Designed for

  • Kernel and systems engineers
  • eBPF developers frustrated with verifier errors
  • Security tooling authors

Not designed for

  • General-purpose programming
  • User-space applications
  • Beginners new to Linux internals

Requirements

  • Linux (kernel with eBPF support)
  • clang
  • bpftool (for loading, optional)

Install the compiler

Solnix is currently in preview. Download the compiler binary directly from GitHub Releases:

Solnix Compiler v0.1.0-preview (GitHub Releases)

Verify installation:

solnixc --version

Solnix is currently in experimental preview. The language, compiler, and runtime semantics are subject to change. Do not use Solnix in production systems yet.

Your first Solnix program

This program attaches to a syscall tracepoint and safely writes to a map using a verifier-checked guard.

map results {
    type: .array;
    key: u32;
    value: u64;
    max: 8;
}

unit example {
    section: "tracepoint/syscalls/sys_enter_execve";
    license: "GPL";

    reg a = 10;
    reg b = 20;

    if guard(a < b) {
        imm k0 = 0;
        heap p0 = results.lookup(k0);
        *p0 = 1;
    }

    return 0;
}

Compile

solnixc compile example.snx -o example.o

The output is a verified eBPF object file ready to be loaded using standard tools such as bpftool.

Why guards exist

Solnix requires explicit guard blocks to prove conditions to the eBPF verifier. Inside a guarded block, the compiler guarantees that safety assumptions remain valid.

  • No unchecked pointer dereferences
  • No implicit null assumptions
  • No verifier-ambiguous control flow

Next steps

  • Read the Language Reference
  • Explore verified examples
  • Understand the eBPF verifier model
  • Track upcoming LSM support