Vulnerability database
Every flaw the U.S. government’s cybersecurity agency (CISA) has confirmed attackers are using, plus the new WordPress plugin and theme bugs published each day, sorted by what they mean for a small business. We refresh it twice a day. If you see something your website or office runs, tell us.
3 results
Aug 24, 2026The Lean 4 kernel does not check that the body of an opaque declaration is closed.CVE-2026-72711 · Other software · leanprover · reported by VulnCheckMedium 6.8
The Lean 4 kernel does not check that the body of an opaque declaration is closed. environment::add_opaque omits the check_no_metavar_no_fvar call that the definition and theorem paths perform, so a value containing a free variable that is absent from the local context is not rejected outright. A metaprogram can first cause the kernel to create a temporary local of type False and record its type in the type checker's inference cache, then restore the local context while that cache entry persists on the same type checker instance, and finally submit an opaque declaration whose value is the now-unbound variable. The cache lookup answers before the branch that would test membership of the local context, so the kernel infers the cached type and admits an opaque constant of type False, from which any proposition follows. The declaration is accepted through the ordinary checked path at maximum kernel checking, without sorry, unsafeCast, debug.skipKernelTC, addDeclWithoutChecking, foreign code or a modified .olean file, and the result carries no axioms. Fixed in 4.32.2 by adding the missing closure check.
- Product
- lean4
- What to do
- Apply the vendor’s update. The NVD record links to the advisory.
Aug 20, 2026The Lean 4 kernel does not verify that the structure named in a projection expression matches the type of the value being projected, and environment::add_inductCVE-2026-72844 · Other software · leanprover · reported by VulnCheckMedium 6.8
The Lean 4 kernel does not verify that the structure named in a projection expression matches the type of the value being projected, and environment::add_inductive in src/kernel/inductive.cpp did not type check the nested inductive applications that are replaced by auxiliary types, so their parametric arguments escaped checking. A metaprogram running in the Lean process can register an ill-typed nested inductive whose constructor applies a .proj C 0 projection to a value of the unrelated type W, and the kernel admits the declaration through the ordinary checked addDecl path at maximum kernel checking, without sorry, unsafeCast, debug.skipKernelTC, addDeclWithoutChecking, FFI, or a modified .olean file. The result is a type confusion yielding a proof of False that carries no axioms, from which any proposition can be derived. The published proof of concept additionally pads two expressions until their hashes and approximate depths collide, which defeats kernel caching; that is the technique used to reach the flaw, not its cause. Exploitation requires running a metaprogram in-process, for example by building a project or importing a malicious Lake dependency.
- Product
- lean4
- What to do
- Apply the vendor’s update. The NVD record links to the advisory.
Mar 16, 2026Lean 4 VS Code Extension is a Visual Studio Code extension for the Lean 4 proof assistant.CVE-2026-32732 · Other software · leanprover · reported by GitHubNone
Lean 4 VS Code Extension is a Visual Studio Code extension for the Lean 4 proof assistant. Projects that use @leanprover/unicode-input-component are vulnerable to an XSS exploit in 0.1.9 of the package and lower. The component re-inserted text in the input element back into the input element as unescaped HTML. The issue has been resolved in 0.2.0.
- Product
- vscode-lean4
- What to do
- Apply the vendor’s update. The NVD record links to the advisory.
Where this comes from: the exploited list is CISA’s Known Exploited Vulnerabilities catalog. Everything else is the whole National Vulnerability Database, where each record is published by the team that found the bug (Wordfence, Patchstack, WPScan, the vendors themselves and others); we show who. Exploit odds are FIRST’s EPSS, updated daily. Titles and categories are ours, so check the linked record before acting on a detail. For a write-up of the big ones, see our advisories. Every vendor, and every WordPress plugin and theme with a recorded flaw, also has its own page. All of it is free to reuse as JSON, CSV or RSS.
Weekly security brief
The flaws that hit local websites, every Friday.
One short email: what got exploited this week, which WordPress plugins broke, and what to check. Unsubscribe in one click.
Tell us what you're building.
A website, your marketing, a security check, an app, or the thing you've been running out of a spreadsheet for three years. A few lines is plenty.
Not ready to talk yet? Run the free website check and see what Google sees.