Safety verification in Computer Numerical Control (CNC) machining has traditionally relied on simulation-based methods that require repetitive tests when requirements change. This paper introduces a formal verification framework that conceptualizes the physical CNC workspace as a Spatial Heap, treating physical occupancy as a managed logical resource. Central to our approach is a Parser-Prover Handshake that decouples machine kinematics from formal logic. By mapping tool trajectories and safety buffers into a discrete spatial model prior to evaluation, the framework enables the use of Separation Logic (SL) to verify safety via formal triples. Within this model, physical collisions are redefined as logical Spatial Data Races, detected through the failure of the separating conjunction to establish disjointness. Furthermore, we extend the methodology to collaborative environments using Concurrent Separation Logic (CSL), where physical hand-offs are verified as formal ownership transfers. Additionally, the framework scales to multi-axis kinematics (e.g., 5-axis Table-Table configurations) by treating the workpiece as a dynamically mutable spatial resource. By serving as a complement to traditional geometric simulation, this approach reduces the number of required iterative test cycles, offering a foundation for autonomous, less-collision manufacturing.

翻译：在计算机数控（CNC）加工中，安全验证传统上依赖基于仿真的方法，当需求发生变化时需要重复测试。本文提出了一种形式化验证框架，将物理CNC工作空间概念化为空间堆，并将物理占用视为一种受管理的逻辑资源。我们方法的核心是一种解析器-证明器握手机制，将机器运动学从形式逻辑中解耦出来。通过在评估之前将刀具轨迹和安全缓冲区映射到离散空间模型，该框架能够利用分离开逻辑通过形式三元组验证安全性。在该模型中，物理碰撞被重新定义为逻辑空间数据竞争，通过分离合取无法确定不相交性来检测。此外，我们将该方法扩展到协作环境，使用并发分离开逻辑验证物理交接作为形式所有权转移。同时，该框架通过将工件视为动态可变的空间资源，扩展到多轴运动学（例如，五轴工作台-工作台配置）。作为传统几何仿真的补充，这种方法减少了所需的迭代测试周期数量，为自主化、少碰撞制造奠定了基础。