diff --git a/CMakeLists.txt b/CMakeLists.txt
index 67ec7ccee..9ab1f3f9c 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -181,6 +181,8 @@ else()
     set(LIB_INSTALL_DIR lib)
 endif()
 
+include_directories(include/ 3rdparty/everest/include/ 3rdparty/everest/include/everest/ 3rdparty/everest/include/everest/kremlin/ 3rdparty/everest/include/everest/kremlib/)
+
 if(ENABLE_ZLIB_SUPPORT)
     find_package(ZLIB)
 
diff --git a/include/CMakeLists.txt b/include/CMakeLists.txt
index c2f2bd4e6..ef33fe828 100644
--- a/include/CMakeLists.txt
+++ b/include/CMakeLists.txt
@@ -3,8 +3,9 @@ option(INSTALL_MBEDTLS_HEADERS "Install mbed TLS headers." ON)
 if(INSTALL_MBEDTLS_HEADERS)
 
     file(GLOB headers "mbedtls/*.h")
+    file(GLOB headers_everest "../3rdparty/everest/include/*.h")
 
-    install(FILES ${headers}
+    install(FILES ${headers} ${headers_everest}
         DESTINATION include/mbedtls
         PERMISSIONS OWNER_READ OWNER_WRITE GROUP_READ WORLD_READ)
 
diff --git a/library/CMakeLists.txt b/library/CMakeLists.txt
index c82784ee1..d1cf26fef 100644
--- a/library/CMakeLists.txt
+++ b/library/CMakeLists.txt
@@ -66,6 +66,16 @@ set(src_crypto
     xtea.c
 )
 
+set(src_everest
+    ../3rdparty/everest/library/everest.c
+    ../3rdparty/everest/library/Hacl_Curve25519.c
+    ../3rdparty/everest/library/x25519.c
+    ../3rdparty/everest/library/kremlib/fstar_uint128.c
+    ../3rdparty/everest/library/kremlib/FStar_UInt64_FStar_UInt32_FStar_UInt16_FStar_UInt8.c
+)
+
+set(src_crypto ${src_crypto} ${src_everest})
+
 set(src_x509
     certs.c
     pkcs11.c
diff --git a/library/Makefile b/library/Makefile
index af472ad93..a75775228 100644
--- a/library/Makefile
+++ b/library/Makefile
@@ -18,6 +18,9 @@ endif
 # To compile on Plan9:
 # CFLAGS += -D_BSD_EXTENSION
 
+# Include directories for Everest code
+CFLAGS+=-I../3rdparty/everest/include -I../3rdparty/everest/include/everest -I../3rdparty/everest/include/everest/kremlib
+
 # if were running on Windows build for Windows
 ifdef WINDOWS
 WINDOWS_BUILD=1
@@ -70,6 +73,13 @@ LOCAL_LDFLAGS += -L../crypto/library
 LOCAL_CFLAGS += -I../crypto/include
 CRYPTO := ../crypto/library/
 
+OBJS_CRYPTO+= \
+		../3rdparty/everest/library/everest.o \
+		../3rdparty/everest/library/Hacl_Curve25519.o \
+		../3rdparty/everest/library/x25519.o \
+		../3rdparty/everest/library/kremlib/fstar_uint128.o \
+		../3rdparty/everest/library/kremlib/FStar_UInt64_FStar_UInt32_FStar_UInt16_FStar_UInt8.o
+
 OBJS_X509=	certs.o		pkcs11.o	x509.o		\
 		x509_create.o	x509_crl.o	x509_crt.o	\
 		x509_csr.o	x509write_crt.o	x509write_csr.o
@@ -153,11 +163,12 @@ libmbedcrypto.%:
 
 .c.o:
 	echo "  CC    $<"
-	$(CC) $(LOCAL_CFLAGS) $(CFLAGS) -c $<
+	$(CC) $(LOCAL_CFLAGS) $(CFLAGS) -o $@ -c $<
 
 clean:
 ifndef WINDOWS
-	rm -f *.o libmbed*
+	rm -f *.o libmbed* $(OBJS_CRYPTO)
 else
-	del /Q /F *.o libmbed*
+	del /Q /F *.o libmbed* $(OBJS_CRYPTO)
 endif
+
diff --git a/programs/Makefile b/programs/Makefile
index 857be7837..f09487712 100644
--- a/programs/Makefile
+++ b/programs/Makefile
@@ -18,6 +18,8 @@ LOCAL_LDFLAGS += -L../crypto/library
 LOCAL_CFLAGS += -I../crypto/include
 LOCAL_CXXFLAGS += -I../crypto/include
 
+LOCAL_CFLAGS+=-I../3rdparty/everest/include
+
 ifndef SHARED
 DEP=../crypto/library/libmbedcrypto.a ../library/libmbedx509.a ../library/libmbedtls.a
 else
diff --git a/tests/Makefile b/tests/Makefile
index 1679ee40b..d1c265e52 100644
--- a/tests/Makefile
+++ b/tests/Makefile
@@ -16,6 +16,8 @@ LOCAL_LDFLAGS += -L../crypto/library
 LOCAL_CFLAGS += -I../crypto/include
 CRYPTO := ../crypto/library/
 
+LOCAL_CFLAGS+=-I../3rdparty/everest/include
+
 # Enable definition of various functions used throughout the testsuite
 # (gethostname, strdup, fileno...) even when compiling with -std=c99. Harmless
 # on non-POSIX platforms.
@@ -185,4 +187,3 @@ $(EMBEDDED_TESTS): embedded_%: suites/$$(firstword $$(subst ., ,$$*)).function s
 		-o ./TESTS/mbedtls/$*
 
 generate-target-tests: $(EMBEDDED_TESTS)
-