diff --git a/hw/application_fpga/Makefile b/hw/application_fpga/Makefile
index 0b1f0d5..eac56b5 100644
--- a/hw/application_fpga/Makefile
+++ b/hw/application_fpga/Makefile
@@ -85,6 +85,14 @@ FIRMWARE_OBJS = \
 	$(P)/fw/tk1/led.o \
 	$(P)/fw/tk1/blake2s/blake2s.o
 
+FIRMWARE_SOURCES = \
+	$(P)/fw/tk1/main.c \
+	$(P)/fw/tk1/proto.c \
+	$(P)/fw/tk1/lib.c \
+	$(P)/fw/tk1/assert.c \
+	$(P)/fw/tk1/led.c \
+	$(P)/fw/tk1/blake2s/blake2s.c
+
 TESTFW_OBJS = \
 	$(P)/fw/testfw/main.o \
 	$(P)/fw/testfw/start.o \
@@ -132,6 +140,11 @@ $(TESTFW_OBJS): $(FIRMWARE_DEPS)
 firmware.elf: $(FIRMWARE_OBJS) $(P)/fw/tk1/firmware.lds
 	$(CC) $(CFLAGS) $(FIRMWARE_OBJS) $(LDFLAGS) -o $@
 
+.PHONY: check
+check:
+	clang-tidy -header-filter=.* -checks=cert-* $(FIRMWARE_SOURCES) -- $(CFLAGS)
+	splint -nolib -predboolint +boolint -nullpass -unrecog -infloops -initallelements -type -unreachable -unqualifiedtrans -fullinitblock $(FIRMWARE_SOURCES)
+
 testfw.elf: $(TESTFW_OBJS) $(P)/fw/tk1/firmware.lds
 	$(CC) $(CFLAGS) $(TESTFW_OBJS) $(LDFLAGS) -o $@
 
diff --git a/hw/application_fpga/fw/tk1/assert.c b/hw/application_fpga/fw/tk1/assert.c
index cd327cf..43628ae 100644
--- a/hw/application_fpga/fw/tk1/assert.c
+++ b/hw/application_fpga/fw/tk1/assert.c
@@ -7,8 +7,8 @@
 #include "led.h"
 #include "lib.h"
 
-void assert_fail(const char *assertion, const char *file,
-		   unsigned int line, const char *function)
+void assert_fail(const char *assertion, const char *file, unsigned int line,
+		 const char *function)
 {
 	htif_puts("assert: ");
 	htif_puts(assertion);
diff --git a/hw/application_fpga/fw/tk1/assert.h b/hw/application_fpga/fw/tk1/assert.h
index a00fc7a..552dbfa 100644
--- a/hw/application_fpga/fw/tk1/assert.h
+++ b/hw/application_fpga/fw/tk1/assert.h
@@ -7,10 +7,9 @@
 #define ASSERT_H
 
 #define assert(expr)                                                           \
-	((expr) ? (void)(0)                                                    \
-		: assert_fail(#expr, __FILE__, __LINE__, __func__))
+	((expr) ? (void)(0) : assert_fail(#expr, __FILE__, __LINE__, __func__))
 
-void assert_fail(const char *assertion, const char *file,
-		   unsigned int line, const char *function);
+void assert_fail(const char *assertion, const char *file, unsigned int line,
+		 const char *function);
 
 #endif
diff --git a/hw/application_fpga/fw/tk1/lib.c b/hw/application_fpga/fw/tk1/lib.c
index a91b086..20b5edd 100644
--- a/hw/application_fpga/fw/tk1/lib.c
+++ b/hw/application_fpga/fw/tk1/lib.c
@@ -10,10 +10,10 @@
 #ifndef NOCONSOLE
 struct {
 	uint32_t arr[2];
-} volatile tohost __attribute__((section(".htif")));
+} static volatile tohost __attribute__((section(".htif")));
 struct {
 	uint32_t arr[2];
-} volatile fromhost __attribute__((section(".htif")));
+} /*@unused@*/ static volatile fromhost __attribute__((section(".htif")));
 
 static void htif_send(uint8_t dev, uint8_t cmd, int64_t data)
 {
@@ -38,17 +38,15 @@ static void htif_set_tohost(uint8_t dev, uint8_t cmd, int64_t data)
 	htif_send(dev, cmd, data);
 }
 
-static int htif_putchar(int ch)
+static void htif_putchar(char ch)
 {
-	htif_set_tohost(1, 1, ch & 0xff);
-	return ch & 0xff;
+	htif_set_tohost((uint8_t)1, (uint8_t)1, (int64_t)ch & 0xff);
 }
 
-int htif_puts(const char *s)
+void htif_puts(const char *s)
 {
-	while (*s)
+	while (*s != '\0')
 		htif_putchar(*s++);
-	return 0;
 }
 
 void htif_hexdump(void *buf, int len)
@@ -69,7 +67,7 @@ void htif_hexdump(void *buf, int len)
 	htif_lf();
 }
 
-void htif_putc(int ch)
+void htif_putc(char ch)
 {
 	htif_putchar(ch);
 }
@@ -104,7 +102,7 @@ void *memset(void *dest, int c, unsigned n)
 	uint8_t *s = dest;
 
 	for (; n; n--, s++)
-		*s = c;
+		*s = (uint8_t)c;
 
 	return dest;
 }
@@ -118,7 +116,7 @@ void memcpy_s(void *dest, size_t destsize, const void *src, size_t n)
 	uint8_t *src_byte = (uint8_t *)src;
 	uint8_t *dest_byte = (uint8_t *)dest;
 
-	for (int i = 0; i < n; i++) {
+	for (size_t i = 0; i < n; i++) {
 		dest_byte[i] = src_byte[i];
 	}
 }
@@ -132,17 +130,17 @@ void wordcpy_s(void *dest, size_t destsize, const void *src, size_t n)
 	uint32_t *src_word = (uint32_t *)src;
 	uint32_t *dest_word = (uint32_t *)dest;
 
-	for (int i = 0; i < n; i++) {
+	for (size_t i = 0; i < n; i++) {
 		dest_word[i] = src_word[i];
 	}
 }
 
-int memeq(void *dest, const void *src, unsigned n)
+int memeq(void *dest, const void *src, size_t n)
 {
 	uint8_t *src_byte = (uint8_t *)src;
 	uint8_t *dest_byte = (uint8_t *)dest;
 
-	for (int i = 0; i < n; i++) {
+	for (size_t i = 0; i < n; i++) {
 		if (dest_byte[i] != src_byte[i]) {
 			return 0;
 		}
diff --git a/hw/application_fpga/fw/tk1/lib.h b/hw/application_fpga/fw/tk1/lib.h
index 39adf95..72dc795 100644
--- a/hw/application_fpga/fw/tk1/lib.h
+++ b/hw/application_fpga/fw/tk1/lib.h
@@ -13,20 +13,20 @@
 #define htif_lf()
 #define htif_puthex(c)
 #define htif_putinthex(n)
-#define htif_puts(s) ((int)0)
+#define htif_puts(s)
 #define htif_hexdump(buf, len)
 #else
-void htif_putc(int ch);
+void htif_putc(char ch);
 void htif_lf();
 void htif_puthex(uint8_t c);
 void htif_putinthex(const uint32_t n);
-int htif_puts(const char *s);
+void htif_puts(const char *s);
 void htif_hexdump(void *buf, int len);
 #endif
 
 void *memset(void *dest, int c, unsigned n);
 void memcpy_s(void *dest, size_t destsize, const void *src, size_t n);
 void wordcpy_s(void *dest, size_t destsize, const void *src, size_t n);
-int memeq(void *dest, const void *src, unsigned n);
+int memeq(void *dest, const void *src, size_t n);
 
 #endif
diff --git a/hw/application_fpga/fw/tk1/main.c b/hw/application_fpga/fw/tk1/main.c
index 724a6c8..6ca9798 100644
--- a/hw/application_fpga/fw/tk1/main.c
+++ b/hw/application_fpga/fw/tk1/main.c
@@ -35,7 +35,7 @@ static volatile uint32_t *ram_scramble    = (volatile uint32_t *)TK1_MMIO_TK1_RA
 
 // Context for the loading of a TKey program
 struct context {
-	int left;	    // Bytes left to receive
+	uint32_t left;	    // Bytes left to receive
 	uint8_t digest[32]; // Program digest
 	uint8_t *loadaddr;  // Where we are currently loading a TKey program
 	uint8_t use_uss;    // Use USS?
@@ -45,8 +45,8 @@ struct context {
 static void print_hw_version();
 static void print_digest(uint8_t *md);
 static uint32_t rnd_word();
-static void compute_cdi(const uint8_t digest[32], const uint8_t use_uss,
-			const uint8_t uss[32]);
+static void compute_cdi(const uint8_t *digest, const uint8_t use_uss,
+			const uint8_t *uss);
 static void copy_name(uint8_t *buf, const size_t bufsiz, const uint32_t word);
 static enum state initial_commands(const struct frame_header *hdr,
 				   const uint8_t *cmd, enum state state,
@@ -89,8 +89,8 @@ static uint32_t rnd_word()
 }
 
 // CDI = blake2s(uds, blake2s(app), uss)
-static void compute_cdi(const uint8_t digest[32], const uint8_t use_uss,
-			const uint8_t uss[32])
+static void compute_cdi(const uint8_t *digest, const uint8_t use_uss,
+			const uint8_t *uss)
 {
 	uint32_t local_cdi[8];
 	blake2s_ctx secure_ctx = {0};
@@ -102,7 +102,7 @@ static void compute_cdi(const uint8_t digest[32], const uint8_t use_uss,
 	rnd_sleep = rnd_word();
 	// Up to 65536 cycles
 	rnd_sleep &= 0xffff;
-	*timer = (rnd_sleep == 0 ? 1 : rnd_sleep);
+	*timer = (uint32_t)(rnd_sleep == 0 ? 1 : rnd_sleep);
 	*timer_ctrl = (1 << TK1_MMIO_TIMER_CTRL_START_BIT);
 	while (*timer_status & (1 << TK1_MMIO_TIMER_STATUS_RUNNING_BIT)) {
 	}
@@ -123,14 +123,14 @@ static void compute_cdi(const uint8_t digest[32], const uint8_t use_uss,
 	}
 
 	// Write hashed result to Compound Device Identity (CDI)
-	blake2s_final(&secure_ctx, local_cdi);
+	blake2s_final(&secure_ctx, &local_cdi);
 
 	// Clear secure_ctx of any residue of UDS. Don't want to keep
 	// that for long even though fw_ram is cleared later.
-	memset(&secure_ctx, 0, sizeof(secure_ctx));
+	(void)memset(&secure_ctx, 0, sizeof(secure_ctx));
 
 	// CDI only word writable
-	wordcpy_s((void *)cdi, 8, local_cdi, 8);
+	wordcpy_s((void *)cdi, 8, &local_cdi, 8);
 }
 
 static void copy_name(uint8_t *buf, const size_t bufsiz, const uint32_t word)
@@ -177,8 +177,8 @@ static enum state initial_commands(const struct frame_header *hdr,
 		}
 
 		rsp[0] = STATUS_OK;
-		wordcpy_s(udi_words, 2, (void *)udi, 2);
-		memcpy_s(&rsp[1], CMDLEN_MAXBYTES - 1, udi_words, 2 * 4);
+		wordcpy_s(&udi_words, 2, (void *)udi, 2);
+		memcpy_s(&rsp[1], CMDLEN_MAXBYTES - 1, &udi_words, 2 * 4);
 		fwreply(*hdr, FW_RSP_GET_UDI, rsp);
 		// still initial state
 		break;
@@ -248,7 +248,7 @@ static enum state loading_commands(const struct frame_header *hdr,
 				   struct context *ctx)
 {
 	uint8_t rsp[CMDLEN_MAXBYTES] = {0};
-	int nbytes = 0;
+	uint32_t nbytes = 0;
 
 	switch (cmd[0]) {
 	case FW_CMD_LOAD_APP_DATA:
@@ -269,17 +269,19 @@ static enum state loading_commands(const struct frame_header *hdr,
 		ctx->left -= nbytes;
 
 		if (ctx->left == 0) {
+			blake2s_ctx b2s_ctx = {0};
+			int blake2err = 0;
+
 			htif_puts("Fully loaded ");
 			htif_putinthex(*app_size);
 			htif_lf();
 
 			// Compute Blake2S digest of the app,
 			// storing it for FW_STATE_RUN
-			blake2s_ctx b2s_ctx;
-
-			blake2s(&ctx->digest, 32, NULL, 0,
-				(const void *)TK1_RAM_BASE, *app_size,
-				&b2s_ctx);
+			blake2err = blake2s(&ctx->digest, 32, NULL, 0,
+					    (const void *)TK1_RAM_BASE,
+					    *app_size, &b2s_ctx);
+			assert(blake2err == 0);
 			print_digest(ctx->digest);
 
 			// And return the digest in final
@@ -323,6 +325,7 @@ static void run(const struct context *ctx)
 
 	// Clear the firmware stack
 	// clang-format off
+#ifndef S_SPLINT_S
 	asm volatile(
 		"li a0, 0xd0000000;" // FW_RAM
 		"li a1, 0xd0000800;" // End of 2 KB FW_RAM (just past the end)
@@ -331,6 +334,7 @@ static void run(const struct context *ctx)
 		"addi a0, a0, 4;"
 		"blt a0, a1, loop;"
 		::: "memory");
+#endif
 	// clang-format on
 
 	// Flip over to application mode
@@ -341,6 +345,7 @@ static void run(const struct context *ctx)
 
 	// Jump to app - doesn't return
 	// clang-format off
+#ifndef S_SPLINT_S
 	asm volatile(
 		// Get value at TK1_MMIO_TK1_APP_ADDR
 		"lui a0,0xff000;"
@@ -348,6 +353,7 @@ static void run(const struct context *ctx)
 		// Jump to it
 		"jalr x0,0(a0);"
 		::: "memory");
+#endif
 	// clang-format on
 
 	__builtin_unreachable();
diff --git a/hw/application_fpga/fw/tk1/proto.c b/hw/application_fpga/fw/tk1/proto.c
index aa7c1c4..13c1910 100644
--- a/hw/application_fpga/fw/tk1/proto.c
+++ b/hw/application_fpga/fw/tk1/proto.c
@@ -17,7 +17,14 @@ static volatile uint32_t *can_tx = (volatile uint32_t *)TK1_MMIO_UART_TX_STATUS;
 static volatile uint32_t *tx =     (volatile uint32_t *)TK1_MMIO_UART_TX_DATA;
 // clang-format on
 
-uint8_t genhdr(uint8_t id, uint8_t endpoint, uint8_t status, enum cmdlen len)
+static uint8_t genhdr(uint8_t id, uint8_t endpoint, uint8_t status,
+		      enum cmdlen len);
+static int parseframe(uint8_t b, struct frame_header *hdr);
+static void write(uint8_t *buf, size_t nbytes);
+static int read(uint8_t *buf, size_t bufsize, size_t nbytes);
+
+static uint8_t genhdr(uint8_t id, uint8_t endpoint, uint8_t status,
+		      enum cmdlen len)
 {
 	return (id << 5) | (endpoint << 3) | (status << 2) | len;
 }
@@ -34,7 +41,7 @@ int readcommand(struct frame_header *hdr, uint8_t *cmd, int state)
 		return -1;
 	}
 
-	memset(cmd, 0, CMDLEN_MAXBYTES);
+	(void)memset(cmd, 0, CMDLEN_MAXBYTES);
 	// Now we know the size of the cmd frame, read it all
 	if (read(cmd, CMDLEN_MAXBYTES, hdr->len) != 0) {
 		htif_puts("read: buffer overrun\n");
@@ -50,7 +57,7 @@ int readcommand(struct frame_header *hdr, uint8_t *cmd, int state)
 	return 0;
 }
 
-int parseframe(uint8_t b, struct frame_header *hdr)
+static int parseframe(uint8_t b, struct frame_header *hdr)
 {
 	if ((b & 0x80) != 0) {
 		// Bad version
@@ -147,7 +154,7 @@ void writebyte(uint8_t b)
 	}
 }
 
-void write(uint8_t *buf, size_t nbytes)
+static void write(uint8_t *buf, size_t nbytes)
 {
 	for (int i = 0; i < nbytes; i++) {
 		writebyte(buf[i]);
@@ -163,7 +170,7 @@ uint8_t readbyte()
 	}
 }
 
-int read(uint8_t *buf, size_t bufsize, size_t nbytes)
+static int read(uint8_t *buf, size_t bufsize, size_t nbytes)
 {
 	if (nbytes > bufsize) {
 		return -1;
diff --git a/hw/application_fpga/fw/tk1/proto.h b/hw/application_fpga/fw/tk1/proto.h
index 7ed21db..d99f0e5 100644
--- a/hw/application_fpga/fw/tk1/proto.h
+++ b/hw/application_fpga/fw/tk1/proto.h
@@ -50,12 +50,8 @@ struct frame_header {
 	enum cmdlen len;
 };
 
-uint8_t genhdr(uint8_t id, uint8_t endpoint, uint8_t status, enum cmdlen len);
-int parseframe(uint8_t b, struct frame_header *hdr);
-void fwreply(struct frame_header hdr, enum fwcmd rspcode, uint8_t *buf);
 void writebyte(uint8_t b);
-void write(uint8_t *buf, size_t nbytes);
 uint8_t readbyte();
-int read(uint8_t *buf, size_t bufsize, size_t nbytes);
+void fwreply(struct frame_header hdr, enum fwcmd rspcode, uint8_t *buf);
 int readcommand(struct frame_header *hdr, uint8_t *cmd, int state);
 #endif