diff --git a/repos/base-sel4/src/base/internal/assert.h b/repos/base-sel4/src/base/internal/assert.h
new file mode 100644
index 0000000000..9a1bebf684
--- /dev/null
+++ b/repos/base-sel4/src/base/internal/assert.h
@@ -0,0 +1,38 @@
+/*
+ * \brief  Low-level assert macro
+ * \author Norman Feske
+ * \date   2015-05-06
+ *
+ * The output of the assert macro is directed to the platform's low-level
+ * debugging facility.
+ */
+
+/*
+ * Copyright (C) 2015 Genode Labs GmbH
+ *
+ * This file is part of the Genode OS framework, which is distributed
+ * under the terms of the GNU General Public License version 2.
+ */
+
+#ifndef _BASE__INTERNAL__ASSERT_H_
+#define _BASE__INTERNAL__ASSERT_H_
+
+/* Genode includes */
+#include <base/snprintf.h>
+
+/* base-internal includes */
+#include <internal/kernel_debugger.h>
+
+#define ASSERT(e) \
+	do { if (!(e)) { \
+		char line_buf[32]; \
+		snprintf(line_buf, sizeof(line_buf), "%d", __LINE__); \
+		kernel_debugger_outstring(ESC_ERR "Assertion failed: " #e ESC_END "\n"); \
+		kernel_debugger_outstring(__FILE__ ":"); \
+		kernel_debugger_outstring(line_buf); \
+		kernel_debugger_panic("\n"); \
+		} \
+	} while(0)
+#else
+
+#endif /* _BASE__INTERNAL__ASSERT_H_ */
diff --git a/repos/base-sel4/src/base/internal/kernel_debugger.h b/repos/base-sel4/src/base/internal/kernel_debugger.h
new file mode 100644
index 0000000000..55b021ad05
--- /dev/null
+++ b/repos/base-sel4/src/base/internal/kernel_debugger.h
@@ -0,0 +1,37 @@
+/*
+ * \brief  Platform-specific kernel-debugger hooks for low-level log messages
+ * \author Norman Feske
+ * \date   2015-05-06
+ */
+
+/*
+ * Copyright (C) 2015 Genode Labs GmbH
+ *
+ * This file is part of the Genode OS framework, which is distributed
+ * under the terms of the GNU General Public License version 2.
+ */
+
+#ifndef _BASE__INTERNAL__KERNEL_DEBUGGER_H_
+#define _BASE__INTERNAL__KERNEL_DEBUGGER_H_
+
+/* base includes */
+#include <base/thread.h>
+
+/* seL4 includes */
+#include <sel4/interfaces/sel4_client.h>
+
+
+static inline void kernel_debugger_outstring(char const *msg)
+{
+	while (*msg) seL4_DebugPutChar(*msg++);
+}
+
+
+static inline void kernel_debugger_panic(char const *msg)
+{
+	kernel_debugger_outstring(msg);
+	kernel_debugger_outstring("\n");
+	seL4_TCB_Suspend(Genode::Thread_base::myself()->tid().tcb_sel);
+}
+
+#endif /* _BASE__INTERNAL__KERNEL_DEBUGGER_H_ */