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. This approach provides a scalable, mathematically grounded alternative to geometric simulation, offering a foundation for autonomous, zero-collision manufacturing.

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