FMToolkit in Practice: Two Ways to Get a Proof

FMToolkit verifies code in two different ways, and this walkthrough shows both. In the first half, we write a formal specification for an existing module, validate the original implementation against it, then use that same specification to catch a subtly wrong optimization before it ships — a case where the spec, not the code, is the source of truth. In the second half, we drop the specification entirely: FMToolkit compares an AI-refactored function directly against the version it replaced, using the existing code itself as the specification. One refactor passes as provably equivalent in under a second; another looks correct and isn't, with FMToolkit surfacing the exact input that breaks it.

Together, the two halves cover the two situations you'll actually run into — when you have a spec to write, and when your current code is the only spec you've got.