Verified Interpreter for CNC G-code in Lean 4
Table of Contents
This is a course project for CS 511 Formal Methods 1 Fall 2025. I aim to combine Lean 4 with computational fabrication, specifically focusing on the verification of CNC G-code interpreters. The inspiration is from the paper of verified interpreter for 3D printing using Rocq by Tekriwal and Sottile 2025. Due to the time constraint, I only implemented a toy interpreter for a subset of G-code commands.
Project Link: Lean CNC G-code Interpreter
Abstract
In this project, I developed a verified interpreter for a subset of CNC G-code using the Lean 4 proof assistant. The interpreter is fully implemented and verified in Lean 4, with machine-checked proofs showing that each execution step preserves key safety invariants, including coordinate finiteness, modal state consistency, and spindle operation constraints. The formal model represents a 3-axis CNC controller supporting linear motion (G0, G1), positioning mode changes (G90, G91), and spindle control (M3, M5). Using these semantics, I proved that all valid programs maintain well-formedness invariants throughout execution, providing formal guarantees that complement traditional simulation-based verification methods used in computer-aided manufacturing workflows.
Introduction
Computer Numerical Control (CNC) machines automate subtractive manufacturing by translating digital toolpaths into precise motions of cutting tools across multiple axes. These machines are very important in modern manufacturing, enabling the production of complex geometries with high precision. However, CNC programs, which are commonly written in the RS-274 standard, or commonly known as G-code, are notoriously error-prone. Small mistakes in toolpaths can waste material, damage parts, or even cause dangerous machine crashes. Current CAM (Computer-Aided Manufacturing) software tools typically rely on simulation (Singh and Duvedi 2014) and manual inspection to detect errors. While effective in many cases, these approaches provide no formal guarantees that toolpaths will always respect machine constraints.
Recent work has begun to address this gap by introducing mechanized semantics for G-code. Researchers have demonstrated verified interpreters for RS-274/G-code in additive manufacturing implemented using Why3 and Rocq (Tekriwal and Sottile 2025; Sottile and Tekriwal 2024). More narrowly, semantics of linear motion have been formalized to enable invariant checking and differential testing (He et al. 2025). Complementary directions have also explored machine learning for corrective G-code generation, where large language models iteratively refine toolpaths with user feedback (Abdelaal et al. 2025). Together, these efforts highlight both the promise and the growing interest in applying formal methods to RS-274 programming. And there remains little exploration of verified G-code interpreters for CNC using the Lean 4 proof assistant.
In this project, I developed a verified interpreter for a subset of CNC G-code in Lean 4. To keep the scope manageable, the model is restricted to a simplified 3-axis CNC operating, with support for a reduced command set: linear motion (G0, G1), positioning modes (G90, G91), and spindle control (M3, M5). The interpreter represents the CNC machine state in Lean and updates it step by step as commands are executed. Lean 4 supports IEEE floats as datatypes, but has limited logical reasoning principles about them, so some properties rely on assumptions rather than full proofs. On top of this state model, I will define invariants that characterize valid and safe machine states, for example, enforcing that only one positioning mode is active at a time, the tool positions remain within the machine’s work envelope, and the spindle is off when idle/rapid move and on during cutting moves. A central part of the work will involve studying prior verified semantics of RS-274 in Coq/Rocq (Tekriwal and Sottile 2025), translating relevant ideas into Lean 4, and proving that the invariants are preserved under execution of each supported command. Building on this existing foundation will make the project feasible within the scope of a semester.
Contributions
The main contributions of this project are:
Formal semantics: I define a small step operational semantics for a core subset of G-code in Lean 4. The semantics captures tool position and spindle state, positioning mode and feed rate.
Safety invariants: I introduce three classes of machine-checked safety properties: coordinate finiteness, modal state consistency, and physical invariants. I also prove that these properties are preserved during execution.
Soundness theorem: I prove a whole program soundness result which shows that if a program finishes successfully, then all safety invariants hold in the final state (Theorem 9).
Executable verification: By using Lean as both a proof assistant and a programming language, the project allows direct execution of G-code programs inside Lean with the corresponding formal proofs.
Learning Outcomes
The main part of this project is translating ideas from the earlier paper, a verified G-code semantics in Coq/Rocq (Tekriwal and Sottile 2025) into Lean 4. Through this work, I learned:
Lean 4: I gained practical experience with Lean 4 as a functional programming language and as a proof assistant. This helped me understand how to write code and reason about its correctness at the same time.
Formal semantics: I developed a better understanding of operational semantics for domain specific languages, especially for CNC G-code. It also gave me a chance to review abstract syntax trees from CS 330 Concepts of Programming Languages from last semester.
Invariant reasoning: I learned how to define and prove safety invariants about machine states from the paper I used (Tekriwal and Sottile 2025), and I adapted these proofs to Lean 4.
Scope and Limitations
Because of time limits, the informal nature of G-code, and the restricted floating point support in Lean 4, this project has several limitations:
Machine model: The CNC machine is modeled as a simplified three axis system that works in two dimensional space. More advanced features such as tool changes and 2.5D or 3D operations are not included.
Command set: The supported G-code commands include only linear motion (G0 and G1), positioning modes (G90 and G91), and spindle control (M3 and M5). Other commands, such as circular interpolation or homing, are not modeled.
Floating point reasoning: Because Lean 4 has limited support for floating point numbers, some proofs rely on axioms about floating point finiteness instead of fully mechanized reasoning.
Simple proofs: The proofs of invariants focus on core properties and do not cover every possible error or edge case. The project serves mainly as a proof of concept and not a full G-code verifier.
No feedrate check: I did not implement feedrate limit checks in this version. In future work, I plan to add checks to ensure that feedrates remain within acceptable bounds.
Related Work
This work is motivated by a growing interest in formally modeling and verifying fabrication languages. In carpentry, Wu et al. introduced the Carpentry Compiler, which translates high-level fabrication plans into low-level machine instructions while explicitly encoding physical constraints into its semantics (Wu et al. 2019). In textile fabrication, researchers have developed verified compilers for knitting, including translations from high-level primitives to 3D machine instructions (McCann et al. 2016) and automatic conversion of meshes into executable knitting programs (Narayanan et al. 2018). More recently, domain-specific languages such as KnitScript have made advanced machine-level capabilities more accessible while preserving correctness (Hofmann et al. 2023). Other efforts have focused on the formal semantics of knitting instructions to enable precise reasoning about machine execution (Lin et al. 2023), formalizing object equivalence in knitted structures (Lin 2024), and proving polynomial-time program equivalence for knitting specifications (Hurtig et al. 2025). Together, these works show how formal semantics can strengthen correctness while also broadening the creative and computational possibilities of digital fabrication.
By drawing inspiration from verified interpreters in manufacturing (Sottile and Tekriwal 2024; Tekriwal and Sottile 2025; He et al. 2025), correctness-driven compilers for physical making (Wu et al. 2019), and formal semantics in adjacent fabrication domains such as knitting (Lin et al. 2023; Lin 2024; Hurtig et al. 2025), this project explores CNC verification within a broader ecosystem of computational fabrication research. In the long term, integrating a formal verifier into CAM toolchains could reduce reliance on human visual checks, provide correctness guarantees for toolpaths, and contribute to safer, more reliable, and more efficient digital manufacturing systems.
Background
RS-274/G-code Overview
RS-274, commonly known as G-code, is the predominant programming language used to control CNC (Computer Numerical Control) machines. It consists of a series of commands that dictate the movements and operations of the machine tool. G-code commands are typically composed of a letter followed by a number, where the letter indicates the type of command (e.g., G for motion commands, M for miscellaneous functions) and the number specifies the particular operation (Kramer et al. 2000). The commands are executed sequentially; thus, the order of commands is crucial for the correct operation of the CNC machine.
The supported G-code commands in this model are:
G0: Rapid positioning command that moves the tool quickly to a target point without cutting.G1: Linear interpolation command that moves the tool to a target point at a given feed rate for cutting.G90: Sets the machine to absolute positioning mode where the coordinates are measured from the origin.G91: Sets the machine to relative positioning mode where coordinates are offsets from the current position.M3: Turns the spindle on.M5: Turns the spindle off.
The commands G90, G91, M3, and M5 are modal commands. They only
change the state of the machine and take no parameters. The commands
G0 and G1 are motion commands. They update the position of the tool
and may take up to four parameters: X, Y, Z, and F. The first
three specify the target coordinates and F updates the feed rate. To
represent these parameters, I define a structure with optional fields
for each one.
For example, a simple G-code program to move a CNC machine tool in a straight line might look like this:
G90 ; Set to absolute positioning
G0 X10 Y10 ; Rapid move to (10, 10)
M3 ; Spindle on
G1 X50 Y10 F100 ; Linear move to (50, 10) at feed rate 100
M5 ; Spindle off
G0 X0 Y0 ; Rapid move back to origin
In the example above, we can observe that there are two types of
commands, moving commands (G0, G1) and modal commands (G90, M3,
M5). Moving commands change the position of the tool, while modal
commands change the state of the machine without moving the tool. It is
important to keep track of both the position of the tool and the modal
state of the machine. I will make sure to capture both aspects in
modeling for this project.
Another thing to note is that the parameters in moving commands are
optional. For example, the fields available to specify in G0 and G1
commands are X, Y, Z, and F, but in the command G1 X50 Y10 F100, the Z
parameter is not specified, which means the Z coordinate should remain
unchanged after executing this command. Thus, commands like G1 Z10 or
G1 X50 are also valid; this creates more complexity in interpreting
the commands.
Lean 4 Proof Assistant
Lean 4 is a modern proof assistant and functional programming language designed for formal verification and theorem proving. Lean 4 provides a rich set of features for defining data types, functions, and logical propositions, as well as tools for constructing and checking proofs. It is also flexible enough to support general coding (Moura and Ullrich 2021). Thus it supports both the implementation of the interpreter and the formal verification of its properties within the same framework.
Unlike Coq/Rocq, Lean 4 provides native floating point primitives, which makes it easier to work with floating point numbers in the G-code. But Lean 4 has limited support for reasoning about floating point numbers in logic, which means that some proofs may require additional axioms or assumptions about floating point behavior.
Design and Implementation
Physical State Representation
In my implementation, the physical state of the CNC machine is
represented by a structure called PhysicalState. It contains the
following fields:
x,y,z: The current coordinates of the tool in three dimensional space as floating point numbers.spindleOn: A boolean that indicates whether the spindle is on for cutting or off for rapid moves.feedRate: The current feed rate of the tool as an integer.distMode: An enum that records if the machine is in absolute mode (G90) or relative mode (G91).BoundsConfig: A data structure that describes the machine work area with minimum and maximum bounds for each axis.
To make sure the initial state is valid, I defined the X, Y, and Z
coordinates to start at 0.0, the spindle to be off, the feed rate to be
0, and the positioning mode to be absolute. Here is the definition of
the ControllerState structure in Lean:
structure ControllerState where
x : Float := 0.0
y : Float := 0.0
z : Float := 0.0
spindleOn : Bool := false
feedRate : Int := 0
distMode : DistanceMode := DistanceMode.absolute
bounds : BoundsConfig := {}
deriving Repr, BEq
G-code Abstract Syntax Tree (AST)
To represent G-code commands in Lean, I define an inductive data type
called GCode. Each constructor corresponds to a specific G-code
command, with optional parameters represented using Option types. Here
is the definition:
inductive GCode
| G0 (x y z : Option Float) (f : Option Int)
| G1 (x y z : Option Float) (f : Option Int)
| G90
| G91
| M3
| M5
This structure allows me to easily construct and manipulate G-code commands within Lean. For example, the command ‘G1 X50 Y10 F100’ can be represented as:
GCode.G1 (some 50.0) (some 10.0) none (some 100)
Error Handling
For error handling, I focus on two main classes of errors:
Out of bounds movement: A motion command tries to move the tool outside the work envelope, that is, outside the allowed range of any axis.
Spindle state violations: The spindle must be off during rapid moves (
G0) and on during cutting moves (G1). If aG0command is issued while the spindle is on, or aG1command is issued while it is off, an error is raised.
Note that these spindle constraints do not reflect the G-code in the real-world, they are simplifying assumptions used in this formal model.
To represent errors, I define an enum StepError that lists the
possible error cases:
inductive StepError
| OutOfBounds (axis : String) (value : Float) (min : Float) (max : Float)
| SpindleOnWhenRapidMove
| SpindleOffWhenLinearMove
deriving Repr, BEq
The BoundsConfig structure stores the axis limits, and before each
move I check if the new position is inside these limits:
structure BoundsConfig where
xMin : Float := 0.0
xMax : Float := 200.0
yMin : Float := 0.0
yMax : Float := 200.0
zMin : Float := 0.0
zMax : Float := 20.0
deriving Repr, BEq
The spindle check is simpler, since it depends only on the command and
the current spindle state. If any check fails, the interpreter returns a
StepError and stops execution because the machine is in an invalid
state.
Semantics
Target Coordinate Computation
Using the parsed AST, I compute the target coordinates based on the current positioning mode and the optional parameters. If an optional parameter is not given, the current coordinate on that axis remains unchanged.
def computeTarget
(st : ControllerState)
(X? Y? Z? : Option Float) :
Float × Float × Float :=
match st.distMode with
| .absolute =>
(X?.getD st.x, Y?.getD st.y, Z?.getD st.z)
| .relative =>
let dx := X?.getD 0.0
let dy := Y?.getD 0.0
let dz := Z?.getD 0.0
(st.x + dx, st.y + dy, st.z + dz)
Lemma 1. For any state st and optional parameters X?, Y?,
Z?, the function computeTarget produces a deterministic coordinate
triple.
Proof. The initial state of the CNC machine is always X, Y, Z = 0.0,
which are finite floating point numbers. The function first matches on
st.distMode. If the optional parameter for that axis is not given, it
uses the current value. If the value is provided, in both branches, the
result is computed using deterministic operations:
In absolute mode, it uses
Option.getDto extract values from the optional parameters, and updates the coordinates accordingly.In relative mode, it adds the current coordinates to the extracted values, which are also deterministic.
The output is uniquely determined by the input. ◻
Step Function
The main interpreter function, step, takes the current controller
state and one G-code command, and returns either an updated state or a
StepError. Motion commands are handled by a helper function
applyMove, which performs coordinate computation (via computeTarget
from 4.4.1), spindle-state checks, and bounds checks.
def applyMove
(st : ControllerState)
(X? Y? Z? : Option Float)
(F? : Option Int)
(spindleCheck : ControllerState → Option StepError) :
Except StepError ControllerState :=
-- First: Check spindle state
match spindleCheck st with
| some err => Except.error err
| none =>
-- Second: Compute target coordinates
let (newX, newY, newZ) := computeTarget st X? Y? Z?
-- Third: Check if target is within bounds
match checkBounds st newX newY newZ with
| some err => Except.error err
| none =>
-- All checks passed, apply the move
Except.ok { st with
x := newX,
y := newY,
z := newZ,
feedRate := F?.getD st.feedRate }
def step
(st : ControllerState)
(cmd : GCode) :
Except StepError ControllerState :=
match cmd with
| .G0 X? Y? Z? F? =>
applyMove st X? Y? Z? F? checkSpindleForRapidMove
| .G1 X? Y? Z? F? =>
applyMove st X? Y? Z? F? checkSpindleForLinearMove
| .G90 => Except.ok { st with distMode := .absolute }
| .G91 => Except.ok { st with distMode := .relative }
| .M3 => Except.ok { st with spindleOn := true }
| .M5 => Except.ok { st with spindleOn := false }
Lemma 2. For any state st and G-code command cmd, the function
step produces either a new state or a StepError.
Proof. We proceed by cases on cmd.
Case 1:
cmdis a motion command (G0orG1). In this case,stepcallsapplyMove, which performs spindle checks and bounds checks. If any check fails, it returns aStepError. If all checks pass, it returns an updated state.Case 2:
cmdis a modal command (G90,G91,M3, orM5). In this case,stepdirectly returns an updated state without any possibility of error.
Thus, in all cases, step produces either a new state or a
StepError. ◻
Interpreter Execution
Execution over a full G-code program is implemented using foldlM. If
any command fails, execution stops and returns the error.
def runProgram
(st : ControllerState)
(prog : List GCode) :
Except StepError ControllerState :=
prog.foldlM step st
Invariant Proofs
Coordinate Invariants
The goal of this part is to show that if the initial coordinates are finite, then each execution step also keeps all coordinates finite, no NaN or infinities. Since Lean has limited support for reasoning about floating-point finiteness, I introduce several helper axioms:
axiom Float.isFinite_add (a1 a2 : Float) :
a1.isFinite = true → a2.isFinite = true →
(a1 + a2).isFinite = true
axiom Float.isFinite_of_float (a : Float) :
a.isFinite = true
axiom Float.isFinite_add_zero (a : Float) :
a.isFinite = true →
(a + 0.0).isFinite = true
axiom Option.getD_some_float (a d : Float) :
(some a).getD d = a
axiom Option.getD_none_float (d : Float) :
(none : Option Float).getD d = d
Lemma 3. If st.x, st.y, and st.z are finite, then the
coordinates returned by computeTarget are also finite.
Proof. The initial coordinates st.x, st.y, and st.z are finite
by definition, they are all initialized to 0.0. The optional parameters
X?, Y?, and Z? can either be some value or none. If they are
some value, by the axiom Float.isFinite_of_float, these values are
finite. If they are none, the current coordinate is used, which is
also finite. We then do a case split on the positioning mode.
Absolute mode (G90): Each coordinate is either taken directly from the optional parameter or kept from the current state. Both values are finite, so the result is finite.
Relative mode (G91): Each coordinate is computed by adding a finite current value to either:
a finite offset provided by the command, or
zero when the parameter is missing.
By the axioms about finite addition, the result stays finite.
Therefore, in both modes, all target coordinates are finite. ◻
Lemma 4. If st.x, st.y, and st.z are finite and the spindle
state is valid for the command, then applying a move produces finite
coordinates.
Proof. From the previous lemma, the target coordinates produced by
computeTarget are finite. The spindle safety check and bounds check
does not change the coordinates, and the state update copies these
finite values into the new state. Thus the resulting coordinates are
finite. ◻
Theorem 5. For any state st with finite coordinates and any
G-code command cmd, executing step st cmd preserves coordinate
finiteness.
Proof. We split on the command of cmd.
Move commands (G0, G1): If the spindle state is valid, finiteness follows from the previous lemma. If invalid, the step function returns an error and leaves the coordinates unchanged.
Modal commands (G90, G91, M3, M5): These commands do not change coordinates, so finiteness is preserved.
Thus all cases preserve coordinate finiteness. ◻
Modal State Invariant
The modal-state invariant ensures that the machine is always in exactly
one positioning mode, absolute (G90) or relative (G91). This is
simple to check because only G90 and G91 modify the mode. Executing
G90 sets the mode to absolute, executing G91 sets it to relative,
and all other commands leave the mode unchanged. Starting from a valid
initial state, the machine stays in one of these two modes for any
sequence of commands.
Theorem 6. For all states st and G-code commands cmd, if the
current positioning mode is either absolute or relative, then after
executing cmd, the new positioning mode is also either absolute or
relative.
Proof. The initial positioning mode is always either absolute by
definition. We then do case analysis on the proceeding command cmd.
Case 1:
cmdisG90. In this case, the step function updates the positioning mode to absolute. Therefore, the new positioning mode is absolute.Case 2:
cmdisG91. In this case, the step function updates the positioning mode to relative. Therefore, the new positioning mode is relative.Case 3:
cmdis any other command (G0,G1,M3,M5). The step function does not modify the positioning mode. Since the current mode is already either absolute or relative, it stays valid.
In all cases, the new mode is either absolute or relative. There is no situation where the mode becomes invalid. ◻
Spindle State Invariant
The spindle-state invariant ensures that the spindle is always either on
(M3) or off (M5). This is also straightforward because only M3 and
M5 update the spindle state. Executing M3 turns the spindle on,
executing M5 turns it off, and all other commands leave it unchanged.
Starting from a valid initial state, the spindle stays in one of these
two states during execution.
Theorem 7. For all states st and G-code commands cmd, if the
current spindle state is either on or off, then after executing the
command cmd, the new spindle state is also either on or off.
Proof. The initial spindle state is always off by definition. We
proceed by case analysis on the command cmd.
Case 1:
cmdisM3. The step function updates the spindle state to on. Therefore, the new spindle state is on.Case 2:
cmdisM5. The step function updates the spindle state to off. Therefore, the new spindle state is off.Case 3:
cmdis any other command (G0,G1,G90,G91). The spindle state is unchanged, so it stays either on or off as assumed.
Thus the spindle state always remains valid after each command.
A simpler proof is that since the spindle state is represented as a boolean, it can only be true (on) or false (off). There are no other possible values, so it is always valid. ◻
A lesson learned is that for a state that only has two valid configurations, representing it as a boolean simplifies reasoning about its validity than using enums.
Step Soundness and Whole Program Soundness
With the individual invariant proofs, we can state a step soundness theorem showing that each step preserves all invariants, including coordinate finiteness, modal state consistency, and spindle state validity. Using this, we can then prove a whole-program soundness theorem by induction on the length of the program.
Theorem 8. (Step Soundness) For all states st and G-code commands cmd, if the current state satisfies all invariants, then after executing the command cmd, the new state also satisfies all invariants.
Proof. This follows directly from the individual invariant proofs established earlier. Each invariant is preserved by the step function, so the conjunction of all invariants is also preserved. More specifically, coordsFinite st’ ∧ physicalStateInvariant st’ ∧ modalStateInvariant st’ holds after executing cmd from st. ◻
The code snippet for the step soundness theorem is shown below:
theorem step_soundness
(st st' : ControllerState) (cmd : GCode) :
step st cmd = Except.ok st' →
coordsFinite st →
physicalStateInvariant st →
modalStateInvariant st →
coordsFinite st' ∧ physicalStateInvariant st' ∧ modalStateInvariant st' := by
intro h_step h_coords h_phys h_modal
constructor
· -- Prove coordsFinite st'
exact step_preserves_invariant st cmd st' h_step h_coords
· -- Prove physicalStateInvariant st' ∧ modalStateInvariant st'
constructor
· -- Prove physicalStateInvariant st'
exact step_preserves_physicalStateInvariant st cmd st' h_step h_phys
· -- Prove modalStateInvariant st'
exact step_preserves_modalStateInvariant st st' cmd h_step h_modal
Using the step soundness theorem, I can prove the whole-program soundness theorem:
Theorem 9. (Whole Program Soundness) For all initial states st and G-code programs prog, if the current state satisfies all invariants, and executing the program prog from st results in a final state st’, then the final state st’ also satisfies all invariants.
Proof. Note the initial state st satisfies all invariants by
definition, the coordinates are all equal to 0.0 which are finite, the
positioning mode is absolute, and the spindle is off. We proceed by
induction on the length of the program prog.
Base Case: prog is empty. In this case, executing the program results in the same state st. Therefore, all invariants hold in the final state st’.
Inductive Case: prog is of the form cmd :: rest. By the induction hypothesis, executing rest from the state after executing cmd preserves all invariants. By the step soundness theorem(theorem 8), executing cmd from st also preserves all invariants. Therefore, all invariants hold in the final state st'.
Thus, by induction, all invariants are preserved throughout the execution of the program. ◻
Testing
To validate the correctness of the verified interpreter, I implemented a suite of test cases covering both normal execution and error conditions. These tests check that the interpreter updates machine state correctly and raises meaningful errors when constraints are violated. The results show that the interpreter behaves as intended:
=== Testing G-code Error Handling ===
Test 1: Correct Program
----------------------
Correct program succeeded!
Final position: X=25.000000, Y=15.000000, Z=2.000000
Spindle: OFF
Test 2: Out of Bounds
---------------------
Out of bounds error caught correctly!
Axis X value 250.000000 is outside bounds [0.000000, 200.000000]
Test 3: Spindle On During Rapid Move
------------------------------------
Spindle on rapid move error caught correctly!
Cannot perform rapid move (G0) when spindle is on
Test 4: Spindle Off During Linear Move
------------------------------------
Spindle off linear move error caught correctly!
Cannot perform linear move (G1) when spindle is off
Conclusion and Future Work
This project presents a verified interpreter for a small but representative subset of CNC G-code, developed in the Lean 4 proof assistant. The interpreter models a simplified 3-axis CNC machine operating in 2D and supports linear motion commands (G0, G1), positioning modes (G90, G91), and spindle control (M3, M5). I defined core safety invariants, including coordinate finiteness, modal state consistency, and spindle-state validity, and proved that each command preserves these invariants. I then combined the proofs into a whole-program soundness theorem showing that any successfully executed program maintains all safety properties.
The project demonstrates that formal verification can complement simulation-based methods commonly used in CAM workflows. As future work, I plan to expand the interpreter to support additional G-code features (e.g., circular interpolation, homing routines), refine error handling for more complex machine behaviors, and investigate integration with existing CAM toolchains to bring formal guarantees into practical manufacturing pipelines.
References
Abdelaal, Mohamed, Samuel Lokadjaja, and Gilbert Engert. 2025. GLLM: Self-Corrective g-Code Generation Using Large Language Models with User Feedback. https://arxiv.org/abs/2501.17584.
He, Yumeng, Chandrakana Nandi, and Sreepathi Pai. 2025. Formalizing Linear Motion g-Code for Invariant Checking and Differential Testing of Fabrication Tools. https://arxiv.org/abs/2509.00699.
Hofmann, Megan, Lea Albaugh, Tongyan Wang, Jennifer Mankoff, and Scott E Hudson. 2023. “KnitScript: A Domain-Specific Scripting Language for Advanced Machine Knitting.” Proceedings of the 36th Annual ACM Symposium on User Interface Software and Technology (New York, NY, USA), UIST ‘23. https://doi.org/10.1145/3586183.3606789.
Hurtig, Nathan, Jenny Han Lin, Thomas S. Price, Adriana Schulz, James McCann, and Gilbert Louis Bernstein. 2025. “Polynomial-Time Program Equivalence for Machine Knitting.” Proc. ACM Program. Lang. (New York, NY, USA) 9 (ICFP). https://doi.org/10.1145/3747517.
Kramer, Thomas R., Frederick M. Proctor, and Elena Messina. 2000. The NIST RS274NGC Interpreter - Version 3. NISTIR 6556. National Institute of Standards; Technology.
Lin, Jenny. 2024. [Formalizing Object Equivalence in Machine Knitting]{.nocase}. December. https://doi.org/10.1184/R1/28063193.v1.
Lin, Jenny, Vidya Narayanan, Yuka Ikarashi, Jonathan Ragan-Kelley, Gilbert Bernstein, and James McCann. 2023. “Semantics and Scheduling for Machine Knitting Compilers.” ACM Trans. Graph. (New York, NY, USA) 42 (4). https://doi.org/10.1145/3592449.
McCann, James, Lea Albaugh, Vidya Narayanan, et al. 2016. “A Compiler for 3D Machine Knitting.” ACM Trans. Graph. (New York, NY, USA) 35 (4). https://doi.org/10.1145/2897824.2925940.
Moura, Leonardo de, and Sebastian Ullrich. 2021. “The Lean 4 Theorem Prover and Programming Language.” Automated Deduction – CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings (Berlin, Heidelberg), 625–35. https://doi.org/10.1007/978-3-030-79876-5_37.
Narayanan, Vidya, Lea Albaugh, Jessica Hodgins, Stelian Coros, and James McCann. 2018. “Automatic Machine Knitting of 3D Meshes.” ACM Trans. Graph. (New York, NY, USA) 37 (3): 35:1–15. https://doi.org/10.1145/3186265.
Singh, Vishal Kumar, and Ravinder kumar Duvedi. 2014. “A Methodology for Simulation and Verification of Tool Path Data for 3-Axis and 5-Axis CNC Machining.” https://api.semanticscholar.org/CorpusID:57829337.
{#ref-10.1145/3677998.3678221 .csl-entry} Sottile, Matthew, and Mohit Tekriwal. 2024. “Design and Implementation of a Verified Interpreter for Additive Manufacturing Programs (Experience Report).” Proceedings of the 2nd ACM SIGPLAN International Workshop on Functional Software Architecture (New York, NY, USA), FUNARCH 2024, 10–17. https://doi.org/10.1145/3677998.3678221.
Tekriwal, Mohit, and Matthew Sottile. 2025. “Mechanized Semantics for Correctness of the RS274 Additive Manufacturing Command Language.” NASA Formal Methods: 17th International Symposium, NFM 2025, Williamsburg, VA, USA, June 11–13, 2025, Proceedings (Berlin, Heidelberg), 341–59. https://doi.org/10.1007/978-3-031-93706-4_20.
Wu, Chenming, Haisen Zhao, Chandrakana Nandi, Jeffrey I. Lipton, Zachary Tatlock, and Adriana Schulz. 2019. “Carpentry Compiler.” ACM Trans. Graph. (New York, NY, USA) 38 (6). https://doi.org/10.1145/3355089.3356518.
