The vulnerability is in the @leanprover/unicode-input-component package (version 0.1.9 and earlier) used by the Lean 4 Visual Studio Code extension. The package re‑inserts user-supplied text into an input element as unescaped HTML, creating a Cross‑Site Scripting (CWE‑80) condition. An attacker could inject malicious scripts that would execute within the context of the extension.

Projects that use the Lean 4 VS Code extension from vendor leanprover (product vscode‑lean4) and include the @leanprover/unicode-input-component package version 0.1.9 or older are affected. The vulnerability was fixed in component version 0.2.0.

The EPSS score is below 1 % and the vulnerability is not listed in the CISA KEV catalog, indicating a low likelihood of exploitation. The attack requires the attacker to provide malicious input to the extension’s input element, so the exploitation vector is user‑initiated input within the project environment.