Beyond Vibe Coding: Formal Verification for AI-Generated Software

十月 22, 2026 | 12:30 - 1:30 上午 (UTC) 协调世界时

准备好开始使用 AI 和最新技术了吗？ Microsoft Reactor 提供活动、培训和社区资源，帮助开发人员、企业家和初创公司利用 AI 技术等。快加入我们吧！

Beyond Vibe Coding: Formal Verification for AI-Generated Software

十月 22, 2026 | 12:30 - 1:30 上午 (UTC) 协调世界时

准备好开始使用 AI 和最新技术了吗？ Microsoft Reactor 提供活动、培训和社区资源，帮助开发人员、企业家和初创公司利用 AI 技术等。快加入我们吧！

Beyond Vibe Coding: Formal Verification for AI-Generated Software

十月 22, 2026 | 12:30 - 1:30 上午 (UTC) 协调世界时

形式:
直播

主题: 开放源

语言: 英语

AI coding agents can now write substantial amounts of open-source software, but generated code still needs more than a plausible implementation and a passing test suite.

In this session, Carl will demonstrate a workflow in which AI writes code, creates a formal specification, and produces a machine-checked proof of correctness. He is applying this approach to RangeSetBlaze, an open-source Rust library, using Lean to state and prove key correctness properties.

The broader idea is language-independent: AI may make formal verification practical for ordinary software development by taking on much of the proof engineering itself. The session will explore what this workflow looks like in practice, where it works, where it breaks down, and how formal proofs can complement testing and code review as AI takes on more of the coding.