Abstract. We describe the first software tool for the verification of TinyOS 2, MSP430 applications at compile-time. Given assertions upon the state of the sensor node, the tool boundedly explores all program executions and returns to the programmer an error trace leading to any assertion violation. Besides memory-related errors (out-of-bounds arrays, null- pointer dereferences), we verify application-specific assertions, including low-level assertions upon the state of the registers and peripherals.