events

Beyond Vibe Coding: Formal Verification for AI-Generated Software

Microsoft Reactor Redmond hosts an online session on formal verification for AI-generated software. Carl demonstrates a workflow in which an AI coding agent writes code, produces a formal specification, and generates a machine-checked proof

In inglese

Starts

2026-10-22T00:30:00+00:00

Organizer

Microsoft Reactor Redmond

Location

Online event

Microsoft Reactor Redmond hosts an online session on formal verification for AI-generated software. Carl demonstrates a workflow in which an AI coding agent writes code, produces a formal specification, and generates a machine-checked proof of correctness, applied to RangeSetBlaze, an open-source Rust library, with key properties stated and proved in Lean. The approach is presented as language-independent, with AI taking on much of the proof engineering. The session covers where the workflow succeeds, where it breaks down, and how formal proofs can complement testing and code review as AI takes on more coding.