diff --git a/targets/c-host/fail.c b/targets/c-host/fail.c
index 932df8b..b48fbaf 100644
--- a/targets/c-host/fail.c
+++ b/targets/c-host/fail.c
@@ -1,4 +1,5 @@
 #include "../lib.h"
+#include "../lib_cored.h"
 
 void fail_start_trace(void) {}
 void fail_stop_trace(void) {}
@@ -6,18 +7,47 @@ void fail_marker_positive(void) {}
 void fail_marker_negative(void) {}
 void fail_marker_detected(void) {}
 
+void init_outputs(plain_t x_c, plain_t y_c, plain_t z_c);
 int wasm_module(void);
+enc_t get_cored_res(void);
 
-MAIN() {
-  int result;
+void os_main(void) {
+  init_outputs(100, 142, 100);
 
   fail_start_trace();
-  result = wasm_module();
+  sign_t static_sig = wasm_module();
   fail_stop_trace();
 
-  if (result == 100) {
+  sign_t vote_result_sig;
+  switch (static_sig) {
+  case SIG_s_XYZ:
+  case SIG_s_XY:
+  case SIG_s_XZ:
+    vote_result_sig = SIG_X;
+    break;
+  case SIG_s_YZ:
+    vote_result_sig = SIG_Y;
+    break;
+  default:
+    break;
+  }
+
+  // Inversely apply constant program flow signature.
+  enc_t cored_res = get_cored_res();
+  cored_res -= static_sig;
+
+  /* Validate Vote result */
+  if (!check(cored_res, THE_A, vote_result_sig)) {
+    fail_marker_detected();
+    return;
+  }
+
+  plain_t res = decode(cored_res, THE_A, vote_result_sig);
+  if (res == 100) {
     fail_marker_positive();
+    return;
   } else {
     fail_marker_negative();
+    return;
   }
 }
diff --git a/targets/c-host/linux.c b/targets/c-host/linux.c
index 6dc3145..f035b0a 100644
--- a/targets/c-host/linux.c
+++ b/targets/c-host/linux.c
@@ -1,15 +1,56 @@
+#include "../lib_cored.h"
 #include <stdio.h>
 
+void init_outputs(plain_t x_c, plain_t y_c, plain_t z_c);
 int wasm_module(void);
+enc_t get_cored_res(void);
+
+void fail_marker_detected(void) {}
 
 int main(int argc, char *argv[]) {
-  int result = wasm_module();
+  init_outputs(100, 142, 100);
+  sign_t static_sig = wasm_module();
 
-  if (result == 100) {
-    printf("OK Marker\n");
+  sign_t vote_result_sig;
+  switch (static_sig) {
+  case SIG_s_XYZ:
+  case SIG_s_XY:
+  case SIG_s_XZ:
+    vote_result_sig = SIG_X;
+    break;
+  case SIG_s_YZ:
+    vote_result_sig = SIG_Y;
+    break;
+  default:
+    // printf("ERROR: Unknown static_sig %d\n", static_sig);
+    break;
+  }
+
+  // Inversely apply constant program flow signature.
+  enc_t cored_res = get_cored_res();
+  printf("Inversely apply: cored_res=%d static_sig=%d\n", cored_res,
+         static_sig);
+  cored_res -= static_sig;
+
+  /* Validate Vote result */
+  printf(
+      "Validating vote result: cored_res=%d THE_A=%d vote_result_sig = % d\n ",
+      cored_res, THE_A, vote_result_sig);
+  if (!check(cored_res, THE_A, vote_result_sig)) {
+    printf("Validation failed :(\n");
+    // fail_marker_detected();
+    return 1;
+  }
+
+  plain_t res = decode(cored_res, THE_A, vote_result_sig);
+  // printf("Decoded result: %d (%f)\n", res, q_to_float(res));
+  if (res == 100) {
+    // fail_marker_positive();
+    printf("Marker Positive\n");
     return 0;
   } else {
-    printf("FAIL Marker\n");
+    printf("Marker Negative\n");
+    // fail_marker_negative();
     return 1;
   }
 }
diff --git a/targets/lib.h b/targets/lib.h
index 0f74c1e..0ab4162 100644
--- a/targets/lib.h
+++ b/targets/lib.h
@@ -4,37 +4,16 @@
 #define INLINE __attribute__((always_inline)) inline
 #define NOINLINE __attribute__((noinline))
 
-#define __QUOTE(x) #x
-#define QUOTE(x) __QUOTE(x)
-
-#define MAIN() void os_main(void)
-#define POSIX_PRINTF(...)
-
-#define ARCH_ASM_CLOBBER_ALL "eax", "ebx", "ecx", "edx", "esi", "edi", "ebp"
-#define MARKER(str)                                                            \
-  __asm__ volatile(QUOTE(str) ":"                                              \
-                   : /* no inputs */                                           \
-                   : /* no outputs */                                          \
-                   : "memory", ARCH_ASM_CLOBBER_ALL)
-
-typedef __UINT8_TYPE__ uint8_t;
-typedef __UINT16_TYPE__ uint16_t;
-typedef __UINT32_TYPE__ uint32_t;
-
-typedef __INT8_TYPE__ int8_t;
-typedef __INT16_TYPE__ int16_t;
-typedef __INT32_TYPE__ int32_t;
-
 // Mark start of injection
-void __attribute__((noinline)) fail_start_trace(void);
+void NOINLINE fail_start_trace(void);
 // Mark end of injection
-void __attribute__((noinline)) fail_stop_trace(void);
+void NOINLINE fail_stop_trace(void);
 
 // everything ok: valid code and right values
-void __attribute__((noinline)) fail_marker_positive(void);
+void NOINLINE fail_marker_positive(void);
 // everything ok: valid code but wrong values
-void __attribute__((noinline)) fail_marker_negative(void);
+void NOINLINE fail_marker_negative(void);
 // invalid code
-void __attribute__((noinline)) fail_marker_detected(void);
+void NOINLINE fail_marker_detected(void);
 
 #endif
diff --git a/targets/lib_cored.h b/targets/lib_cored.h
new file mode 100644
index 0000000..8074fa9
--- /dev/null
+++ b/targets/lib_cored.h
@@ -0,0 +1,37 @@
+#ifndef _include_lib_cored_h
+#define _include_lib_cored_h
+
+#include <stdint.h>
+
+#define SENSORS_COUNT 3
+#define FILTER_COUNT 3
+
+typedef uint16_t enc_t;
+typedef uint8_t plain_t;
+typedef int8_t sign_t;
+
+#define check(vc, A, B) (((vc - B) % A) == 0)
+#define encode(v, A, B) ((((plain_t)v) * ((sign_t)A)) + ((sign_t)B))
+#define decode(vc, A, B) ((vc - B) / A)
+
+#define equals(vc1, vc2, B1, B2) ((vc1 - vc2) == (B1 - B2))
+
+#define THE_A 110
+
+// CONSTANT Replica results signatures
+#define SIG_X 32
+#define SIG_Y 23
+#define SIG_Z 67
+#define SIG_MAX SIG_Z
+
+// CONSTANT Voter Result Signatures
+#define SIG_s_XYZ ((SIG_X - SIG_Y) + (SIG_X - SIG_Z))
+#define SIG_s_XY (SIG_X - SIG_Y)
+#define SIG_s_YZ (SIG_Y - SIG_Z)
+#define SIG_s_XZ (SIG_X - SIG_Z)
+
+#define XC filter_out[0]
+#define YC filter_out[1]
+#define ZC filter_out[2]
+
+#endif
diff --git a/targets/wasm-host/fail.c b/targets/wasm-host/fail.c
index 8c487d0..e8358c6 100644
--- a/targets/wasm-host/fail.c
+++ b/targets/wasm-host/fail.c
@@ -1,4 +1,5 @@
 #include "../lib.h"
+#include "../lib_cored.h"
 
 #include "bh_platform.h"
 #include "wasm_export.h"
@@ -11,16 +12,18 @@ void fail_marker_positive(void) {}
 void fail_marker_negative(void) {}
 void fail_marker_detected(void) {}
 
+void fail_start_trace_wasm(wasm_exec_env_t exec_env) {}
+void fail_stop_trace_wasm(wasm_exec_env_t exec_env) {}
+void fail_marker_positive_wasm(wasm_exec_env_t exec_env) {}
+void fail_marker_negative_wasm(wasm_exec_env_t exec_env) {}
+void fail_marker_detected_wasm(wasm_exec_env_t exec_env) {}
+
 #define STACK_SIZE (4 * 1024)
 #define HEAP_SIZE STACK_SIZE
 #define RUNTIME_POOL_SIZE 4 * STACK_SIZE
 
-MAIN() {
+void os_main() {
   char error_buf[128];
-  wasm_module_t module;
-  wasm_module_inst_t module_inst;
-  wasm_function_inst_t func;
-  wasm_exec_env_t exec_env;
 
   /* initialize the wasm runtime */
   static char global_heap_buf[RUNTIME_POOL_SIZE];
@@ -35,42 +38,109 @@ MAIN() {
     return;
   }
 
+  static NativeSymbol native_symbols[] = {
+      {"fail_start_trace", fail_start_trace_wasm, "()"},
+      {"fail_stop_trace", fail_stop_trace_wasm, "()"},
+      {"fail_marker_positive", fail_marker_positive_wasm, "()"},
+      {"fail_marker_negative", fail_marker_negative_wasm, "()"},
+      {"fail_marker_detected", fail_marker_detected_wasm, "()"},
+  };
+  int n_native_symbols = sizeof(native_symbols) / sizeof(NativeSymbol);
+  if (!wasm_runtime_register_natives("env", native_symbols, n_native_symbols)) {
+    return;
+  }
+
   /* parse the WASM file from buffer and create a WASM module */
-  module = wasm_runtime_load(__WASM_ARRAY__, __WASM_ARRAY_LEN__, error_buf,
-                             sizeof(error_buf));
+  wasm_module_t module = wasm_runtime_load(__WASM_ARRAY__, __WASM_ARRAY_LEN__,
+                                           error_buf, sizeof(error_buf));
 
   if (!module) {
     return;
   }
 
   /* create an instance of the WASM module (WASM linear memory is ready) */
-  module_inst = wasm_runtime_instantiate(module, STACK_SIZE, HEAP_SIZE,
-                                         error_buf, sizeof(error_buf));
+  wasm_module_inst_t module_inst = wasm_runtime_instantiate(
+      module, STACK_SIZE, HEAP_SIZE, error_buf, sizeof(error_buf));
 
   if (!module_inst) {
     return;
   }
 
-  /* lookup a WASM function by its name, the function signature can NULL here */
-  func = wasm_runtime_lookup_function(module_inst, "wasm_module");
+  // Single exec_env for all functions (probably'd need a single one per
+  // thread?)
+  wasm_exec_env_t exec_env =
+      wasm_runtime_create_exec_env(module_inst, STACK_SIZE);
+  uint32_t args[FILTER_COUNT];
 
-  /* create an execution environment to execute arbitrary WASM functions */
-  exec_env = wasm_runtime_create_exec_env(module_inst, STACK_SIZE);
+  // Place encoded input values for cored voter.
+  // They'll be broken by FAIL* on read, so I don't need to inject this (?)
+  // fail_start_trace();
+  wasm_function_inst_t init_func =
+      wasm_runtime_lookup_function(module_inst, "init_outputs");
+  args[0] = 100;
+  args[1] = 142;
+  args[2] = 100;
+  if (!wasm_runtime_call_wasm(exec_env, init_func, 3, args)) {
+    return;
+  }
 
-  /* arguments are always transferred in 32-bit element */
-  uint32_t args[1] = {0};
-
-  /* call an arbitrary WASM function */
+  // CoRed vote
+  wasm_function_inst_t func =
+      wasm_runtime_lookup_function(module_inst, "wasm_module");
+  args[0] = 0;
+  args[1] = 0;
+  args[2] = 0;
   fail_start_trace();
   if (!wasm_runtime_call_wasm(exec_env, func, 0, args)) {
-    /* function wasn't called correctly */
+    return;
   }
   fail_stop_trace();
+  sign_t static_sig = args[0];
 
-  /* the return value is stored in args[0] */
-  uint32_t result = args[0];
+  // Obtain dynamic signature produced by CoRed
+  wasm_function_inst_t cored_res_func =
+      wasm_runtime_lookup_function(module_inst, "get_cored_res");
+  args[0] = 0;
+  args[1] = 0;
+  args[2] = 0;
+  if (!wasm_runtime_call_wasm(exec_env, cored_res_func, 0, args)) {
+    return;
+  }
+  enc_t cored_res = args[0];
 
-  if (result == 100) {
+  sign_t vote_result_sig;
+  switch (static_sig) {
+  case SIG_s_XYZ:
+  case SIG_s_XY:
+  case SIG_s_XZ:
+    vote_result_sig = SIG_X;
+    break;
+  case SIG_s_YZ:
+    vote_result_sig = SIG_Y;
+    break;
+  default:
+    // printf("ERROR: Unknown static_sig %d\n", static_sig);
+    break;
+  }
+
+  // Inversely apply constant program flow signature.
+  // printf("Inversely apply: cored_res=%d static_sig=%d\n", cored_res,
+  //        static_sig);
+  cored_res -= static_sig;
+
+  /* Validate Vote result */
+  // printf(
+  //     "Validating vote result: cored_res=%d THE_A=%d vote_result_sig = % d\n
+  //     ", cored_res, THE_A, vote_result_sig);
+  if (!check(cored_res, THE_A, vote_result_sig)) {
+    // printf("Validation failed :(\n");
+    fail_marker_detected();
+    return;
+  }
+
+  plain_t res = decode(cored_res, THE_A, vote_result_sig);
+  // printf("Decoded result: %d (%f)\n", res, q_to_float(res));
+  if (res == 100) {
     fail_marker_positive();
   } else {
     fail_marker_negative();
diff --git a/targets/wasm-host/linux.c b/targets/wasm-host/linux.c
index 0507ad9..4e3a6d4 100644
--- a/targets/wasm-host/linux.c
+++ b/targets/wasm-host/linux.c
@@ -1,19 +1,23 @@
+#include "../lib_cored.h"
+
 #include "bh_platform.h"
 #include "wasm_export.h"
 
 #include "__WASM_ARRAY_FILE__"
 #include <stdio.h>
 
+void fail_start_trace_wasm(wasm_exec_env_t exec_env) {}
+void fail_stop_trace_wasm(wasm_exec_env_t exec_env) {}
+void fail_marker_positive_wasm(wasm_exec_env_t exec_env) {}
+void fail_marker_negative_wasm(wasm_exec_env_t exec_env) {}
+void fail_marker_detected_wasm(wasm_exec_env_t exec_env) {}
+
 #define STACK_SIZE (4 * 1024)
 #define HEAP_SIZE STACK_SIZE
 #define RUNTIME_POOL_SIZE 4 * STACK_SIZE
 
 int main(int argc, char *argv[]) {
   char error_buf[128];
-  wasm_module_t module;
-  wasm_module_inst_t module_inst;
-  wasm_function_inst_t func;
-  wasm_exec_env_t exec_env;
 
   /* initialize the wasm runtime */
   static char global_heap_buf[RUNTIME_POOL_SIZE];
@@ -29,9 +33,21 @@ int main(int argc, char *argv[]) {
     return 1;
   }
 
+  static NativeSymbol native_symbols[] = {
+      {"fail_start_trace", fail_start_trace_wasm, "()"},
+      {"fail_stop_trace", fail_stop_trace_wasm, "()"},
+      {"fail_marker_positive", fail_marker_positive_wasm, "()"},
+      {"fail_marker_negative", fail_marker_negative_wasm, "()"},
+      {"fail_marker_detected", fail_marker_detected_wasm, "()"},
+  };
+  int n_native_symbols = sizeof(native_symbols) / sizeof(NativeSymbol);
+  if (!wasm_runtime_register_natives("env", native_symbols, n_native_symbols)) {
+    return 1;
+  }
+
   /* parse the WASM file from buffer and create a WASM module */
-  module = wasm_runtime_load(__WASM_ARRAY__, __WASM_ARRAY_LEN__, error_buf,
-                             sizeof(error_buf));
+  wasm_module_t module = wasm_runtime_load(__WASM_ARRAY__, __WASM_ARRAY_LEN__,
+                                           error_buf, sizeof(error_buf));
 
   if (!module) {
     printf("Load failed: %s\n", error_buf);
@@ -39,42 +55,93 @@ int main(int argc, char *argv[]) {
   }
 
   /* create an instance of the WASM module (WASM linear memory is ready) */
-  module_inst = wasm_runtime_instantiate(module, STACK_SIZE, HEAP_SIZE,
-                                         error_buf, sizeof(error_buf));
+  wasm_module_inst_t module_inst = wasm_runtime_instantiate(
+      module, STACK_SIZE, HEAP_SIZE, error_buf, sizeof(error_buf));
 
   if (!module_inst) {
     printf("Inst failed: %s\n", error_buf);
     return 1;
   }
 
-  /* lookup a WASM function by its name, the function signature can NULL here */
-  func = wasm_runtime_lookup_function(module_inst, "wasm_module");
+  wasm_exec_env_t exec_env =
+      wasm_runtime_create_exec_env(module_inst, STACK_SIZE);
+  uint32_t args[FILTER_COUNT];
 
-  /* create an execution environment to execute arbitrary WASM functions */
-  exec_env = wasm_runtime_create_exec_env(module_inst, STACK_SIZE);
-
-  /* arguments are always transferred in 32-bit element */
-  uint32_t args[1] = {0};
-
-  /* call an arbitrary WASM function */
-  if (!wasm_runtime_call_wasm(exec_env, func, 0, args)) {
-    /* function wasn't called correctly */
-    printf("Failed to call function 'wasm_module'!\n");
+  wasm_function_inst_t init_func =
+      wasm_runtime_lookup_function(module_inst, "init_outputs");
+  args[0] = 100;
+  args[1] = 142;
+  args[2] = 100;
+  if (!wasm_runtime_call_wasm(exec_env, init_func, 3, args)) {
+    printf("Failed to call init_outputs\n");
+    return 1;
   }
 
-  /* the return value is stored in args[0] */
-  uint32_t result = args[0];
+  // CoRed vote
+  wasm_function_inst_t func =
+      wasm_runtime_lookup_function(module_inst, "wasm_module");
+  args[0] = 0;
+  args[1] = 0;
+  args[2] = 0;
+  if (!wasm_runtime_call_wasm(exec_env, func, 0, args)) {
+    printf("Failed to call wasm_module\n");
+    return 1;
+  }
+  sign_t static_sig = args[0];
+
+  // Obtain dynamic signature produced by CoRed
+  wasm_function_inst_t cored_res_func =
+      wasm_runtime_lookup_function(module_inst, "get_cored_res");
+  args[0] = 0;
+  args[1] = 0;
+  args[2] = 0;
+  if (!wasm_runtime_call_wasm(exec_env, cored_res_func, 0, args)) {
+    printf("Failed to call get_cored_res\n");
+    return 1;
+  }
+  enc_t cored_res = args[0];
 
   wasm_runtime_destroy_exec_env(exec_env);
   wasm_runtime_deinstantiate(module_inst);
   wasm_runtime_unload(module);
   wasm_runtime_destroy();
 
-  if (result == 100) {
-    printf("OK Marker\n");
+  sign_t vote_result_sig;
+  switch (static_sig) {
+  case SIG_s_XYZ:
+  case SIG_s_XY:
+  case SIG_s_XZ:
+    vote_result_sig = SIG_X;
+    break;
+  case SIG_s_YZ:
+    vote_result_sig = SIG_Y;
+    break;
+  default:
+    printf("ERROR: Unknown static_sig %d\n", static_sig);
+    break;
+  }
+
+  // Inversely apply constant program flow signature.
+  printf("Inversely apply: cored_res=%d static_sig=%d\n", cored_res,
+         static_sig);
+  cored_res -= static_sig;
+
+  /* Validate Vote result */
+  printf(
+      "Validating vote result: cored_res=%d THE_A=%d vote_result_sig = % d\n ",
+      cored_res, THE_A, vote_result_sig);
+  if (!check(cored_res, THE_A, vote_result_sig)) {
+    printf("Validation failed :(\n");
+    return 1;
+  }
+
+  plain_t res = decode(cored_res, THE_A, vote_result_sig);
+  // printf("Decoded result: %d (%f)\n", res, q_to_float(res));
+  if (res == 100) {
+    printf("Marker Positive\n");
     return 0;
   } else {
-    printf("FAIL Marker\n");
+    printf("Marker Negative\n");
     return 1;
   }
 }
diff --git a/targets/wasm-module/cored.c b/targets/wasm-module/cored.c
new file mode 100644
index 0000000..cc81a48
--- /dev/null
+++ b/targets/wasm-module/cored.c
@@ -0,0 +1,45 @@
+#include "../lib.h"
+#include "../lib_cored.h"
+
+static enc_t cored_res;
+static enc_t filter_out[FILTER_COUNT];
+
+void init_outputs(plain_t x_c, plain_t y_c, plain_t z_c) {
+  /* Replicated Filtersteps */
+  XC = encode(x_c, THE_A, SIG_X);
+  YC = encode(y_c, THE_A, SIG_Y);
+  ZC = encode(z_c, THE_A, SIG_Z);
+}
+
+enc_t INLINE apply(enc_t vc, sign_t bdyn) {
+  if (bdyn > SIG_MAX) {
+    fail_marker_detected();
+  }
+  return vc + bdyn;
+}
+
+sign_t wasm_module(void) {
+  if (equals(XC, YC, SIG_X, SIG_Y)) {
+    if (equals(XC, ZC, SIG_X, SIG_Z)) {
+      cored_res = apply(XC, (XC - YC) + (XC - ZC));
+      return SIG_s_XYZ;
+    } else {
+      cored_res = apply(XC, (XC - YC));
+      return SIG_s_XY;
+    }
+  } else if (equals(YC, ZC, SIG_Y, SIG_Z)) {
+    cored_res = apply(YC, (YC - ZC));
+    return SIG_s_YZ;
+  } else if (equals(XC, ZC, SIG_X, SIG_Z)) {
+    cored_res = apply(XC, (XC - ZC));
+    return SIG_s_XZ;
+  } else {
+    fail_marker_detected();
+    return 0;
+  }
+}
+
+enc_t get_cored_res() { return cored_res; }
+// enc_t get_xc() { return XC; }
+// enc_t get_yc() { return YC; }
+// enc_t get_zc() { return ZC; }
diff --git a/wasm.just b/wasm.just
index 552de9f..afadf78 100644
--- a/wasm.just
+++ b/wasm.just
@@ -15,6 +15,7 @@ WASI_CFLAGS := "\
 -Wl,--initial-memory=65536 \
 -Wl,--export=__heap_base \
 -Wl,--export=__data_end \
+-Wl,--allow-undefined \
 "
 CROSS_CFLAGS_NOWASM := "\
 -O0 \