55 citations · 78 across the 8 of their papers we have counts for
12 papers
Skill Issue: Lessons from Optimizing Repository SKILLs for Coding Agents
Mykhailo Kozyrev, Andrei Kozyrev, Anton Podkopaev
Coding agents increasingly read repository knowledge from SKILLs --- plain \texttt{.md} files versioned alongside the code. Recent work synthesizes these files automatically, by op…
RocqSmith: Can Automatic Optimization Forge Better Proof Agents?
Andrei Kozyrev, Nikita Khramov, Denis Lochmelis +3
This work studies the applicability of automatic AI agent optimization methods to real-world agents in formal verification settings, focusing on automated theorem proving in Rocq a…
Are Agents Probabilistic Automata? A Trace-Based, Memory-Constrained Theory of Agentic AI
Roham Koohestani, Ziyou Li, Anton Podkopaev +1
This paper studies standard controller architectures for agentic AI and derives automata-theoretic models of their interaction behavior via trace semantics and abstraction. We mode…
RocqStar: Leveraging Similarity-driven Retrieval and Agentic Systems for Rocq generation
Andrei Kozyrev, Nikita Khramov, Gleb Solovev +1
Interactive Theorem Proving was repeatedly shown to be fruitful when combined with Generative Artificial Intelligence. This paper assesses multiple approaches to Rocq generation an…
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…
LitmusKt: Concurrency Stress Testing for Kotlin
Denis Lochmelis, Evgenii Moiseenko, Yaroslav Golubev +1
We present LitmusKt - the first tool for litmus testing concurrent programs in Kotlin. The tool's novelty also lies in the fact that Kotlin is a multiplatform language, i.e., it co…