AI Enables Agentic Proof-Oriented Programming With Pulse

Nik Swamy at Microsoft Research reports that, recently, using Copilot CLI configured with Claude Opus 4.5, he produced about 10,000 lines of machine-checked F* and Pulse code and proofs, covering concurrent imperative libraries such as bubble sort, ring buffer, priority queue, hashtable, and concurrency primitives. The code has been committed to the Pulse repository, suggesting AI can materially accelerate proof-oriented programming workflows.