diff --git a/.gitignore b/.gitignore
index 9c300842e..9d42bfb6c 100644
--- a/.gitignore
+++ b/.gitignore
@@ -21,6 +21,7 @@
 /spec/design/*.thy
 /spec/design/ARM/*.thy
 /spec/design/ARM_HYP/*.thy
+/spec/design/RISCV64/*.thy
 /spec/design/X64/*.thy
 
 /spec/machine/*/MachineTypes.thy
diff --git a/spec/design/Makefile b/spec/design/Makefile
index cc518ff2d..e5a894f00 100644
--- a/spec/design/Makefile
+++ b/spec/design/Makefile
@@ -23,9 +23,10 @@ SKEL_FILES    := $(shell find ${SKEL_PATH} -name "*.thy")
 MSKEL_FILES   := $(shell find ${MSKEL_PATH} -name "*.thy")
 HASKELL_FILES := $(shell find ${HASKELL_PATH} -regex ".*\.l?hs") # FIXME: add .hs
 HASKELL_TRANS := ${L4V_REPO_PATH}/tools/haskell-translator/make_spec.sh
-ARCH_DIRS     += ARM ARM_HYP X64
+ARCH_DIRS     += ARM ARM_HYP RISCV64 X64
 MACHINE_FILES += ${MACHINE_PATH}/ARM/MachineTypes.thy \
                  ${MACHINE_PATH}/ARM_HYP/MachineTypes.thy \
+                 ${MACHINE_PATH}/RISCV64/MachineTypes.thy \
                  ${MACHINE_PATH}/X64/MachineTypes.thy
 
 design : version
diff --git a/spec/design/m-skel/RISCV64/MachineTypes.thy b/spec/design/m-skel/RISCV64/MachineTypes.thy
new file mode 100644
index 000000000..ee94d0e9c
--- /dev/null
+++ b/spec/design/m-skel/RISCV64/MachineTypes.thy
@@ -0,0 +1,134 @@
+(*
+ * Copyright 2014, General Dynamics C4 Systems
+ *
+ * This software may be distributed and modified according to the terms of
+ * the GNU General Public License version 2. Note that NO WARRANTY is provided.
+ * See "LICENSE_GPLv2.txt" for details.
+ *
+ * @TAG(GD_GPL)
+ *)
+
+chapter "RISCV 64bit Machine Types"
+
+theory MachineTypes
+imports
+  "../../../lib/Word_Lib/Enumeration"
+  "../../../lib/$L4V_ARCH/WordSetup"
+  "../../../lib/Monad_WP/NonDetMonad"
+  "../../../lib/HaskellLib_H"
+  Platform
+begin
+
+context Arch begin global_naming RISCV64
+
+text {*
+  An implementation of the machine's types, defining register set
+  and some observable machine state.
+*}
+
+section "Types"
+
+#INCLUDE_HASKELL SEL4/Machine/RegisterSet/RISCV64.hs CONTEXT RISCV64 decls_only NOT UserContext UserMonad getRegister setRegister newContext
+(*<*)
+
+section "Machine Words"
+
+type_synonym machine_word_len = 64
+
+definition
+  word_size_bits :: "'a :: numeral"
+where
+  "word_size_bits \<equiv> 3"
+
+end
+
+context begin interpretation Arch .
+requalify_types register
+end
+
+context Arch begin global_naming RISCV64
+
+#INCLUDE_HASKELL SEL4/Machine/RegisterSet/RISCV64.hs CONTEXT RISCV64 instanceproofs
+(*>*)
+#INCLUDE_HASKELL SEL4/Machine/RegisterSet/RISCV64.hs CONTEXT RISCV64 bodies_only NOT getRegister setRegister newContext
+
+section "Machine State"
+
+text {*
+  Most of the machine state is left underspecified at this level.
+  We know it exists, we will declare some interface functions, but
+  at this level we do not have access to how this state is transformed
+  or what effect it has on the machine.
+*}
+typedecl machine_state_rest
+
+end
+
+qualify RISCV64 (in Arch)
+
+record
+  machine_state =
+  irq_masks :: "RISCV64.irq \<Rightarrow> bool"
+  irq_state :: nat
+  underlying_memory :: "word64 \<Rightarrow> word8"
+  device_state :: "word64 \<Rightarrow> word8 option"
+  machine_state_rest :: RISCV64.machine_state_rest
+
+consts irq_oracle :: "nat \<Rightarrow> word8"
+
+end_qualify
+
+context Arch begin global_naming RISCV64
+
+text {*
+  The machine monad is used for operations on the state defined above.
+*}
+type_synonym 'a machine_monad = "(machine_state, 'a) nondet_monad"
+
+end
+
+translations
+  (type) "'c RISCV64.machine_monad" <= (type) "(RISCV64.machine_state, 'c) nondet_monad"
+
+context Arch begin global_naming RISCV64
+
+text {*
+  After kernel initialisation all IRQs are masked.
+*}
+definition
+  "init_irq_masks \<equiv> \<lambda>_. True"
+
+text {*
+  The initial contents of the user-visible memory is 0.
+*}
+definition
+  init_underlying_memory :: "word64 \<Rightarrow> word8"
+  where
+  "init_underlying_memory \<equiv> \<lambda>_. 0"
+
+text {*
+  We leave open the underspecified rest of the machine state in
+  the initial state.
+*}
+definition
+  init_machine_state :: machine_state where
+ "init_machine_state \<equiv> \<lparr> irq_masks = init_irq_masks,
+                         irq_state = 0,
+                         underlying_memory = init_underlying_memory,
+                         device_state = empty,
+                         machine_state_rest = undefined \<rparr>"
+
+#INCLUDE_HASKELL SEL4/Machine/Hardware/RISCV64.hs CONTEXT RISCV64 ONLY VMFaultType HypFaultType VMPageSize pageBits ptTranslationBits pageBitsForSize
+
+end
+
+context begin interpretation Arch .
+requalify_types vmpage_size
+end
+
+context Arch begin global_naming RISCV64
+
+#INCLUDE_HASKELL SEL4/Machine/Hardware/RISCV64.hs CONTEXT RISCV64 instanceproofs ONLY VMFaultType HypFaultType VMPageSize
+
+end
+end
diff --git a/spec/design/skel/RISCV64/ArchFaultHandler_H.thy b/spec/design/skel/RISCV64/ArchFaultHandler_H.thy
new file mode 100644
index 000000000..280d6925b
--- /dev/null
+++ b/spec/design/skel/RISCV64/ArchFaultHandler_H.thy
@@ -0,0 +1,26 @@
+(*
+ * Copyright 2014, General Dynamics C4 Systems
+ *
+ * This software may be distributed and modified according to the terms of
+ * the GNU General Public License version 2. Note that NO WARRANTY is provided.
+ * See "LICENSE_GPLv2.txt" for details.
+ *
+ * @TAG(GD_GPL)
+ *)
+
+chapter "Fault Handlers"
+
+theory ArchFaultHandler_H
+imports "../TCB_H" "../Structures_H"
+begin
+
+context Arch begin global_naming RISCV64_H
+
+#INCLUDE_HASKELL_PREPARSE SEL4/API/Failures/RISCV64.hs
+
+#INCLUDE_HASKELL SEL4/API/Faults/RISCV64.hs decls_only
+#INCLUDE_HASKELL SEL4/API/Faults/RISCV64.hs bodies_only
+
+end
+
+end
diff --git a/spec/machine/RISCV64/MachineOps.thy b/spec/machine/RISCV64/MachineOps.thy
new file mode 100644
index 000000000..986582297
--- /dev/null
+++ b/spec/machine/RISCV64/MachineOps.thy
@@ -0,0 +1,244 @@
+(*
+ * Copyright 2014, General Dynamics C4 Systems
+ *
+ * This software may be distributed and modified according to the terms of
+ * the GNU General Public License version 2. Note that NO WARRANTY is provided.
+ * See "LICENSE_GPLv2.txt" for details.
+ *
+ * @TAG(GD_GPL)
+ *)
+
+chapter "Machine Operations"
+
+theory MachineOps
+imports
+  "../../../lib/$L4V_ARCH/WordSetup"
+  "../../../lib/Monad_WP/NonDetMonad"
+  "../MachineMonad"
+begin
+
+section "Wrapping and Lifting Machine Operations"
+
+text {*
+  Most of the machine operations below work on the underspecified
+  part of the machine state @{typ machine_state_rest} and cannot fail.
+  We could express the latter by type (leaving out the failure flag),
+  but if we later wanted to implement them,
+  we'd have to set up a new hoare-logic
+  framework for that type. So instead, we provide a wrapper for these
+  operations that explicitly ignores the fail flag and sets it to
+  False. Similarly, these operations never return an empty set of
+  follow-on states, which would require the operation to fail.
+  So we explicitly make this (non-existing) case a null operation.
+
+  All this is done only to avoid a large number of axioms (2 for each operation).
+*}
+
+context Arch begin global_naming RISCV64
+
+section "The Operations"
+
+definition
+  loadWord :: "machine_word \<Rightarrow> machine_word machine_monad"
+  where "loadWord p \<equiv> do m \<leftarrow> gets underlying_memory;
+                         assert (p && mask 3 = 0);
+                         return (word_rcat (map (\<lambda>i. m (p + (7 - of_int i))) [0 .. 7]))
+                      od"
+
+definition
+  storeWord :: "machine_word \<Rightarrow> machine_word \<Rightarrow> unit machine_monad"
+  where "storeWord p w \<equiv> do
+                            assert (p && mask 3 = 0);
+                            modify (underlying_memory_update (
+                                      fold (\<lambda>i m. m((p + (of_int i)) := word_rsplit w ! (7 - nat i))) [0 .. 7]))
+                         od"
+
+lemma upto0_7_def:
+  "[0..7] = [0,1,2,3,4,5,6,7]" by eval
+
+lemma loadWord_storeWord_is_return:
+  "p && mask 3 = 0 \<Longrightarrow> (do w \<leftarrow> loadWord p; storeWord p w od) = return ()"
+  apply (rule ext)
+  by (simp add: loadWord_def storeWord_def bind_def assert_def return_def
+    modify_def gets_def get_def eval_nat_numeral put_def upto0_7_def
+    word_rsplit_rcat_size word_size)
+
+
+text {* This instruction is required in the simulator, only. *}
+definition
+  storeWordVM :: "machine_word \<Rightarrow> machine_word \<Rightarrow> unit machine_monad"
+  where "storeWordVM w p \<equiv> return ()"
+
+consts'
+  configureTimer_impl :: "unit machine_rest_monad"
+  configureTimer_val :: "machine_state \<Rightarrow> irq"
+
+definition
+  configureTimer :: "irq machine_monad"
+where
+  "configureTimer \<equiv> do
+    machine_op_lift configureTimer_impl;
+    gets configureTimer_val
+  od"
+
+consts' (* XXX: replaces configureTimer in new boot code
+          TODO: remove configureTimer when haskell updated *)
+  initTimer_impl :: "unit machine_rest_monad"
+definition
+  initTimer :: "unit machine_monad"
+where "initTimer \<equiv> machine_op_lift initTimer_impl"
+
+consts'
+  resetTimer_impl :: "unit machine_rest_monad"
+
+definition
+  resetTimer :: "unit machine_monad"
+where "resetTimer \<equiv> machine_op_lift resetTimer_impl"
+
+consts'
+  invalidateTLB_impl :: "unit machine_rest_monad"
+definition
+  invalidateTLB :: "unit machine_monad"
+where "invalidateTLB \<equiv> machine_op_lift invalidateTLB_impl"
+
+lemmas cache_machine_op_defs = invalidateTLB_def
+
+definition
+  debugPrint :: "unit list \<Rightarrow> unit machine_monad"
+where
+  debugPrint_def[simp]:
+ "debugPrint \<equiv> \<lambda>message. return ()"
+
+
+-- "Interrupt controller operations"
+
+text {*
+  Interrupts that cannot occur while the kernel is running (e.g. at preemption points),
+  but that can occur from user mode. Empty on plain x86-64.
+*}
+definition
+  "non_kernel_IRQs = {}"
+
+text {*
+  @{term getActiveIRQ} is now derministic.
+  It 'updates' the irq state to the reflect the passage of
+  time since last the irq was gotten, then it gets the active
+  IRQ (if there is one).
+*}
+definition
+  getActiveIRQ :: "bool \<Rightarrow> (irq option) machine_monad"
+where
+  "getActiveIRQ in_kernel \<equiv> do
+    is_masked \<leftarrow> gets $ irq_masks;
+    modify (\<lambda>s. s \<lparr> irq_state := irq_state s + 1 \<rparr>);
+    active_irq \<leftarrow> gets $ irq_oracle \<circ> irq_state;
+    if is_masked active_irq \<or> active_irq = 0xFF \<or> (in_kernel \<and> active_irq \<in> non_kernel_IRQs)
+    then return None
+    else return ((Some active_irq) :: irq option)
+  od"
+
+definition
+  maskInterrupt :: "bool \<Rightarrow> irq \<Rightarrow> unit machine_monad"
+where
+  "maskInterrupt m irq \<equiv>
+  modify (\<lambda>s. s \<lparr> irq_masks := (irq_masks s) (irq := m) \<rparr>)"
+
+definition
+  ackInterrupt :: "irq \<Rightarrow> unit machine_monad"
+where
+  "ackInterrupt \<equiv> \<lambda>irq. return ()"
+
+definition
+  setInterruptMode :: "irq \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> unit machine_monad"
+where
+  "setInterruptMode \<equiv> \<lambda>irq levelTrigger polarityLow. return ()"
+
+section "Memory Clearance"
+
+text {* Clear memory contents to recycle it as user memory *}
+definition
+  clearMemory :: "machine_word \<Rightarrow> nat \<Rightarrow> unit machine_monad"
+  where
+ "clearMemory ptr bytelength \<equiv> mapM_x (\<lambda>p. storeWord p 0) [ptr, ptr + word_size .e. ptr + (of_nat bytelength) - 1]"
+
+definition
+  clearMemoryVM :: "machine_word \<Rightarrow> nat \<Rightarrow> unit machine_monad"
+  where
+  "clearMemoryVM ptr bits \<equiv> return ()"
+
+text {*
+  Initialize memory to be used as user memory.
+  Note that zeroing out the memory is redundant in the specifications.
+  In any case, we cannot abstract from the call to cleanCacheRange,
+  which appears in the implementation.
+*}
+abbreviation (input) "initMemory == clearMemory"
+
+text {*
+  Free memory that had been initialized as user memory.
+  While freeing memory is a no-op in the implementation,
+  we zero out the underlying memory in the specifications to avoid garbage.
+  If we know that there is no garbage,
+  we can compute from the implementation state
+  what the exact memory content in the specifications is.
+*}
+definition
+  freeMemory :: "machine_word \<Rightarrow> nat \<Rightarrow> unit machine_monad"
+  where
+ "freeMemory ptr bits \<equiv>
+  mapM_x (\<lambda>p. storeWord p 0) [ptr, ptr + word_size  .e.  ptr + 2 ^ bits - 1]"
+
+
+section "User Monad"
+
+type_synonym user_regs = "register \<Rightarrow> machine_word"
+
+datatype user_context = UserContext (user_regs : user_regs)
+
+type_synonym 'a user_monad = "(user_context, 'a) nondet_monad"
+
+definition
+  getRegister :: "register \<Rightarrow> machine_word user_monad"
+where
+  "getRegister r \<equiv> gets (\<lambda>s. user_regs s r)"
+
+definition
+  "modify_registers f uc \<equiv> UserContext (f (user_regs uc))"
+
+definition
+  setRegister :: "register \<Rightarrow> machine_word \<Rightarrow> unit user_monad"
+where
+  "setRegister r v \<equiv> modify (\<lambda>s. UserContext ((user_regs s) (r := v)))"
+
+definition
+  "getRestartPC \<equiv> getRegister FaultIP"
+
+definition
+  "setNextPC \<equiv> setRegister NextIP"
+
+
+consts'
+  hwASIDFlush_impl :: "machine_word \<Rightarrow> unit machine_rest_monad"
+definition
+  hwASIDFlush :: "machine_word \<Rightarrow> unit machine_monad"
+where
+  "hwASIDFlush asid \<equiv> machine_op_lift (hwASIDFlush_impl asid)"
+
+consts'
+  sFence_impl :: "unit machine_rest_monad"
+definition
+  sFence :: "unit machine_monad"
+where
+  "sFence \<equiv> machine_op_lift sFence_impl"
+
+consts'
+  sBadAddr_val :: "machine_state \<Rightarrow> machine_word"
+definition
+  readSBADAddr :: "machine_word machine_monad"
+ where
+  "readSBADAddr = gets sBadAddr_val"
+
+end
+
+
+end
diff --git a/spec/machine/RISCV64/Platform.thy b/spec/machine/RISCV64/Platform.thy
new file mode 100644
index 000000000..aa9f4209b
--- /dev/null
+++ b/spec/machine/RISCV64/Platform.thy
@@ -0,0 +1,67 @@
+(*
+ * Copyright 2014, General Dynamics C4 Systems
+ *
+ * This software may be distributed and modified according to the terms of
+ * the GNU General Public License version 2. Note that NO WARRANTY is provided.
+ * See "LICENSE_GPLv2.txt" for details.
+ *
+ * @TAG(GD_GPL)
+ *)
+
+chapter "Platform Definitions"
+
+theory Platform
+imports
+  "../../../lib/Lib"
+  "../../../lib/Word_Lib/Word_Enum"
+  "../../../lib/Defs"
+  "../Setup_Locale"
+begin
+
+context Arch begin global_naming RISCV64
+
+type_synonym irq = word32
+type_synonym paddr = word64
+
+
+abbreviation (input) "toPAddr \<equiv> id"
+abbreviation (input) "fromPAddr \<equiv> id"
+
+definition
+  kernelBase :: word64 where
+  "kernelBase = 0xFFFFFFFF80000000"
+
+definition
+  paddrLoad :: word64 where
+  "paddrLoad = 0xC0000000"
+
+definition
+  kernelBaseOffset :: word64 where
+  "kernelBaseOffset = kernelBase - paddrLoad"
+
+definition
+  pptrBase :: word64 where
+  "pptrBase = 0xFFFFFFC000000000"
+
+definition
+  ptrFromPAddr :: "paddr \<Rightarrow> word64" where
+  "ptrFromPAddr paddr \<equiv> paddr + pptrBase"
+
+definition
+  addrFromPPtr :: "word64 \<Rightarrow> paddr" where
+  "addrFromPPtr pptr \<equiv> pptr - pptrBase"
+
+definition
+  addrFromKPPtr :: "word64 \<Rightarrow> paddr" where
+  "addrFromKPPtr pptr \<equiv> pptr - kernelBaseOffset"
+
+definition
+  minIRQ :: "irq" where
+  "minIRQ \<equiv> 0"
+
+definition
+  maxIRQ :: "irq" where
+  "maxIRQ \<equiv> 5"
+
+end
+end