diff --git a/arch/x86/kernel/cpu.c b/arch/x86/kernel/cpu.c
index ce1b7add..ab90c36d 100644
--- a/arch/x86/kernel/cpu.c
+++ b/arch/x86/kernel/cpu.c
@@ -1033,6 +1033,10 @@ static void __x86_wakeup(int apicid, unsigned long ip)
 
 /** IHK Functions **/
 
+/*@
+  @ assigns \nothing;
+  @ ensures \interrupt_disabled == 0;
+  @*/
 void cpu_halt(void)
 {
 	asm volatile("hlt");
@@ -1335,6 +1339,10 @@ void arch_show_extended_context(void)
 }
 #endif
 
+/*@
+  @ requires \valid(reg);
+  @ assigns \nothing;
+  @*/
 void arch_show_interrupt_context(const void *reg)
 {
 	const struct x86_user_context *uctx = reg;
@@ -1423,8 +1431,8 @@ int ihk_mc_interrupt_cpu(int cpu, int vector)
 }
 
 /*@
-  @ requires \valid(proc);
-  @ ensures proc->fp_regs == NULL;
+  @ requires \valid(thread);
+  @ ensures thread->fp_regs == NULL;
   @*/
 void
 release_fp_regs(struct thread *thread)
@@ -1439,6 +1447,9 @@ release_fp_regs(struct thread *thread)
 	thread->fp_regs = NULL;
 }
 
+/*@
+  @ requires \valid(thread);
+  @*/
 void
 save_fp_regs(struct thread *thread)
 {
@@ -1470,6 +1481,10 @@ save_fp_regs(struct thread *thread)
 	}
 }
 
+/*@
+  @ requires \valid(thread);
+  @ assigns thread->fp_regs;
+  @*/
 void
 restore_fp_regs(struct thread *thread)
 {
@@ -1518,18 +1533,27 @@ ihk_mc_user_context_t *lookup_user_context(struct thread *thread)
 	return uctx;
 } /* lookup_user_context() */
 
+/*@
+  @ assigns \nothing;
+  @*/
 void init_tick(void)
 {
 	dkprintf("init_tick():\n");
 	return;
 }
 
+/*@
+  @ assigns \nothing;
+  @*/
 void init_delay(void)
 {
 	dkprintf("init_delay():\n");
 	return;
 }
 
+/*@
+  @ assigns \nothing;
+  @*/
 void sync_tick(void)
 {
 	dkprintf("sync_tick():\n");
diff --git a/arch/x86/kernel/gencore.c b/arch/x86/kernel/gencore.c
index 32f1fba7..d54272c4 100644
--- a/arch/x86/kernel/gencore.c
+++ b/arch/x86/kernel/gencore.c
@@ -271,6 +271,17 @@ void fill_note(void *note, struct thread *thread, void *regs)
  * should be zero.
  */
 
+/*@
+  @ requires \valid(thread);
+  @ requires \valid(regs);
+  @ requires \valid(coretable);
+  @ requires \valid(chunks);
+  @ behavior success:
+  @   ensures \result == 0;
+  @   assigns coretable;
+  @ behavior failure:
+  @   ensures \result == -1;
+  @*/
 int gencore(struct thread *thread, void *regs, 
 	    struct coretable **coretable, int *chunks)
 {
@@ -510,6 +521,10 @@ int gencore(struct thread *thread, void *regs,
  * \param coretable An array of core chunks.
  */
 
+/*@
+  @ requires \valid(coretable);
+  @ assigns \nothing;
+  @*/
 void freecore(struct coretable **coretable)
 {
 	struct coretable *ct = *coretable;
diff --git a/arch/x86/kernel/local.c b/arch/x86/kernel/local.c
index 5d9a8e0b..84262fc9 100644
--- a/arch/x86/kernel/local.c
+++ b/arch/x86/kernel/local.c
@@ -38,6 +38,11 @@ void init_processors_local(int max_id)
 	kprintf("locals = %p\n", locals);
 }
 
+/*@
+  @ requires \valid(id);
+  @ ensures \result == locals + (LOCALS_SPAN * id);
+  @ assigns \nothing;
+  @*/
 struct x86_cpu_local_variables *get_x86_cpu_local_variable(int id)
 {
 	return (struct x86_cpu_local_variables *)
@@ -98,6 +103,10 @@ void init_boot_processor_local(void)
 }
 
 /** IHK **/
+/*@
+  @ ensures \result == %gs;
+  @ assigns \nothing;
+  */
 int ihk_mc_get_processor_id(void)
 {
 	int id;
@@ -107,6 +116,10 @@ int ihk_mc_get_processor_id(void)
 	return id;
 }
 
+/*@
+  @ ensures \result == (locals + (LOCALS_SPAN * %gs))->apic_id;
+  @ assigns \nothing;
+  */
 int ihk_mc_get_hardware_processor_id(void)
 {
 	struct x86_cpu_local_variables *v =  get_x86_this_cpu_local();