We present construction of resource-aware safe typed assembly language as an EDSL in dependently-typed Idris language. We use this assembly language to compile Linux kernel probes — small pieces of instrumentation code injected directly into the kernel and thus having to satisfy strict safety properties. We believe that the techniques presented can be generally applied to embedding a typed assembly language into a functional language with dependent types.