Showing cs.SEShow all
2 papers · 1 filter
cs.SE2025
Can LLMs Enable Verification in Mainstream Programming?
Aleksandr Shefer, Igor Engel, Stanislav Alekseev +3
Although formal methods are capable of producing reliable software, they have seen minimal adoption in everyday programming. Automatic code generation using large language models i…
cs.SE2024
CoqPilot, a plugin for LLM-based generation of proofs
Andrei Kozyrev, Gleb Solovev, Nikita Khramov +1
We present CoqPilot, a VS Code extension designed to help automate writing of Coq proofs. The plugin collects the parts of proofs marked with the admit tactic in a Coq file, i.e.,…