Formal Verification of Agents

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.