Can Open-Weight LLMs Produce Kernel-Verified Coq Proofs? A Pilot Study

arXiv:2608.05420 · cs.LO, cs.LG · Submitted 2026-08-05 · Read on arXiv

Ahmed Ryan, Md Erfan, Akond Ashfaque Ur Rahman, Md Rayhanur Rahman

cs.LO, cs.LG

Submitted: 2026-08-05

License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/

Terminology

• Verification — 25× in this paper · explained in 2 episodes
• Benchmark — 11× in this paper · explained in 2 episodes
• EMMA — 7× in this paper · explained in 2 episodes
• Language Models (LLMs) — 2× in this paper · explained in 2 episodes
• Large Language Models (LLMs) — 2× in this paper · explained in 9 episodes
• Axioms — 1× in this paper · explained in 2 episodes
• Benchmarking — 1× in this paper · explained in 4 episodes
• Commentary — 1× in this paper · explained in 2 episodes
• Fine-Tuning — 1× in this paper · explained in 5 episodes
• Formal Verification — 1× in this paper · explained in 2 episodes
• Large Language Model (LLM) — 1× in this paper · explained in 3 episodes
• Verifier — 1× in this paper · explained in 2 episodes

Related papers

• Reasoning about Continuous-Variable Quantum Systems
• Formalizing Flag Algebras in Lean
• An Information-Flow Perspective on Explainability Requirements: Specification and Verification
• A programming language combining quantum and classical control
• Causal Past Logic for Runtime Verification of Distributed LLM Agent Workflows
• Global Convergence of Detailed Balanced Mass Action Systems