Formal Verification + AI: Midspiral's Practical Approach to Bug-Free Code

Bugs are part of software development. You program, you test, you ship, your users report bugs, you fix them. Since programmers have been programming, this has been how we program. What if an entire class of bugs could escape this loop? Enter formal verification. It’s possible to guarantee that a subset of your program — the subset where bugs are catastrophically costly — ships with zero bugs. Not after tests pass, not after simulations run, but before the code even compiles. Most founders and engineers have never come across this practice because it has long been reserved for high-stakes domains like NASA and avionics. But with AI, the technology is becoming increasingly accessible. AI ushered us into an era of fast-paced, high-volume autonomous coding systems, but it came at the cost of dubious correctness. It’s possible to maintain the velocity AND guarantee correctness (without the complex web of agentic systems). The founders of Midspiral were some of the first to ask, “What if formal verification were part of every engineering workflow alongside AI?” And in this workshop, they will be showing — in a hands-on, live coding format — that it can be regardless of whether you are a verification expert or have never even heard of a mathematical proof before. This will be an interactive workshop where we will cover: What formal verification actually is, in plain language — what it can and cannot do Walk through practical examples of formally verifying greenfield and brownfield TypeScript functions and features with AI Answer practical, technical, and philosophical questions about the space Bring a laptop, some TypeScript, and your most challenging questions. No prior formal methods background needed or expected. This is for everyone who is tired of having AI catch bugs that the AI introduced in the first place. We will be using LemmaScript for the bulk of the session. It’s open source, so feel free to play with it beforehand. Presented by Midspiral and hosted by Antithesis.