{"id":"edfff7cb-74c3-4fd7-9446-88e5e8ff12ce","arxiv_id":"2506.10026","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":6.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"A Coq-mechanized, LTS-based logical relation certifies protocol compliance for heterogeneous message-passing systems, with a fundamental theorem for session-typed processes.","lead":"This paper builds a machine-checked method for verifying that message-passing systems follow a communication protocol even when components are written in different languages or are hardware devices such as sensors. It is relevant to cloud and IoT systems, where no single type system spans all components.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Fig. 8's cut/let stepping rule swaps M1 and M2 and omits substitution, so the process-language semantics as stated cannot support the FTLR and adequacy claims.","rationale":"The reader's weakest assumption (LTS-representability of arbitrary components) is a scope limitation rather than a correctness risk: the framework explicitly restricts to components expressible as an LTS over the fixed action alphabet, and the theorems are about that regime. The Fig. 8 cut-let rule, by contrast, threatens the internal soundness of the main case study: Theorem 22 (FTLR) and Corollary 23 (adequacy) are claimed for the process language whose runtime semantics is given by Fig. 8. As written, that semantics misplaces the continuation, leaves the bound variable unsubstituted, and makes simple cut reduction deadlock instead of reducing to the continuation. Because the paper cites a Coq mechanization as its main evidence, the artifact could still contain the corrected rule; but the paper's text alone is then inconsistent with the artifact, and the reader cannot verify the central claim without checking it. This keeps the verdict CONDITIONAL, but the condition is now specifically about the cut rule rather than only about artifact pinning. The paper deserves credit for attempting mechanization and for giving a precise LTS-based framework; the issue is a concrete definitional error in a core construct, not a mismatch with external consensus.","tokens_in":19070,"tokens_out":17286,"duration_ms":215366,"concrete_test":"Inspect the Coq repository (github.com/balzers/LAgnoLR): locate the transition for let x:A←M1;M2 and compare it with Fig. 8. Then test the concrete term let x:1←send(); recvx();M with []⊢M::1. If the Coq rule is (let...,a) → proc[a](M2[x:=b']) ⊎ proc[b'](M1), the term reduces to M and adequacy succeeds; if the Coq rule matches the paper's swapped, unsubstituted version, the term deadlocks with proc[b'](recvx();M) and adequacy fails.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The most load-bearing flaw is in Fig. 8's rule for the cut/let construct. The typing rule Cut (Fig. 6) says Γ1⊢M1::A and Γ2,x:A⊢M2::B imply Γ1,Γ2⊢let x:A←M1;M2::B; semantically M2 is the continuation providing B on the outer channel, while M1 provides A on a fresh channel substituted for x. Fig. 8 instead gives (let x:A←M1;M2,a) ϵ→ proc[b'](M2) ⊎ proc[a](M1): M2 is placed on the fresh channel b', M1 on the outer channel a, and x is never substituted. With this rule, the closed term let x:1←send(); recvx();M steps to proc[b'](recvx();M) ⊎ proc[a](send()); after proc[a](send()) fires a!(), the residual is blocked on b' and never reaches the intended behavior of M. Thus the object language as defined cannot satisfy Theorem 22 or Corollary 23. If the Coq artifact contains a corrected rule (M2 on a with x:=b', M1 on b'), then the paper misstates the mechanized semantics; if it matches Fig. 8, the FTLR claim is false. Either way, the central once-and-for-all verification scenario is not established by the text as written.","agreement_with_reader":"disagree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper defines a language-agnostic logical relation for protocol compliance in message-passing systems. Components are modeled as nameless objects with a labelled-transition semantics over a fixed action alphabet; protocols are specified by linear-logic-style behavioral types (1, ⊗, ⊸, &, ⊕); and the logical relation is given as mutually recursive term/value interpretations E⟦A⟧ and V⟦A⟧ over configuration families. The paper presents two verification modes: per-instance certification of a bit-flipping automaton (Theorem 12) and once-and-for-all certification for well-typed terms of a session-type process language (Theorem 22, FTLR, and Corollary 23, adequacy). It claims that the logical relation and both scenarios are mechanized in Coq with the stdpp library.","tokens_in":19361,"tokens_out":11207,"duration_ms":147723,"significance":"If the technical issues identified below are repaired, this is a valuable contribution. The logical relation is defined entirely over LTS behavior rather than syntax, so untyped and foreign objects are potentially in scope; the relation has no fitted parameters; Theorem 12 is a concrete inhabitance proof; and the FTLR/adequacy result would reduce protocol certification to typechecking. The paper is transparent about substitution-related design choices in §5 and gives appropriate credit to related mechanization work. The claimed Coq mechanization is a strength in principle, although it cannot currently be checked from the submission.","major_comments":[{"comment":"The stepping rule (let x:A←M1;M2,a) ϵ↦→Obj proc[b'](M2)⊎proc[a](M1) is inconsistent with the typing rule Cut in Fig. 6. In Cut, M1 provides A and M2 provides B using x, so after reduction M1 should reside on the fresh channel (say b') and M2, with x instantiated to b', should reside on the outer channel a. As printed, M2 is placed on b' without the substitution of b' for x, and M1 is placed on a. For the closed term let x:1←send(); recvx();send(), the rule steps to proc[b'](recvx();send())⊎proc[a](send()); after proc[a](send()) fires a!(), the residual process on b' is stuck on the free variable x, so no configuration can reach the transition required by Corollary 23. The correct rule should be of the form (let x:A←M1;M2,a) ϵ↦→Obj proc[a](\\widehat{b'/x}(M2))⊎proc[b'](M1), or the paper must explain how the raw terms in Fig. 8 are instantiated. Because Theorem 22 and Corollary 23 are the paper's central once-and-for-all verification results, this rule must be corrected and reconciled with the claimed Coq proofs.","section":"§3.2.3, Fig. 8 (Cut/let rule)"},{"comment":"Definition 14 is stated only for two finite maps with the same codomain Y and a relation R:Y×Y→Type, but it is immediately applied to a typing context Γ:Vars⇀Types and a substitution σ:Vars⇀A, which have different codomains. The same problem occurs in Definition 19, where S is valued in NCfg×A while Γ is valued in Types. As written, Lemma 16 and the statement of Theorem 22 are ill-typed. The intended generalization is to maps m1:X⇀Y1 and m2:X⇀Y2 with a heterogeneous relation R:Y1×Y2→Type; please restate Definition 14 in this form and re-verify Lemma 16 accordingly.","section":"§3.2.2, Definition 14 / Definition 19"},{"comment":"The paper's headline contribution is a Coq mechanization, but the submission contains no pinned artifact: only a bare GitHub URL is given, with no commit hash, Coq/stdpp version, or build instructions. The claims in Theorem 12, Theorem 22, and Corollary 23 therefore cannot be independently checked from the manuscript as submitted. Please bundle the development or provide a stable pointer and environment instructions.","section":"§4, Mechanization artifact"}],"minor_comments":[{"comment":"The cut rule also should state a freshness side condition for the fresh channel b': writing 'for b'∈A' without a side condition permits b' to coincide with a channel already present in the configuration, which could create spurious communication.","section":"§3.2.3, Fig. 8"},{"comment":"The paragraph on substitution says the authors are 'unclear about which approach is favorable' for well-typed terms; since the paper's FTLR is stated for raw terms, this remark should be clarified so that readers know exactly which substitution definition was mechanized and how Fig. 8 is meant to interact with it.","section":"§5, Discussion and Future Work"},{"comment":"Lemma 13, the composition lemma for substitutions, is stated without freshness or distinctness conditions on the bound variables of M; the mechanization may handle this, but the paper should state the hypotheses needed for the induction to go through.","section":"§3.2.2, after Definition 14"}],"recommendation":"major_revision","confidential_remarks":"The core approach is novel and potentially significant, and the reader's stress-test concern about Fig. 8 is real and load-bearing. If the Coq artifact contains a corrected rule, the paper largely needs a careful revision of the text; if the artifact matches Fig. 8, the FTLR claim is false as stated. I would ask for a pinned, buildable artifact before acceptance, because the mechanization claim cannot be assessed otherwise."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Short version: this is a useful idea—a language-agnostic logical relation over LTS configurations for protocol compliance, with the bit-flip automaton and session-typed process language as case studies—but the paper as written has a load-bearing bug in the process-language semantics, and the Coq claims can't be checked because no artifact is pinned. I would not cite it in its current form, but if the artifact exists and the rule is a typo, it's worth a revision.\n\nWhat's actually new: the relation is defined over nameless configurations and configurations as multisets, with complementarity in the LTS rather than juxtaposition of terms, so inhabitants can come from different languages. That is a real step beyond Gollamudi et al.'s language-specific mechanization and Yao et al.'s unmechanized timed relation. The definitions in Sections 2 and 3 are for the most part coherent; Theorem 12 (the bit-flipping automaton inhabits (1⊕1)&(1⊕1)) is believable, and the per-instance scenario is clearly explained. The frame rule, Step-Comm, and the logical relation cases are standard, and I see no circularity or fitted parameters.\n\nThe soft spots, in proportion. The serious one is Fig. 8. The typing rule Cut says let x:A←M1;M2 provides B via the continuation M2, with M1 supplying A on a fresh channel substituted for x. The stepping rule instead puts M2 on a fresh channel b' and M1 on the outer channel a, and does no substitution. With that rule, the closed term let x:1←send(); recvx();M steps to proc[b'](recvx();M) ⊎ proc[a](send()), and after the send on a the residual is blocked on b'. That directly contradicts Theorem 22 and Corollary 23. Either the Coq development contains a corrected rule (then the paper misstates the mechanized semantics) or it matches Fig. 8 (then the FTLR is false). This is not a minor typo in a side lemma; it is the once-and-for-all verification scenario.\n\nThe paper is transparent about the unresolved substitution design choice for typed terms in Section 5, which is good, but that is not the same issue. Also, no pinned artifact or build instructions are given, only a GitHub URL, so the machine-checked claims are not independently checkable from the submission itself.\n\nBottom line: the framework deserves attention, and a serious referee could sort out whether the Coq artifact fixes the cut rule. But as submitted, the central theorem is not established. I'd send it to review with a request for the artifact and a corrected semantics.","headline":"Useful language-agnostic logical relation, but the printed cut rule swaps M1/M2 and omits substitution, so the FTLR and adequacy claims are not supported as written.","tokens_in":19882,"tokens_out":3618,"would_cite":false,"duration_ms":42164,"reading_group":"maybe","serious_thinker":"no","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["68Q60","03B70","68Q85"],"pacs":[],"model":"deepseek-v4-flash","headline":"This paper constructs a language-agnostic logical relation, defined over labelled transition systems, that certifies protocol compliance of heterogeneous message-passing systems—covering typed code, untyped code, and physical devices—and…","keywords":["logical relations","message-passing protocols","verification","type system","session types","intuitionistic linear logic","labelled transition systems","Coq mechanization"],"falsifier":"Build a configuration that the mechanized relation accepts at type $A$, compose it with a complementary configuration of the dual protocol, and check whether the composite can perform an external action that no well-typed session of type $A$ could ever perform; if such a configuration exists, the relation is too permissive and does not actually capture protocol compliance.","tokens_in":18899,"feed_emoji":"🔁","tokens_out":9426,"duration_ms":98575,"temperature":0.7,"pith_summary":"This paper tries to establish a single verification criterion for protocol compliance that works across heterogeneous message-passing systems: programs written in different languages, untyped code, and physical devices like sensors. It defines a logical relation, entirely in terms of labelled transition systems, whose inhabitants are exactly configurations that behave according to a specified protocol type. Because the definition never mentions syntax, any object that can be given an LTS can be checked, and the paper proves the relation is principled enough that every well-typed term in a session-type calculus inhabits its type. This matters because today's distributed and IoT systems cannot assume a common implementation language or type system, so existing type-based verification does not apply. The entire development is mechanized in the Coq theorem prover, making the proofs machine-checked.","feed_headline":"Machine-checked logical relation certifies cross-language protocols","feed_subtitle":"Works for typed and untyped code and even physical sensors; well-typed programs verify once and for all.","key_machinery":"The load-bearing object is the language-agnostic logical relation defined in Fig. 3, given by two mutually recursive interpretations: $E\\llbracket A\\rrbracket$ (term interpretation: a configuration that reaches a value after silent internal steps) and $V\\llbracket A\\rrbracket$ (value interpretation: a configuration ready to perform the external communication prescribed by $A$). Its supporting infrastructure is the process language structure (Definition 6), which packages a set of nameless objects and an LTS transition relation, together with the runtime system of Definition 7 that composes configurations by multiset union and complementary synchronization. The relation is what carries the argument: inhabiting $E\\llbracket A\\rrbracket$ means complying with protocol $A$, and the fundamental theorem (Theorem 22) transfers type-system correctness into this semantic compliance via complementary configurations. The mechanization uses finite maps and multisets, with configurations represented as multisets of atomic processes.","core_discovery":"The paper's central claim is that protocol compliance of a heterogeneous message-passing configuration is captured by the mutually recursive logical relation $E\\llbracket A\\rrbracket$ and $V\\llbracket A\\rrbracket$ of Fig. 3: a nameless configuration is in the term interpretation $E\\llbracket A\\rrbracket$ if it can silently step to a configuration in the value interpretation $V\\llbracket A\\rrbracket$, and $V\\llbracket A\\rrbracket$ specifies, by structural induction on the protocol type $A$, the exact send/receive behaviour expected at that type, including sending a channel, receiving a channel, branching on selectors $\\pi_1/\\pi_2$, and sending the closing signal at type $1$. The relation is defined purely over labelled transition systems, so arbitrary objects—typed or untyped, software or hardware—can be inhabitants as long as they are representable as nameless processes with an LTS. The paper demonstrates this with Theorem 12, showing a bit-flipping automaton inhabits $E\\llbracket (1 \\oplus 1) \\mathbin{\\&} (1 \\oplus 1) \\rrbracket$ (per-instance verification), and Theorem 22, the fundamental theorem, showing every well-typed process term inhabits its type when placed with complementary configurations (once-and-for-all verification), from which Corollary 23 derives adequacy: a closed process of type $1$ eventually sends its closing signal and terminates. All of these results are mechanized in Coq.","pith_inferences":["One testable extension is to take a real device's datasheet, translate its communication spec into an LTS over the paper's action alphabet, and check inhabitance of the promised protocol type; a failure would indicate a spec mismatch.","The fixed action alphabet means the framework in its present form cannot certify protocols with payloads beyond booleans, channels, and the closing signal, such as messages carrying numbers or strings; extending the alphabet is a natural next step.","The adequacy corollary is a termination guarantee only for closed processes of type $1$, and a similar guarantee for open or larger-typed processes is not derived in the paper.","Because the logical relation is unary, it certifies compliance but does not by itself establish relational properties such as noninterference or program equivalence; the paper lists binary logical relations as future work."],"forward_implications":["A specific hardware device can be certified against a protocol specification once, by showing its LTS inhabits $E\\llbracket A\\rrbracket$, with no need for source code or a type system.","For any type system whose well-typed terms can be embedded in this framework, the fundamental theorem makes per-program verification automatic: typechecking suffices, and if typechecking is decidable, verification is fully automatic.","Different components written in different languages can be composed safely, since compliance is defined on observable transitions rather than syntax.","The framework supports higher-order channels, where a channel name is passed as message content, so dynamically established communication links can be certified.","The Coq mechanization means future extensions, such as adding new languages or new protocol types, only require extending the language table and reproving countability rather than redoing the whole framework."],"supporting_citations":[{"why":"Supplies the originating notion of nameless family of configurations and the logical relation for timed message-passing protocols that this work generalizes.","marker":"[41]"},{"why":"Prior mechanization of a semantic logical relation for session types, which this work contrasts with and extends to a language-agnostic setting.","marker":"[13]"},{"why":"Connects session types to intuitionistic linear logic, grounding the typing rules used in the once-and-for-all verification scenario.","marker":"[5]"},{"why":"Provides the semantic typing idea that allows untyped terms to inhabit the logical relation.","marker":"[7]"},{"why":"Supports the logical approach to type soundness that underpins the fundamental theorem of the logical relation.","marker":"[36]"},{"why":"DimSum is the closest multi-language verification framework, whose flexible event sets are replaced here by a fixed action alphabet for uniform composability.","marker":"[31]"},{"why":"Supplies the labelled transition system and π-calculus operational model on which the action-based semantics is built.","marker":"[22, 23, 32]"}],"fun_headline_variants":["Cross-language protocol compliance, machine-checked","Logical relation verifies protocols across languages and devices","Coq-certified protocol compliance for heterogeneous systems","Protocol checks work for typed, untyped, and even sensors","First language-agnostic logical relation for protocols, in Coq"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The whole approach assumes that every component, including a physical sensor or code written in any language, can be described by a list of possible communication steps using only a fixed set of message kinds—sending or receiving a choice label, a channel name, or a closing signal—and that components interact only by matching a send with a receive.","fun_headline_variants_meta":{"raw":{"variants":["Cross-language protocol compliance, machine-checked","Logical relation verifies protocols across languages and devices","Coq-certified protocol compliance for heterogeneous systems","Protocol checks work for typed, untyped, and even sensors","First language-agnostic logical relation for protocols, in Coq"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000871,"raw_usage":{"total_tokens":3841,"prompt_tokens":1083,"completion_tokens":2758,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":699,"completion_tokens_details":{"reasoning_tokens":2681}},"tokens_in":699,"tokens_out":2758,"duration_ms":22317,"temperature":1.0,"reasoning_tokens":2681,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-07T05:14:18.696570+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Build a configuration that the mechanized relation accepts at type $A$, compose it with a complementary configuration of the dual protocol, and check whether the composite can perform an external action that no well-typed session of type $A$ could ever perform; if such a configuration exists, the relation is too permissive and does not actually capture protocol compliance.","supporting_citations":[{"cited_title":"Semantic logical relations for timed message-passing protocols","cited_arxiv_id":null,"evidence_quote":"Supplies the originating notion of nameless family of configurations and the logical relation for timed message-passing protocols that this work generalizes."},{"cited_title":"A semantic logical relation for termination of intuitionistic linear logic session types","cited_arxiv_id":null,"evidence_quote":"Prior mechanization of a semantic logical relation for session types, which this work contrasts with and extends to a language-agnostic setting."},{"cited_title":"Constable, Stuart F","cited_arxiv_id":null,"evidence_quote":"Provides the semantic typing idea that allows untyped terms to inhabit the logical relation."},{"cited_title":"A logical approach to type soundness","cited_arxiv_id":null,"evidence_quote":"Supports the logical approach to type soundness that underpins the fundamental theorem of the logical relation."}],"review_version":1}