Fil-C on Nix

Filnix wiki

mbrock/filnix

Memory-safe Nix packages

Filnix builds Nixpkgs packages with Fil-C, the memory-safe implementation of C and C++. A memory error in a Fil-C program stops it with a panic instead of corrupting memory. This wiki collects how to use the results, how the toolchain is maintained, what individual ports needed, and how the port campaigns run.

Docs

Using filnix/opt/fil, a relocatable root, NixOS services, PHP Compiler and toolchainDev shell, pins, findings to report upstream Notes on portsBoehm GC and jemalloc on FUGC, Guile, GTK, Ruby Thread cancellationWhat Fil-C's glibc needs to get right Port campaignsRunner, caches, audits and repairs filnix, read as NixThe NixOS and finix modules and the port DSL drawn as structure: bindings as tables, options with their descriptions, names linked to where they are bound.

nanofil

A guide to nanofilA C compiler in Prolog that emits Fil-C code: one C function through every stage, the ideas to hold, a map of the modules and where to start a change. Compile C in the browsernanofil on SWI-Prolog in WebAssembly, drawing the syntax, IR and assembly it makes. How Fil-C worksCapabilities, the collector, safepoints and the libc sandwich, each idea linked to its concept. How Iris worksFrom Hoare logic to Iris, how it is built in Rocq, and nanofil's machine as an Iris language. The formal campaignFil-C's checks removed only where a machine-checked proof says they cannot fire: checked IR in Rocq, the runtime as axioms, certificates replayed by an extracted checker. The model, read as RocqThe Rocq development drawn as structure: inductive types as tables, relations as inference rules, proofs folded under them with their states. All of nanofilEvery page: the source read as Prolog, the concepts, the program logic, the campaign notes, contracts, measurements and the archive.

Explainers

Fil-BIND: BIND 9 in memory-safe CBIND 9.20.30 on Fil-C, the year's CVEs, what it costs. Video, Docker, tarball and NixOS. PHP on Fil-C: memory-safe PHPPHP 8.5 and its native extensions, without a rewrite. Real server performance, security tradeoffs, and an experimental LLVM JIT. Docker, tarball, Nix and NixOS. Fil-C NixOS: a memory-safe NixOS and finixA whole system whose packages are Fil-C builds, systemd and PAM included: one module, what it costs, and how filc-ps proves nothing else runs native. Misaligned pointers in global and thread-local initializersA clang assertion and silent shadow corruption in Fil-C 0.686, and a compile error instead. Video and reproducers. Frame slot coloring at -O0: from cubic to near-linear48 s to 0.66 s for one function, with identical frames. Video and interactive model. memcmp without the eight heap allocations&a and &b put eight heap objects in every memcmp call — a third of PHP's allocation on WordPress. One ctz removes them. Sealed closures: call it, don't open itA staging proof of concept: closures whose callers cannot read, replace or rebind their data, and the inliner bypass review found. Fil-C frame accesses in their own alias scopeEscaped frames make LLVM reload one upper bound 14 times instead of 2. One alias scope, with calls deliberately left out.