diff --git a/scripts/data_files/vs2010-app-template.vcxproj b/scripts/data_files/vs2010-app-template.vcxproj
index 1db7ee4..5480a44 100644
--- a/scripts/data_files/vs2010-app-template.vcxproj
+++ b/scripts/data_files/vs2010-app-template.vcxproj
Binary files differ
diff --git a/scripts/data_files/vs2010-main-template.vcxproj b/scripts/data_files/vs2010-main-template.vcxproj
index 773b58a..7071cd2 100644
--- a/scripts/data_files/vs2010-main-template.vcxproj
+++ b/scripts/data_files/vs2010-main-template.vcxproj
@@ -85,8 +85,8 @@
       </PrecompiledHeader>
       <WarningLevel>Level3</WarningLevel>
       <Optimization>Disabled</Optimization>
-      <PreprocessorDefinitions>WIN32;_DEBUG;_WINDOWS;_USRDLL;MBEDTLS_EXPORTS;%(PreprocessorDefinitions)</PreprocessorDefinitions>
-      <AdditionalIncludeDirectories>../../include</AdditionalIncludeDirectories>
+      <PreprocessorDefinitions>WIN32;_DEBUG;_WINDOWS;_USRDLL;MBEDTLS_EXPORTS;KRML_VERIFIED_UINT128;%(PreprocessorDefinitions)</PreprocessorDefinitions>
+      <AdditionalIncludeDirectories>../../include;../../3rdparty/everest/include/;../../3rdparty/everest/include/everest;../../3rdparty/everest/include/everest/vs2010;../../3rdparty/everest/include/everest/kremlib</AdditionalIncludeDirectories>
       <CompileAs>CompileAsC</CompileAs>
     </ClCompile>
     <Link>
@@ -100,8 +100,8 @@
       </PrecompiledHeader>
       <WarningLevel>Level3</WarningLevel>
       <Optimization>Disabled</Optimization>
-      <PreprocessorDefinitions>WIN32;_DEBUG;_WINDOWS;_USRDLL;MBEDTLS_EXPORTS;%(PreprocessorDefinitions)</PreprocessorDefinitions>
-      <AdditionalIncludeDirectories>../../include</AdditionalIncludeDirectories>
+      <PreprocessorDefinitions>WIN32;_DEBUG;_WINDOWS;_USRDLL;MBEDTLS_EXPORTS;KRML_VERIFIED_UINT128;%(PreprocessorDefinitions)</PreprocessorDefinitions>
+      <AdditionalIncludeDirectories>../../include;../../3rdparty/everest/include/;../../3rdparty/everest/include/everest;../../3rdparty/everest/include/everest/vs2010;../../3rdparty/everest/include/everest/kremlib</AdditionalIncludeDirectories>
       <CompileAs>CompileAsC</CompileAs>
     </ClCompile>
     <Link>
@@ -117,8 +117,8 @@
       <Optimization>MaxSpeed</Optimization>
       <FunctionLevelLinking>true</FunctionLevelLinking>
       <IntrinsicFunctions>true</IntrinsicFunctions>
-      <PreprocessorDefinitions>WIN32;NDEBUG;_WINDOWS;_USRDLL;MBEDTLS_EXPORTS;%(PreprocessorDefinitions)</PreprocessorDefinitions>
-      <AdditionalIncludeDirectories>../../include</AdditionalIncludeDirectories>
+      <PreprocessorDefinitions>WIN32;NDEBUG;_WINDOWS;_USRDLL;MBEDTLS_EXPORTS;KRML_VERIFIED_UINT128;%(PreprocessorDefinitions)</PreprocessorDefinitions>
+      <AdditionalIncludeDirectories>../../include;../../3rdparty/everest/include/;../../3rdparty/everest/include/everest;../../3rdparty/everest/include/everest/vs2010;../../3rdparty/everest/include/everest/kremlib</AdditionalIncludeDirectories>
     </ClCompile>
     <Link>
       <SubSystem>Windows</SubSystem>
@@ -135,8 +135,8 @@
       <Optimization>MaxSpeed</Optimization>
       <FunctionLevelLinking>true</FunctionLevelLinking>
       <IntrinsicFunctions>true</IntrinsicFunctions>
-      <PreprocessorDefinitions>WIN64;NDEBUG;_WINDOWS;_USRDLL;MBEDTLS_EXPORTS;%(PreprocessorDefinitions)</PreprocessorDefinitions>
-      <AdditionalIncludeDirectories>../../include</AdditionalIncludeDirectories>
+      <PreprocessorDefinitions>WIN64;NDEBUG;_WINDOWS;_USRDLL;MBEDTLS_EXPORTS;KRML_VERIFIED_UINT128;%(PreprocessorDefinitions)</PreprocessorDefinitions>
+      <AdditionalIncludeDirectories>../../include;../../3rdparty/everest/include/;../../3rdparty/everest/include/everest;../../3rdparty/everest/include/everest/vs2010;../../3rdparty/everest/include/everest/kremlib</AdditionalIncludeDirectories>
     </ClCompile>
     <Link>
       <SubSystem>Windows</SubSystem>
diff --git a/scripts/generate_visualc_files.pl b/scripts/generate_visualc_files.pl
index 42f3024..5d07b88 100755
--- a/scripts/generate_visualc_files.pl
+++ b/scripts/generate_visualc_files.pl
@@ -22,6 +22,8 @@
 my $mbedtls_header_dir = 'include/mbedtls';
 my $psa_header_dir = 'include/psa';
 my $source_dir = 'library';
+my $everest_header_dir = '3rdparty/everest/include/everest';
+my @everest_source_dirs = ('3rdparty/everest/library', '3rdparty/everest/library/kremlib', '3rdparty/everest/library/vs2010');
 
 # Need windows line endings!
 my $vsx_hdr_tpl = <<EOT;
@@ -53,9 +55,11 @@
 exit( main() );
 
 sub check_dirs {
+    foreach my $d (@everest_source_dirs) { if (not (-d $d)) { return 0; } }
     return -d $vsx_dir
         && -d $mbedtls_header_dir
         && -d $psa_header_dir
+        && -d $everest_header_dir
         && -d $source_dir
         && -d $programs_dir;
 }
@@ -139,12 +143,14 @@
 }
 
 sub gen_main_file {
-    my ($mbedtls_headers, $psa_headers, $source_headers, $sources, $hdr_tpl, $src_tpl, $main_tpl, $main_out) = @_;
+    my ($mbedtls_headers, $psa_headers, $source_headers, $everest_headers, $sources, $everest_sources, $hdr_tpl, $src_tpl, $main_tpl, $main_out) = @_;
 
     my $header_entries = gen_entry_list( $hdr_tpl, @$mbedtls_headers );
     $header_entries .= gen_entry_list( $hdr_tpl, @$psa_headers );
     $header_entries .= gen_entry_list( $hdr_tpl, @$source_headers );
+    $header_entries .= gen_entry_list( $hdr_tpl, @$everest_headers );
     my $source_entries = gen_entry_list( $src_tpl, @$sources );
+    $source_entries .= gen_entry_list( $src_tpl, @$everest_sources );
 
     my $out = slurp_file( $main_tpl );
     $out =~ s/SOURCE_ENTRIES\r\n/$source_entries/m;
@@ -205,11 +211,18 @@
     map { s!/!\\!g } @psa_headers;
     map { s!/!\\!g } @sources;
 
+    my @everest_headers = <$everest_header_dir/*.h>;
+    my @everest_sources = ();
+    foreach my $d (@everest_source_dirs) { push @everest_sources, <$d/*.c>; }
+    @everest_sources = grep !/3rdparty\/everest\/library\/Hacl_Curve25519.c/, @everest_sources;
+    map { s!/!\\!g } @everest_headers;
+    map { s!/!\\!g } @everest_sources;
+
     gen_app_files( @app_list );
 
     gen_main_file( \@mbedtls_headers, \@psa_headers, \@source_headers,
-                   \@sources, $vsx_hdr_tpl, $vsx_src_tpl,
-                   $vsx_main_tpl_file, $vsx_main_file );
+                   \@everest_headers, \@sources, \@everest_sources, $vsx_hdr_tpl,
+                   $vsx_src_tpl, $vsx_main_tpl_file, $vsx_main_file );
 
     gen_vsx_solution( @app_list );