diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 6670d82bf..69ad92fa1 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -9,6 +9,7 @@ on:
 env:
   CARGO_TERM_COLOR: always
   ABY_SOURCE: "./../ABY"
+  SEAL_SOURCE: "./../SEAL"
 
 jobs:
   build:
@@ -31,7 +32,9 @@ jobs:
     - name: Cache third_party build
       uses: actions/cache@v2
       with:
-        path: ${ABY_SOURCE}/build
+        path: |
+          ${ABY_SOURCE}/build
+          ${SEAL_SOURCE}/build
         key: ${{ runner.os }}
     - name: Check
       run: python3 driver.py --check
diff --git a/.vscode/settings.json b/.vscode/settings.json
new file mode 100644
index 000000000..cad7657df
--- /dev/null
+++ b/.vscode/settings.json
@@ -0,0 +1,3 @@
+{
+    "cmake.configureOnOpen": false
+}
\ No newline at end of file
diff --git a/Cargo.lock b/Cargo.lock
index 30ac3424f..91b0e227f 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -138,7 +138,7 @@ dependencies = [
  "log",
  "num_cpus",
  "pairing",
- "rand_core",
+ "rand_core 0.6.3",
  "rayon",
  "subtle",
 ]
@@ -149,6 +149,15 @@ version = "1.3.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "bef38d45163c2f1dde094a7dfd33ccf595c92905c8f8f4fdc18d06fb1037718a"
 
+[[package]]
+name = "bitmaps"
+version = "2.1.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "031043d04099746d8db04daf1fa424b2bc8bd69d92b25962dcde24da39ab64a2"
+dependencies = [
+ "typenum",
+]
+
 [[package]]
 name = "bitvec"
 version = "0.22.3"
@@ -202,7 +211,7 @@ dependencies = [
  "ff",
  "group",
  "pairing",
- "rand_core",
+ "rand_core 0.6.3",
  "subtle",
 ]
 
@@ -246,6 +255,7 @@ dependencies = [
  "good_lp",
  "hashconsing",
  "ieee754",
+ "im",
  "itertools 0.10.3",
  "lang-c",
  "lazy_static",
@@ -441,7 +451,7 @@ dependencies = [
  "bitvec",
  "byteorder",
  "ff_derive 0.11.0 (registry+https://github.com/rust-lang/crates.io-index)",
- "rand_core",
+ "rand_core 0.6.3",
  "subtle",
 ]
 
@@ -578,7 +588,7 @@ checksum = "bc5ac374b108929de78460075f3dc439fa66df9d8fc77e8f12caa5165fcf0c89"
 dependencies = [
  "byteorder",
  "ff",
- "rand_core",
+ "rand_core 0.6.3",
  "subtle",
 ]
 
@@ -630,6 +640,20 @@ version = "0.2.6"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "9007da9cacbd3e6343da136e98b0d2df013f553d35bdec8b518f07bea768e19c"
 
+[[package]]
+name = "im"
+version = "15.0.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "111c1983f3c5bb72732df25cddacee9b546d08325fb584b5ebd38148be7b0246"
+dependencies = [
+ "bitmaps",
+ "rand_core 0.5.1",
+ "rand_xoshiro",
+ "sized-chunks",
+ "typenum",
+ "version_check",
+]
+
 [[package]]
 name = "indexmap"
 version = "1.7.0"
@@ -1009,7 +1033,7 @@ checksum = "2e7573632e6454cf6b99d7aac4ccca54be06da05aca2ef7423d22d27d4d4bcd8"
 dependencies = [
  "libc",
  "rand_chacha",
- "rand_core",
+ "rand_core 0.6.3",
  "rand_hc",
 ]
 
@@ -1020,9 +1044,15 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "e6c10a63a0fa32252be49d21e7709d4d4baf8d231c2dbce1eaa8141b9b127d88"
 dependencies = [
  "ppv-lite86",
- "rand_core",
+ "rand_core 0.6.3",
 ]
 
+[[package]]
+name = "rand_core"
+version = "0.5.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "90bde5296fc891b0cef12a6d03ddccc162ce7b2aff54160af9338f8d40df6d19"
+
 [[package]]
 name = "rand_core"
 version = "0.6.3"
@@ -1038,7 +1068,16 @@ version = "0.3.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "d51e9f596de227fda2ea6c84607f5558e196eeaf43c986b724ba4fb8fdf497e7"
 dependencies = [
- "rand_core",
+ "rand_core 0.6.3",
+]
+
+[[package]]
+name = "rand_xoshiro"
+version = "0.4.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a9fcdd2e881d02f1d9390ae47ad8e5696a9e4be7b547a1da2afbc61973217004"
+dependencies = [
+ "rand_core 0.5.1",
 ]
 
 [[package]]
@@ -1191,6 +1230,16 @@ dependencies = [
  "failure",
 ]
 
+[[package]]
+name = "sized-chunks"
+version = "0.6.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "16d69225bde7a69b235da73377861095455d298f2b970996eec25ddbb42b3d1e"
+dependencies = [
+ "bitmaps",
+ "typenum",
+]
+
 [[package]]
 name = "strsim"
 version = "0.8.0"
diff --git a/driver.py b/driver.py
index 7c806f231..61c1f73cc 100755
--- a/driver.py
+++ b/driver.py
@@ -23,6 +23,10 @@ def verify_path_empty(path) -> bool:
             if verify_path_empty(ABY_SOURCE):
                 subprocess.run(["git", "clone", "https://github.com/edwjchen/ABY.git", ABY_SOURCE])
                 subprocess.run(["./scripts/build_aby.zsh"])
+        if f == "seal":
+            if verify_path_empty(SEAL_SOURCE):
+                subprocess.run(["git", "clone", "https://github.com/Northrim/SEAL.git", SEAL_SOURCE])
+                subprocess.run(["./scripts/build_seal.zsh"])
 
     # install python requirements
     subprocess.run(["pip3", "install", "-r", "requirements.txt"])
@@ -76,6 +80,12 @@ def build(features):
         if "smt" in features and "zok" in features:
             subprocess.run(["./scripts/build_mpc_zokrates_test.zsh"], check=True)
         subprocess.run(["./scripts/build_aby.zsh"], check=True)
+    if "seal" in features:
+        if "c" in features:
+            subprocess.run(["./scripts/build_fhe_c_test.zsh"], check=True)
+        if "smt" in features and "zok" in features:
+            subprocess.run(["./scripts/build_fhe_zokrates_test.zsh"], check=True)
+        subprocess.run(["./scripts/build_seal.zsh"], check=True)
 
 def test(features):
     """
@@ -101,6 +111,8 @@ def test(features):
     if "zok" in features and "smt" in features:
         if "aby" in features:
             subprocess.run(["python3", "./scripts/aby_tests/zokrates_test_aby.py"], check=True)
+        if "seal" in features:
+            subprocess.run(["python3", "./scripts/seal_tests/zokrates_test_seal.py"], check=True)
         if "lp" in features:
             subprocess.run(["./scripts/test_zok_to_ilp.zsh"], check=True)
         if "r1cs" in features:
@@ -111,6 +123,8 @@ def test(features):
     if "c" in features:
         if "aby" in features:
             subprocess.run(["python3", "./scripts/aby_tests/c_test_aby.py"], check=True)
+        if "seal" in features:
+            subprocess.run(["python3", "./scripts/seal_tests/c_test_seal.py"], check=True)
 
 def benchmark(features):
     mode = load_mode()
@@ -165,6 +179,8 @@ def clean(features):
     print("cleaning!")
     if "aby" in features:
         subprocess.run(["./scripts/clean_aby.zsh"])
+    if "seal" in features:
+        subprocess.run(["./scripts/clean_seal.zsh"])
     subprocess.run(["rm", "-rf", "scripts/aby_tests/__pycache__"])
     subprocess.run(["rm", "-rf", "P", "V", "pi", "perf.data perf.data.old flamegraph.svg"])
 
@@ -210,7 +226,7 @@ def verify_feature(f):
     parser.add_argument("-m", "--mode", type=str, help="set `debug` or `release` mode")
     parser.add_argument("-A", "--all_features", action="store_true", help="set all features on")
     parser.add_argument("-L", "--list_features", action="store_true", help="print active features")
-    parser.add_argument("-F", "--features", nargs="+", help="set features on <aby, c, lp, r1cs, smt, zok>, reset features with -F none")
+    parser.add_argument("-F", "--features", nargs="+", help="set features on <aby, c, lp, r1cs, seal, smt, zok>, reset features with -F none")
     parser.add_argument("--benchmark", action="store_true", help="build benchmarks")
     parser.add_argument("extra", metavar="PASS_THROUGH_ARGS", nargs=argparse.REMAINDER, help="Extra arguments for --flamegraph. Prefix with --")
     args = parser.parse_args()
diff --git a/examples/C/fhe/unit_tests/arithmetic_tests/add.c b/examples/C/fhe/unit_tests/arithmetic_tests/add.c
new file mode 100644
index 000000000..fab58cef4
--- /dev/null
+++ b/examples/C/fhe/unit_tests/arithmetic_tests/add.c
@@ -0,0 +1,3 @@
+int main(__attribute__((private(0))) int a, __attribute__((private(1))) int b) { 
+   return a + b;
+}
\ No newline at end of file
diff --git a/examples/C/fhe/unit_tests/arithmetic_tests/mult.c b/examples/C/fhe/unit_tests/arithmetic_tests/mult.c
new file mode 100644
index 000000000..9404cd925
--- /dev/null
+++ b/examples/C/fhe/unit_tests/arithmetic_tests/mult.c
@@ -0,0 +1,3 @@
+int main(__attribute__((private(0))) int a, __attribute__((private(1))) int b) { 
+   return a * b;
+}
\ No newline at end of file
diff --git a/examples/C/fhe/unit_tests/arithmetic_tests/mult_add_pub.c b/examples/C/fhe/unit_tests/arithmetic_tests/mult_add_pub.c
new file mode 100644
index 000000000..917ec25c6
--- /dev/null
+++ b/examples/C/fhe/unit_tests/arithmetic_tests/mult_add_pub.c
@@ -0,0 +1,3 @@
+int main(__attribute__((private(0))) int a, __attribute__((private(1))) int b, __attribute__((public)) int v) { 
+   return a * b + v;
+}
\ No newline at end of file
diff --git a/examples/C/fhe/unit_tests/boolean_tests/boolean_and.c b/examples/C/fhe/unit_tests/boolean_tests/boolean_and.c
new file mode 100644
index 000000000..6e4e8258b
--- /dev/null
+++ b/examples/C/fhe/unit_tests/boolean_tests/boolean_and.c
@@ -0,0 +1,5 @@
+#include <stdbool.h>
+
+bool main(__attribute__((private(0))) bool a, __attribute__((private(1))) bool b) { 
+   return a && b;
+}
\ No newline at end of file
diff --git a/examples/C/fhe/unit_tests/boolean_tests/boolean_equals.c b/examples/C/fhe/unit_tests/boolean_tests/boolean_equals.c
new file mode 100644
index 000000000..d0b00b09b
--- /dev/null
+++ b/examples/C/fhe/unit_tests/boolean_tests/boolean_equals.c
@@ -0,0 +1,5 @@
+#include <stdbool.h>
+
+bool main(__attribute__((private(0))) bool a, __attribute__((private(1))) bool b) { 
+   return a == b;
+}
\ No newline at end of file
diff --git a/examples/C/fhe/unit_tests/boolean_tests/boolean_or.c b/examples/C/fhe/unit_tests/boolean_tests/boolean_or.c
new file mode 100644
index 000000000..b66126c02
--- /dev/null
+++ b/examples/C/fhe/unit_tests/boolean_tests/boolean_or.c
@@ -0,0 +1,5 @@
+#include <stdbool.h>
+
+bool main(__attribute__((private(0))) bool a, __attribute__((private(1))) bool b) { 
+   return a || b;
+}
\ No newline at end of file
diff --git a/examples/C/fhe/unit_tests/nary_arithmetic_tests/nary_arithmetic_add.c b/examples/C/fhe/unit_tests/nary_arithmetic_tests/nary_arithmetic_add.c
new file mode 100644
index 000000000..c8af060fa
--- /dev/null
+++ b/examples/C/fhe/unit_tests/nary_arithmetic_tests/nary_arithmetic_add.c
@@ -0,0 +1,3 @@
+int main(__attribute__((private(0))) int a, __attribute__((private(1))) int b, __attribute__((private(1))) int c) { 
+  return a + b + c;
+}
\ No newline at end of file
diff --git a/examples/C/fhe/unit_tests/nary_boolean_tests/nary_boolean_and.c b/examples/C/fhe/unit_tests/nary_boolean_tests/nary_boolean_and.c
new file mode 100644
index 000000000..c80224b47
--- /dev/null
+++ b/examples/C/fhe/unit_tests/nary_boolean_tests/nary_boolean_and.c
@@ -0,0 +1,5 @@
+#include <stdbool.h>
+
+bool main(__attribute__((private(0))) bool a, __attribute__((private(1))) bool b, __attribute__((private(1))) bool c) { 
+  return a && b && c;
+}
\ No newline at end of file
diff --git a/examples/ZoKrates/fhe/unit_tests/arithmetic_tests/add.zok b/examples/ZoKrates/fhe/unit_tests/arithmetic_tests/add.zok
new file mode 100644
index 000000000..f90f2f531
--- /dev/null
+++ b/examples/ZoKrates/fhe/unit_tests/arithmetic_tests/add.zok
@@ -0,0 +1,2 @@
+def main(private u32 a, private u32 b) -> u32:
+  return a + b
\ No newline at end of file
diff --git a/examples/ZoKrates/fhe/unit_tests/arithmetic_tests/mult.zok b/examples/ZoKrates/fhe/unit_tests/arithmetic_tests/mult.zok
new file mode 100644
index 000000000..2b3e028b7
--- /dev/null
+++ b/examples/ZoKrates/fhe/unit_tests/arithmetic_tests/mult.zok
@@ -0,0 +1,2 @@
+def main(private u32 a, private u32 b) -> u32:
+  return a * b
diff --git a/examples/ZoKrates/fhe/unit_tests/arithmetic_tests/mult_add_pub.zok b/examples/ZoKrates/fhe/unit_tests/arithmetic_tests/mult_add_pub.zok
new file mode 100644
index 000000000..804a9c902
--- /dev/null
+++ b/examples/ZoKrates/fhe/unit_tests/arithmetic_tests/mult_add_pub.zok
@@ -0,0 +1,3 @@
+
+def main(private u32 a, private u32 b, public u32 v) -> u32:
+  return a * b + v
diff --git a/examples/ZoKrates/fhe/unit_tests/boolean_tests/boolean_and.zok b/examples/ZoKrates/fhe/unit_tests/boolean_tests/boolean_and.zok
new file mode 100644
index 000000000..da377ffd4
--- /dev/null
+++ b/examples/ZoKrates/fhe/unit_tests/boolean_tests/boolean_and.zok
@@ -0,0 +1,2 @@
+def main(private bool a, private bool b) -> bool:
+    return a && b
\ No newline at end of file
diff --git a/examples/ZoKrates/fhe/unit_tests/boolean_tests/boolean_equals.zok b/examples/ZoKrates/fhe/unit_tests/boolean_tests/boolean_equals.zok
new file mode 100644
index 000000000..977a07225
--- /dev/null
+++ b/examples/ZoKrates/fhe/unit_tests/boolean_tests/boolean_equals.zok
@@ -0,0 +1,2 @@
+def main(private bool a, private bool b) -> bool:
+    return a == b
\ No newline at end of file
diff --git a/examples/ZoKrates/fhe/unit_tests/boolean_tests/boolean_or.zok b/examples/ZoKrates/fhe/unit_tests/boolean_tests/boolean_or.zok
new file mode 100644
index 000000000..025fa0597
--- /dev/null
+++ b/examples/ZoKrates/fhe/unit_tests/boolean_tests/boolean_or.zok
@@ -0,0 +1,2 @@
+def main(private bool a, private bool b) -> bool:
+    return a || b
\ No newline at end of file
diff --git a/examples/ZoKrates/fhe/unit_tests/nary_arithmetic_tests/nary_arithmetic_add.zok b/examples/ZoKrates/fhe/unit_tests/nary_arithmetic_tests/nary_arithmetic_add.zok
new file mode 100644
index 000000000..f78e1af69
--- /dev/null
+++ b/examples/ZoKrates/fhe/unit_tests/nary_arithmetic_tests/nary_arithmetic_add.zok
@@ -0,0 +1,2 @@
+def main(private u32 a, private u32 b,  private u32 c) -> u32:
+  return a + b + c
diff --git a/examples/ZoKrates/fhe/unit_tests/nary_boolean_tests/nary_boolean_and.zok b/examples/ZoKrates/fhe/unit_tests/nary_boolean_tests/nary_boolean_and.zok
new file mode 100644
index 000000000..a113942fd
--- /dev/null
+++ b/examples/ZoKrates/fhe/unit_tests/nary_boolean_tests/nary_boolean_and.zok
@@ -0,0 +1,2 @@
+def main(private bool a, private bool b, private bool c) -> bool:
+  return a && b && c
diff --git a/examples/circ.rs b/examples/circ.rs
index 2872b0594..7f1df3e6d 100644
--- a/examples/circ.rs
+++ b/examples/circ.rs
@@ -20,6 +20,7 @@ use circ::ir::{
     term::extras::Letified,
 };
 use circ::target::aby::trans::to_aby;
+use circ::target::fhe::trans::to_fhe;
 #[cfg(feature = "lp")]
 use circ::target::ilp::trans::to_ilp;
 #[cfg(feature = "r1cs")]
@@ -101,6 +102,7 @@ enum Backend {
     },
     Smt {},
     Ilp {},
+    Fhe {},
     Mpc {
         #[structopt(long, default_value = "hycc", name = "cost_model")]
         cost_model: String,
@@ -187,6 +189,7 @@ fn main() {
         Backend::Ilp { .. } => Mode::Opt,
         Backend::Mpc { .. } => Mode::Mpc(options.parties),
         Backend::Smt { .. } => Mode::Proof,
+        Backend::Fhe { .. } => Mode::Fhe,
     };
     let language = determine_language(&options.frontend.language, &options.path);
     let cs = match language {
@@ -246,6 +249,7 @@ fn main() {
             ],
             // vec![Opt::Sha, Opt::ConstantFold, Opt::Mem, Opt::ConstantFold],
         ),
+        Mode::Fhe => opt(cs, vec![Opt::ConstantFold]),
         Mode::Proof | Mode::ProofOfHighValue(_) => opt(
             cs,
             vec![
@@ -384,6 +388,15 @@ fn main() {
                 todo!()
             }
         }
+        Backend::Fhe { .. } => {
+            println!("Converting to fhe");
+            let lang_str = match language {
+                DeterminedLanguage::C => "c".to_string(),
+                DeterminedLanguage::Zsharp => "zok".to_string(),
+                _ => panic!("Language isn't supported by FHE backend: {:#?}", language),
+            };
+            to_fhe(cs, &path_buf, &lang_str);
+        }
         #[cfg(not(feature = "smt"))]
         Backend::Smt { .. } => {
             panic!("Missing feature: smt");
diff --git a/scripts/build_fhe_c_test.zsh b/scripts/build_fhe_c_test.zsh
new file mode 100755
index 000000000..d33a475ad
--- /dev/null
+++ b/scripts/build_fhe_c_test.zsh
@@ -0,0 +1,40 @@
+#!/usr/bin/env zsh
+
+set -ex
+
+disable -r time
+
+# cargo build --release --features c --example circ 
+
+BIN=./target/release/examples/circ
+export CARGO_MANIFEST_DIR=$(pwd)
+
+case "$OSTYPE" in 
+    darwin*)
+        alias measure_time="gtime --format='%e seconds %M kB'"
+    ;;
+    linux*)
+        alias measure_time="time --format='%e seconds %M kB'"
+    ;;
+esac
+
+function fhe_test {
+    cpath=$1
+    RUST_BACKTRACE=1 measure_time $BIN $cpath fhe
+}
+
+# build boolean tests
+fhe_test ./examples/C/fhe/unit_tests/boolean_tests/boolean_and.c
+fhe_test ./examples/C/fhe/unit_tests/boolean_tests/boolean_or.c
+fhe_test ./examples/C/fhe/unit_tests/boolean_tests/boolean_equals.c
+
+# build nary boolean tests
+fhe_test ./examples/C/fhe/unit_tests/nary_boolean_tests/nary_boolean_and.c
+
+# build arithmetic tests
+fhe_test ./examples/C/fhe/unit_tests/arithmetic_tests/add.c
+fhe_test ./examples/C/fhe/unit_tests/arithmetic_tests/mult.c
+fhe_test ./examples/C/fhe/unit_tests/arithmetic_tests/mult_add_pub.c
+
+# build nary arithmetic tests
+fhe_test ./examples/C/fhe/unit_tests/nary_arithmetic_tests/nary_arithmetic_add.c
\ No newline at end of file
diff --git a/scripts/build_fhe_zokrates_test.zsh b/scripts/build_fhe_zokrates_test.zsh
new file mode 100755
index 000000000..1d589ed44
--- /dev/null
+++ b/scripts/build_fhe_zokrates_test.zsh
@@ -0,0 +1,41 @@
+#!/usr/bin/env zsh
+
+set -ex
+
+disable -r time
+
+# cargo build --release --features smt,zok --example circ
+
+BIN=./target/release/examples/circ
+#export CARGO_MANIFEST_DIR=$(pwd)
+
+case "$OSTYPE" in 
+    darwin*)
+        alias measure_time="gtime --format='%e seconds %M kB'"
+    ;;
+    linux*)
+        alias measure_time="time --format='%e seconds %M kB'"
+    ;;
+esac
+
+function fhe_test {
+    zpath=$1
+    RUST_BACKTRACE=1 measure_time $BIN $zpath fhe
+}
+
+# build boolean tests
+fhe_test ./examples/ZoKrates/fhe/unit_tests/boolean_tests/boolean_and.zok
+fhe_test ./examples/ZoKrates/fhe/unit_tests/boolean_tests/boolean_or.zok 
+fhe_test ./examples/ZoKrates/fhe/unit_tests/boolean_tests/boolean_equals.zok 
+
+# build nary boolean tests
+fhe_test ./examples/ZoKrates/fhe/unit_tests/nary_boolean_tests/nary_boolean_and.zok
+
+# build arithmetic tests
+fhe_test ./examples/ZoKrates/fhe/unit_tests/arithmetic_tests/add.zok
+fhe_test ./examples/ZoKrates/fhe/unit_tests/arithmetic_tests/mult.zok
+fhe_test ./examples/ZoKrates/fhe/unit_tests/arithmetic_tests/mult_add_pub.zok
+
+# build nary arithmetic tests
+fhe_test ./examples/ZoKrates/fhe/unit_tests/nary_arithmetic_tests/nary_arithmetic_add.zok
+
diff --git a/scripts/build_seal.zsh b/scripts/build_seal.zsh
new file mode 100755
index 000000000..33ba7728b
--- /dev/null
+++ b/scripts/build_seal.zsh
@@ -0,0 +1,9 @@
+#!/usr/bin/env zsh
+
+if [[ ! -z ${SEAL_SOURCE} ]]; then 
+    cd ${SEAL_SOURCE}
+    cmake -S . -B build -DSEAL_BUILD_EXAMPLES=ON
+    cmake --build build
+else
+    echo "Missing SEAL_SOURCE environment variable."
+fi
\ No newline at end of file
diff --git a/scripts/clean_seal.zsh b/scripts/clean_seal.zsh
new file mode 100755
index 000000000..18a3cb411
--- /dev/null
+++ b/scripts/clean_seal.zsh
@@ -0,0 +1,4 @@
+#!/usr/bin/env zsh
+
+rm -rf ./scripts/seal_tests/tests
+rm -rf ./scripts/seal_tests/__pycache__
diff --git a/scripts/seal_tests/c_test_seal.py b/scripts/seal_tests/c_test_seal.py
new file mode 100644
index 000000000..f6ffa5660
--- /dev/null
+++ b/scripts/seal_tests/c_test_seal.py
@@ -0,0 +1,9 @@
+#!/usr/bin/env python
+
+from util import run_tests
+from test_suite import *
+
+if __name__ == "__main__":
+    tests = boolean_tests + arithmetic_tests + nary_arithmetic_tests + nary_boolean_tests
+
+    run_tests('c', tests)
diff --git a/scripts/seal_tests/make_tests.py b/scripts/seal_tests/make_tests.py
new file mode 100644
index 000000000..a59976d8a
--- /dev/null
+++ b/scripts/seal_tests/make_tests.py
@@ -0,0 +1,104 @@
+def batch_add_inputs(s):
+    filename = "scripts/seal_tests/tests/batch_add_" + str(s) + ".txt"
+    with open(filename, 'w') as f:
+        line1 = ["arr", "a"]
+        line2 = ["arr", "b"]
+        line3 = ["res"] + [str(s)] * s
+        for i in range(s):
+            line1.append(str(i))
+            line2.append(str(s-i))
+        f.write(" ".join(line1) + "\n")
+        f.write(" ".join(line2) + "\n")
+        f.write(" ".join(line3))    
+
+def batch_mul_inputs(s):
+    filename = "scripts/seal_tests/tests/batch_mul_" + str(s) + ".txt"
+    with open(filename, 'w') as f:
+        line1 = ["arr", "a"]
+        line2 = ["arr", "b"]
+        line3 = ["res"]
+        for i in range(s):
+            line1.append(str(i))
+            line2.append(str(s-i))
+            line3.append(str(i * (s-i)))
+        f.write(" ".join(line1) + "\n")
+        f.write(" ".join(line2) + "\n")
+        f.write(" ".join(line3))
+
+def batch_add_bytecode(s):
+    filename = "scripts/seal_tests/tests/batch_add_bytecode_" + str(s) + ".txt"
+    with open(filename, 'w') as f:
+        f.write("3 1 a 1 " + str(s) + " 1 ARR_IN\n")
+        f.write("3 1 b 1 " + str(s) + " 0 ARR_IN\n")
+        f.write("2 1 1 0 2 ADD\n")
+        f.write("2 0 2 " + str(s) + " ARR_OUT")
+
+def batch_mul_bytecode(s):
+    filename = "scripts/seal_tests/tests/batch_mul_bytecode_" + str(s) + ".txt"
+    with open(filename, 'w') as f:
+        f.write("3 1 a 1 " + str(s) + " 1 ARR_IN\n")
+        f.write("3 1 b 1 " + str(s) + " 0 ARR_IN\n")
+        f.write("2 1 1 0 2 MUL\n")
+        f.write("2 0 2 " + str(s) + " ARR_OUT")
+
+def naive_add_inputs(s):
+    filename = "scripts/seal_tests/tests/naive_add_" + str(s) + ".txt"
+    with open(filename, 'w') as f:
+        lines = []
+        for i in range(s):
+            lines.append(f"a_{i} {i}")
+            lines.append(f"b_{i} {s-i}")
+        lines.append(f"res {s}")
+        f.write("\n".join(lines))
+
+def naive_mul_inputs(s):
+    filename = "scripts/seal_tests/tests/naive_mul_" + str(s) + ".txt"
+    with open(filename, 'w') as f:
+        lines = []
+        for i in range(s):
+            lines.append(f"a_{i} {i}")
+            lines.append(f"b_{i} {s-i}")
+        lines.append("res 0")
+        f.write("\n".join(lines))    
+
+def naive_add_bytecode(s):
+    filename = "scripts/seal_tests/tests/naive_add_bytecode_" + str(s) + ".txt"
+    with open(filename, 'w') as f:
+        for i in range(s):
+            f.write(f"2 1 a_{i} 1 {2*i} IN\n")
+            f.write(f"2 1 b_{i} 1 {2*i + 1} IN\n")
+        for i in range(s):
+            f.write(f"2 1 {2*i} {2*i + 1} {2*s + i} ADD\n")
+        f.write(f"1 0 {2*s} OUT")
+
+def naive_mul_bytecode(s):
+    filename = "scripts/seal_tests/tests/naive_mul_bytecode_" + str(s) + ".txt"
+    with open(filename, 'w') as f:
+        for i in range(s):
+            f.write(f"2 1 a_{i} 1 {2*i} IN\n")
+            f.write(f"2 1 b_{i} 1 {2*i + 1} IN\n")
+        for i in range(s):
+            f.write(f"2 1 {2*i} {2*i + 1} {2*s + i} MUL\n")
+        f.write(f"1 0 {2*s} OUT")
+
+
+sizes = [4, 16, 64, 256, 1024]
+
+for s in sizes:
+    batch_add_inputs(s)
+    batch_mul_inputs(s)
+    batch_add_bytecode(s)
+    batch_mul_bytecode(s)
+
+    naive_add_inputs(s)
+    naive_mul_inputs(s)
+    naive_add_bytecode(s)
+    naive_mul_bytecode(s)
+
+with open("scripts/seal_tests/tests/code_to_add.txt", "w") as f:
+    for s in sizes:
+        f.write(f"    run_test(['99'], [\"./../SEAL/build/bin/sealinterpreter -M fhe -b  ./scripts/seal_tests/tests/batch_add_bytecode_{s}.txt -t ./scripts/seal_tests/tests/batch_add_{s}.txt\"], True)\n")
+        f.write(f"    run_test(['99'], [\"./../SEAL/build/bin/sealinterpreter -M fhe -b  ./scripts/seal_tests/tests/naive_add_bytecode_{s}.txt -t ./scripts/seal_tests/tests/naive_add_{s}.txt\"], True)\n")
+    for s in sizes:
+        f.write(f"    run_test(['99'], [\"./../SEAL/build/bin/sealinterpreter -M fhe -b  ./scripts/seal_tests/tests/batch_mul_bytecode_{s}.txt -t ./scripts/seal_tests/tests/batch_mul_{s}.txt\"], True)\n")
+        f.write(f"    run_test(['99'], [\"./../SEAL/build/bin/sealinterpreter -M fhe -b  ./scripts/seal_tests/tests/naive_mul_bytecode_{s}.txt -t ./scripts/seal_tests/tests/naive_mul_{s}.txt\"], True)\n")
\ No newline at end of file
diff --git a/scripts/seal_tests/test_inputs/add.txt b/scripts/seal_tests/test_inputs/add.txt
new file mode 100644
index 000000000..9d0338538
--- /dev/null
+++ b/scripts/seal_tests/test_inputs/add.txt
@@ -0,0 +1,3 @@
+a 1 
+b 2
+res 3
\ No newline at end of file
diff --git a/scripts/seal_tests/test_inputs/and_1.txt b/scripts/seal_tests/test_inputs/and_1.txt
new file mode 100644
index 000000000..bffd79e1a
--- /dev/null
+++ b/scripts/seal_tests/test_inputs/and_1.txt
@@ -0,0 +1,3 @@
+a 0
+b 0
+res 0
\ No newline at end of file
diff --git a/scripts/seal_tests/test_inputs/and_2.txt b/scripts/seal_tests/test_inputs/and_2.txt
new file mode 100644
index 000000000..a9e356a5b
--- /dev/null
+++ b/scripts/seal_tests/test_inputs/and_2.txt
@@ -0,0 +1,3 @@
+a 1
+b 0
+res 0
\ No newline at end of file
diff --git a/scripts/seal_tests/test_inputs/and_3.txt b/scripts/seal_tests/test_inputs/and_3.txt
new file mode 100644
index 000000000..d516da12a
--- /dev/null
+++ b/scripts/seal_tests/test_inputs/and_3.txt
@@ -0,0 +1,3 @@
+a 0
+b 1
+res 0
\ No newline at end of file
diff --git a/scripts/seal_tests/test_inputs/and_4.txt b/scripts/seal_tests/test_inputs/and_4.txt
new file mode 100644
index 000000000..e7129253a
--- /dev/null
+++ b/scripts/seal_tests/test_inputs/and_4.txt
@@ -0,0 +1,3 @@
+a 1
+b 1
+res 1
\ No newline at end of file
diff --git a/scripts/seal_tests/test_inputs/eq_1.txt b/scripts/seal_tests/test_inputs/eq_1.txt
new file mode 100644
index 000000000..a9e356a5b
--- /dev/null
+++ b/scripts/seal_tests/test_inputs/eq_1.txt
@@ -0,0 +1,3 @@
+a 1
+b 0
+res 0
\ No newline at end of file
diff --git a/scripts/seal_tests/test_inputs/eq_2.txt b/scripts/seal_tests/test_inputs/eq_2.txt
new file mode 100644
index 000000000..e7129253a
--- /dev/null
+++ b/scripts/seal_tests/test_inputs/eq_2.txt
@@ -0,0 +1,3 @@
+a 1
+b 1
+res 1
\ No newline at end of file
diff --git a/scripts/seal_tests/test_inputs/mult_1.txt b/scripts/seal_tests/test_inputs/mult_1.txt
new file mode 100644
index 000000000..596a6ab24
--- /dev/null
+++ b/scripts/seal_tests/test_inputs/mult_1.txt
@@ -0,0 +1,3 @@
+a 0 
+b 5
+res 0
\ No newline at end of file
diff --git a/scripts/seal_tests/test_inputs/mult_2.txt b/scripts/seal_tests/test_inputs/mult_2.txt
new file mode 100644
index 000000000..f3a9b265c
--- /dev/null
+++ b/scripts/seal_tests/test_inputs/mult_2.txt
@@ -0,0 +1,3 @@
+a 1 
+b 5
+res 5
\ No newline at end of file
diff --git a/scripts/seal_tests/test_inputs/mult_3.txt b/scripts/seal_tests/test_inputs/mult_3.txt
new file mode 100644
index 000000000..0c84b4868
--- /dev/null
+++ b/scripts/seal_tests/test_inputs/mult_3.txt
@@ -0,0 +1,3 @@
+a 2 
+b 5
+res 10
\ No newline at end of file
diff --git a/scripts/seal_tests/test_inputs/mult_add_pub_1.txt b/scripts/seal_tests/test_inputs/mult_add_pub_1.txt
new file mode 100644
index 000000000..3c5e755dd
--- /dev/null
+++ b/scripts/seal_tests/test_inputs/mult_add_pub_1.txt
@@ -0,0 +1,4 @@
+a 5 
+v 7
+b 7
+res 42
\ No newline at end of file
diff --git a/scripts/seal_tests/test_inputs/mult_add_pub_2.txt b/scripts/seal_tests/test_inputs/mult_add_pub_2.txt
new file mode 100644
index 000000000..3c5e755dd
--- /dev/null
+++ b/scripts/seal_tests/test_inputs/mult_add_pub_2.txt
@@ -0,0 +1,4 @@
+a 5 
+v 7
+b 7
+res 42
\ No newline at end of file
diff --git a/scripts/seal_tests/test_inputs/nary_add.txt b/scripts/seal_tests/test_inputs/nary_add.txt
new file mode 100644
index 000000000..780d3579c
--- /dev/null
+++ b/scripts/seal_tests/test_inputs/nary_add.txt
@@ -0,0 +1,4 @@
+a 1
+b 2
+c 3
+res 6
\ No newline at end of file
diff --git a/scripts/seal_tests/test_inputs/nary_and.txt b/scripts/seal_tests/test_inputs/nary_and.txt
new file mode 100644
index 000000000..1fffca872
--- /dev/null
+++ b/scripts/seal_tests/test_inputs/nary_and.txt
@@ -0,0 +1,4 @@
+a 1
+b 1
+c 1
+res 1
\ No newline at end of file
diff --git a/scripts/seal_tests/test_inputs/or_1.txt b/scripts/seal_tests/test_inputs/or_1.txt
new file mode 100644
index 000000000..b7504f131
--- /dev/null
+++ b/scripts/seal_tests/test_inputs/or_1.txt
@@ -0,0 +1,3 @@
+a 0 
+b 0
+res 0
\ No newline at end of file
diff --git a/scripts/seal_tests/test_inputs/or_2.txt b/scripts/seal_tests/test_inputs/or_2.txt
new file mode 100644
index 000000000..b35d53a3c
--- /dev/null
+++ b/scripts/seal_tests/test_inputs/or_2.txt
@@ -0,0 +1,3 @@
+a 1
+b 0
+res 1
\ No newline at end of file
diff --git a/scripts/seal_tests/test_inputs/or_3.txt b/scripts/seal_tests/test_inputs/or_3.txt
new file mode 100644
index 000000000..e97a331be
--- /dev/null
+++ b/scripts/seal_tests/test_inputs/or_3.txt
@@ -0,0 +1,3 @@
+a 0
+b 1
+res 1
\ No newline at end of file
diff --git a/scripts/seal_tests/test_inputs/or_4.txt b/scripts/seal_tests/test_inputs/or_4.txt
new file mode 100644
index 000000000..e7129253a
--- /dev/null
+++ b/scripts/seal_tests/test_inputs/or_4.txt
@@ -0,0 +1,3 @@
+a 1
+b 1
+res 1
\ No newline at end of file
diff --git a/scripts/seal_tests/test_suite.py b/scripts/seal_tests/test_suite.py
new file mode 100644
index 000000000..d81215828
--- /dev/null
+++ b/scripts/seal_tests/test_suite.py
@@ -0,0 +1,102 @@
+boolean_tests = [
+    [
+        "Boolean && - 1",
+        "boolean_and",
+        "./scripts/seal_tests/test_inputs/and_1.txt",
+    ],
+    [
+        "Boolean && - 2",
+        "boolean_and",
+        "./scripts/seal_tests/test_inputs/and_2.txt",
+    ],
+    [
+        "Boolean && - 3",
+        "boolean_and",
+        "./scripts/seal_tests/test_inputs/and_3.txt",
+    ],
+    [
+        "Boolean && - 4",
+        "boolean_and",
+        "./scripts/seal_tests/test_inputs/and_4.txt",
+    ],
+    [
+        "Boolean || - 1",
+        "boolean_or",
+        "./scripts/seal_tests/test_inputs/or_1.txt",
+    ],
+    [
+        "Boolean || - 2",
+        "boolean_or",
+        "./scripts/seal_tests/test_inputs/or_2.txt",
+
+    ],
+    [
+        "Boolean || - 3",
+        "boolean_or",
+        "./scripts/seal_tests/test_inputs/or_3.txt",
+
+    ],
+    [
+        "Boolean || - 4",
+        "boolean_or",
+        "./scripts/seal_tests/test_inputs/or_4.txt",
+    ],
+    [
+        "Boolean == - 1",
+        "boolean_equals",
+        "./scripts/seal_tests/test_inputs/eq_1.txt",
+    ],
+    [
+        "Boolean == - 2",
+        "boolean_equals",
+        "./scripts/seal_tests/test_inputs/eq_2.txt",
+    ],
+]
+
+arithmetic_tests = [
+    [
+        "Add two numbers",
+        "add",
+        "./scripts/seal_tests/test_inputs/add.txt",
+    ], 
+    [
+        "Multiply two numbers - 1",
+        "mult",
+        "./scripts/seal_tests/test_inputs/mult_1.txt",
+    ], 
+    [
+        "Multiply two numbers - 2",
+        "mult",
+        "./scripts/seal_tests/test_inputs/mult_2.txt",
+    ], 
+    [
+        "Multiply two numbers - 3",
+        "mult",
+        "./scripts/seal_tests/test_inputs/mult_3.txt",
+    ], 
+    [
+        "Multiply two numbers together and add with public value",
+        "mult_add_pub",
+        "./scripts/seal_tests/test_inputs/mult_add_pub_1.txt",
+    ], 
+    [
+        "Multiply two numbers together and add with public value, check only server side public value is added",
+        "mult_add_pub",
+        "./scripts/seal_tests/test_inputs/mult_add_pub_2.txt",
+    ], 
+]
+nary_arithmetic_tests = [
+    [
+        "Test a + b + c",
+        "nary_arithmetic_add",
+        "./scripts/seal_tests/test_inputs/nary_add.txt",
+    ],
+]
+
+nary_boolean_tests = [
+    [
+        "Test a & b & c",
+        "nary_boolean_and",
+        "./scripts/seal_tests/test_inputs/nary_and.txt",
+    ],
+]
\ No newline at end of file
diff --git a/scripts/seal_tests/util.py b/scripts/seal_tests/util.py
new file mode 100644
index 000000000..b87366be7
--- /dev/null
+++ b/scripts/seal_tests/util.py
@@ -0,0 +1,107 @@
+import os 
+from subprocess import Popen, PIPE
+import sys
+from typing import List
+from tqdm import tqdm
+import time
+
+def rename_test(name: str, lang: str) -> str:
+    """Append path with language type"""
+    return f"{name}_{lang}"
+
+def build_cmd(name:str, test_file: str) -> List[str]:
+    bytecode = f"./scripts/seal_tests/tests/{name}_bytecode.txt"
+    return [os.getenv("SEAL_SOURCE") + "/build/bin/sealinterpreter", "-M", "fhe", "-b", bytecode, "-t", test_file] 
+
+def get_result(file_path):
+    if os.path.exists(file_path):
+        with open(file_path) as f:
+            lines = f.read().splitlines()
+            for line in lines:
+                l = line.split()
+                if l and l[0] == "res":
+                    return l[1:]
+            raise RuntimeError("Unable to find result: "+file_path)
+    else:
+        raise RuntimeError("Unable to open file: "+file_path)
+
+
+def run_test(expected: List[str], cmd: List[str], verbose = False) -> bool:
+    try:
+        start = time.time()
+        proc = Popen(" ".join(cmd), shell=True, stdout=PIPE, stderr=PIPE)
+
+        out, err = proc.communicate(timeout=30)
+        end = time.time()
+        if verbose:
+            print("Command:", " ".join(cmd))
+            print("  Time: ", end - start)
+
+        if err:
+            raise RuntimeError("Error: "+err.decode("utf-8").strip())
+
+        output = []
+        for o in out.split():
+            output.append(o.decode("utf-8"))
+
+        assert (output == expected), "out: "+" ".join(output)+"\nexpected: "+" ".join(expected)
+        return True, ""
+    except Exception as e:
+        #print("Exception: ", e)
+        return False, e
+
+def run_tests(lang: str, tests: List[dict]):
+    """
+    tests will be a list of all tests to run. each element in the list will be 
+    1. description of test case: str
+    2. test name: str
+    4. test file path: str 
+    """
+    print(f"Running Custom tests for {lang} frontend")
+    run_test(['99'], ["./../SEAL/build/bin/sealinterpreter -M fhe -b  ./scripts/seal_tests/tests/batch_add_bytecode_4.txt -t ./scripts/seal_tests/tests/batch_add_4.txt"], True)
+    run_test(['99'], ["./../SEAL/build/bin/sealinterpreter -M fhe -b  ./scripts/seal_tests/tests/naive_add_bytecode_4.txt -t ./scripts/seal_tests/tests/naive_add_4.txt"], True)
+    run_test(['99'], ["./../SEAL/build/bin/sealinterpreter -M fhe -b  ./scripts/seal_tests/tests/batch_add_bytecode_16.txt -t ./scripts/seal_tests/tests/batch_add_16.txt"], True)
+    run_test(['99'], ["./../SEAL/build/bin/sealinterpreter -M fhe -b  ./scripts/seal_tests/tests/naive_add_bytecode_16.txt -t ./scripts/seal_tests/tests/naive_add_16.txt"], True)
+    run_test(['99'], ["./../SEAL/build/bin/sealinterpreter -M fhe -b  ./scripts/seal_tests/tests/batch_add_bytecode_64.txt -t ./scripts/seal_tests/tests/batch_add_64.txt"], True)
+    run_test(['99'], ["./../SEAL/build/bin/sealinterpreter -M fhe -b  ./scripts/seal_tests/tests/naive_add_bytecode_64.txt -t ./scripts/seal_tests/tests/naive_add_64.txt"], True)
+    run_test(['99'], ["./../SEAL/build/bin/sealinterpreter -M fhe -b  ./scripts/seal_tests/tests/batch_add_bytecode_256.txt -t ./scripts/seal_tests/tests/batch_add_256.txt"], True)
+    run_test(['99'], ["./../SEAL/build/bin/sealinterpreter -M fhe -b  ./scripts/seal_tests/tests/naive_add_bytecode_256.txt -t ./scripts/seal_tests/tests/naive_add_256.txt"], True)
+    run_test(['99'], ["./../SEAL/build/bin/sealinterpreter -M fhe -b  ./scripts/seal_tests/tests/batch_add_bytecode_1024.txt -t ./scripts/seal_tests/tests/batch_add_1024.txt"], True)
+    run_test(['99'], ["./../SEAL/build/bin/sealinterpreter -M fhe -b  ./scripts/seal_tests/tests/naive_add_bytecode_1024.txt -t ./scripts/seal_tests/tests/naive_add_1024.txt"], True)
+    run_test(['99'], ["./../SEAL/build/bin/sealinterpreter -M fhe -b  ./scripts/seal_tests/tests/batch_mul_bytecode_4.txt -t ./scripts/seal_tests/tests/batch_mul_4.txt"], True)
+    run_test(['99'], ["./../SEAL/build/bin/sealinterpreter -M fhe -b  ./scripts/seal_tests/tests/naive_mul_bytecode_4.txt -t ./scripts/seal_tests/tests/naive_mul_4.txt"], True)
+    run_test(['99'], ["./../SEAL/build/bin/sealinterpreter -M fhe -b  ./scripts/seal_tests/tests/batch_mul_bytecode_16.txt -t ./scripts/seal_tests/tests/batch_mul_16.txt"], True)
+    run_test(['99'], ["./../SEAL/build/bin/sealinterpreter -M fhe -b  ./scripts/seal_tests/tests/naive_mul_bytecode_16.txt -t ./scripts/seal_tests/tests/naive_mul_16.txt"], True)
+    run_test(['99'], ["./../SEAL/build/bin/sealinterpreter -M fhe -b  ./scripts/seal_tests/tests/batch_mul_bytecode_64.txt -t ./scripts/seal_tests/tests/batch_mul_64.txt"], True)
+    run_test(['99'], ["./../SEAL/build/bin/sealinterpreter -M fhe -b  ./scripts/seal_tests/tests/naive_mul_bytecode_64.txt -t ./scripts/seal_tests/tests/naive_mul_64.txt"], True)
+    run_test(['99'], ["./../SEAL/build/bin/sealinterpreter -M fhe -b  ./scripts/seal_tests/tests/batch_mul_bytecode_256.txt -t ./scripts/seal_tests/tests/batch_mul_256.txt"], True)
+    run_test(['99'], ["./../SEAL/build/bin/sealinterpreter -M fhe -b  ./scripts/seal_tests/tests/naive_mul_bytecode_256.txt -t ./scripts/seal_tests/tests/naive_mul_256.txt"], True)
+    run_test(['99'], ["./../SEAL/build/bin/sealinterpreter -M fhe -b  ./scripts/seal_tests/tests/batch_mul_bytecode_1024.txt -t ./scripts/seal_tests/tests/batch_mul_1024.txt"], True)
+    run_test(['99'], ["./../SEAL/build/bin/sealinterpreter -M fhe -b  ./scripts/seal_tests/tests/naive_mul_bytecode_1024.txt -t ./scripts/seal_tests/tests/naive_mul_1024.txt"], True)
+
+    print(f"Running FHE tests for {lang} frontend")
+    failed_test_descs = []
+    num_retries = 2
+    
+    for test in tqdm(tests, leave=False, dynamic_ncols=True):
+        assert len(test) == 3, "test configurations are wrong for test: "+test[0]
+        desc = test[0]
+        name = test[1]
+        rename = rename_test(name, lang)
+
+        cmd = build_cmd(rename, test[2])
+
+        expected = get_result(test[2])
+
+        test_results = []
+        for _ in range(num_retries):
+            test_results.append(run_test(expected, cmd))
+        
+        if all([not r[0] for r in test_results]):
+            failed_test_descs += [(desc, e[1], " ".join(cmd)) for e in test_results]
+    
+    if len(failed_test_descs) == 0:
+        print("All tests passed ✅")
+
+    failed_test_descs = [f"{r}:\n{e}\n{cmd}" for r, e, cmd in failed_test_descs]
+    assert len(failed_test_descs) == 0, "there were failed test cases:\n======\n" + "\n\n".join(failed_test_descs)
\ No newline at end of file
diff --git a/scripts/seal_tests/zokrates_test_seal.py b/scripts/seal_tests/zokrates_test_seal.py
new file mode 100644
index 000000000..89867678d
--- /dev/null
+++ b/scripts/seal_tests/zokrates_test_seal.py
@@ -0,0 +1,11 @@
+#!/usr/bin/env python
+
+from util import run_tests
+from test_suite import *
+
+if __name__ == "__main__":
+    tests = boolean_tests + arithmetic_tests + nary_arithmetic_tests + nary_boolean_tests
+    
+    run_tests('zok', tests)
+
+
diff --git a/src/front/c/mod.rs b/src/front/c/mod.rs
index fac7c53d7..3bf23406c 100644
--- a/src/front/c/mod.rs
+++ b/src/front/c/mod.rs
@@ -241,7 +241,7 @@ impl CGen {
                                 ))
                             }
                         }
-                        Mode::Proof => PROVER_VIS,
+                        Mode::Fhe | Mode::Proof => PROVER_VIS,
                         _ => unimplemented!("Mode {} is not supported.", self.mode),
                     },
                     _ => panic!("Unknown visibility: {:#?}", name),
@@ -639,7 +639,7 @@ impl CGen {
         self.gen_stmt(f.body.clone());
         if let Some(r) = self.circ.exit_fn() {
             match self.mode {
-                Mode::Mpc(_) => {
+                Mode::Mpc(_) | Mode::Fhe => {
                     let ret_term = r.unwrap_term();
                     let ret_terms = ret_term.term.terms();
                     self.circ
diff --git a/src/front/mod.rs b/src/front/mod.rs
index 6bfa13bbf..d198b64bd 100644
--- a/src/front/mod.rs
+++ b/src/front/mod.rs
@@ -30,6 +30,8 @@ pub trait FrontEnd {
 pub enum Mode {
     /// Generating an MPC circuit. Inputs are public or private (to a party in 1..N).
     Mpc(u8),
+    /// Generating an FHE circuit. Inputs are public (plaintext) or private (ciphertext).
+    Fhe,
     /// Generating for a proof circuit. Inputs are public of private (to the prover).
     Proof,
     /// Generating for an optimization circuit. Inputs are existentially quantified.
@@ -44,6 +46,7 @@ impl Display for Mode {
     fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result {
         match *self {
             Mode::Mpc(n) => write!(f, "{}-pc", n),
+            Mode::Fhe => write!(f, "fhe"),
             Mode::Proof => write!(f, "proof"),
             Mode::Opt => write!(f, "opt"),
             Mode::ProofOfHighValue(v) => write!(f, "proof_of_high_value({})", v),
diff --git a/src/front/zsharp/mod.rs b/src/front/zsharp/mod.rs
index 8ea80dfde..add57d59c 100644
--- a/src/front/zsharp/mod.rs
+++ b/src/front/zsharp/mod.rs
@@ -658,7 +658,7 @@ impl<'ast> ZGen<'ast> {
         }
         if let Some(r) = self.circ_exit_fn() {
             match self.mode {
-                Mode::Mpc(_) => {
+                Mode::Mpc(_) | Mode::Fhe => {
                     let ret_term = r.unwrap_term();
                     let ret_terms = ret_term.terms();
                     self.circ
@@ -718,7 +718,7 @@ impl<'ast> ZGen<'ast> {
         match visibility {
             None | Some(ast::Visibility::Public(_)) => PUBLIC_VIS,
             Some(ast::Visibility::Private(private)) => match self.mode {
-                Mode::Proof | Mode::Opt | Mode::ProofOfHighValue(_) => {
+                Mode::Fhe | Mode::Proof | Mode::Opt | Mode::ProofOfHighValue(_) => {
                     if private.number.is_some() {
                         self.err(
                             format!(
diff --git a/src/target/fhe/mod.rs b/src/target/fhe/mod.rs
new file mode 100644
index 000000000..d7c038e5f
--- /dev/null
+++ b/src/target/fhe/mod.rs
@@ -0,0 +1,3 @@
+//! FHE
+pub mod trans;
+pub mod utils;
diff --git a/src/target/fhe/trans.rs b/src/target/fhe/trans.rs
new file mode 100644
index 000000000..c203fcc79
--- /dev/null
+++ b/src/target/fhe/trans.rs
@@ -0,0 +1,362 @@
+//! Lowering IR to FHE
+
+//use crate::front::datalog::Inputs;
+use crate::ir::term::*;
+use crate::target::fhe::utils::*;
+use std::path::Path;
+
+#[derive(Clone)]
+enum EmbeddedTerm {
+    Bool,
+    Bv,
+    Arr,
+}
+
+struct ToFHE {
+    md: ComputationMetadata,
+    inputs: TermSet,
+    cache: TermMap<EmbeddedTerm>,
+    term_to_stext_cnt: TermMap<i32>,
+    stext_cnt: i32,
+    bytecode_path: String,
+    bytecode_output: Vec<String>,
+}
+
+impl ToFHE {
+    fn new(md: ComputationMetadata, path: &Path, lang: &str) -> Self {
+        Self {
+            md,
+            inputs: TermSet::new(),
+            cache: TermMap::new(),
+            term_to_stext_cnt: TermMap::new(),
+            stext_cnt: 0,
+            bytecode_path: get_path(path, lang, "bytecode"),
+            bytecode_output: Vec::new(),
+        }
+    }
+
+    fn map_terms_to_shares(&mut self, term_: Term) {
+        for t in PostOrderIter::new(term_) {
+            self.term_to_stext_cnt.insert(t, self.stext_cnt);
+            self.stext_cnt += 1;
+        }
+    }
+
+    fn get_var_name(t: &Term) -> String {
+        match &t.op {
+            Op::Var(name, _) => {
+                let new_name = name.to_string().replace('.', "_");
+                let n = new_name.split('_').collect::<Vec<&str>>();
+
+                match n.len() {
+                    5 => n[3].to_string(),
+                    6.. => {
+                        let l = n.len() - 1;
+                        format!("{}_{}", n[l - 2], n[l])
+                    }
+                    _ => {
+                        panic!("Invalid variable name: {}", name);
+                    }
+                }
+            }
+
+            _ => panic!("Term {} is not of type Var", t),
+        }
+    }
+
+    fn unwrap_vis(&self, name: &str) -> u8 {
+        match self.md.input_vis.get(name).unwrap() {
+            Some(_) => 1,
+            None => 0,
+        }
+    }
+
+    fn embed_eq(&mut self, t: Term, a_term: Term, b_term: Term) {
+        let s = self.term_to_stext_cnt.get(&t).unwrap();
+        let a = self.term_to_stext_cnt.get(&t.cs[0]).unwrap();
+        let b = self.term_to_stext_cnt.get(&t.cs[1]).unwrap();
+        let op;
+        match check(&a_term) {
+            Sort::Bool => {
+                self.check_bool(&a_term);
+                self.check_bool(&b_term);
+                self.cache.insert(t, EmbeddedTerm::Bool);
+                op = "B_EQ";
+            }
+            Sort::BitVector(_) => {
+                self.check_bv(&a_term);
+                self.check_bv(&b_term);
+                self.cache.insert(t, EmbeddedTerm::Bool);
+                op = "V_EQ";
+            }
+            e => panic!("Unimplemented sort for Eq: {:?}", e),
+        }
+        let line = format!("2 1 {} {} {} {}\n", a, b, s, op);
+        self.bytecode_output.push(line);
+    }
+
+    /// Given term `t`, type-check `t` is of type Bool
+    fn check_bool(&self, t: &Term) {
+        match self
+            .cache
+            .get(t)
+            .unwrap_or_else(|| panic!("Missing expression for {:?}", t))
+        {
+            EmbeddedTerm::Bool => (),
+            _ => panic!("Check_bool failed"),
+        };
+    }
+
+    fn embed_bool(&mut self, t: Term) {
+        let s = self.term_to_stext_cnt.get(&t).unwrap();
+        match &t.op {
+            Op::Var(name, Sort::Bool) => {
+                // write to bytecode file
+                if !self.inputs.contains(&t) && self.md.input_vis.contains_key(name) {
+                    let term_name = ToFHE::get_var_name(&t);
+                    let enc = self.unwrap_vis(name);
+                    let op = "IN";
+
+                    let line = format!("2 1 {} {} {} {}\n", term_name, enc, s, op);
+                    self.bytecode_output.insert(0, line);
+                    self.inputs.insert(t.clone());
+                }
+                if !self.cache.contains_key(&t) {
+                    self.cache.insert(t.clone(), EmbeddedTerm::Bool);
+                }
+            }
+            Op::Const(Value::Bool(b)) => {
+                let op = "CONS";
+                let line = format!("1 1 {} {} {}\n", *b as i32, s, op);
+                self.bytecode_output.push(line);
+                self.cache.insert(t.clone(), EmbeddedTerm::Bool);
+            }
+            Op::Eq => {
+                self.embed_eq(t.clone(), t.cs[0].clone(), t.cs[1].clone());
+            }
+            Op::Ite => {
+                unimplemented!("Bool Ite unimplemented");
+            }
+            Op::Not => {
+                let op = "NOT";
+
+                self.check_bool(&t.cs[0]);
+
+                let a = self.term_to_stext_cnt.get(&t.cs[0]).unwrap();
+                let line = format!("1 1 {} {} {}\n", a, s, op);
+                self.bytecode_output.push(line);
+
+                self.cache.insert(t.clone(), EmbeddedTerm::Bool);
+            }
+            Op::BoolNaryOp(o) => {
+                self.bytecode_output.push(format!("{} 1", t.cs.len()));
+
+                for cterm in &t.cs {
+                    self.check_bool(cterm);
+                    self.bytecode_output
+                        .push(format!(" {}", self.term_to_stext_cnt.get(cterm).unwrap()));
+                }
+
+                let op = match o {
+                    BoolNaryOp::Or => "B_OR",
+                    BoolNaryOp::And => "B_AND",
+                    BoolNaryOp::Xor => "B_XOR",
+                };
+
+                self.bytecode_output.push(format!(" {} {}\n", s, op));
+
+                self.cache.insert(t.clone(), EmbeddedTerm::Bool);
+            }
+            _ => panic!("Non-field in embed_bool: {:?}", t),
+        }
+    }
+
+    /// Given term `t`, type-check `t` is of type Bv
+    fn check_bv(&self, t: &Term) {
+        match self
+            .cache
+            .get(t)
+            .unwrap_or_else(|| panic!("Missing expression for {:?}", t))
+        {
+            EmbeddedTerm::Bv => (),
+            _ => panic!("Check_bv failed"),
+        };
+    }
+
+    fn embed_bv(&mut self, t: Term) {
+        let s = self.term_to_stext_cnt.get(&t).unwrap();
+        match &t.op {
+            Op::Var(name, Sort::BitVector(_)) => {
+                // write to bytecode file
+                if !self.inputs.contains(&t) && self.md.input_vis.contains_key(name) {
+                    let term_name = ToFHE::get_var_name(&t);
+                    let enc = self.unwrap_vis(name);
+                    let op = "IN";
+
+                    let line = format!("2 1 {} {} {} {}\n", term_name, enc, s, op);
+                    self.bytecode_output.insert(0, line);
+                    self.inputs.insert(t.clone());
+                }
+                if !self.cache.contains_key(&t) {
+                    self.cache.insert(t.clone(), EmbeddedTerm::Bv);
+                }
+            }
+            Op::Const(Value::BitVector(b)) => {
+                let op = "CONS";
+                let line = format!("1 1 {} {} {}\n", b.as_sint(), s, op);
+                self.bytecode_output.push(line);
+                self.cache.insert(t.clone(), EmbeddedTerm::Bv);
+            }
+            Op::BvNaryOp(o) => {
+                self.bytecode_output.push(format!("{} 1", t.cs.len()));
+
+                for cterm in &t.cs {
+                    self.check_bv(cterm);
+                    self.bytecode_output
+                        .push(format!(" {}", self.term_to_stext_cnt.get(cterm).unwrap()));
+                }
+
+                let op = match o {
+                    BvNaryOp::Xor => "V_XOR",
+                    BvNaryOp::Or => "V_OR",
+                    BvNaryOp::And => "V_AND",
+                    BvNaryOp::Add => "ADD",
+                    BvNaryOp::Mul => "MUL",
+                };
+
+                self.bytecode_output.push(format!(" {} {}\n", s, op));
+
+                self.cache.insert(t.clone(), EmbeddedTerm::Bv);
+            }
+            _ => {
+                panic!("Non-field in embed_bv: {:?}", t);
+            }
+        }
+    }
+
+    // Given term `t`, type-check `t` is of type arr
+    fn check_arr(&self, t: &Term) {
+        match self
+            .cache
+            .get(t)
+            .unwrap_or_else(|| panic!("Missing expression for {:?}", t))
+        {
+            EmbeddedTerm::Arr => (),
+            _ => panic!("Check_arr failed"),
+        };
+    }
+
+    fn embed_arr(&mut self, t: Term) {
+        let s = self.term_to_stext_cnt.get(&t).unwrap();
+        match &t.op {
+            Op::Var(name, Sort::Array(_, _, len)) => {
+                // write to bytecode file
+                if !self.inputs.contains(&t) && self.md.input_vis.contains_key(name) {
+                    let term_name = ToFHE::get_var_name(&t);
+                    let enc = self.unwrap_vis(name);
+                    let op = "ARR_IN";
+
+                    let line = format!("3 1 {} {} {} {} {}\n", term_name, enc, len, s, op);
+                    self.bytecode_output.insert(0, line);
+                }
+                if !self.cache.contains_key(&t) {
+                    self.cache.insert(t.clone(), EmbeddedTerm::Arr);
+                }
+            }
+            Op::Const(Value::Array(arr)) => {
+                self.bytecode_output.push(format!("{} 1", arr.size));
+
+                for ival in arr.key_sort.elems_iter_values().take(arr.size) {
+                    let val = arr.select(&ival);
+                    if let Value::Array(_) = val.clone() {
+                        panic!("Const arr does not support multi-dim arrays")
+                    }
+                    self.bytecode_output.push(format!(" {}", val));
+                }
+
+                let op = "ARR_CONS";
+                let line = format!("{} {}\n", s, op);
+                self.bytecode_output.push(line);
+                self.cache.insert(t.clone(), EmbeddedTerm::Arr);
+            }
+            Op::Map(op) => {
+                self.bytecode_output.push(format!("{} 1", t.cs.len()));
+                for cterm in &t.cs {
+                    self.check_arr(cterm);
+                    self.bytecode_output
+                        .push(format!(" {}", self.term_to_stext_cnt.get(cterm).unwrap()));
+                }
+                let opstr = match **op {
+                    Op::BoolNaryOp(BoolNaryOp::Or) => "B_OR",
+                    Op::BoolNaryOp(BoolNaryOp::And) => "B_AND",
+                    Op::BoolNaryOp(BoolNaryOp::Xor) => "B_XOR",
+                    Op::BvNaryOp(BvNaryOp::Add) => "ADD",
+                    Op::BvNaryOp(BvNaryOp::Mul) => "MUL",
+                    _ => panic!("Map does not support operation {}", op),
+                };
+                self.bytecode_output.push(format!(" {} {}\n", s, opstr));
+                self.cache.insert(t.clone(), EmbeddedTerm::Arr);
+            }
+            _ => {
+                unimplemented!("Array operation not implemented");
+            }
+        }
+    }
+
+    fn embed(&mut self, t: Term) {
+        for c in PostOrderIter::new(t) {
+            match check(&c) {
+                Sort::Bool => {
+                    self.embed_bool(c);
+                }
+                Sort::BitVector(_) => {
+                    self.embed_bv(c);
+                }
+                Sort::Array(..) => {
+                    self.embed_arr(c);
+                }
+                e => panic!("Unsupported sort in embed: {:?}", e),
+            }
+        }
+    }
+
+    /// Given a term `t`, lower `t` to FHE program
+    fn lower(&mut self, t: Term) {
+        self.embed(t.clone());
+
+        match check(&t) {
+            Sort::Array(_, _, len) => {
+                let op = "ARR_OUT";
+                let s = self.term_to_stext_cnt.get(&t).unwrap();
+                let line = format!("2 0 {} {} {}\n", s, len, op);
+                self.bytecode_output.push(line);
+            }
+            _ => {
+                let op = "OUT";
+                let s = self.term_to_stext_cnt.get(&t).unwrap();
+                let line = format!("1 0 {} {}\n", s, op);
+                self.bytecode_output.push(line);
+            }
+        }
+
+        // write lines to file
+        write_lines_to_file(&self.bytecode_path, &self.bytecode_output);
+    }
+}
+
+/// Convert this (IR) `ir` to FHE.
+pub fn to_fhe(ir: Computation, path: &Path, lang: &str) {
+    let Computation {
+        outputs: terms,
+        metadata: md,
+        ..
+    } = ir;
+
+    let mut converter = ToFHE::new(md, path, lang);
+
+    for t in terms {
+        // println!("Terms: {}", t);
+        converter.map_terms_to_shares(t.clone());
+        converter.lower(t.clone());
+    }
+}
diff --git a/src/target/fhe/utils.rs b/src/target/fhe/utils.rs
new file mode 100644
index 000000000..94e55054f
--- /dev/null
+++ b/src/target/fhe/utils.rs
@@ -0,0 +1,48 @@
+//! Utility functions to write compiler output to FHE
+
+//TODO: parameterize these functions so they can be shared between ABY and SEAL backends
+
+use std::fs;
+use std::io::prelude::*;
+use std::path::Path;
+
+/// Given Path `path` and String denominator `lang`, return the filename of the path
+pub fn get_path(path: &Path, lang: &str, t: &str) -> String {
+    let filename = Path::new(&path.iter().last().unwrap())
+        .file_stem()
+        .unwrap()
+        .to_os_string()
+        .into_string()
+        .unwrap();
+
+    match fs::create_dir_all("scripts/seal_tests/tests") {
+        Err(why) => panic!("couldn't create {}: {}", "scripts/seal_tests/tests", why),
+        Ok(file) => file,
+    };
+
+    let name = format!("{}_{}", filename, lang);
+    let path = format!("scripts/seal_tests/tests/{}_{}.txt", name, t);
+    match fs::File::create(&path) {
+        Err(why) => panic!("couldn't create {}: {}", path, why),
+        Ok(file) => file,
+    };
+    path
+}
+
+/// Write output to temporary file
+pub fn write_lines_to_file(path: &str, lines: &[String]) {
+    if !Path::new(&path).exists() {
+        fs::File::create(&path).expect(&*format!("Failed to create: {}", path));
+    }
+
+    let data = lines.join("");
+
+    let mut file = fs::OpenOptions::new()
+        .write(true)
+        .append(true)
+        .open(path)
+        .expect("Failed to open seal_tmp file");
+
+    file.write_all(data.as_bytes())
+        .expect("Failed to write to seal_tmp file");
+}
diff --git a/src/target/mod.rs b/src/target/mod.rs
index 8fcb9319c..e760b466c 100644
--- a/src/target/mod.rs
+++ b/src/target/mod.rs
@@ -1,6 +1,7 @@
 //! Target circuit representations (and lowering passes)
 
 pub mod aby;
+pub mod fhe;
 #[cfg(feature = "lp")]
 pub mod ilp;
 pub mod r1cs;
diff --git a/third_party/ABY b/third_party/ABY
new file mode 160000
index 000000000..378b2048e
--- /dev/null
+++ b/third_party/ABY
@@ -0,0 +1 @@
+Subproject commit 378b2048ea0c9ad701b9dac8a0ca31f16bdfd83b
diff --git a/util.py b/util.py
index 215990306..2198d6b19 100644
--- a/util.py
+++ b/util.py
@@ -4,20 +4,21 @@
 # Gloable variables
 feature_path = ".features.txt"
 mode_path = ".mode.txt"
-valid_features = {"aby", "c", "lp", "r1cs", "smt", "zok"}
+valid_features = {"aby", "c", "lp", "r1cs", "seal", "smt", "zok"}
 cargo_features = {"c", "lp", "r1cs", "smt", "zok"}
 
 # Environment variables
 ABY_SOURCE="./../ABY"
-EZPC_SOURCE="./../EZPC"
+SEAL_SOURCE="./../SEAL"
 
 def set_env(features):
     for f in features:
         if f == 'aby':
             if not os.getenv("ABY_SOURCE"):
                 os.environ["ABY_SOURCE"] = ABY_SOURCE
-            if not os.getenv("EZPC_SOURCE"):
-                os.environ["EZPC_SOURCE"] = EZPC_SOURCE
+        if f == 'seal':
+            if not os.getenv("SEAL_SOURCE"):
+                os.environ["SEAL_SOURCE"] = SEAL_SOURCE
 
 def save_mode(mode):
     """ Save mode to file """