Proof Before It Merges: FMT as a Git Hook

Video 1 shows FMT running as a git pre-commit hook — the simplest way to put a proof gate between a human and the codebase. A developer "refactors" an average function by distributing a floor-divide across its two terms; it compiles, looks harmless, and is exactly the kind of change a human reviewer would wave through. FMT doesn't: it proves the rewrite isn't equivalent to the original, hands back the exact input where the two disagree, and blocks the commit before it ever lands — with an explicit override for the rare case someone really means to ship it anyway.