Halmos + Foundry: How Symbolic Testing Catches the Bugs Your Fuzzer Will Never Find

Smart contract fuzzing has become table stakes for security-conscious teams. Tools like Echidna, Medusa, and Foundry's built-in fuzzer catch a remarkable range of bugs. But fuzzing has a fundamental limitation: it explores random paths through an astronomical state space, hoping to stumble on the one sequence that triggers a vulnerability. What if the bug requires a specific 256-bit input that a random search will statistically never produce? Enter Halmos — a16z crypto's open-source symbolic testing tool that turns your existing Foundry tests into formal verification specifications. Instead of testing with random inputs, Halmos tests with all possible inputs simultaneously by converting your contract logic into mathematical constraints and feeding them to an SMT solver. This article walks through practical Halmos usage: from installation to writing symbolic tests that would have caught real exploits that fuzzing missed. Why Fuzzing Isn't Enough: A Real Example Consider the Alkemi proto