AI Proposes, FMT Proves: A Neuro-Symbolic Workflow

Video 4 shows what it looks like when an AI assistant and a formal verification engine work together instead of one just trusting the other. Across four short acts, FMT first maps which functions in a real codebase can be formally verified at all, then proves an AI-proposed refactor is safe to merge with zero test coverage, then catches a second AI refactor that looks algebraically correct but silently breaks whenever both inputs are odd, and finally audits the project's git history to flag a bug that already shipped and passed every test. If you've ever wondered how a team gets the speed of AI-assisted coding without inheriting AI-assisted bugs, this is a concrete, four-act answer.