AI for Verifiable Coding: Human-Aligned Collaborative Agents for Autoformalization, Proofs, and Heuristics

LLM code assistants are powerful but untrustworthy: they hallucinate, mishandle corner cases, and lack correctness guarantees. This workshop advances AI for verifiable coding, where human-aligned agents collaborate with proof assistants, model checkers, and analyzers to co-develop specifications, code, proofs, and heuristics with machine-checkable guarantees toward provably safe software. Unlike generic code LLMs, verifiable generation requires expressive specifications and structured proofs where models draft artifacts and formal tools refute, repair, or certify them. Agents must also autoformalize informal requirements/mathematics, search proofs for complex conditions, and discover invariants, lemmas, and solver strategies. Our workshop focuses on five unique perspectives. (1) AI-assisted testing/debugging (e.g., fuzzing, debugging by speaker Shan Lu); (2) Agentic verification for security/smart contracts (speakers Dawn Song; Ilya Sergey); (3) Human-in-the-loop spec generation (speaker Emily First); (4) Verification of AI systems (robustness/safety by speaker Vijay Ganesh); (5) Scalability and automation (speakers Leonardo de Moura; Tudor Achim). We further cultivate an inclusive, interdisciplinary community across LLM and programming languages, with diverse speakers, mentorship, and networking for long-term impact.