Pith. sign in

REVIEW 3 major objections 4 minor 19 references

CHC-based Automated Verification of WebAssembly Programs

T0 review · 3 major / 4 minor · reviewed 2026-08-01 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

Pith's one-line read This paper shows that a WebAssembly program's safety—whether any "unreachable" instruction can actually be reached—can be decided by translating the program into constrained Horn clauses and letting an off-the-shelf solver check satisfiabil

desk verdict Interesting CHC-based Wasm verification approach with a likely soundness bug in the `if` rule; needs a fix and a proof before the results can be trusted. read the letter →

arxiv 2607.17220 v1 pith:JGJQR6EG submitted 2026-07-19 cs.PL

Akihisa Yagi , Ken Sakayori , Naoki Kobayashi This is my paper · ORCID
classification cs.PL
keywords WebAssemblyverificationconstrainedHornclausescall_indirectunreachableinstructionsafetyfunctionreferencetablespanichandlersummarizationbit-vectorencodingstaticprogramanalysis
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

WebAssembly programs are hard to verify automatically because they are stack-based, low-level, full of indirect calls through function tables, and often padded with large compiler-generated panic handlers. This paper argues that all three obstacles can be overcome by translating a subset of WebAssembly into constrained Horn clauses (CHCs): the statically fixed stack height allows a flat bit-vector encoding of the operand stack, indirect calls are filtered by the function type required at the call site, and panic handlers are summarized by deleting everything that cannot skip a final unreachable instruction. The resulting CHC satisfiability problem is then solved by existing solvers, giving a yes/no answer to whether an unreachable instruction can be reached. In preliminary experiments on 90 programs, the prototype tool succeeded on 56 with one solver and 54 with another, with the remaining cases mostly timeouts and false alarms from unsupported instructions. The authors are careful to state that the reduction is conjectured, not yet proved, to be sound and complete.

What carries the argument

The load-bearing object is the predicate f_l attached to each instruction label l: it takes the current state (stack values, locals, globals, table array, memory array) and returns the post-function state plus a safety flag. The CHC rules for call_indirect are where the method distinguishes itself: instead of enumerating all functions, the encoding uses F(tf), the finite set of function indices whose declared type matches the type required by the call site, and generates clauses only for those candidates, plus a clause for the trap when the table entry is not in F(tf). Two further optimizations remove array reads entirely: when the table is read-only, call_indirect is expanded to case splits

What would settle it

Run each verified-safe program in a reference WebAssembly interpreter and execute it with arbitrary inputs; if any program reaches an unreachable instruction despite a solver 'safe' verdict, the reduction is unsound. A cheaper check: construct a program with a call_indirect whose table entry has the expected type but whose index was updated via set_table, and compare the solver's verdict with the interpreter's behavior, since the flat encoding of table updates is the subtlest rule.

Watch

Extended reading notes

Core claim

The paper's central claim is that reachability of an unreachable instruction in a WebAssembly program can be reduced, automatically, to the satisfiability of a set of constrained Horn clauses. The reduction introduces one predicate per instruction, whose arguments describe the current operand stack, locals, globals, tables, and memory, plus the summarized outcome of running the rest of the function. Because WebAssembly validation fixes the stack height at each program point, the operand stack can be flattened into separate bit-vector arguments instead of an array, which keeps the clauses tractable. For indirect calls, the encoding filters candidate callees by the statically known function ty

Load-bearing premise

The whole method rests on the conjecture that the generated clauses exactly match the WebAssembly operational semantics—the paper explicitly leaves this unproved; if any instruction rule deviates, a solver's 'safe' answer may not mean the original program is safe.

Editorial extensions

If this is right

  • Safety verification of WebAssembly becomes a push-button activity: a program is verified by compiling it into CHCs and running a solver, with no annotations, specifications, or manual proof effort.
  • Indirect function calls are handled precisely rather than over-approximated, so results about dynamic dispatch through function tables can be trusted up to the assumed soundness of the reduction.
  • Large panic handlers no longer dominate the CHC encoding; slicing them away can make previously intractable programs solvable.
  • Because the encoding uses the finite set of type-matching functions, changes to a module or its function tables are reflected directly in the clause set, allowing incremental re-verification.
  • If the soundness-and-completeness conjecture is established, the approach gives a clean reduction from Wasm safety to CHC solving, letting future improvements in CHC solvers directly benefit WebAssembly.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The unproved soundness-and-completeness conjecture is the main risk; a mechanized proof against an operational semantics would turn the prototype into a dependable verifier.
  • The type-filtering idea transfers to other languages with typed indirect calls, such as Rust's dyn dispatch or C++ virtual calls compiled to Wasm; one could test it by compiling the same programs with different compilers and comparing solver behavior.
  • The panic-handler rewrite might be generalized to any abort path, e.g., assert-failure handlers in C; a testable extension is to apply the same e; unreachable rule to other verification targets and measure clause-size reduction.
  • The observable false alarms from replacing unsupported instructions with unreachable suggest that a staged translation—supporting more instructions directly, rather than over-approximating them—is the immediate next step; one could measure how many of the false alarms disappear as instruction coverage grows.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

3 major / 4 minor

Summary. The paper proposes an automated verification method for a subset of WebAssembly by translating programs into constrained Horn clauses (CHCs) and using existing CHC solvers. The main technical contributions are a type-based filtering optimization for `call_indirect` instructions, two further optimizations for function-reference tables, and a control-flow-based summarization of panic handlers. The method is implemented in a tool called WASMVERIFIER and evaluated on 90 benchmarks (13 original, 3 Rust-compiled, 74 SV-COMP C programs), reporting 56 solved by Z3 Spacer and 54 by Eldarica, with remaining cases timing out or producing false alarms. The authors state explicitly in Sections 3.2 and 7 that the central CHC reduction is only conjectured to be sound and complete, with no formal proof yet established.

Significance. If the CHC reduction is correct, the paper would be a useful contribution to automated WebAssembly verification, particularly for handling indirect calls via type filtering and for reducing the impact of large panic handlers. The evaluation uses external SV-COMP benchmarks and no fitted parameters, which is a strength. However, the central soundness claim is not merely unproven; it is contradicted by a concrete encoding bug for `if` instructions (and likely for table bounds). Until these issues are fixed and a correctness proof is supplied, the experimental results cannot be interpreted as evidence that the tool verifies WebAssembly programs.

major comments (3)
  1. [Section 3.2] The rule for `if` is wrong. The nested sequences E0 and E1 are translated with the unchanged branch-label stack B: `⋃_{e∈E0} C(e,B) ∪ ⋃_{e∈E1} C(e,B)`. In WebAssembly, `if` is a structured control instruction with an implicit label at its `end`; `br 0` inside a branch must target the continuation after the `if`, exactly as in `block`. The `block` rule pushes `\hat l::B` and the `loop` rule pushes `l::B`, but `if` pushes nothing. As written, a `br 0` inside an `if` resolves to the enclosing label, so the generated CHC satisfiability does not correspond to actual reachability of `unreachable`. If the implementation instead pushes a label, the printed definition is wrong; either way the central soundness claim fails on this point. The paper's own conjecture in the same section is therefore not merely unproven but contradicted by the displayed rule.
  2. [Sections 1 and 3.2] The `call_indirect` encoding does not model out-of-bounds table accesses, despite the paper claiming that an invalid table access causes a trap treated as reaching `unreachable`. The target language (Section 2) omits table sizes and treats tables as unbounded arrays, so `(HT)i[s]` is total and no bounds check appears in the `call_indirect` clauses. The third clause only traps when `(HT)i[s]` is not one of the type-matching function indices. Consequently, an out-of-bounds indirect call is not modeled as unsafe, and the verification result can be unsound with respect to the stated safety property. Table sizes and bounds constraints need to be added, or the claim about invalid table access must be qualified.
  3. [Sections 3.2 and 7] The paper twice states that the reduction is only conjectured sound and complete and that 'a formal proof ... has not yet been established.' This is not a minor caveat: the entire experimental claim that solver verdicts imply program safety depends on this theorem. A verification paper must provide a correctness proof, or at least a rigorous proof sketch covering every rule in Appendix A. The concrete `if`-rule bug above shows that the missing proof is not a formality.
minor comments (4)
  1. [Section 3.2] There is a typo: 'The variable v safe is represents whether the execution is safe' should be 'v safe represents whether the execution is safe'.
  2. [Appendix A] The notation in the rules such as `C(get_local i,B) = {f l(· · ·,(HL)i,· · ·)←f^l((S:=)(H L)i::S,· · ·)}` is ambiguous about which predicate argument is being updated. A uniform notation or a legend clarifying the `(S:=)` / `(HL)i:=` convention would improve readability.
  3. [Section 5.1] Figure 3 is a table, not a figure. The 'Failed' column conflates timeouts and false alarms; the text distinguishes them, but the table should also separate these categories to match the narrative.
  4. [Section 5.1] The abstract says 'We confirmed the effectiveness of our approach through preliminary experiments.' Given that only 56/90 programs were solved by Z3 and 12 produced false alarms due to unsupported instructions, this claim is overly strong. Reporting results separately for the subset of programs that use only supported instructions would be more informative.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the CHC translation and optimizations are not fitted to benchmarks; the unproven soundness conjecture is a correctness risk, not a circular step.

full rationale

The paper's derivation does not reduce to its inputs by construction. The CHC translation in Section 3 is a syntax-directed definition over the target language's semantics, with no parameters fitted to the benchmark outcomes. The indirect-call optimizations (Section 3.3) use statically computed sets F(tf) and I((HT)i, m), which are derived from the program text and table initialization, not from the solver results. The panic-handler summarization (Section 4) is a conservative rewrite justified by control-flow reasoning; it may add false alarms but does not presuppose the properties being verified. The experimental claims are measured against external SV-COMP, Rust, and original benchmarks, so solver successes are not equivalent to any fitted value. The main weakness asserted in the paper is the unproven soundness/completeness of the reduction: "We conjecture that this reduction is sound and complete. A formal proof of these properties has not yet been established" (Section 3.2). This is a significant correctness gap, and the rule for `if` may indeed mis-handle branch labels, but that is a potential unsoundness, not a circularity. The paper does not import a load-bearing self-citation: prior work by the authors [4, 13, 18] appears only as general CHC-verification background. No step renames a known result or defines a concept in terms of the target claim. Therefore the circularity score is 0.

Assumptions & free parameters 0 free parameters · 4 assumptions · 0 invented entities

No new physical or mathematical entities are postulated. Translation artifacts like per-entry globals h_i,n are purely internal encodings. The main load is the unproven soundness/completeness conjecture and the conservativeness assumptions for the panic-handler rewrite.

assumptions (4)
  • ad hoc to paper The CHC reduction is sound and complete: a generated CHC set is satisfiable iff the target Wasm program cannot reach unreachable.
    §3.2: 'We conjecture that this reduction is sound and complete. A formal proof of these properties has not yet been established.' This is the central unproved assumption.
  • domain assumption WebAssembly validation fixes the stack height and types at every instruction, permitting the flat encoding of operands.
    §1: 'WebAssembly’s validation phase guarantees that the shape and types of the operand stack are statically determined at each instruction.'
  • domain assumption Panic-handler rewrite e;unreachable → unreachable is sound for safety reachability.
    §4: argued verbally; side condition checked by a 'simple conservative control-flow analysis'; no formal proof supplied.
  • domain assumption F(tf), the set of functions whose type is tf, is statically complete because the language does not allow functions to be created at runtime.
    §3.2: 'Since the target language does not allow functions to be created at runtime, the finite set F(tf) can be computed statically.'

how reviews work

0 comments
Cite this review

Pith. "Pith review of CHC-based Automated Verification of WebAssembly Programs." pith.science (2026). https://pith.science/paper/JGJQR6EG

@misc{pith2026260717220,
  author       = {Pith},
  title        = {Pith review of: CHC-based Automated Verification of WebAssembly Programs},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/JGJQR6EG}},
  note         = {Machine review of arXiv:2607.17220}
}
read the original abstract

WebAssembly is a stack-based imperative language widely used to develop safe and efficient Web applications. In this paper, we propose an automated static verification method for a subset of WebAssembly using a constrained Horn clauses (CHCs) satisfiability solver. Our main challenges are how to handle indirect function calls effectively and how to analyze huge panic handlers. A na\"ive approach to the former problem would be to model a function reference table as an array of functions' entry points, but it would suffer from having too many candidates for indirect calls, resulting in a large case analysis. We address the problem by utilizing type information and filtering candidates for each indirect function call. For the latter problem, a panic handler, which is a function that is called when an error occurs, can be very large and complex. We mitigate this problem by summarizing the panic handler using control-flow analysis. We confirmed the effectiveness of our approach through preliminary experiments.

Figures

Figures reproduced from arXiv: 2607.17220 by the authors.

Figure 1
Figure 1. An overview of our approach to handle panic handlers [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Overview of the optimization for panic handlers [PITH_FULL_IMAGE:figures/full_fig_p009_2.png] view at source ↗
Figure 3
Figure 3. Execution results on each benchmark with Z3 Spacer [PITH_FULL_IMAGE:figures/full_fig_p011_3.png] view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

19 extracted references · 6 canonical work pages

  1. [1]

    Aaron Bembenek & Toby Murray (2026):Bit-Vector CHC Solving for Binary Analysis and Binary Analysis for Bit-Vector CHC Solving.arXiv preprint arXiv:2603.27107, doi:10.48550/arXiv.2603.27107

    work page doi:10.48550/arxiv.2603.27107 2026

  2. [2]

    Dirk Beyer (2026):SV-Benchmarks: Benchmark Set for Software Verification and Testing (SV-COMP 2026, Test-Comp 2026), doi:10.5281/zenodo.18650775

    work page doi:10.5281/zenodo.18650775 2026

  3. [3]

    In:Fields of Logic and Computation II: Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday, Springer, pp

    Nikolaj Bjørner, Arie Gurfinkel, Ken McMillan & Andrey Rybalchenko (2015):Horn clause solvers for program verification. In:Fields of Logic and Computation II: Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday, Springer, pp. 24–51, doi:10.1007/978-3-319-23534-9_2

    doi:10.1007/978-3-319-23534-9_2 2015

  4. [4]

    1393–1418, doi:10.1007/s10817-020-09571-y

    Adrien Champion, Tomoya Chiba, Naoki Kobayashi & Ryosuke Sato (2020):ICE-based refinement type discovery for higher-order functional programs.Journal of Automated Reasoning64(7), pp. 1393–1418, doi:10.1007/s10817-020-09571-y. Akihisa Yagi, Ken Sakayori & Naoki Kobayashi13

    work page doi:10.1007/s10817-020-09571-y 2020

  5. [5]

    WebAssembly Documentation

    WebAssembly Community Group:WebAssembly Security. WebAssembly Documentation. Available at https://webassembly.org/docs/security/. Accessed: 2025-12-01

    2025

  6. [6]

    In:International Conference on Computer Aided Verification, Springer, pp

    Arie Gurfinkel, Temesghen Kahsai, Anvesh Komuravelli & Jorge A Navas (2015):The SeaHorn verifi- cation framework. In:International Conference on Computer Aided Verification, Springer, pp. 343–361, doi:10.1007/978-3-319-21690-4_20

    doi:10.1007/978-3-319-21690-4_20 2015

  7. [7]

    In: Proceedings of the 38th ACM SIGPLAN conference on programming language design and implementation, pp

    Andreas Haas, Andreas Rossberg, Derek L Schuff, Ben L Titzer, Michael Holman, Dan Gohman, Luke Wagner, Alon Zakai & Jean-François Bastien (2017):Bringing the web up to speed with WebAssembly. In: Proceedings of the 38th ACM SIGPLAN conference on programming language design and implementation, pp. 185–200, doi:10.1145/3062341.3062363

    arXiv 2017

  8. [8]

    In:2018 Formal Methods in Computer Aided Design (FMCAD), IEEE, pp

    Hossein Hojjat & Philipp Rümmer (2018):The ELDARICA horn solver. In:2018 Formal Methods in Computer Aided Design (FMCAD), IEEE, pp. 1–7, doi:10.23919/FMCAD.2018.8603013

    arXiv 2018

Show all 19 references
  1. [9]

    637–650, doi:10.1145/2775051.2676980

    Ralf Jung, David Swasey, Filip Sieczkowski, Kasper Svendsen, Aaron Turon, Lars Birkedal & Derek Dreyer (2015):Iris: Monoids and invariants as an orthogonal basis for concurrent reasoning.ACM SIGPLAN Notices50(1), pp. 637–650, doi:10.1145/2775051.2676980

    2015

  2. [10]

    In:International Conference on Computer Aided Verification, Springer, pp

    Temesghen Kahsai, Philipp Rümmer, Huascar Sanchez & Martin Schäf (2016):JayHorn: A framework for verifying Java programs. In:International Conference on Computer Aided Verification, Springer, pp. 352– 358, doi:10.1007/978-3-319-41528-4_19

    2016 doi

  3. [11]

    175–205, doi:10.1007/s10703-016-0249-4

    Anvesh Komuravelli, Arie Gurfinkel & Sagar Chaki (2016):SMT-based model checking for recursive pro- grams.Formal Methods in System Design48(3), pp. 175–205, doi:10.1007/s10703-016-0249-4

    2016 doi

  4. [12]

    In:International symposium on code generation and optimization, 2004

    Chris Lattner & Vikram Adve (2004):LLVM: A compilation framework for lifelong program analysis & transformation. In:International symposium on code generation and optimization, 2004. CGO 2004., IEEE, pp. 75–86, doi:10.1109/CGO.2004.1281665

    2004 arXiv

  5. [13]

    1–54, doi:10.1145/3462205

    Yusuke Matsushita, Takeshi Tsukada & Naoki Kobayashi (2021):RustHorn: CHC-based verification for Rust programs.ACM Transactions on Programming Languages and Systems (TOPLAS)43(4), pp. 1–54, doi:10.1145/3462205

    2021 doi

  6. [14]

    Leonardo de Moura & Nikolaj Bjørner (2008):Z3: An Efficient SMT Solver. In C. R. Ramakrishnan & Jakob Rehof, editors:Tools and Algorithms for the Construction and Analysis of Systems, Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 337–340, doi:10.1007/978-3-540-78800-3_24

    2008 doi

  7. [15]

    Master’s thesis, ETSI_Informatica

    David Munuera Mazarro (2023):Specification and verification of WebAssembly programs. Master’s thesis, ETSI_Informatica

    2023

  8. [16]

    1096–1120, doi:10.1145/3591265

    Xiaojia Rao, Aïna Linn Georges, Maxime Legoupil, Conrad Watt, Jean Pichon-Pharabod, Philippa Gardner & Lars Birkedal (2023):Iris-wasm: Robust and modular verification of webassembly programs.Proceedings of the ACM on Programming Languages7(PLDI), pp. 1096–1120, doi:10.1145/3591265

    2023 doi

  9. [17]

    World Wide Web Consortium (W3C)

    Andreas Rossberg (2025):WebAssembly Core Specification. World Wide Web Consortium (W3C). Available athttps://www.w3.org/TR/wasm-core-2/. Accessed: 2025-11-26

    2025

  10. [18]

    John Toman, Ren Siqi, Kohei Suenaga, Atsushi Igarashi & Naoki Kobayashi (2020):ConSORT: Context- and Flow-Sensitive Ownership Refinement Types for Imperative Programs. In Peter Müller, editor:Programming Languages and Systems - 29th European Symposium on Programming, ESOP 2020...

    2020 doi

  11. [19]

    In:Proceedings of the 7th ACM SIGPLAN International Conference on certified programs and proofs, pp

    Conrad Watt (2018):Mechanising and verifying the WebAssembly specification. In:Proceedings of the 7th ACM SIGPLAN International Conference on certified programs and proofs, pp. 53–65, doi:10.1145/3167082. 14CHC-based Automated Verification of WebAssembly Programs A CHC Generat...

    2018 doi

Pith tools

Reviewed August 1, 2026 · model on record in the stance chip above.