arXiv Science⌕ Search

arXiv · 2610.37673

Well-Typed ComfyUI Cannot Go Wrong: Gradual Refinement Types for Generative-AI Workflow Graphs

Abstract

Generative-AI workflows are programs assembled from independently developed models and operators. Their correctness depends on relationships among model families, tensor geometry, control modalities, and quantization levels. In ComfyUI, these relationships can be violated even when every connection is accepted by its validator, causing expensive runtime crashes or silent failures. To measure how often such semantic composition failures occur, we classify all 8,766 issues and 1,368 discussion threads of ComfyUI's GitHub repository with an LLM, checked for cross-model agreement. They account for 8\% of issue reports and 21\% of issue-tracker runtime failures, and 32\% of them are silent. Because execution cannot reliably reveal those failures, we present ComfyTy, a gradual refinement type system that checks component compatibility before execution as a compositional property of workflow graphs. Each node declares a reusable schema that states which model families, sizes, modalities, and quantizations it accepts and produces. Wiring nodes together combines their schemas into constraints, which ComfyTy solves to find and report incompatibilities. To evaluate ComfyTy, we first inject faults into official ComfyUI workflows and execute every resulting graph. ComfyTy detects 66.4\% of the confirmed injected faults, all of which ComfyUI's own validator admits. On real workflows across more model families, it raises no false alarm on 765 known-good workflows and detects 67\% of 108 failures rebuilt from user reports. Finally, in a user study with 10 participants, its diagnostics raise fault-localization accuracy on faulty workflows from 35.0\% to 87.5\% and repair accuracy from 30.0\% to 62.5\%.

Explore related subjects

Keep this discovery

Explore connections, maps & timelines

BibTeXRIS

Pingchuan Ma, Zhantong Xue, Hui Li, Zhaoyu Wang, Yuguang Zhou, Shuai Wang, Xiaoqin Zhang. 2026-10-03. Well-Typed ComfyUI Cannot Go Wrong: Gradual Refinement Types for Generative-AI Workflow Graphs. https://arxiv.org/abs/2610.37673

Cite the original work for its findings. Save a collection to share your selection of sources.

KEEP EXPLORING

Related papers

A Type System for Communication-Safe Hardware Design

Hardware components communicate through clock-cycle-sensitive protocols. Hardware Description Languages (HDLs), however, provide limited support for expressing these protocols or for checking that independently developed components agree on them. When components disagree, the composed design can perform unsynchronized exchanges or stop making progress. We call these failures communication-safety violations. Communication safety is thus a global property, determined by interactions between components. This makes it difficult to check modularly. This paper presents Pact, a typed extension of Anvil for modular verification of communication safety in synchronous hardware. Pact types describe message-passing, control-flow, and clock-cycle behaviour. Each component is checked against its type. Compatible types guarantee that the components compose into a communication-safe system. Pact also supports incremental design. It can check a subsystem before the rest of the system exists. The check produces a summary type that captures the communication behaviour left for future compositions. To reduce annotation burden, Pact infers types by abstracting payload values while preserving communication, timing, control, and fairness. These inferred types are optimal for the checker: whenever some checker-accepted types can prove compatibility, the inferred types can prove it as well. Type inference and type checking are decidable, and compatibility is decided by a sound and complete algorithm. We implement Pact by extending the Anvil compiler and evaluate it along five dimensions: detecting communication errors in incremental design, expressiveness on ten clock-cycle-accurate translations of open-source hardware IPs, compatibility-checking time, generated hardware overhead, and annotation burden. Pact expresses realistic protocols and verifies all ten benchmarks in reasonable time.

cs.PL↗

Proof Repair and (Co)algebra Equivalences

Maintaining formal proofs in response to breaking changes in their dependencies is a major challenge of proof engineering. Proof repair is a kind of proof automation that lessens the burden of this challenge by automatically adapting proofs in response to those changes. While proof repair is well understood through an algorithmic lens, it has, until now, been poorly understood through a theoretical lens. We address this gap by giving the first foundational treatment of proof repair, focusing in particular on type-theoretic proof repair in response to changes in datatypes. Our key insight is that the core component of a proof repair algorithm---a ``configuration''---is exactly an algebra isomorphism. We formalize and prove this insight, answering open questions from prior work. We then take this one step further and show that, by taking the dual of this representation, we obtain proof repair over coinductive types. All of our results are formalized in Agda.

cs.PL↗

Polymorphic First-Class Environments

First-class environments expose runtime environments as ordinary values and support a substitution-free, environment-based operational semantics. They also support applications such as first-class modules, dynamic composition of environment fragments, and sandboxing via local environments. Existing environment-based calculi, however, are mostly studied in a simply typed setting and stop short of System F and polymorphism. We present $F_E$, a polymorphic calculus with first-class environments that conservatively extends System F with a small-step environment semantics. $F_E$ eliminates all forms of substitution in System F. Term and type abstractions evaluate to closures, boxes run code under local environments, and box types expose the local typing assumptions of both. Manifest types, together with a two-sided type equivalence, play a dual role: they model type-level instantiation, and enable transparent type components in environments and modules. We prove type soundness, normalization, decidability, and standard properties of type equivalence, and conservativity over System F. The metatheory of $F_E$ is based on instantiation lemmas rather than substitution lemmas. This foundation supports polymorphic first-class modules with dynamic composition and sandboxing. We study $F_E$ in two forms. Our main presentation is an explicit, type-passing calculus that follows conventional System F. We also develop an implicitly-typed variant aligned with the semantics of polymorphic functional languages. All metatheory is mechanized in the Rocq theorem prover.

cs.PL↗