Sensor networks are often deployed in hostile situations. A number of protocols are being developed to secure these networks. Current means to verify these protocols include simulation, manual inspection, and running them on sensor network testbeds. These techniques leave room for subtle errors in protocol implementations that can be exploited by adversaries. The contribution of this work is the design, implementation and early evaluation of a domain-specific verification framework for nesC implementations of sensor network security protocols. We call our verification framework Slede. Technical underpinnings of Slede include support for automatic extraction of PROMELA models from nesC source code, an annotation language to guide the verification process, and an automatic intrusion model generator. Preliminary evaluation shows that Slede was able to discover flaws in a canonical cryptographic protocol by Needham and Schroeder and two security protocols specific to sensor networks. We also demonstrate that a protocol aware intrusion model automatically generated by Slede incurs a small extra cost compared to models handwritten by model checking experts. By automating a significant portion of the verification process, Slede promises to make it easier to apply finite-state model checking to verify nesC protocol implementations.