diff --git a/.gitignore b/.gitignore
index 9ea63b89b..19c432731 100644
--- a/.gitignore
+++ b/.gitignore
@@ -17,6 +17,7 @@
 /spec/cspec/*/c/plat/
 /spec/cspec/*/c/sources_list_updated
 /spec/cspec/*/c/autoconf.h
+/spec/cspec/*/c/build
 
 /spec/haskell/doc/**/*.aux
 /spec/haskell/doc/**/*.bbl
diff --git a/spec/Makefile b/spec/Makefile
index 671dddc51..918734a55 100644
--- a/spec/Makefile
+++ b/spec/Makefile
@@ -42,7 +42,7 @@ ExecSpec ASpec : design-spec
 
 # Preprocess the kernel's source code and bitfield theory files.
 c-kernel: c-parser .FORCE
-	cd cspec/$(L4V_ARCH)/c && L4V_REPO_PATH=$(L4V_REPO_PATH) $(MAKE) cspec
+	cd cspec/$(L4V_ARCH)/c && L4V_REPO_PATH=$(L4V_REPO_PATH) L4V_ARCH=$(L4V_ARCH) $(MAKE) cspec
 .PHONY: c-kernel
 
 # Run the haskell translator
diff --git a/spec/cspec/ARM/KernelInc_C.thy b/spec/cspec/ARM/KernelInc_C.thy
index 6cefc75e4..52ad7ff7a 100644
--- a/spec/cspec/ARM/KernelInc_C.thy
+++ b/spec/cspec/ARM/KernelInc_C.thy
@@ -12,10 +12,10 @@ theory KernelInc_C
 imports
   Kernel_C
   "../Substitute"
-  "c/arch/object/structures_defs"
-  "c/arch/object/structures_proofs"
-  "c/32/mode/api/shared_types_defs"
-  "c/32/mode/api/shared_types_proofs"
+  "c/build/generated/arch/object/structures_defs"
+  "c/build/generated/arch/object/structures_proofs"
+  "c/build/generated/mode/api/shared_types_defs"
+  "c/build/generated/mode/api/shared_types_proofs"
 begin
 
 end
diff --git a/spec/cspec/ARM/c/Makefile b/spec/cspec/ARM/c/Makefile
index 08d5a81c2..bea03e0a6 100644
--- a/spec/cspec/ARM/c/Makefile
+++ b/spec/cspec/ARM/c/Makefile
@@ -17,10 +17,6 @@ export PATH
 TOOLPREFIX ?= arm-none-eabi-
 SHELL=bash
 
-ARCH=arm
-ARMV=armv7-a
-PLAT=imx6
-CPU=cortex-a9
 CONFIG_DOMAIN_SCHEDULE=config_sched.c
 
 ifeq ($(shell which ${TOOLPREFIX}cpp),)
@@ -33,18 +29,33 @@ ifeq ($(shell which ${TOOLPREFIX}cpp),)
 endif
 
 # modifies are produced by the parser
-SKIP_MODIFIES=1
+SKIP_MODIFIES=ON
 FASTPATH=yes
 CSPEC_DIR=..
 
+build/CMakeCache.txt:
+	mkdir -p build
+	cd build && \
+	cmake -DCROSS_COMPILER_PREFIX=${TOOLPREFIX} \
+		-DCMAKE_TOOLCHAIN_FILE=../${SOURCE_ROOT}/gcc.cmake -C ../${SOURCE_ROOT}/configs/${L4V_ARCH}_verified.cmake \
+		-DCSPEC_DIR=`pwd`/../${CSPEC_DIR} \
+		-DSKIP_MODIFIES=${SKIP_MODIFIES} \
+		-DUMM_TYPES=`pwd`/../${UMM_TYPES} \
+		-DKernelDomainSchedule=`pwd`/../${CONFIG_DOMAIN_SCHEDULE} -G Ninja ../${SOURCE_ROOT}
+
+kernel_all_pp: build/CMakeCache.txt
+	cd build && ninja kernel_all_pp_wrapper
+	cp -a build/kernel_all_pp.c kernel_all.c_pp
+
+.PHONY: kernel_all_pp
+
 # called by ../../spec/Makefile
-cspec: kernel_all.c_pp ${UMM_TYPES} theories
-# theories is defined in seL4 makefile
+cspec: ${UMM_TYPES} kernel_all_pp
+	cd build && ninja kernel_theories
+
 .PHONY: cspec
 
 # Create "umm_types" if necessary.
-${UMM_TYPES}: kernel_all.c_pp
-	python ../../mk_umm_types.py --root $(L4V_REPO_PATH) $< $@
-
-include ${SOURCE_ROOT}/Makefile
+${UMM_TYPES}: kernel_all_pp
+	python ../../mk_umm_types.py --root $(L4V_REPO_PATH) kernel_all.c_pp $@
 
diff --git a/spec/cspec/ARM_HYP/KernelInc_C.thy b/spec/cspec/ARM_HYP/KernelInc_C.thy
index 6cefc75e4..52ad7ff7a 100644
--- a/spec/cspec/ARM_HYP/KernelInc_C.thy
+++ b/spec/cspec/ARM_HYP/KernelInc_C.thy
@@ -12,10 +12,10 @@ theory KernelInc_C
 imports
   Kernel_C
   "../Substitute"
-  "c/arch/object/structures_defs"
-  "c/arch/object/structures_proofs"
-  "c/32/mode/api/shared_types_defs"
-  "c/32/mode/api/shared_types_proofs"
+  "c/build/generated/arch/object/structures_defs"
+  "c/build/generated/arch/object/structures_proofs"
+  "c/build/generated/mode/api/shared_types_defs"
+  "c/build/generated/mode/api/shared_types_proofs"
 begin
 
 end
diff --git a/spec/cspec/ARM_HYP/c/Makefile b/spec/cspec/ARM_HYP/c/Makefile
index 0c53d21f7..bea03e0a6 100644
--- a/spec/cspec/ARM_HYP/c/Makefile
+++ b/spec/cspec/ARM_HYP/c/Makefile
@@ -17,10 +17,6 @@ export PATH
 TOOLPREFIX ?= arm-none-eabi-
 SHELL=bash
 
-ARCH=arm
-ARMV=armv7-a
-PLAT=tk1
-CPU=cortex-a15
 CONFIG_DOMAIN_SCHEDULE=config_sched.c
 
 ifeq ($(shell which ${TOOLPREFIX}cpp),)
@@ -33,18 +29,33 @@ ifeq ($(shell which ${TOOLPREFIX}cpp),)
 endif
 
 # modifies are produced by the parser
-SKIP_MODIFIES=1
+SKIP_MODIFIES=ON
 FASTPATH=yes
 CSPEC_DIR=..
 
+build/CMakeCache.txt:
+	mkdir -p build
+	cd build && \
+	cmake -DCROSS_COMPILER_PREFIX=${TOOLPREFIX} \
+		-DCMAKE_TOOLCHAIN_FILE=../${SOURCE_ROOT}/gcc.cmake -C ../${SOURCE_ROOT}/configs/${L4V_ARCH}_verified.cmake \
+		-DCSPEC_DIR=`pwd`/../${CSPEC_DIR} \
+		-DSKIP_MODIFIES=${SKIP_MODIFIES} \
+		-DUMM_TYPES=`pwd`/../${UMM_TYPES} \
+		-DKernelDomainSchedule=`pwd`/../${CONFIG_DOMAIN_SCHEDULE} -G Ninja ../${SOURCE_ROOT}
+
+kernel_all_pp: build/CMakeCache.txt
+	cd build && ninja kernel_all_pp_wrapper
+	cp -a build/kernel_all_pp.c kernel_all.c_pp
+
+.PHONY: kernel_all_pp
+
 # called by ../../spec/Makefile
-cspec: kernel_all.c_pp ${UMM_TYPES} theories
-# theories is defined in seL4 makefile
+cspec: ${UMM_TYPES} kernel_all_pp
+	cd build && ninja kernel_theories
+
 .PHONY: cspec
 
 # Create "umm_types" if necessary.
-${UMM_TYPES}: kernel_all.c_pp
-	python ../../mk_umm_types.py --root $(L4V_REPO_PATH) $< $@
-
-include ${SOURCE_ROOT}/Makefile
+${UMM_TYPES}: kernel_all_pp
+	python ../../mk_umm_types.py --root $(L4V_REPO_PATH) kernel_all.c_pp $@
 
diff --git a/spec/cspec/X64/KernelInc_C.thy b/spec/cspec/X64/KernelInc_C.thy
index 81223e620..52ad7ff7a 100644
--- a/spec/cspec/X64/KernelInc_C.thy
+++ b/spec/cspec/X64/KernelInc_C.thy
@@ -12,10 +12,10 @@ theory KernelInc_C
 imports
   Kernel_C
   "../Substitute"
-  "c/arch/object/structures_defs"
-  "c/arch/object/structures_proofs"
-  "c/64/mode/api/shared_types_defs"
-  "c/64/mode/api/shared_types_proofs"
+  "c/build/generated/arch/object/structures_defs"
+  "c/build/generated/arch/object/structures_proofs"
+  "c/build/generated/mode/api/shared_types_defs"
+  "c/build/generated/mode/api/shared_types_proofs"
 begin
 
 end
diff --git a/spec/cspec/X64/c/Makefile b/spec/cspec/X64/c/Makefile
index 38801e4ea..fd353f1ab 100644
--- a/spec/cspec/X64/c/Makefile
+++ b/spec/cspec/X64/c/Makefile
@@ -16,9 +16,6 @@ PATH:=${PARSERPATH}:${PATH}
 export PATH
 SHELL=bash
 
-ARCH=x86
-SEL4_ARCH=x86_64
-PLAT=pc99
 CONFIG_DOMAIN_SCHEDULE=config_sched.c
 
 ifeq ($(shell which ${TOOLPREFIX}cpp),)
@@ -31,18 +28,33 @@ ifeq ($(shell which ${TOOLPREFIX}cpp),)
 endif
 
 # modifies are produced by the parser
-SKIP_MODIFIES=1
+SKIP_MODIFIES=ON
 FASTPATH=yes
 CSPEC_DIR=..
 
+build/CMakeCache.txt:
+	mkdir -p build
+	cd build && \
+	cmake -DCROSS_COMPILER_PREFIX=${TOOLPREFIX} \
+		-DCMAKE_TOOLCHAIN_FILE=../${SOURCE_ROOT}/gcc.cmake -C ../${SOURCE_ROOT}/configs/${L4V_ARCH}_verified.cmake \
+		-DCSPEC_DIR=`pwd`/../${CSPEC_DIR} \
+		-DSKIP_MODIFIES=${SKIP_MODIFIES} \
+		-DUMM_TYPES=`pwd`/../${UMM_TYPES} \
+		-DKernelDomainSchedule=`pwd`/../${CONFIG_DOMAIN_SCHEDULE} -G Ninja ../${SOURCE_ROOT}
+
+kernel_all_pp: build/CMakeCache.txt
+	cd build && ninja kernel_all_pp_wrapper
+	cp -a build/kernel_all_pp.c kernel_all.c_pp
+
+.PHONY: kernel_all_pp
+
 # called by ../../spec/Makefile
-cspec: kernel_all.c_pp ${UMM_TYPES} theories
-# theories is defined in seL4 makefile
+cspec: ${UMM_TYPES} kernel_all_pp
+	cd build && ninja kernel_theories
+
 .PHONY: cspec
 
 # Create "umm_types" if necessary.
-${UMM_TYPES}: kernel_all.c_pp
-	python ../../mk_umm_types.py --root $(L4V_REPO_PATH) $< $@
-
-include ${SOURCE_ROOT}/Makefile
+${UMM_TYPES}: kernel_all_pp
+	python ../../mk_umm_types.py --root $(L4V_REPO_PATH) kernel_all.c_pp $@