Videos
See FMToolkit prove it, not just say it — short demos of proof-gated commits, AI-assisted refactors, and formal verification catching real bugs.
Why Formal Methods Matter: The Calendar Problem
A single, familiar rule — is a year a leap year? — hides more complexity than it looks like, and shows why testing alone can't catch what formal verification proves gone.
Proof Before It Merges: FMT as a Git Hook
A refactor that compiles, looks harmless, and would sail through code review — until FMT proves it isn't equivalent and blocks the commit.
Gating Claude's Own Rewrites
The same proof gate, moved from a human committing code to an AI writing it — wired into Claude through an MCP connector and a standing rule in CLAUDE.md.
AI Proposes, FMT Proves: A Neuro-Symbolic Workflow
Four short acts: mapping what's formally verifiable, proving a safe AI refactor, catching an unsafe one, and auditing git history for a bug that already shipped.
FMToolkit in Practice: Two Ways to Get a Proof
A full walkthrough of FMToolkit covering both ways it proves code correct: against a written specification, and against the code it's replacing.