Abstract. We provide the first tool for verifying the logic of context-aware applications written for the mainstream sensor network operating system TinyOS; we focus on detecting programming errors related to incorrect adaptation to context.