MoonWalker is a software model checker which can automatically detect errors in CIL bytecode programs, i.e. applications written for the .NET platform.

MoonWalker has been developed on the Mono platform. The current version of MoonWalker is able to find deadlocks and assertion violations in CIL programs, generated with Mono's C# compiler.

The design of MoonWalker is inspired by the Java PathFinder (JPF), a model checker for Java programs. The performance of MoonWalker is comparable to JPF.

_{MoonWalker was formerly known as MMC, the Mono Model Checker.}