Formal Verification of Agents

Your Code Has Bugs. Lean4 Has Proofs: Formal Verification for Engineers — Varun Pant, AWS

Aug 28, 2026 · 10:07

Varun Pant of AWS argues that formal verification is the only check that can prove AI-generated code correct for every input, as tests and human review cannot scale to the thousands of weekly pull requests coding agents now produce. He advocates spec-driven development with the Lean proof assistant, where humans own the specification and machines own the code and proof, validated by a small independent kernel. Pant walks through Lean's tactics via a chess analogy and details production examples: an AI rewrote zlib in Lean, generating 32,000 lines of proof; Cedar's Lean specification and Rust implementation are reconciled by roughly 100 million differential tests nightly; Verus uses Z3 solvers; and AWS's in-progress Starta tool aims to bring any language into the same verified core.

How Kepler Built Verifiable AI for Financial Services — Vinoo Ganesh

Jul 29, 2026 · 22:30

Vinoo Ganesh, CEO of Kepler, argues that AI in financial services must be augmented with a deterministic substrate to produce verifiable work product, because language models are probability machines unreliable for arithmetic. Kepler's three tenets—atomic provenance (every number ties to its source and stripped if unverifiable), scope determinism (model plans but never computes; deterministic tools handle math), and derivation chains (every number's origin replayable)—ensure numerical accuracy. The system treats each extracted number like a pull request, with reconciliation ensuring entities are caught and nothing invented. Ganesh contrasts citations (after-the-fact audit) with verification (deterministic proof), and notes that compliance with regulators like the SEC requires traceable decision-making. Customers are most excited about reclaiming analyst time from tasks like reading earnings transcripts and building financial models, rather than replacing portfolio managers.

"I've never seen anything scarier than an LLM with tool calls." — Erik Meijer aka @HeadinTheBox

Jul 13, 2026 · 21:13

Erik Meijer of Leibniz Labs argues that AI agents with tool calls are intrinsically dangerous and must be tamed through formal verification. He recounts how adding tool calls to LLMs turned harmless chatbots into agents capable of irreversible side effects, like deleting files or emptying bank accounts. His solution, implemented in Automind, uses proof-carrying code: the agent submits a plan as a program (Free Monad) together with a machine-checkable safety proof, and a small checker verifies the proof before allowing execution. This air-gaps the agent from its tools, ensuring policy compliance statically. Meijer demonstrates that elementary type systems and compiler techniques, such as taint analysis on program expressions, can provably prevent unsafe actions, turning agents from 'vibe-coding' risks into provably safe systems.