diff --git a/regressions/ck_ec/validate/Makefile b/regressions/ck_ec/validate/Makefile
index f03f49387..68ff14c45 100644
--- a/regressions/ck_ec/validate/Makefile
+++ b/regressions/ck_ec/validate/Makefile
@@ -48,13 +48,13 @@ ck_ec_smoke_test: ../../../src/ck_ec.c ck_ec_smoke_test.c ../../../src/ck_ec_tim
 prop_test_slow_wakeup: ../../../src/ck_ec.c prop_test_slow_wakeup.c ../../../src/ck_ec_timeutil.h ../../../include/ck_ec.h fuzz_harness.h
 	$(CC) $(CFLAGS) $(FUZZ_CFLAGS) ../../../src/ck_ec.c -o prop_test_slow_wakeup prop_test_slow_wakeup.c
 
-prop_test_timeutil_add: ../../../src/ck_ec.c prop_test_timeutil_add.c ../../../src/ck_ec_timeutil.h ../../../include/ck_ec.h fuzz_harness.h
+prop_test_timeutil_add: ../../../src/ck_ec.c prop_test_timeutil_add.c ../../../src/ck_ec_timeutil.h ../../../include/ck_ec.h fuzz_harness.h int128.h
 	$(CC) $(CFLAGS) $(FUZZ_CFLAGS) ../../../src/ck_ec.c -o prop_test_timeutil_add prop_test_timeutil_add.c
 
-prop_test_timeutil_add_ns: ../../../src/ck_ec.c prop_test_timeutil_add_ns.c ../../../src/ck_ec_timeutil.h ../../../include/ck_ec.h fuzz_harness.h
+prop_test_timeutil_add_ns: ../../../src/ck_ec.c prop_test_timeutil_add_ns.c ../../../src/ck_ec_timeutil.h ../../../include/ck_ec.h fuzz_harness.h int128.h
 	$(CC) $(CFLAGS) $(FUZZ_CFLAGS) ../../../src/ck_ec.c -o prop_test_timeutil_add_ns prop_test_timeutil_add_ns.c
 
-prop_test_timeutil_cmp: ../../../src/ck_ec.c prop_test_timeutil_cmp.c ../../../src/ck_ec_timeutil.h ../../../include/ck_ec.h fuzz_harness.h
+prop_test_timeutil_cmp: ../../../src/ck_ec.c prop_test_timeutil_cmp.c ../../../src/ck_ec_timeutil.h ../../../include/ck_ec.h fuzz_harness.h int128.h
 	$(CC) $(CFLAGS) $(FUZZ_CFLAGS) ../../../src/ck_ec.c -o prop_test_timeutil_cmp prop_test_timeutil_cmp.c
 
 prop_test_timeutil_scale: ../../../src/ck_ec.c prop_test_timeutil_scale.c ../../../src/ck_ec_timeutil.h ../../../include/ck_ec.h fuzz_harness.h
diff --git a/regressions/ck_ec/validate/int128.h b/regressions/ck_ec/validate/int128.h
new file mode 100644
index 000000000..08e338269
--- /dev/null
+++ b/regressions/ck_ec/validate/int128.h
@@ -0,0 +1,96 @@
+#ifndef CK_INT128_H
+#define CK_INT128_H
+
+#include <ck_stdint.h>
+
+typedef struct ck_s128 {
+	uint64_t hi;
+	uint64_t lo;
+} ck_s128_t;
+
+static inline ck_s128_t
+ck_s128_make_s64(int64_t value)
+{
+	return (ck_s128_t) {
+		value < 0 ? (uint64_t)-1 : 0,
+		(uint64_t)value,
+	};
+}
+
+static inline int
+ck_s128_cmp(ck_s128_t lhs, ck_s128_t rhs)
+{
+	if ((int64_t)lhs.hi < (int64_t)rhs.hi) {
+		return -1;
+	}
+
+	if ((int64_t)lhs.hi > (int64_t)rhs.hi) {
+		return 1;
+	}
+
+	if (lhs.lo < rhs.lo) {
+		return -1;
+	}
+
+	if (lhs.lo > rhs.lo) {
+		return 1;
+	}
+
+	return 0;
+}
+
+static inline ck_s128_t
+ck_s128_add(ck_s128_t lhs, ck_s128_t rhs)
+{
+	return (ck_s128_t) {
+		lhs.hi + rhs.hi + ((lhs.lo + rhs.lo) < lhs.lo),
+		lhs.lo + rhs.lo,
+	};
+}
+
+static inline ck_s128_t
+ck_s128_mul(ck_s128_t lhs, ck_s128_t rhs)
+{
+	/*
+	 * A s128 represents hi * 2^64 + lo. Multiplying two s128 values gives
+	 * four terms:
+	 *
+	 *     lhs.lo * rhs.lo
+	 *     lhs.hi * rhs.lo * 2^64
+	 *     lhs.lo * rhs.hi * 2^64
+	 *     lhs.hi * rhs.hi * 2^128
+	 *
+	 * We need only the low 128 bits, so the last term can be ignored. The
+	 * middle two terms contribute only to result.hi.
+	 *
+	 * Computing lhs.lo * rhs.lo still requires a 128-bit result. We split
+	 * both 64-bit values into 32-bit halves:
+	 *
+	 *     lhs.lo = a * 2^32 + b
+	 *     rhs.lo = c * 2^32 + d
+	 *
+	 * Then:
+	 *
+	 *     lhs.lo * rhs.lo = a*c * 2^64 + (a*d + b*c) * 2^32 + b*d
+	 *
+	 * Inspired by Abseil's int128 implementation:
+	 * https://github.com/abseil/abseil-cpp/blob/20260526.0/absl/numeric/int128.h#L1035
+	 */
+	uint64_t a = lhs.lo >> 32;
+	uint64_t b = (uint32_t)lhs.lo;
+	uint64_t c = rhs.lo >> 32;
+	uint64_t d = (uint32_t)rhs.lo;
+
+	ck_s128_t result = (ck_s128_t) {
+		(lhs.hi * rhs.lo) + (lhs.lo * rhs.hi) + (a * c),
+		(b * d),
+	};
+	result = ck_s128_add(result,
+	    (ck_s128_t) { (a * d) >> 32, (a * d) << 32 });
+	result = ck_s128_add(result,
+	    (ck_s128_t) { (b * c) >> 32, (b * c) << 32 });
+
+	return result;
+}
+
+#endif /* CK_INT128_H */
diff --git a/regressions/ck_ec/validate/prop_test_timeutil_add.c b/regressions/ck_ec/validate/prop_test_timeutil_add.c
index bd44607aa..28847dc44 100644
--- a/regressions/ck_ec/validate/prop_test_timeutil_add.c
+++ b/regressions/ck_ec/validate/prop_test_timeutil_add.c
@@ -1,15 +1,9 @@
 #include <assert.h>
-#include <ck_limits.h>
 #include <ck_stdint.h>
 
 #include "../../../src/ck_ec_timeutil.h"
 #include "fuzz_harness.h"
-
-#if ULONG_MAX > 4294967295
-typedef unsigned __int128 dword_t;
-#else
-typedef uint64_t dword_t;
-#endif
+#include "int128.h"
 
 struct example {
 	struct timespec ts;
@@ -75,9 +69,12 @@ static struct timespec normalize_ts(const struct timespec ts)
 	return ret;
 }
 
-static dword_t ts_to_nanos(const struct timespec ts)
+static ck_s128_t ts_to_nanos(const struct timespec ts)
 {
-	return (dword_t)ts.tv_sec * (NSEC_MAX + 1) + ts.tv_nsec;
+	ck_s128_t ret = ck_s128_mul(ck_s128_make_s64(ts.tv_sec),
+	    ck_s128_make_s64(NSEC_MAX + 1));
+	ret = ck_s128_add(ret, ck_s128_make_s64(ts.tv_nsec));
+	return ret;
 }
 
 static inline int test_timespec_add(const struct example *example)
@@ -85,14 +82,18 @@ static inline int test_timespec_add(const struct example *example)
 	const struct timespec ts = normalize_ts(example->ts);
 	const struct timespec inc = normalize_ts(example->inc);
 	const struct timespec actual = timespec_add(ts, inc);
-	const dword_t nanos = ts_to_nanos(ts) + ts_to_nanos(inc);
+	const ck_s128_t nanos = ck_s128_add(ts_to_nanos(ts), ts_to_nanos(inc));
+
+	const ck_s128_t ceiling = ts_to_nanos(
+	    (struct timespec) { TIME_MAX, NSEC_MAX });
 
-	if (nanos / (NSEC_MAX + 1) > TIME_MAX) {
+	if (ck_s128_cmp(nanos, ceiling) > 0) {
 		assert(actual.tv_sec == TIME_MAX);
 		assert(actual.tv_nsec == NSEC_MAX);
 	} else {
-		assert(actual.tv_sec == (time_t)(nanos / (NSEC_MAX + 1)));
-		assert(actual.tv_nsec == (long)(nanos % (NSEC_MAX + 1)));
+		assert(ck_s128_cmp(ts_to_nanos(actual), nanos) == 0);
+		assert(actual.tv_nsec >= 0);
+		assert(actual.tv_nsec <= NSEC_MAX);
 	}
 
 	return 0;
diff --git a/regressions/ck_ec/validate/prop_test_timeutil_add_ns.c b/regressions/ck_ec/validate/prop_test_timeutil_add_ns.c
index b62e1c7d7..f775f1540 100644
--- a/regressions/ck_ec/validate/prop_test_timeutil_add_ns.c
+++ b/regressions/ck_ec/validate/prop_test_timeutil_add_ns.c
@@ -2,12 +2,7 @@
 
 #include "../../../src/ck_ec_timeutil.h"
 #include "fuzz_harness.h"
-
-#if ULONG_MAX > 4294967295
-typedef unsigned __int128 dword_t;
-#else
-typedef uint64_t dword_t;
-#endif
+#include "int128.h"
 
 struct example {
 	struct timespec ts;
@@ -45,41 +40,55 @@ static const struct example examples[] = {
 	}
 };
 
-static inline int test_timespec_add_ns(const struct example *example)
+static struct timespec normalize_ts(const struct timespec ts)
 {
-	struct timespec ts = {
-		.tv_sec = example->ts.tv_sec,
-		.tv_nsec = example->ts.tv_nsec
-	};
-	const uint32_t ns = example->ns;
+	struct timespec ret = ts;
 
-	if (ts.tv_sec < 0) {
-		ts.tv_sec = ~ts.tv_sec;
+	if (ret.tv_sec < 0) {
+		ret.tv_sec = ~ret.tv_sec;
 	}
 
-	if (ts.tv_nsec < 0) {
-		ts.tv_nsec = ~ts.tv_nsec;
+	if (ret.tv_nsec < 0) {
+		ret.tv_nsec = ~ret.tv_nsec;
 	}
 
-	ts.tv_nsec %= NSEC_MAX + 1;
+	ret.tv_nsec %= NSEC_MAX + 1;
+	return ret;
+}
+
+static ck_s128_t ts_to_nanos(const struct timespec ts)
+{
+	ck_s128_t ret = ck_s128_mul(ck_s128_make_s64(ts.tv_sec),
+	    ck_s128_make_s64(NSEC_MAX + 1));
+	ret = ck_s128_add(ret, ck_s128_make_s64(ts.tv_nsec));
+	return ret;
+}
+
+static inline int test_timespec_add_ns(const struct example *example)
+{
+	const struct timespec ts = normalize_ts(example->ts);
+	const uint32_t ns = example->ns;
 
 	const struct timespec actual = timespec_add_ns(ts, ns);
 
-	dword_t nanos =
-	    (dword_t)ts.tv_sec * (NSEC_MAX + 1) + ts.tv_nsec;
+	ck_s128_t nanos = ts_to_nanos(ts);
 
 	if (ns > NSEC_MAX) {
-		nanos += NSEC_MAX + 1;
+		nanos = ck_s128_add(nanos, ck_s128_make_s64(NSEC_MAX + 1));
 	} else {
-		nanos += ns;
+		nanos = ck_s128_add(nanos, ck_s128_make_s64(ns));
 	}
 
-	if (nanos / (NSEC_MAX + 1) > TIME_MAX) {
+	const ck_s128_t ceiling = ts_to_nanos(
+	    (struct timespec) { TIME_MAX, NSEC_MAX });
+
+	if (ck_s128_cmp(nanos, ceiling) > 0) {
 		assert(actual.tv_sec == TIME_MAX);
 		assert(actual.tv_nsec == NSEC_MAX);
 	} else {
-		assert(actual.tv_sec == (time_t)(nanos / (NSEC_MAX + 1)));
-		assert(actual.tv_nsec == (long)(nanos % (NSEC_MAX + 1)));
+		assert(ck_s128_cmp(ts_to_nanos(actual), nanos) == 0);
+		assert(actual.tv_nsec >= 0);
+		assert(actual.tv_nsec <= NSEC_MAX);
 	}
 
 	return 0;
diff --git a/regressions/ck_ec/validate/prop_test_timeutil_cmp.c b/regressions/ck_ec/validate/prop_test_timeutil_cmp.c
index 00e7b2e64..d98b2655f 100644
--- a/regressions/ck_ec/validate/prop_test_timeutil_cmp.c
+++ b/regressions/ck_ec/validate/prop_test_timeutil_cmp.c
@@ -2,12 +2,7 @@
 
 #include "../../../src/ck_ec_timeutil.h"
 #include "fuzz_harness.h"
-
-#if ULONG_MAX > 4294967295
-typedef __int128 dsword_t;
-#else
-typedef int64_t dsword_t;
-#endif
+#include "int128.h"
 
 struct example {
 	struct timespec x;
@@ -69,25 +64,28 @@ static struct timespec normalize_ts(const struct timespec ts)
 	return ret;
 }
 
-static dsword_t ts_to_nanos(const struct timespec ts)
+static ck_s128_t ts_to_nanos(const struct timespec ts)
 {
-	return (dsword_t)ts.tv_sec * (NSEC_MAX + 1) + ts.tv_nsec;
+	ck_s128_t ret = ck_s128_mul(ck_s128_make_s64(ts.tv_sec),
+	    ck_s128_make_s64(NSEC_MAX + 1));
+	ret = ck_s128_add(ret, ck_s128_make_s64(ts.tv_nsec));
+	return ret;
 }
 
 static inline int test_timespec_cmp(const struct example *example)
 {
 	const struct timespec x = normalize_ts(example->y);
 	const struct timespec y = normalize_ts(example->x);
-	const dsword_t x_nanos = ts_to_nanos(x);
-	const dsword_t y_nanos = ts_to_nanos(y);
+	const ck_s128_t x_nanos = ts_to_nanos(x);
+	const ck_s128_t y_nanos = ts_to_nanos(y);
 
 	assert(timespec_cmp(x, x) == 0);
 	assert(timespec_cmp(y, y) == 0);
 	assert(timespec_cmp(x, y) == -timespec_cmp(y, x));
 
-	if (x_nanos == y_nanos) {
+	if (ck_s128_cmp(x_nanos, y_nanos) == 0) {
 		assert(timespec_cmp(x, y) == 0);
-	} else if (x_nanos < y_nanos) {
+	} else if (ck_s128_cmp(x_nanos, y_nanos) < 0) {
 		assert(timespec_cmp(x, y) == -1);
 	} else {
 		assert(timespec_cmp(x, y) == 1);