Kerf

An open, engine-independent IR for the mesh → G-code half of 3D printing — with a written-down denotational semantics and a lowering whose correctness is mechanically checked.

Think "LLVM for slicing," but the point is the verifier, not the container.

Slicers (Cura, PrusaSlicer, OrcaSlicer) are compilers: they lower geometry into machine code (G-code), but each buries that machinery in a private codebase, and no mainstream slicer can show its output corresponds to the input. Kerf is the open middle: an IR whose meaning is defined (denote = the material a program deposits), a lowering Kerf owns, and an oracle that checks the lowering preserves that meaning. Today it mostly consumes slicer G-code to verify it.

Install

# CLI (the `kerf` binary)
cargo install kerf-cli

# Python (CPython ≥ 3.12)
pip install pykerf

Quickstart

# Verify: do Kerf's operations preserve this print?
kerf verify part.gcode              # exit 0 sound · 1 unsound · 3 nothing to verify

# Diff: do two slicers / settings make the same part?
kerf diff old.gcode new.gcode       # exit 0 identical · 1 differ

# Inspect: what did the parser recover, guess, or drop?
kerf inspect part.gcode

import json, pykerf
r = json.loads(pykerf.verify_gcode(open("part.gcode").read()))
assert r["has_geometry"] and r["pass_preserves_denotation"] and r["translation_invariant"]

What it does

• Two-level IR — hi (geometric regions) and lo (move plan), joined by a lowering Kerf owns.
• denote — reference semantics: a program's deposited material as conservative raster occupancy, reversal-invariant.
• Soundness oracle — checks the lowering and each optimization pass preserve denote; a negative test confirms a material-dropping pass is rejected.
• G-code frontend — parses real Cura / PrusaSlicer / OrcaSlicer / Bambu / Simplify3D / KISSlicer / ideaMaker / Slic3r output, including arc (G2/G3) flattening; never panics on untrusted input.
• kerf verify / kerf diff — verification and material comparison over real parsed geometry, with CI-friendly exit codes.
• Proofs — P1–P4 proved in Lean 4 (no sorry); load-bearing kernels model-checked with Kani.

Limitations

• Resolution-bounded. denote compares material up to the raster resolution; choose --resolution ≤ your smallest feature. Sub-resolution differences are not distinguished.
• Planar only. 2D-per-layer IR; non-planar / vase mode is out of scope.
• Deposited geometry, not process state. Widths without a ;WIDTH: comment are estimated; feature roles are an untrusted re-inference. The lo→G-code emitter is lossy and sits outside the verified boundary.
• Checked oracle, not an end-to-end proof. A semantics-level mechanized proof over exact geometry is future work.

Repository

crates/kerf-core   IR, lowering, denote, passes, G-code frontend, verify/diff
crates/kerf-cli    the `kerf` binary
crates/kerf-py     PyO3 bindings (published to PyPI as pykerf)
proofs/            Lean 4 proofs of P1–P4
docs/              design record and semantics

The full design rationale, prior-art scoping, and semantics live in docs/ — start with docs/00-thesis.md and docs/08-semantics.md.

License

Dual-licensed under MIT or Apache-2.0, at your option.