As Gross World LoC (GWL) goes up, a nice-to-have would be for any of that code to be any good.
See CONTRIBUTING.md
- The Scalable Formal Oversight Research Agenda
- Position: Formal Methods are the Principled Foundation of Safe AI
- Position: Trustworthy AI Agents Require the Integration of Large Language Models and Formal Methods
- How to Solve Secure Program Synthesis
- A Proposal for Safe and Hallucination-free Coding AI
- The Coming Need for Formal Specification
- Prediction: AI will make formal verification go mainstream
- Formal Verification: A Bulwark Against the Rising Tide of AI Slop
- Formal Verification: The Final Line of Defense in the AI Era
- Proof Assistants in the Age of AI
- CSLib: Lean's Formal Software Foundation
- "It must be an interesting time to be in programming languages and formal methods..."
- Formal Verification in the Age of AI
- The Agentic Mullet: code in the front, proofs in the back
(Ordered by reverse chronological order)
- Bound Propagation meets Constraint Simplification: Improving Logic-based XAI for Neural Networks (Gomes et al.) (2026/03)
- Towards Real-World Industrial-Scale Verification: LLM-Driven Theorem Proving on seL4 (Zhang et al.) (2026/02)
- Lean Finder: Semantic Search for Mathlib That Understands User Intents (Lu et al.) (2026/02)
- Formal methods for safety-critical machine learning: a systematic literature review (Newcomb, Ochoa) (2026/02)
- Imandra CodeLogician: Neuro-Symbolic Reasoning for Precise Analysis of Software Logic (Lin et al.) (2026/01)
- Autonomous Agents and Policy Compliance: A Framework for Reasoning About Penalties (Tummala, Inclezan) (2025/12)
- A Solver-in-the-Loop Framework for Improving LLMs on Answer Set Programming for Logic Puzzle Solving (Schrader et al.) (2025/12)
- Agentic Property-Based Testing: Finding Bugs Across the Python Ecosystem (Maaz et al.) (2025/10)
- Approximately Aligned Decoding (Melcer et al.) (2025/10)
- ShinkaEvolve: Towards Open-Ended And Sample-Efficient Program Evolution (Lange et al.) (2025/09)
- AlphaEvolve: A coding agent for scientific and algorithmic discovery (Novikov et al.) (2025/06)
- Saarthi: The First AI Formal Verification Engineer (Kumar et al.) (2025/02)
- Chain-of-Programming (CoP) : Empowering Large Language Models for Geospatial Code Generation (Hou et al.) (2024/11)
- Formal Reasoning Meets LLMs: Toward AI for Mathematics and Verification (CACM)
- Megalodon: Efficient LLM Pretraining and Inference with Unlimited Context Length (Ma et al.) (2024/04)
See also fmxai.org for a browsable map of the broader FMxAI ecosystem.
- SVIL 2026 workshop
- FMxAI conference series
- Post AGI Formal Methods workshop
- AIPV workshop
- AITP conference
-
From Vague Words to Verifiable Code: How AI is Building the Bridge to Flawless Software
-
Lies, Damned Lies, and Proofs: Formal Methods are not Slopless
TODO
This is the more speculative/scifi side of things, as opposed to worldview section which is very grounded.