Rocq guard checker misses recursive calls via higher-order arguments (CVE-2026-72705)
A checked proof of False, including 0 = 1, needs no axioms, tactics, plugins, or unsafe flags.
Stories per day · 30 days
2 RSS
5 stories, newest first · one card per story
Stories tagged #soundness
Lean 4 kernel accepts false proofs via opaque declarations (CVE-2026-72711)
A checked proof of False, including 0 = 1, passes the Lean 4 kernel at --trust=0 without axioms or unsafe features.
Reasoning Models Are Accurate but Unsound on Identification
CERTID benchmark shows frontier reasoning models give unsound causal identification answers, with false-claim rates varying seventeen-fold across Gemini Flash, Gemini Pro, and GPT-5.5.
Human-LLM Deliberation as Interactive Proof: Conditions for Verifiability Without Transparency
A paper models human-LLM deliberation as an interactive proof with soundness bounds for accepting claims.
Sound Debloating of Redundant Checks in Zero-Knowledge Machine-Learning Circuits
Automated framework soundly removes up to 48.7% of redundant constraints in ezkl and zkml ZK-ML circuits, cutting prover time by up to 72.8%.