# Correct-by-Construction G-Code Generation: A Neuro-Symbolic Approach via Separation Logic

arXiv: https://arxiv.org/abs/2605.10568 · HTML: https://mlsanity.com/paper/2605.10568/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 11 May 2026.

## Built on by (most cited first, 1 of 1)

- [CNCGEN: A Dataset and Framework for Machining Process Planning and Toolpath Generation from B-rep Models](https://mlsanity.com/paper/2609.39738/) (2026)

## Abstract (arXiv)

This paper proposes a neuro-symbolic framework for G-code generation that seeks to integrate the neural generative capabilities of the GLLM method (Abdelaal et al., 2025) with formal verification via a Separation Logic (SL) prover. To establish a reliable physical baseline, the framework extracts deterministic boundary representations from 3D CAD models (STEP files) using the OpenCASCADE framework. This extracted geometric data supports a two-component architecture: the LLM serves as an initial code generator, while the SL Prover, utilizing a Spatial Heap model, evaluates the output. By conceptualizing physical collisions as logical Spatial Data Races -- violations of the separating conjunction in SL -- our framework translates proof failures into structured mathematical feedback. These failures are condensed into bounding boxes that serve as directives for the LLM's iterative self-correction. Ultimately, this work aims to develop a self-correcting system that reduces the need for human supervision, leading to safer and verified autonomous manufacturing.