Formal Verification of CNC Trajectories via Separation Logic

Traditional geometric simulations used for safety verification can be computationally expensive, require repetitive testing when requirements change, and often lack formal safety guarantees. SLING AI provides a formal verification framework that conceptualizes the physical CNC workspace as a “Spatial Heap,” treating physical occupancy as a managed logical memory resource.

Core Technologies & Intellectual Property (IP)

Our solutions are based on original research and patent-pending architectures:

  • Separation Logic-based G-code Collision Pre-verification
    • The Tech: A framework that verifies toolpaths do not overlap with prohibited zones by applying Separation Logic to G-code analysis.
    • Status:
      • Korean Patent Application Filed (Feb 2026, App No. 10-2026-0033761; Under Examination)
      • Subsequent Korean Patent Application Filed (May 2026, App No. 10-2026-0080180; Provisional Specification)
      • Subsequent Korean Patent Application Filed (May 2026, App No. 10-2026-0088912; Provisional Specification)
    • Publication: Preprint (DOI): 10.48550/arXiv.2605.10437
G-Code Trajectory & Kinematics Parser & Discrete Spatial Set Translation (Minkowski Sum Safety Footprint Expansion) Separation Logic Prover Engine (Spatial Heap Disjointness Evaluation) Deterministic Spatial Safety Collision-Free Execution Spatial Data Race Detected Pre-execution Collision Flag

Key Features

  • Parser-Prover Handshake: Our architecture decouples continuous machine kinematics from formal logic. A parser translates continuous tool trajectories and safety buffers into discrete spatial sets before evaluation, enabling tractable logical inference.
  • Deterministic Collision Detection: Physical collisions are modeled logically as “Spatial Data Races.” The system detects potential collisions prior to execution when the separating conjunction fails to establish spatial disjointness between the tool and environmental fixtures.
  • Conservative Safety Margins: To account for real-world mechanical uncertainties such as servo lag or tool deflection, we expand the tool’s spatial footprint using discrete Minkowski sum operations to establish conservative safety margins.
  • Multi-Axis & Multi-Tool Scalability: By extending our framework with Concurrent Separation Logic (CSL), the system verifies complex collaborative environments and 5-axis Table-Table configurations. It achieves this by treating independent cutting tools and moving workpieces as concurrent, dynamically mutable spatial threads moving through a unified coordinate system.

Correct-by-Construction Neuro-Symbolic G-Code Generation

While Large Language Models (LLMs) offer significant potential for automating code synthesis, applying them directly to cyber-physical systems introduces operational risks due to spatial hallucinations and a lack of formal safety guarantees. SLING AI addresses this challenge with a two-way neuro-symbolic architecture that combines the generative capabilities of LLMs with the formal verification of a Separation Logic prover.

Core Technologies & Intellectual Property (IP)

  • Neuro-Symbolic G-code Generation & Verification Architecture
    • The Tech: A hybrid architecture that combines LLM-based G-code generation with a Separation Logic-based prover to evaluate and verify code safety.
    • Status:
      • Korean Patent Application Filed (May 2026, App No. 10-2026-0083867; Provisional Specification)
      • Korean Patent Application Filed (May 2026, App No. 10-2026-0090306; Provisional Specification)
    • Publication: Preprint (DOI): 10.48550/arXiv.2605.10568
3D CAD (STEP) B-Rep Extraction LLM Generator (CAD-RAG Pipeline) Candidate G-Code Synthesized Path Separation Logic Verifier (Disjointness Check) Proven Safe Collision Detected (Spatial Data Race) Automated Self-Correction Bounding Box Feedback Correct-by-Construction Formally Verified Code

Key Features

  • Deterministic Physical Grounding: Before code generation, our system extracts Boundary Representations (B-Rep) directly from standard 3D CAD (STEP) files using the OpenCASCADE framework.
  • CAD-Augmented Generation (RAG): The extracted physical ground truth is padded with mathematically defined safety bounds and integrated into the LLM’s context window via a specialized Retrieval-Augmented Generation (RAG) pipeline to reduce spatial hallucinations.
  • Generator-Verifier Architecture: The LLM operates as an initial “Generator” to synthesize candidate toolpaths based on natural language intent, while the domain-specific Separation Logic prover acts as a “Verifier” to evaluate the neural output for spatial disjointness.
  • Automated Self-Correction: If the prover detects a logical collision (Spatial Data Race), it condenses the conflicting voxels into a localized bounding box. This deterministic error signal is converted into structured feedback, guiding the LLM to refine its trajectory until formal safety criteria are met and the code is verified as correct-by-construction.
This site uses Just the Docs, a documentation theme for Jekyll.