diff --git a/Cargo.lock b/Cargo.lock
index 312d01957f..8087eaac9c 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -658,6 +658,7 @@ dependencies = [
  "fe-common",
  "fe-driver",
  "fe-parser",
+ "fe-specgen",
  "fe-test-runner",
  "fs_extra",
  "include_dir",
@@ -805,6 +806,7 @@ dependencies = [
  "fe-common",
  "fe-mir",
  "fe-parser",
+ "fe-specgen",
  "fe-test-runner",
  "fe-yulc",
  "indexmap",
@@ -862,6 +864,13 @@ dependencies = [
  "wasm-bindgen-test",
 ]
 
+[[package]]
+name = "fe-specgen"
+version = "0.22.0"
+dependencies = [
+ "smol_str",
+]
+
 [[package]]
 name = "fe-test-files"
 version = "0.22.0"
diff --git a/crates/analyzer/src/db.rs b/crates/analyzer/src/db.rs
index f094a51ecc..e5ce2edf71 100644
--- a/crates/analyzer/src/db.rs
+++ b/crates/analyzer/src/db.rs
@@ -110,6 +110,8 @@ pub trait AnalyzerDb: SourceDb + Upcast<dyn SourceDb> + UpcastMut<dyn SourceDb>
     fn module_submodules(&self, module: ModuleId) -> Rc<[ModuleId]>;
     #[salsa::invoke(queries::module::module_tests)]
     fn module_tests(&self, module: ModuleId) -> Vec<FunctionId>;
+    #[salsa::invoke(queries::module::module_invariants)]
+    fn module_invariants(&self, module: ModuleId) -> Vec<FunctionId>;
 
     // Module Constant
     #[salsa::cycle(queries::module::module_constant_type_cycle)]
diff --git a/crates/analyzer/src/db/queries/module.rs b/crates/analyzer/src/db/queries/module.rs
index 37286fa1e9..ac8f585b5c 100644
--- a/crates/analyzer/src/db/queries/module.rs
+++ b/crates/analyzer/src/db/queries/module.rs
@@ -760,3 +760,12 @@ pub fn module_tests(db: &dyn AnalyzerDb, ingot: ModuleId) -> Vec<FunctionId> {
         .filter(|function| function.is_test(db))
         .collect()
 }
+
+pub fn module_invariants(db: &dyn AnalyzerDb, ingot: ModuleId) -> Vec<FunctionId> {
+    ingot
+        .all_functions(db)
+        .iter()
+        .copied()
+        .filter(|function| function.is_invariant(db))
+        .collect()
+}
diff --git a/crates/analyzer/src/namespace/items.rs b/crates/analyzer/src/namespace/items.rs
index 779c719664..572fbb89d5 100644
--- a/crates/analyzer/src/namespace/items.rs
+++ b/crates/analyzer/src/namespace/items.rs
@@ -555,6 +555,10 @@ impl ModuleId {
         db.module_tests(*self)
     }
 
+    pub fn invariants(&self, db: &dyn AnalyzerDb) -> Vec<FunctionId> {
+        db.module_invariants(*self)
+    }
+
     /// Returns `true` if the `item` is in scope of the module.
     pub fn is_in_scope(&self, db: &dyn AnalyzerDb, item: Item) -> bool {
         if let Some(val) = item.module(db) {
@@ -1351,6 +1355,13 @@ impl FunctionId {
             .iter()
             .any(|attribute| attribute.name(db) == "test")
     }
+
+    pub fn is_invariant(&self, db: &dyn AnalyzerDb) -> bool {
+        Item::Function(*self)
+            .attributes(db)
+            .iter()
+            .any(|attribute| attribute.name(db) == "invariant")
+    }
 }
 
 trait FunctionsAsItems {
diff --git a/crates/codegen/src/yul/isel/test.rs b/crates/codegen/src/yul/isel/test.rs
index 9fe6186933..b94473696a 100644
--- a/crates/codegen/src/yul/isel/test.rs
+++ b/crates/codegen/src/yul/isel/test.rs
@@ -22,7 +22,21 @@ pub fn lower_test(db: &dyn CodegenDb, test: FunctionId) -> yul::Object {
         .map(yul::Statement::FunctionDefinition)
         .collect();
     let test_func_name = identifier! { (db.codegen_function_symbol_name(test)) };
-    let call = function_call_statement! {[test_func_name]()};
+    let call_args = test
+        .signature(db.upcast())
+        .params
+        .iter()
+        .enumerate()
+        .filter_map(|(n, param)| {
+            if param.name == "ctx" {
+                None
+            } else {
+                let value = literal_expression! { (n * 32) };
+                Some(expression! { calldataload([value]) })
+            }
+        })
+        .collect::<Vec<_>>();
+    let call = function_call_statement! {[test_func_name]([call_args...])};
 
     let code = code! {
         [dep_functions...]
diff --git a/crates/codegen/src/yul/runtime/mod.rs b/crates/codegen/src/yul/runtime/mod.rs
index 5cb6fb7a64..8c2e55202b 100644
--- a/crates/codegen/src/yul/runtime/mod.rs
+++ b/crates/codegen/src/yul/runtime/mod.rs
@@ -163,7 +163,8 @@ pub trait RuntimeProvider {
             expression! { signextend([significant], [value]) }
         } else {
             let mask = BitMask::new(from_size);
-            expression! { and([value], [mask.as_expr()]) }
+            // expression! { and([value], [mask.as_expr()]) }
+            value
         }
     }
 
diff --git a/crates/driver/Cargo.toml b/crates/driver/Cargo.toml
index f7f579a774..5c7eba4ef8 100644
--- a/crates/driver/Cargo.toml
+++ b/crates/driver/Cargo.toml
@@ -20,6 +20,7 @@ fe-codegen = {path = "../codegen", version = "^0.22.0"}
 fe-parser = {path = "../parser", version = "^0.22.0"}
 fe-yulc = {path = "../yulc", version = "^0.22.0", features = ["solc-backend"], optional = true}
 fe-test-runner = {path = "../test-runner", version = "^0.22.0"}
+fe-specgen = {path = "../specgen", version = "^0.22.0"}
 indexmap = "1.6.2"
 vfs = "0.5.1"
 smol_str = "0.1.21"
diff --git a/crates/driver/src/lib.rs b/crates/driver/src/lib.rs
index 91c6a47012..e0badd2da3 100644
--- a/crates/driver/src/lib.rs
+++ b/crates/driver/src/lib.rs
@@ -7,6 +7,7 @@ use fe_common::db::Upcast;
 use fe_common::diagnostics::Diagnostic;
 use fe_common::files::FileKind;
 use fe_parser::ast::SmolStr;
+use fe_specgen::KSpec;
 use fe_test_runner::TestSink;
 use indexmap::{indexmap, IndexMap};
 use serde_json::Value;
@@ -86,6 +87,23 @@ pub fn compile_single_file_tests(
     }
 }
 
+#[cfg(feature = "solc-backend")]
+pub fn generate_single_file_specs(
+    db: &mut Db,
+    path: &str,
+    src: &str,
+    optimize: bool,
+) -> Result<Vec<KSpec>, CompileError> {
+    let module = ModuleId::new_standalone(db, path, src);
+    let diags = module.diagnostics(db);
+
+    if diags.is_empty() {
+        Ok(generate_module_specs(db, module, optimize))
+    } else {
+        Err(CompileError(diags))
+    }
+}
+
 // Run analysis with ingot
 // Return vector error,waring...
 pub fn check_ingot(
@@ -176,6 +194,46 @@ pub fn compile_ingot_tests(
     }
 }
 
+#[cfg(feature = "solc-backend")]
+pub fn generate_ingot_specs(
+    db: &mut Db,
+    name: &str,
+    files: &[(impl AsRef<str>, impl AsRef<str>)],
+    optimize: bool,
+) -> Result<Vec<KSpec>, CompileError> {
+    let std = IngotId::std_lib(db);
+    let ingot = IngotId::from_files(
+        db,
+        name,
+        IngotMode::Main,
+        FileKind::Local,
+        files,
+        indexmap! { "std".into() => std },
+    );
+
+    let mut diags = ingot.diagnostics(db);
+    ingot.sink_external_ingot_diagnostics(db, &mut diags);
+    if !diags.is_empty() {
+        return Err(CompileError(diags));
+    }
+
+    if diags.is_empty() {
+        // Ok(ingot
+        //     .all_modules(db)
+        //     .iter()
+        //     .fold(vec![], |mut accum, module| {
+        //         accum.push((
+        //             module.name(db),
+        //             generate_module_specs(db, *module, optimize),
+        //         ));
+        //         accum
+        //     }))
+        Ok(vec![])
+    } else {
+        Err(CompileError(diags))
+    }
+}
+
 /// Returns graphviz string.
 // TODO: This is temporary function for debugging.
 pub fn dump_mir_single_file(db: &mut Db, path: &str, src: &str) -> Result<String, CompileError> {
@@ -196,6 +254,7 @@ fn compile_test(db: &mut Db, test: FunctionId, optimize: bool) -> CompiledTest {
     let yul_test = fe_codegen::yul::isel::lower_test(db, test)
         .to_string()
         .replace('"', "\\\"");
+    // panic!("{}", yul_test);
     let bytecode = compile_to_evm("test", &yul_test, optimize);
     CompiledTest::new(test.name(db), bytecode)
 }
@@ -209,6 +268,21 @@ fn compile_module_tests(db: &mut Db, module_id: ModuleId, optimize: bool) -> Vec
         .collect()
 }
 
+#[cfg(feature = "solc-backend")]
+fn generate_spec(db: &mut Db, test: FunctionId, optimize: bool) -> KSpec {
+    let code = compile_test(db, test, optimize).bytecode;
+    KSpec::new(test.name(db), code, test.signature(db).params.len())
+}
+
+#[cfg(feature = "solc-backend")]
+fn generate_module_specs(db: &mut Db, module_id: ModuleId, optimize: bool) -> Vec<KSpec> {
+    module_id
+        .invariants(db)
+        .iter()
+        .map(|test| generate_spec(db, *test, optimize))
+        .collect()
+}
+
 #[cfg(feature = "solc-backend")]
 fn compile_module(
     db: &mut Db,
diff --git a/crates/fe/Cargo.toml b/crates/fe/Cargo.toml
index a350ac1ff4..280da63937 100644
--- a/crates/fe/Cargo.toml
+++ b/crates/fe/Cargo.toml
@@ -24,3 +24,4 @@ fe-test-runner = {path = "../test-runner", version = "^0.22.0"}
 fe-common = {path = "../common", version = "^0.22.0"}
 fe-driver = {path = "../driver", version = "^0.22.0"}
 fe-parser = {path = "../parser", version = "^0.22.0"}
+fe-specgen = {path = "../specgen", version = "^0.22.0"}
diff --git a/crates/fe/src/main.rs b/crates/fe/src/main.rs
index 71f4781428..d1a2580bb9 100644
--- a/crates/fe/src/main.rs
+++ b/crates/fe/src/main.rs
@@ -30,5 +30,9 @@ fn main() {
         Commands::Test(arg) => {
             task::test(arg);
         }
+        #[cfg(feature = "solc-backend")]
+        Commands::Specs(arg) => {
+            task::specs(arg);
+        }
     }
 }
diff --git a/crates/fe/src/task/mod.rs b/crates/fe/src/task/mod.rs
index 34ac1b6350..73c78e2904 100644
--- a/crates/fe/src/task/mod.rs
+++ b/crates/fe/src/task/mod.rs
@@ -1,6 +1,7 @@
 mod build;
 mod check;
 mod new;
+mod specs;
 #[cfg(feature = "solc-backend")]
 mod test;
 mod utils;
@@ -9,6 +10,7 @@ pub use build::{build, BuildArgs};
 pub use check::{check, CheckArgs};
 use clap::Subcommand;
 pub use new::{create_new_project, NewProjectArgs};
+pub use specs::{specs, SpecsArgs};
 #[cfg(feature = "solc-backend")]
 pub use test::{test, TestArgs};
 
@@ -19,4 +21,5 @@ pub enum Commands {
     New(NewProjectArgs),
     #[cfg(feature = "solc-backend")]
     Test(TestArgs),
+    Specs(SpecsArgs),
 }
diff --git a/crates/fe/src/task/specs.rs b/crates/fe/src/task/specs.rs
new file mode 100644
index 0000000000..8d93da8dfe
--- /dev/null
+++ b/crates/fe/src/task/specs.rs
@@ -0,0 +1,185 @@
+#![cfg(feature = "solc-backend")]
+use std::fs;
+use std::io::{Error, Write};
+use std::path::Path;
+
+use clap::Args;
+use fe_common::diagnostics::print_diagnostics;
+use fe_specgen::KSpec;
+
+const DEFAULT_OUTPUT_DIR_NAME: &str = "specs";
+const DEFAULT_INGOT: &str = "main";
+
+#[derive(Args)]
+#[clap(about = "Generate specs for the current project")]
+pub struct SpecsArgs {
+    input_path: String,
+    #[clap(short, long, default_value = DEFAULT_OUTPUT_DIR_NAME)]
+    output_dir: String,
+    #[clap(long)]
+    overwrite: bool,
+    #[clap(long, takes_value(true))]
+    optimize: Option<bool>,
+}
+
+fn generate_single_file_specs(specs_arg: &SpecsArgs) -> Vec<KSpec> {
+    let input_path = &specs_arg.input_path;
+    let optimize = specs_arg.optimize.unwrap_or(true);
+
+    let mut db = fe_driver::Db::default();
+    let content = match std::fs::read_to_string(input_path) {
+        Err(err) => {
+            eprintln!("Failed to load file: `{input_path}`. Error: {err}");
+            std::process::exit(1)
+        }
+        Ok(content) => content,
+    };
+
+    match fe_driver::generate_single_file_specs(&mut db, input_path, &content, optimize) {
+        Ok(specs) => specs,
+        Err(error) => {
+            eprintln!("Unable to compile {input_path}.");
+            print_diagnostics(&db, &error.0);
+            std::process::exit(1)
+        }
+    }
+}
+
+// fn build_ingot(compile_arg: &BuildArgs) -> (String, CompiledModule) {
+//     let emit = &compile_arg.emit;
+//     let with_bytecode = emit.contains(&Emit::Bytecode);
+//     let input_path = &compile_arg.input_path;
+//     let optimize = compile_arg.optimize.unwrap_or(true);
+
+//     if !Path::new(input_path).exists() {
+//         eprintln!("Input directory does not exist: `{input_path}`.");
+//         std::process::exit(1)
+//     }
+
+//     let files = match load_files_from_dir(input_path) {
+//         Ok(files) if files.is_empty() => {
+//             eprintln!("Input directory is not an ingot: `{input_path}`");
+//             std::process::exit(1)
+//         }
+//         Ok(files) => files,
+//         Err(err) => {
+//             eprintln!("Failed to load project files. Error: {err}");
+//             std::process::exit(1)
+//         }
+//     };
+
+//     let mut db = fe_driver::Db::default();
+//     let compiled_module = match fe_driver::compile_ingot(
+//         &mut db,
+//         DEFAULT_INGOT, // TODO: real ingot name
+//         &files,
+//         with_bytecode,
+//         optimize,
+//     ) {
+//         Ok(module) => module,
+//         Err(error) => {
+//             eprintln!("Unable to compile {input_path}.");
+//             print_diagnostics(&db, &error.0);
+//             std::process::exit(1)
+//         }
+//     };
+
+//     // no file content for ingots
+//     ("".to_string(), compiled_module)
+// }
+
+pub fn specs(specs_arg: SpecsArgs) {
+    let input_path = &specs_arg.input_path;
+
+    let specs = if Path::new(input_path).is_file() {
+        generate_single_file_specs(&specs_arg)
+    } else {
+        // build_ingot(&compile_arg)
+        panic!()
+    };
+
+    let output_dir = &specs_arg.output_dir;
+    let overwrite = specs_arg.overwrite;
+    match write_specs(specs, output_dir, overwrite) {
+        Ok(_) => eprintln!("Compiled {input_path}. Outputs in `{output_dir}`"),
+        Err(err) => {
+            eprintln!("Failed to write output to directory: `{output_dir}`. Error: {err}");
+            std::process::exit(1)
+        }
+    }
+}
+
+fn write_specs(mut specs: Vec<KSpec>, output_dir: &str, overwrite: bool) -> Result<(), String> {
+    let output_dir = Path::new(output_dir);
+    if output_dir.is_file() {
+        return Err(format!(
+            "A file exists at path `{}`, the location of the output directory. Refusing to overwrite.",
+            output_dir.display()
+        ));
+    }
+
+    if !overwrite {
+        verify_nonexistent_or_empty(output_dir)?;
+    }
+
+    fs::create_dir_all(output_dir).map_err(ioerr_to_string)?;
+
+    for spec in specs {
+        let file_name = format!("{}-spec.k", &spec.name());
+        write_output(&output_dir.join(file_name), &spec.to_string())?;
+    }
+
+    Ok(())
+}
+
+fn write_output(path: &Path, content: &str) -> Result<(), String> {
+    let mut file = fs::OpenOptions::new()
+        .write(true)
+        .create(true)
+        .truncate(true)
+        .open(path)
+        .map_err(ioerr_to_string)?;
+    file.write_all(content.as_bytes())
+        .map_err(ioerr_to_string)?;
+    Ok(())
+}
+
+fn ioerr_to_string(error: Error) -> String {
+    format!("{error}")
+}
+
+fn verify_nonexistent_or_empty(dir: &Path) -> Result<(), String> {
+    if !dir.exists() || dir.read_dir().map_err(ioerr_to_string)?.next().is_none() {
+        Ok(())
+    } else {
+        Err(format!(
+            "Directory '{}' is not empty. Use --overwrite to overwrite.",
+            dir.display()
+        ))
+    }
+}
+
+fn mir_dump(input_path: &str) {
+    let mut db = fe_driver::Db::default();
+    if Path::new(input_path).is_file() {
+        let content = match std::fs::read_to_string(input_path) {
+            Err(err) => {
+                eprintln!("Failed to load file: `{input_path}`. Error: {err}");
+                std::process::exit(1)
+            }
+            Ok(content) => content,
+        };
+
+        match fe_driver::dump_mir_single_file(&mut db, input_path, &content) {
+            Ok(text) => println!("{text}"),
+            Err(err) => {
+                eprintln!("Unable to dump mir `{input_path}");
+                print_diagnostics(&db, &err.0);
+                std::process::exit(1)
+            }
+        }
+    } else {
+        eprintln!("dumping mir for ingot is not supported yet");
+        std::process::exit(1)
+    }
+}
diff --git a/crates/library/std/src/spec.fe b/crates/library/std/src/spec.fe
new file mode 100644
index 0000000000..386fc2e51b
--- /dev/null
+++ b/crates/library/std/src/spec.fe
@@ -0,0 +1,61 @@
+use ingot::evm
+
+fn valid() {
+    unsafe { 
+        evm::return_mem(offset: 0, len: 0) 
+    }
+}
+
+fn invalid() {
+    unsafe { 
+        evm::revert_mem(offset: 0, len: 0) 
+    }
+}
+
+pub fn given_eq(_ a: u256, _ b: u256) {
+    if evm::eq(a, b) == 0 {
+        valid()
+    }
+}
+
+pub fn given_ne(_ a: u256, _ b: u256) {
+    if evm::eq(a, b) == 1 {
+        valid()
+    }
+}
+
+pub fn given_lte(_ a: u256, _ b: u256) {
+    if evm::gt(a, b) == 1 {
+        valid()
+    }
+}
+
+pub fn given_gte(_ a: u256, _ b: u256) {
+    if evm::lt(a, b) == 1 {
+        valid()
+    }
+}
+
+pub fn assert_eq(_ a: u256, _ b: u256) {
+    if evm::eq(a, b) == 0 {
+        invalid()
+    }
+}
+
+pub fn assert_ne(_ a: u256, _ b: u256) {
+    if evm::eq(a, b) == 1 {
+        invalid()
+    }
+}
+
+pub fn assert_lte(_ a: u256, _ b: u256) {
+    if evm::gt(a, b) == 1 {
+        invalid()
+    }
+}
+
+pub fn assert_gte(_ a: u256, _ b: u256) {
+    if evm::lt(a, b) == 1 {
+        invalid()
+    }
+}
diff --git a/crates/specgen/Cargo.toml b/crates/specgen/Cargo.toml
new file mode 100644
index 0000000000..0beb036cf6
--- /dev/null
+++ b/crates/specgen/Cargo.toml
@@ -0,0 +1,10 @@
+[package]
+name = "fe-specgen"
+version = "0.22.0"
+authors = ["The Fe Developers <snakecharmers@ethereum.org>"]
+edition = "2021"
+license = "GPL-3.0-or-later"
+repository = "https://github.com/ethereum/fe"
+
+[dependencies]
+smol_str = "0.1.21"
\ No newline at end of file
diff --git a/crates/specgen/fixtures/sanity.fe b/crates/specgen/fixtures/sanity.fe
new file mode 100644
index 0000000000..4443205b50
--- /dev/null
+++ b/crates/specgen/fixtures/sanity.fe
@@ -0,0 +1,91 @@
+// use std::{evm, spec}
+use std::spec
+use std::evm
+
+// #invariant
+// fn simple1(a: u256) {
+//     spec::given_lte(a, 26)
+
+//     spec::assert_lte(a, 42)
+// }
+
+// #invariant
+// fn simple2(a: u256) {
+//     spec::given_lte(a, 42)
+
+//     spec::assert_ne(a, 43)
+// }
+
+// #invariant
+// fn simple3(a: u256, b: u256) {
+//     spec::given_lte(a, b)
+//     spec::given_eq(a, 42)
+
+//     spec::assert_ne(b, 26)
+// }
+
+// #invariant
+// fn simple4(a: u256, b: u256) {
+//     spec::given_lte(a, 42)
+//     spec::given_lte(b, 26)
+
+//     spec::assert_lte(evm::add(a, b), 68)
+// }
+
+// #invariant
+// fn simple5(a: u256) {
+//     spec::given_lte(a, 42)
+//     spec::given_gte(a, 26)
+
+//     spec::assert_ne(a, 25)
+//     spec::assert_ne(a, 45)
+// }
+
+// #invariant
+// fn simple6(a: u256) {
+//     spec::given_lte(a, 42)
+//     spec::given_gte(a, 42)
+
+//     spec::assert_eq(a, 43)
+// }
+
+// fn sq(_ a: u256) -> u256 {
+//     return evm::mul(a, a)
+// }
+
+// #invariant
+// fn simple7(a: u256, b: u256, c: u256) {
+//     spec::given_lte(a, 1023)
+//     spec::given_lte(b, 1023)
+//     spec::given_lte(c, 1023)
+
+//     // a ^ 2 + b ^ 2 = c ^ 2
+//     spec::given_eq(
+//         evm::add(sq(a), sq(b)),
+//         sq(c)
+//     ) 
+//     spec::given_eq(a, 3)
+//     spec::given_eq(b, 4)
+
+//     spec::assert_eq(c, 5)
+// }
+
+// #invariant
+// fn simple8(a: u256, b: u256, c: u256) {
+//     spec::given_lte(a, 1023)
+//     spec::given_lte(b, 1023)
+//     spec::given_lte(c, 1023)
+
+//     // a + b = c
+//     spec::given_eq(evm::add(a, b), c)
+//     spec::given_eq(a, 42)
+//     spec::given_eq(c, 68)
+
+//     spec::assert_eq(b, 26)
+// }
+
+#invariant
+fn simple9(a: u256, b: u256, c: u256) {
+    spec::given_gte(a, 26)
+    spec::given_lte(c, 42)
+}
\ No newline at end of file
diff --git a/crates/specgen/src/lib.rs b/crates/specgen/src/lib.rs
new file mode 100644
index 0000000000..d83b2d7cf8
--- /dev/null
+++ b/crates/specgen/src/lib.rs
@@ -0,0 +1,49 @@
+use smol_str::SmolStr;
+use std::fmt::Display;
+
+const KSPEC_TEMPLATE: &str = include_str!("../template.k");
+
+pub struct KSpec {
+    name: SmolStr,
+    code: String,
+    args: usize,
+}
+
+impl KSpec {
+    pub fn new(name: SmolStr, code: String, args: usize) -> Self {
+        Self { name, code, args }
+    }
+
+    pub fn name(&self) -> SmolStr {
+        self.name.clone()
+    }
+}
+
+impl Display for KSpec {
+    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
+        let calldata = (0..self.args)
+            .map(|n| format!("#buf(32, ARG_{})", n))
+            .collect::<Vec<_>>()
+            .join(" +Bytes ");
+
+        let requirements = (0..self.args)
+            .map(|n| {
+                format!(
+                    "andBool 0  <=Int ARG_{} andBool ARG_{} <Int (2 ^Int 256)",
+                    n, n
+                )
+            })
+            .collect::<Vec<_>>()
+            .join("\n");
+
+        write!(
+            f,
+            "{}",
+            KSPEC_TEMPLATE
+                .replace("$NAME", &format!("{}-SPEC", &self.name.to_uppercase()))
+                .replace("$CODE", &format!("\"0x{}\"", &self.code))
+                .replace("$CALLDATA", &calldata)
+                .replace("$REQUIREMENTS", &requirements)
+        )
+    }
+}
diff --git a/crates/specgen/template.k b/crates/specgen/template.k
new file mode 100644
index 0000000000..94178ec1f6
--- /dev/null
+++ b/crates/specgen/template.k
@@ -0,0 +1,107 @@
+module $NAME
+    imports VERIFICATION
+
+    claim
+
+    <kevm>
+        <k> #execute => #halt </k>
+        <exit-code> 1 </exit-code>
+        <mode> NORMAL </mode>
+        <schedule> ISTANBUL </schedule>
+
+        <ethereum>
+            <evm>
+                <output> _ => #buf(0, 0) </output>
+                <statusCode> _ => EVMC_SUCCESS </statusCode>
+                <callStack> _ </callStack>
+                <interimStates> _ </interimStates>
+                <touchedAccounts> _ => ?_ </touchedAccounts>
+
+                <callState>
+                    // todo: gen this part
+                    <program> #parseByteStack($CODE) </program>
+                    <jumpDests> #computeValidJumpDests(#parseByteStack($CODE)) </jumpDests>
+
+                    <id> ACCT_ID </id> // contract owner
+                    <caller> CALLER_ID </caller> // who called this contract; in the beginning, origin // msg.sender
+
+                    // todo: gen this part
+                    <callData> $CALLDATA </callData>
+
+                    <callValue> 0 </callValue>
+                    <wordStack> .WordStack => ?_ </wordStack>
+                    <localMem> .Bytes => ?_ </localMem>
+                    <pc> 0 => ?_ </pc>
+                    <gas> #gas(_VGAS) => ?_ </gas>
+                    <memoryUsed> 0 => ?_ </memoryUsed>
+                    <callGas> _ => ?_ </callGas>
+
+                    <static> false </static> // NOTE: non-static call
+                    <callDepth> CALL_DEPTH </callDepth>
+                </callState>
+
+                <substate>
+                    <selfDestruct> _ </selfDestruct>
+                    <log> _ </log>
+                    <refund> _ </refund>
+                    <accessedAccounts> _ => ?_ </accessedAccounts>
+                    <accessedStorage> _ => ?_ </accessedStorage>
+                </substate>
+
+                <gasPrice> _ </gasPrice>
+                <origin> ORIGIN_ID </origin>
+
+                <blockhashes> _ </blockhashes>
+                <block>
+                    <previousHash> _ </previousHash>
+                    <ommersHash> _ </ommersHash>
+                    <coinbase> _ </coinbase>
+                    <stateRoot> _ </stateRoot>
+                    <transactionsRoot> _ </transactionsRoot>
+                    <receiptsRoot> _ </receiptsRoot>
+                    <logsBloom> _ </logsBloom>
+                    <difficulty> _ </difficulty>
+                    <number> _ </number>
+                    <gasLimit> _ </gasLimit>
+                    <gasUsed> _ </gasUsed>
+                    <timestamp> _ </timestamp>
+                    <extraData> _ </extraData>
+                    <mixHash> _ </mixHash>
+                    <blockNonce> _ </blockNonce>
+                    <ommerBlockHeaders> _ </ommerBlockHeaders>
+                    <baseFee> _ </baseFee>
+                </block>
+            </evm>
+
+            <network>
+                <chainID> _ </chainID>
+
+                <activeAccounts> SetItem(ACCT_ID) _:Set </activeAccounts>
+
+                <accounts>
+                    <account>
+                        <acctID> ACCT_ID </acctID>
+                        <balance> _ </balance>
+                        // todo: gen this part
+                        <code> #parseByteStack($CODE) </code>
+                        <storage> _ </storage>
+                        <origStorage> _ </origStorage>
+                        <nonce> _ </nonce>
+                    </account>
+                </accounts>
+
+                <txOrder> _ </txOrder>
+                <txPending> _ </txPending>
+                <messages> _ </messages>
+            </network>
+        </ethereum>
+    </kevm>
+
+    requires 0 <=Int ACCT_ID    andBool ACCT_ID    <Int (2 ^Int 160)
+        andBool 0  <=Int CALLER_ID  andBool CALLER_ID  <Int (2 ^Int 160)
+        andBool 0  <=Int ORIGIN_ID  andBool ORIGIN_ID  <Int (2 ^Int 160)
+        andBool 0  <=Int CALL_DEPTH andBool CALL_DEPTH <Int 1024
+        $REQUIREMENTS
+
+endmodule
+
diff --git a/crates/test-files/fixtures/kspecs/abi/address.k b/crates/test-files/fixtures/kspecs/abi/address.k
new file mode 100644
index 0000000000..d05a673f94
--- /dev/null
+++ b/crates/test-files/fixtures/kspecs/abi/address.k
@@ -0,0 +1,106 @@
+module $TEST_NAME
+    imports VERIFICATION
+
+    claim
+
+    <kevm>
+        <k> #execute => #halt </k>
+        <exit-code> 1 </exit-code>
+        <mode> NORMAL </mode>
+        <schedule> ISTANBUL </schedule>
+
+        <ethereum>
+            <evm>
+                <output> _ => #buf(32, OUT) </output>
+                <statusCode> _ => EVMC_SUCCESS </statusCode>
+                <endPC> _ => ?_ </endPC>
+                <callStack> _ </callStack>
+                <interimStates> _ </interimStates>
+                <touchedAccounts> _ => ?_ </touchedAccounts>
+
+                <callState>
+                    <program> #parseByteStack($Foo::RUNTIME) </program>
+                    <jumpDests> #computeValidJumpDests(#parseByteStack($Foo::RUNTIME)) </jumpDests>
+
+                    <id> ACCT_ID </id> // contract owner
+                    <caller> CALLER_ID </caller> // who called this contract; in the beginning, origin // msg.sender
+
+                    <callData> #abiCallData("_address", #address(IN)) </callData>
+
+                    <callValue> 0 </callValue>
+                    <wordStack> .WordStack => ?_ </wordStack>
+                    <localMem> .Memory => ?_ </localMem>
+                    <pc> 0 => ?_ </pc>
+                    <gas> #gas(_VGAS) => ?_ </gas>
+                    <memoryUsed> 0 => ?_ </memoryUsed>
+                    <callGas> _ => ?_ </callGas>
+
+                    <static> false </static> // NOTE: non-static call
+                    <callDepth> CALL_DEPTH </callDepth>
+                </callState>
+
+                <substate>
+                    <selfDestruct> _ </selfDestruct>
+                    <log> _ </log>
+                    <refund> _ </refund> // TODO: more detail
+                    <accessedAccounts> _ => ?_ </accessedAccounts>
+                    <accessedStorage> _ => ?_ </accessedStorage>
+                </substate>
+
+                <gasPrice> _ </gasPrice>
+                <origin> ORIGIN_ID </origin> // who fires tx
+
+                <blockhashes> _ </blockhashes>
+                <block>
+                    <previousHash> _ </previousHash>
+                    <ommersHash> _ </ommersHash>
+                    <coinbase> _ </coinbase>
+                    <stateRoot> _ </stateRoot>
+                    <transactionsRoot> _ </transactionsRoot>
+                    <receiptsRoot> _ </receiptsRoot>
+                    <logsBloom> _ </logsBloom>
+                    <difficulty> _ </difficulty>
+                    <number> _ </number>
+                    <gasLimit> _ </gasLimit>
+                    <gasUsed> _ </gasUsed>
+                    <timestamp> _ </timestamp>
+                    <extraData> _ </extraData>
+                    <mixHash> _ </mixHash>
+                    <blockNonce> _ </blockNonce>
+                    <ommerBlockHeaders> _ </ommerBlockHeaders>
+                    <baseFee> _ </baseFee>
+                </block>
+            </evm>
+
+            <network>
+                <chainID> _ </chainID>
+
+                <activeAccounts> SetItem(ACCT_ID) _:Set </activeAccounts>
+
+                <accounts>
+                    <account>
+                        <acctID> ACCT_ID </acctID>
+                        <balance> _ </balance>
+                        <code> #parseByteStack($Foo::RUNTIME) </code>
+                        <storage> _ </storage>
+                        <origStorage> _ </origStorage>
+                        <nonce> _ </nonce>
+                    </account>
+                </accounts>
+
+                <txOrder> _ </txOrder>
+                <txPending> _ </txPending>
+                <messages> _ </messages>
+            </network>
+        </ethereum>
+    </kevm>
+
+    requires 0 <=Int ACCT_ID    andBool ACCT_ID    <Int (2 ^Int 160)
+        andBool 0  <=Int CALLER_ID  andBool CALLER_ID  <Int (2 ^Int 160)
+        andBool 0  <=Int ORIGIN_ID  andBool ORIGIN_ID  <Int (2 ^Int 160)
+        andBool 0  <=Int CALL_DEPTH andBool CALL_DEPTH <Int 1024
+        andBool 0  <=Int IN         andBool IN         <Int (2 ^Int 160)
+        andBool IN ==Int OUT
+
+endmodule
+
diff --git a/crates/test-files/fixtures/kspecs/abi/address_revert.k b/crates/test-files/fixtures/kspecs/abi/address_revert.k
new file mode 100644
index 0000000000..2ff03e6c37
--- /dev/null
+++ b/crates/test-files/fixtures/kspecs/abi/address_revert.k
@@ -0,0 +1,107 @@
+module $TEST_NAME
+    imports VERIFICATION
+
+    claim
+
+    <kevm>
+        <k> #execute => #halt </k>
+        <exit-code> 1 </exit-code>
+        <mode> NORMAL </mode>
+        <schedule> ISTANBUL </schedule>
+
+        <ethereum>
+            <evm>
+                // todo: check code
+                <output> _ => b".6\xa7\t\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x03" </output>
+                <statusCode> _ => EVMC_REVERT </statusCode>
+                <endPC> _ => ?_ </endPC>
+                <callStack> _ </callStack>
+                <interimStates> _ </interimStates>
+                <touchedAccounts> _ => ?_ </touchedAccounts>
+
+                <callState>
+                    <program> #parseByteStack($Foo::RUNTIME) </program>
+                    <jumpDests> #computeValidJumpDests(#parseByteStack($Foo::RUNTIME)) </jumpDests>
+
+                    <id> ACCT_ID </id> // contract owner
+                    <caller> CALLER_ID </caller> // who called this contract; in the beginning, origin // msg.sender
+
+                    // address sig ++ input
+                    <callData> #buf(4, 652482574) ++ #buf(32, IN) </callData>
+
+                    <callValue> 0 </callValue>
+                    <wordStack> .WordStack => ?_ </wordStack>
+                    <localMem> .Memory => ?_ </localMem>
+                    <pc> 0 => ?_ </pc>
+                    <gas> #gas(_VGAS) => ?_ </gas>
+                    <memoryUsed> 0 => ?_ </memoryUsed>
+                    <callGas> _ => ?_ </callGas>
+
+                    <static> false </static> // NOTE: non-static call
+                    <callDepth> CALL_DEPTH </callDepth>
+                </callState>
+
+                <substate>
+                    <selfDestruct> _ </selfDestruct>
+                    <log> _ </log>
+                    <refund> _ </refund> // TODO: more detail
+                    <accessedAccounts> _ => ?_ </accessedAccounts>
+                    <accessedStorage> _ => ?_ </accessedStorage>
+                </substate>
+
+                <gasPrice> _ </gasPrice>
+                <origin> ORIGIN_ID </origin> // who fires tx
+
+                <blockhashes> _ </blockhashes>
+                <block>
+                    <previousHash> _ </previousHash>
+                    <ommersHash> _ </ommersHash>
+                    <coinbase> _ </coinbase>
+                    <stateRoot> _ </stateRoot>
+                    <transactionsRoot> _ </transactionsRoot>
+                    <receiptsRoot> _ </receiptsRoot>
+                    <logsBloom> _ </logsBloom>
+                    <difficulty> _ </difficulty>
+                    <number> _ </number>
+                    <gasLimit> _ </gasLimit>
+                    <gasUsed> _ </gasUsed>
+                    <timestamp> _ </timestamp>
+                    <extraData> _ </extraData>
+                    <mixHash> _ </mixHash>
+                    <blockNonce> _ </blockNonce>
+                    <ommerBlockHeaders> _ </ommerBlockHeaders>
+                    <baseFee> _ </baseFee>
+                </block>
+            </evm>
+
+            <network>
+                <chainID> _ </chainID>
+
+                <activeAccounts> SetItem(ACCT_ID) _:Set </activeAccounts>
+
+                <accounts>
+                    <account>
+                        <acctID> ACCT_ID </acctID>
+                        <balance> _ </balance>
+                        <code> #parseByteStack($Foo::RUNTIME) </code>
+                        <storage> _ </storage>
+                        <origStorage> _ </origStorage>
+                        <nonce> _ </nonce>
+                    </account>
+                </accounts>
+
+                <txOrder> _ </txOrder>
+                <txPending> _ </txPending>
+                <messages> _ </messages>
+            </network>
+        </ethereum>
+    </kevm>
+
+    requires 0 <=Int ACCT_ID    andBool ACCT_ID    <Int (2 ^Int 160)
+        andBool 0  <=Int CALLER_ID  andBool CALLER_ID  <Int (2 ^Int 160)
+        andBool 0  <=Int ORIGIN_ID  andBool ORIGIN_ID  <Int (2 ^Int 160)
+        andBool 0  <=Int CALL_DEPTH andBool CALL_DEPTH <Int 1024
+        andBool (2 ^Int 160)  <=Int IN andBool IN <Int (2 ^Int 256)
+
+endmodule
+
diff --git a/crates/test-files/fixtures/kspecs/abi/address_u16.k b/crates/test-files/fixtures/kspecs/abi/address_u16.k
new file mode 100644
index 0000000000..d256b654fc
--- /dev/null
+++ b/crates/test-files/fixtures/kspecs/abi/address_u16.k
@@ -0,0 +1,108 @@
+module $TEST_NAME
+    imports VERIFICATION
+
+    claim
+
+    <kevm>
+        <k> #execute => #halt </k>
+        <exit-code> 1 </exit-code>
+        <mode> NORMAL </mode>
+        <schedule> ISTANBUL </schedule>
+
+        <ethereum>
+            <evm>
+                <output> _ => #buf(32, OUT_ADDR) ++ #buf(32, OUT_U16)  </output>
+                <statusCode> _ => EVMC_SUCCESS </statusCode>
+                <endPC> _ => ?_ </endPC>
+                <callStack> _ </callStack>
+                <interimStates> _ </interimStates>
+                <touchedAccounts> _ => ?_ </touchedAccounts>
+
+                <callState>
+                    <program> #parseByteStack($Foo::RUNTIME) </program>
+                    <jumpDests> #computeValidJumpDests(#parseByteStack($Foo::RUNTIME)) </jumpDests>
+
+                    <id> ACCT_ID </id> // contract owner
+                    <caller> CALLER_ID </caller> // who called this contract; in the beginning, origin // msg.sender
+
+                    <callData> #abiCallData("_address_u16", #address(IN_ADDR), #uint16(IN_U16)) </callData>
+
+                    <callValue> 0 </callValue>
+                    <wordStack> .WordStack => ?_ </wordStack>
+                    <localMem> .Memory => ?_ </localMem>
+                    <pc> 0 => ?_ </pc>
+                    <gas> #gas(_VGAS) => ?_ </gas>
+                    <memoryUsed> 0 => ?_ </memoryUsed>
+                    <callGas> _ => ?_ </callGas>
+
+                    <static> false </static> // NOTE: non-static call
+                    <callDepth> CALL_DEPTH </callDepth>
+                </callState>
+
+                <substate>
+                    <selfDestruct> _ </selfDestruct>
+                    <log> _ </log>
+                    <refund> _ </refund> // TODO: more detail
+                    <accessedAccounts> _ => ?_ </accessedAccounts>
+                    <accessedStorage> _ => ?_ </accessedStorage>
+                </substate>
+
+                <gasPrice> _ </gasPrice>
+                <origin> ORIGIN_ID </origin> // who fires tx
+
+                <blockhashes> _ </blockhashes>
+                <block>
+                    <previousHash> _ </previousHash>
+                    <ommersHash> _ </ommersHash>
+                    <coinbase> _ </coinbase>
+                    <stateRoot> _ </stateRoot>
+                    <transactionsRoot> _ </transactionsRoot>
+                    <receiptsRoot> _ </receiptsRoot>
+                    <logsBloom> _ </logsBloom>
+                    <difficulty> _ </difficulty>
+                    <number> _ </number>
+                    <gasLimit> _ </gasLimit>
+                    <gasUsed> _ </gasUsed>
+                    <timestamp> _ </timestamp>
+                    <extraData> _ </extraData>
+                    <mixHash> _ </mixHash>
+                    <blockNonce> _ </blockNonce>
+                    <ommerBlockHeaders> _ </ommerBlockHeaders>
+                    <baseFee> _ </baseFee>
+                </block>
+            </evm>
+
+            <network>
+                <chainID> _ </chainID>
+
+                <activeAccounts> SetItem(ACCT_ID) _:Set </activeAccounts>
+
+                <accounts>
+                    <account>
+                        <acctID> ACCT_ID </acctID>
+                        <balance> _ </balance>
+                        <code> #parseByteStack($Foo::RUNTIME) </code>
+                        <storage> _ </storage>
+                        <origStorage> _ </origStorage>
+                        <nonce> _ </nonce>
+                    </account>
+                </accounts>
+
+                <txOrder> _ </txOrder>
+                <txPending> _ </txPending>
+                <messages> _ </messages>
+            </network>
+        </ethereum>
+    </kevm>
+
+    requires 0 <=Int ACCT_ID    andBool ACCT_ID    <Int (2 ^Int 160)
+        andBool 0  <=Int CALLER_ID  andBool CALLER_ID  <Int (2 ^Int 160)
+        andBool 0  <=Int ORIGIN_ID  andBool ORIGIN_ID  <Int (2 ^Int 160)
+        andBool 0  <=Int CALL_DEPTH andBool CALL_DEPTH <Int 1024
+        andBool 0  <=Int IN_ADDR    andBool IN_ADDR    <Int (2 ^Int 160)
+        andBool 0  <=Int IN_U16     andBool IN_U16     <Int (2 ^Int 16)
+        andBool IN_ADDR ==Int OUT_ADDR
+        andBool IN_U16  ==Int OUT_U16
+
+endmodule
+
diff --git a/crates/test-files/fixtures/kspecs/abi/address_u16_revert_0.k b/crates/test-files/fixtures/kspecs/abi/address_u16_revert_0.k
new file mode 100644
index 0000000000..71020c4041
--- /dev/null
+++ b/crates/test-files/fixtures/kspecs/abi/address_u16_revert_0.k
@@ -0,0 +1,112 @@
+module $TEST_NAME
+    imports VERIFICATION
+
+    claim
+
+    <kevm>
+        <k> #execute => #halt </k>
+        <exit-code> 1 </exit-code>
+        <mode> NORMAL </mode>
+        <schedule> ISTANBUL </schedule>
+
+        <ethereum>
+            <evm>
+                // todo: check code
+                <output> _ => b".6\xa7\t\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x03" </output>
+                <statusCode> _ => EVMC_REVERT </statusCode>
+                <endPC> _ => ?_ </endPC>
+                <callStack> _ </callStack>
+                <interimStates> _ </interimStates>
+                <touchedAccounts> _ => ?_ </touchedAccounts>
+
+                <callState>
+                    <program> #parseByteStack($Foo::RUNTIME) </program>
+                    <jumpDests> #computeValidJumpDests(#parseByteStack($Foo::RUNTIME)) </jumpDests>
+
+                    <id> ACCT_ID </id> // contract owner
+                    <caller> CALLER_ID </caller> // who called this contract; in the beginning, origin // msg.sender
+
+                    // _address_u16 sig ++ input
+                    <callData> #buf(4, 802626159) ++ #buf(32, IN_ADDR) ++ #buf(32, IN_U16) </callData>
+
+                    <callValue> 0 </callValue>
+                    <wordStack> .WordStack => ?_ </wordStack>
+                    <localMem> .Memory => ?_ </localMem>
+                    <pc> 0 => ?_ </pc>
+                    <gas> #gas(_VGAS) => ?_ </gas>
+                    <memoryUsed> 0 => ?_ </memoryUsed>
+                    <callGas> _ => ?_ </callGas>
+
+                    <static> false </static> // NOTE: non-static call
+                    <callDepth> CALL_DEPTH </callDepth>
+                </callState>
+
+                <substate>
+                    <selfDestruct> _ </selfDestruct>
+                    <log> _ </log>
+                    <refund> _ </refund> // TODO: more detail
+                    <accessedAccounts> _ => ?_ </accessedAccounts>
+                    <accessedStorage> _ => ?_ </accessedStorage>
+                </substate>
+
+                <gasPrice> _ </gasPrice>
+                <origin> ORIGIN_ID </origin> // who fires tx
+
+                <blockhashes> _ </blockhashes>
+                <block>
+                    <previousHash> _ </previousHash>
+                    <ommersHash> _ </ommersHash>
+                    <coinbase> _ </coinbase>
+                    <stateRoot> _ </stateRoot>
+                    <transactionsRoot> _ </transactionsRoot>
+                    <receiptsRoot> _ </receiptsRoot>
+                    <logsBloom> _ </logsBloom>
+                    <difficulty> _ </difficulty>
+                    <number> _ </number>
+                    <gasLimit> _ </gasLimit>
+                    <gasUsed> _ </gasUsed>
+                    <timestamp> _ </timestamp>
+                    <extraData> _ </extraData>
+                    <mixHash> _ </mixHash>
+                    <blockNonce> _ </blockNonce>
+                    <ommerBlockHeaders> _ </ommerBlockHeaders>
+                    <baseFee> _ </baseFee>
+                </block>
+            </evm>
+
+            <network>
+                <chainID> _ </chainID>
+
+                <activeAccounts> SetItem(ACCT_ID) _:Set </activeAccounts>
+
+                <accounts>
+                    <account>
+                        <acctID> ACCT_ID </acctID>
+                        <balance> _ </balance>
+                        <code> #parseByteStack($Foo::RUNTIME) </code>
+                        <storage> _ </storage>
+                        <origStorage> _ </origStorage>
+                        <nonce> _ </nonce>
+                    </account>
+                </accounts>
+
+                <txOrder> _ </txOrder>
+                <txPending> _ </txPending>
+                <messages> _ </messages>
+            </network>
+        </ethereum>
+    </kevm>
+
+    requires 0 <=Int ACCT_ID    andBool ACCT_ID    <Int (2 ^Int 160)
+        andBool 0  <=Int CALLER_ID  andBool CALLER_ID  <Int (2 ^Int 160)
+        andBool 0  <=Int ORIGIN_ID  andBool ORIGIN_ID  <Int (2 ^Int 160)
+        andBool 0  <=Int CALL_DEPTH andBool CALL_DEPTH <Int 1024
+        // IN_ADDR invalid
+        andBool (2 ^Int 160)  <=Int IN_ADDR andBool IN_ADDR <Int (2 ^Int 256)
+        // replace above line with below for sanity
+        // andBool 0 <=Int IN_ADDR andBool IN_ADDR <Int (2 ^Int 160)
+        // IN_U16 valid
+        andBool 0 <=Int IN_U16 andBool IN_U16 <Int (2 ^Int 16)
+
+endmodule
+
diff --git a/crates/test-files/fixtures/kspecs/abi/address_u16_revert_1.k b/crates/test-files/fixtures/kspecs/abi/address_u16_revert_1.k
new file mode 100644
index 0000000000..35f1bb66c6
--- /dev/null
+++ b/crates/test-files/fixtures/kspecs/abi/address_u16_revert_1.k
@@ -0,0 +1,112 @@
+module $TEST_NAME
+    imports VERIFICATION
+
+    claim
+
+    <kevm>
+        <k> #execute => #halt </k>
+        <exit-code> 1 </exit-code>
+        <mode> NORMAL </mode>
+        <schedule> ISTANBUL </schedule>
+
+        <ethereum>
+            <evm>
+                // todo: check code
+                <output> _ => b".6\xa7\t\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x03" </output>
+                <statusCode> _ => EVMC_REVERT </statusCode>
+                <endPC> _ => ?_ </endPC>
+                <callStack> _ </callStack>
+                <interimStates> _ </interimStates>
+                <touchedAccounts> _ => ?_ </touchedAccounts>
+
+                <callState>
+                    <program> #parseByteStack($Foo::RUNTIME) </program>
+                    <jumpDests> #computeValidJumpDests(#parseByteStack($Foo::RUNTIME)) </jumpDests>
+
+                    <id> ACCT_ID </id> // contract owner
+                    <caller> CALLER_ID </caller> // who called this contract; in the beginning, origin // msg.sender
+
+                    // _address_u16 sig ++ input
+                    <callData> #buf(4, 802626159) ++ #buf(32, IN_ADDR) ++ #buf(32, IN_U16) </callData>
+
+                    <callValue> 0 </callValue>
+                    <wordStack> .WordStack => ?_ </wordStack>
+                    <localMem> .Memory => ?_ </localMem>
+                    <pc> 0 => ?_ </pc>
+                    <gas> #gas(_VGAS) => ?_ </gas>
+                    <memoryUsed> 0 => ?_ </memoryUsed>
+                    <callGas> _ => ?_ </callGas>
+
+                    <static> false </static> // NOTE: non-static call
+                    <callDepth> CALL_DEPTH </callDepth>
+                </callState>
+
+                <substate>
+                    <selfDestruct> _ </selfDestruct>
+                    <log> _ </log>
+                    <refund> _ </refund> // TODO: more detail
+                    <accessedAccounts> _ => ?_ </accessedAccounts>
+                    <accessedStorage> _ => ?_ </accessedStorage>
+                </substate>
+
+                <gasPrice> _ </gasPrice>
+                <origin> ORIGIN_ID </origin> // who fires tx
+
+                <blockhashes> _ </blockhashes>
+                <block>
+                    <previousHash> _ </previousHash>
+                    <ommersHash> _ </ommersHash>
+                    <coinbase> _ </coinbase>
+                    <stateRoot> _ </stateRoot>
+                    <transactionsRoot> _ </transactionsRoot>
+                    <receiptsRoot> _ </receiptsRoot>
+                    <logsBloom> _ </logsBloom>
+                    <difficulty> _ </difficulty>
+                    <number> _ </number>
+                    <gasLimit> _ </gasLimit>
+                    <gasUsed> _ </gasUsed>
+                    <timestamp> _ </timestamp>
+                    <extraData> _ </extraData>
+                    <mixHash> _ </mixHash>
+                    <blockNonce> _ </blockNonce>
+                    <ommerBlockHeaders> _ </ommerBlockHeaders>
+                    <baseFee> _ </baseFee>
+                </block>
+            </evm>
+
+            <network>
+                <chainID> _ </chainID>
+
+                <activeAccounts> SetItem(ACCT_ID) _:Set </activeAccounts>
+
+                <accounts>
+                    <account>
+                        <acctID> ACCT_ID </acctID>
+                        <balance> _ </balance>
+                        <code> #parseByteStack($Foo::RUNTIME) </code>
+                        <storage> _ </storage>
+                        <origStorage> _ </origStorage>
+                        <nonce> _ </nonce>
+                    </account>
+                </accounts>
+
+                <txOrder> _ </txOrder>
+                <txPending> _ </txPending>
+                <messages> _ </messages>
+            </network>
+        </ethereum>
+    </kevm>
+
+    requires 0 <=Int ACCT_ID    andBool ACCT_ID    <Int (2 ^Int 160)
+        andBool 0  <=Int CALLER_ID  andBool CALLER_ID  <Int (2 ^Int 160)
+        andBool 0  <=Int ORIGIN_ID  andBool ORIGIN_ID  <Int (2 ^Int 160)
+        andBool 0  <=Int CALL_DEPTH andBool CALL_DEPTH <Int 1024
+        // IN_ADDR valid
+        andBool 0 <=Int IN_ADDR andBool IN_ADDR <Int (2 ^Int 160)
+        // IN_U16 invalid
+        andBool (2 ^Int 16) <=Int IN_U16 andBool IN_U16 <Int (2 ^Int 256)
+        // replace above line with below for sanity
+        // andBool 0 <=Int IN_U16 andBool IN_U16 <Int (2 ^Int 16)
+
+endmodule
+
diff --git a/crates/test-files/fixtures/kspecs/abi/foo.fe b/crates/test-files/fixtures/kspecs/abi/foo.fe
new file mode 100644
index 0000000000..8b886c96fc
--- /dev/null
+++ b/crates/test-files/fixtures/kspecs/abi/foo.fe
@@ -0,0 +1,13 @@
+contract Foo:
+    pub fn _u256(baz: u256) -> u256:
+        return baz
+
+    pub fn _address(baz: address) -> address:
+        return baz
+
+    pub fn _u8(baz: u8) -> u8:
+        return baz
+
+    pub fn _address_u16(bar: address, baz: u16) -> (address, u16):
+        return (bar, baz)
+
diff --git a/crates/test-files/fixtures/kspecs/abi/u256.k b/crates/test-files/fixtures/kspecs/abi/u256.k
new file mode 100644
index 0000000000..3eb549999e
--- /dev/null
+++ b/crates/test-files/fixtures/kspecs/abi/u256.k
@@ -0,0 +1,106 @@
+module $TEST_NAME
+    imports VERIFICATION
+
+    claim
+
+    <kevm>
+        <k> #execute => #halt </k>
+        <exit-code> 1 </exit-code>
+        <mode> NORMAL </mode>
+        <schedule> ISTANBUL </schedule>
+
+        <ethereum>
+            <evm>
+                <output> _ => #buf(32, OUT) </output>
+                <statusCode> _ => EVMC_SUCCESS </statusCode>
+                <endPC> _ => ?_ </endPC>
+                <callStack> _ </callStack>
+                <interimStates> _ </interimStates>
+                <touchedAccounts> _ => ?_ </touchedAccounts>
+
+                <callState>
+                    <program> #parseByteStack($Foo::RUNTIME) </program>
+                    <jumpDests> #computeValidJumpDests(#parseByteStack($Foo::RUNTIME)) </jumpDests>
+
+                    <id> ACCT_ID </id> // contract owner
+                    <caller> CALLER_ID </caller> // who called this contract; in the beginning, origin // msg.sender
+
+                    <callData> #abiCallData("_u256", #uint256(IN)) </callData>
+
+                    <callValue> 0 </callValue>
+                    <wordStack> .WordStack => ?_ </wordStack>
+                    <localMem> .Memory => ?_ </localMem>
+                    <pc> 0 => ?_ </pc>
+                    <gas> #gas(_VGAS) => ?_ </gas>
+                    <memoryUsed> 0 => ?_ </memoryUsed>
+                    <callGas> _ => ?_ </callGas>
+
+                    <static> false </static> // NOTE: non-static call
+                    <callDepth> CALL_DEPTH </callDepth>
+                </callState>
+
+                <substate>
+                    <selfDestruct> _ </selfDestruct>
+                    <log> _ </log>
+                    <refund> _ </refund> // TODO: more detail
+                    <accessedAccounts> _ => ?_ </accessedAccounts>
+                    <accessedStorage> _ => ?_ </accessedStorage>
+                </substate>
+
+                <gasPrice> _ </gasPrice>
+                <origin> ORIGIN_ID </origin> // who fires tx
+
+                <blockhashes> _ </blockhashes>
+                <block>
+                    <previousHash> _ </previousHash>
+                    <ommersHash> _ </ommersHash>
+                    <coinbase> _ </coinbase>
+                    <stateRoot> _ </stateRoot>
+                    <transactionsRoot> _ </transactionsRoot>
+                    <receiptsRoot> _ </receiptsRoot>
+                    <logsBloom> _ </logsBloom>
+                    <difficulty> _ </difficulty>
+                    <number> _ </number>
+                    <gasLimit> _ </gasLimit>
+                    <gasUsed> _ </gasUsed>
+                    <timestamp> _ </timestamp>
+                    <extraData> _ </extraData>
+                    <mixHash> _ </mixHash>
+                    <blockNonce> _ </blockNonce>
+                    <ommerBlockHeaders> _ </ommerBlockHeaders>
+                    <baseFee> _ </baseFee>
+                </block>
+            </evm>
+
+            <network>
+                <chainID> _ </chainID>
+
+                <activeAccounts> SetItem(ACCT_ID) _:Set </activeAccounts>
+
+                <accounts>
+                    <account>
+                        <acctID> ACCT_ID </acctID>
+                        <balance> _ </balance>
+                        <code> #parseByteStack($Foo::RUNTIME) </code>
+                        <storage> _ </storage>
+                        <origStorage> _ </origStorage>
+                        <nonce> _ </nonce>
+                    </account>
+                </accounts>
+
+                <txOrder> _ </txOrder>
+                <txPending> _ </txPending>
+                <messages> _ </messages>
+            </network>
+        </ethereum>
+    </kevm>
+
+    requires 0 <=Int ACCT_ID    andBool ACCT_ID    <Int (2 ^Int 160)
+        andBool 0  <=Int CALLER_ID  andBool CALLER_ID  <Int (2 ^Int 160)
+        andBool 0  <=Int ORIGIN_ID  andBool ORIGIN_ID  <Int (2 ^Int 160)
+        andBool 0  <=Int CALL_DEPTH andBool CALL_DEPTH <Int 1024
+        andBool 0  <=Int IN         andBool IN         <Int (2 ^Int 256)
+        andBool IN ==Int OUT
+
+endmodule
+
diff --git a/crates/test-files/fixtures/kspecs/abi/u8.k b/crates/test-files/fixtures/kspecs/abi/u8.k
new file mode 100644
index 0000000000..cb95738328
--- /dev/null
+++ b/crates/test-files/fixtures/kspecs/abi/u8.k
@@ -0,0 +1,106 @@
+module $TEST_NAME
+    imports VERIFICATION
+
+    claim
+
+    <kevm>
+        <k> #execute => #halt </k>
+        <exit-code> 1 </exit-code>
+        <mode> NORMAL </mode>
+        <schedule> ISTANBUL </schedule>
+
+        <ethereum>
+            <evm>
+                <output> _ => #buf(32, OUT) </output>
+                <statusCode> _ => EVMC_SUCCESS </statusCode>
+                <endPC> _ => ?_ </endPC>
+                <callStack> _ </callStack>
+                <interimStates> _ </interimStates>
+                <touchedAccounts> _ => ?_ </touchedAccounts>
+
+                <callState>
+                    <program> #parseByteStack($Foo::RUNTIME) </program>
+                    <jumpDests> #computeValidJumpDests(#parseByteStack($Foo::RUNTIME)) </jumpDests>
+
+                    <id> ACCT_ID </id> // contract owner
+                    <caller> CALLER_ID </caller> // who called this contract; in the beginning, origin // msg.sender
+
+                    <callData> #abiCallData("_u8", #uint8(IN)) </callData>
+
+                    <callValue> 0 </callValue>
+                    <wordStack> .WordStack => ?_ </wordStack>
+                    <localMem> .Memory => ?_ </localMem>
+                    <pc> 0 => ?_ </pc>
+                    <gas> #gas(_VGAS) => ?_ </gas>
+                    <memoryUsed> 0 => ?_ </memoryUsed>
+                    <callGas> _ => ?_ </callGas>
+
+                    <static> false </static> // NOTE: non-static call
+                    <callDepth> CALL_DEPTH </callDepth>
+                </callState>
+
+                <substate>
+                    <selfDestruct> _ </selfDestruct>
+                    <log> _ </log>
+                    <refund> _ </refund> // TODO: more detail
+                    <accessedAccounts> _ => ?_ </accessedAccounts>
+                    <accessedStorage> _ => ?_ </accessedStorage>
+                </substate>
+
+                <gasPrice> _ </gasPrice>
+                <origin> ORIGIN_ID </origin> // who fires tx
+
+                <blockhashes> _ </blockhashes>
+                <block>
+                    <previousHash> _ </previousHash>
+                    <ommersHash> _ </ommersHash>
+                    <coinbase> _ </coinbase>
+                    <stateRoot> _ </stateRoot>
+                    <transactionsRoot> _ </transactionsRoot>
+                    <receiptsRoot> _ </receiptsRoot>
+                    <logsBloom> _ </logsBloom>
+                    <difficulty> _ </difficulty>
+                    <number> _ </number>
+                    <gasLimit> _ </gasLimit>
+                    <gasUsed> _ </gasUsed>
+                    <timestamp> _ </timestamp>
+                    <extraData> _ </extraData>
+                    <mixHash> _ </mixHash>
+                    <blockNonce> _ </blockNonce>
+                    <ommerBlockHeaders> _ </ommerBlockHeaders>
+                    <baseFee> _ </baseFee>
+                </block>
+            </evm>
+
+            <network>
+                <chainID> _ </chainID>
+
+                <activeAccounts> SetItem(ACCT_ID) _:Set </activeAccounts>
+
+                <accounts>
+                    <account>
+                        <acctID> ACCT_ID </acctID>
+                        <balance> _ </balance>
+                        <code> #parseByteStack($Foo::RUNTIME) </code>
+                        <storage> _ </storage>
+                        <origStorage> _ </origStorage>
+                        <nonce> _ </nonce>
+                    </account>
+                </accounts>
+
+                <txOrder> _ </txOrder>
+                <txPending> _ </txPending>
+                <messages> _ </messages>
+            </network>
+        </ethereum>
+    </kevm>
+
+    requires 0 <=Int ACCT_ID    andBool ACCT_ID    <Int (2 ^Int 160)
+        andBool 0  <=Int CALLER_ID  andBool CALLER_ID  <Int (2 ^Int 160)
+        andBool 0  <=Int ORIGIN_ID  andBool ORIGIN_ID  <Int (2 ^Int 160)
+        andBool 0  <=Int CALL_DEPTH andBool CALL_DEPTH <Int 1024
+        andBool 0  <=Int IN         andBool IN         <Int (2 ^Int 8)
+        andBool IN ==Int OUT
+
+endmodule
+
diff --git a/crates/test-files/fixtures/kspecs/sanity/foo.fe b/crates/test-files/fixtures/kspecs/sanity/foo.fe
new file mode 100644
index 0000000000..8687e6d882
--- /dev/null
+++ b/crates/test-files/fixtures/kspecs/sanity/foo.fe
@@ -0,0 +1,31 @@
+use std::evm
+
+# always returns 42
+contract Returns42:
+    pub fn __call__():
+        unsafe:
+            evm::mstore(offset: 0, value: 42)
+            evm::return_mem(offset: 0, len: 32)
+
+
+# always returns `input`
+contract ReturnsIn:
+    pub fn __call__():
+        unsafe:
+            let input: u256 = evm::call_data_load(offset: 0)
+            evm::mstore(offset: 0, value: input)
+            evm::return_mem(offset: 0, len: 32)
+
+
+# returns `input`, except when `input == 42`, in which case it will return `26`
+contract ReturnsInCond:
+    pub fn __call__():
+        unsafe:
+            let input: u256 = evm::call_data_load(offset: 0)
+            let output: u256 = input
+
+            if input == 42:
+                output = 26
+
+            evm::mstore(offset: 0, value: output)
+            evm::return_mem(offset: 0, len: 32)
diff --git a/crates/test-files/fixtures/kspecs/sanity/returns_42.k b/crates/test-files/fixtures/kspecs/sanity/returns_42.k
new file mode 100644
index 0000000000..a3d72d965b
--- /dev/null
+++ b/crates/test-files/fixtures/kspecs/sanity/returns_42.k
@@ -0,0 +1,105 @@
+module $TEST_NAME
+    imports VERIFICATION
+
+    claim
+
+    <kevm>
+        <k> #execute => #halt </k>
+        <exit-code> 1 </exit-code>
+        <mode> NORMAL </mode>
+        <schedule> ISTANBUL </schedule>
+
+        <ethereum>
+            <evm>
+                <output> _ => #buf(32, OUT) </output>
+                <statusCode> _ => EVMC_SUCCESS </statusCode>
+                <endPC> _ => ?_ </endPC>
+                <callStack> _ </callStack>
+                <interimStates> _ </interimStates>
+                <touchedAccounts> _ => ?_ </touchedAccounts>
+
+                <callState>
+                    <program> #parseByteStack($Returns42::RUNTIME) </program>
+                    <jumpDests> #computeValidJumpDests(#parseByteStack($Returns42::RUNTIME)) </jumpDests>
+
+                    <id> ACCT_ID </id> // contract owner
+                    <caller> CALLER_ID </caller> // who called this contract; in the beginning, origin // msg.sender
+
+                    <callData> _ </callData>
+
+                    <callValue> 0 </callValue>
+                    <wordStack> .WordStack => ?_ </wordStack>
+                    <localMem> .Memory => ?_ </localMem>
+                    <pc> 0 => ?_ </pc>
+                    <gas> #gas(_VGAS) => ?_ </gas>
+                    <memoryUsed> 0 => ?_ </memoryUsed>
+                    <callGas> _ => ?_ </callGas>
+
+                    <static> false </static> // NOTE: non-static call
+                    <callDepth> CALL_DEPTH </callDepth>
+                </callState>
+
+                <substate>
+                    <selfDestruct> _ </selfDestruct>
+                    <log> _ </log>
+                    <refund> _ </refund> // TODO: more detail
+                    <accessedAccounts> _ => ?_ </accessedAccounts>
+                    <accessedStorage> _ => ?_ </accessedStorage>
+                </substate>
+
+                <gasPrice> _ </gasPrice>
+                <origin> ORIGIN_ID </origin> // who fires tx
+
+                <blockhashes> _ </blockhashes>
+                <block>
+                    <previousHash> _ </previousHash>
+                    <ommersHash> _ </ommersHash>
+                    <coinbase> _ </coinbase>
+                    <stateRoot> _ </stateRoot>
+                    <transactionsRoot> _ </transactionsRoot>
+                    <receiptsRoot> _ </receiptsRoot>
+                    <logsBloom> _ </logsBloom>
+                    <difficulty> _ </difficulty>
+                    <number> _ </number>
+                    <gasLimit> _ </gasLimit>
+                    <gasUsed> _ </gasUsed>
+                    <timestamp> _ </timestamp>
+                    <extraData> _ </extraData>
+                    <mixHash> _ </mixHash>
+                    <blockNonce> _ </blockNonce>
+                    <ommerBlockHeaders> _ </ommerBlockHeaders>
+                    <baseFee> _ </baseFee>
+                </block>
+            </evm>
+
+            <network>
+                <chainID> _ </chainID>
+
+                <activeAccounts> SetItem(ACCT_ID) _:Set </activeAccounts>
+
+                <accounts>
+                    <account>
+                        <acctID> ACCT_ID </acctID>
+                        <balance> _ </balance>
+                        <code> #parseByteStack($Returns42::RUNTIME) </code>
+                        <storage> _ </storage>
+                        <origStorage> _ </origStorage>
+                        <nonce> _ </nonce>
+                    </account>
+                </accounts>
+
+                <txOrder> _ </txOrder>
+                <txPending> _ </txPending>
+                <messages> _ </messages>
+            </network>
+        </ethereum>
+    </kevm>
+
+    requires 0 <=Int ACCT_ID    andBool ACCT_ID    <Int (2 ^Int 160)
+        andBool 0 <=Int CALLER_ID  andBool CALLER_ID  <Int (2 ^Int 160)
+        andBool 0 <=Int ORIGIN_ID  andBool ORIGIN_ID  <Int (2 ^Int 160)
+        andBool 0 <=Int CALL_DEPTH andBool CALL_DEPTH <Int 1024
+        andBool 42 ==Int OUT
+
+endmodule
+
diff --git a/crates/test-files/fixtures/kspecs/sanity/returns_42_invalid.k b/crates/test-files/fixtures/kspecs/sanity/returns_42_invalid.k
new file mode 100644
index 0000000000..63b3df651b
--- /dev/null
+++ b/crates/test-files/fixtures/kspecs/sanity/returns_42_invalid.k
@@ -0,0 +1,106 @@
+module $TEST_NAME
+    imports VERIFICATION
+
+    claim
+
+    <kevm>
+        <k> #execute => #halt </k>
+        <exit-code> 1 </exit-code>
+        <mode> NORMAL </mode>
+        <schedule> ISTANBUL </schedule>
+
+        <ethereum>
+            <evm>
+                <output> _ => #buf(32, OUT) </output>
+                <statusCode> _ => EVMC_SUCCESS </statusCode>
+                <endPC> _ => ?_ </endPC>
+                <callStack> _ </callStack>
+                <interimStates> _ </interimStates>
+                <touchedAccounts> _ => ?_ </touchedAccounts>
+
+                <callState>
+                    <program> #parseByteStack($Returns42::RUNTIME) </program>
+                    <jumpDests> #computeValidJumpDests(#parseByteStack($Returns42::RUNTIME)) </jumpDests>
+
+                    <id> ACCT_ID </id> // contract owner
+                    <caller> CALLER_ID </caller> // who called this contract; in the beginning, origin // msg.sender
+
+                    <callData> _ </callData>
+
+                    <callValue> 0 </callValue>
+                    <wordStack> .WordStack => ?_ </wordStack>
+                    <localMem> .Memory => ?_ </localMem>
+                    <pc> 0 => ?_ </pc>
+                    <gas> #gas(_VGAS) => ?_ </gas>
+                    <memoryUsed> 0 => ?_ </memoryUsed>
+                    <callGas> _ => ?_ </callGas>
+
+                    <static> false </static> // NOTE: non-static call
+                    <callDepth> CALL_DEPTH </callDepth>
+                </callState>
+
+                <substate>
+                    <selfDestruct> _ </selfDestruct>
+                    <log> _ </log>
+                    <refund> _ </refund> // TODO: more detail
+                    <accessedAccounts> _ => ?_ </accessedAccounts>
+                    <accessedStorage> _ => ?_ </accessedStorage>
+                </substate>
+
+                <gasPrice> _ </gasPrice>
+                <origin> ORIGIN_ID </origin> // who fires tx
+
+                <blockhashes> _ </blockhashes>
+                <block>
+                    <previousHash> _ </previousHash>
+                    <ommersHash> _ </ommersHash>
+                    <coinbase> _ </coinbase>
+                    <stateRoot> _ </stateRoot>
+                    <transactionsRoot> _ </transactionsRoot>
+                    <receiptsRoot> _ </receiptsRoot>
+                    <logsBloom> _ </logsBloom>
+                    <difficulty> _ </difficulty>
+                    <number> _ </number>
+                    <gasLimit> _ </gasLimit>
+                    <gasUsed> _ </gasUsed>
+                    <timestamp> _ </timestamp>
+                    <extraData> _ </extraData>
+                    <mixHash> _ </mixHash>
+                    <blockNonce> _ </blockNonce>
+                    <ommerBlockHeaders> _ </ommerBlockHeaders>
+                    <baseFee> _ </baseFee>
+                </block>
+            </evm>
+
+            <network>
+                <chainID> _ </chainID>
+
+                <activeAccounts> SetItem(ACCT_ID) _:Set </activeAccounts>
+
+                <accounts>
+                    <account>
+                        <acctID> ACCT_ID </acctID>
+                        <balance> _ </balance>
+                        <code> #parseByteStack($Returns42::RUNTIME) </code>
+                        <storage> _ </storage>
+                        <origStorage> _ </origStorage>
+                        <nonce> _ </nonce>
+                    </account>
+                </accounts>
+
+                <txOrder> _ </txOrder>
+                <txPending> _ </txPending>
+                <messages> _ </messages>
+            </network>
+        </ethereum>
+    </kevm>
+
+    requires 0 <=Int ACCT_ID    andBool ACCT_ID    <Int (2 ^Int 160)
+        andBool 0 <=Int CALLER_ID  andBool CALLER_ID  <Int (2 ^Int 160)
+        andBool 0 <=Int ORIGIN_ID  andBool ORIGIN_ID  <Int (2 ^Int 160)
+        andBool 0 <=Int CALL_DEPTH andBool CALL_DEPTH <Int 1024
+        andBool 43 ==Int OUT
+
+
+endmodule
+
diff --git a/crates/test-files/fixtures/kspecs/sanity/returns_in.k b/crates/test-files/fixtures/kspecs/sanity/returns_in.k
new file mode 100644
index 0000000000..2c40601f2e
--- /dev/null
+++ b/crates/test-files/fixtures/kspecs/sanity/returns_in.k
@@ -0,0 +1,106 @@
+module $TEST_NAME
+    imports VERIFICATION
+
+    claim
+
+    <kevm>
+        <k> #execute => #halt </k>
+        <exit-code> 1 </exit-code>
+        <mode> NORMAL </mode>
+        <schedule> ISTANBUL </schedule>
+
+        <ethereum>
+            <evm>
+                <output> _ => #buf(32, OUT) </output>
+                <statusCode> _ => EVMC_SUCCESS </statusCode>
+                <endPC> _ => ?_ </endPC>
+                <callStack> _ </callStack>
+                <interimStates> _ </interimStates>
+                <touchedAccounts> _ => ?_ </touchedAccounts>
+
+                <callState>
+                    <program> #parseByteStack($ReturnsIn::RUNTIME) </program>
+                    <jumpDests> #computeValidJumpDests(#parseByteStack($ReturnsIn::RUNTIME)) </jumpDests>
+
+                    <id> ACCT_ID </id> // contract owner
+                    <caller> CALLER_ID </caller> // who called this contract; in the beginning, origin // msg.sender
+
+                    <callData> #buf(32, IN) </callData>
+
+                    <callValue> 0 </callValue>
+                    <wordStack> .WordStack => ?_ </wordStack>
+                    <localMem> .Memory => ?_ </localMem>
+                    <pc> 0 => ?_ </pc>
+                    <gas> #gas(_VGAS) => ?_ </gas>
+                    <memoryUsed> 0 => ?_ </memoryUsed>
+                    <callGas> _ => ?_ </callGas>
+
+                    <static> false </static> // NOTE: non-static call
+                    <callDepth> CALL_DEPTH </callDepth>
+                </callState>
+
+                <substate>
+                    <selfDestruct> _ </selfDestruct>
+                    <log> _ </log>
+                    <refund> _ </refund> // TODO: more detail
+                    <accessedAccounts> _ => ?_ </accessedAccounts>
+                    <accessedStorage> _ => ?_ </accessedStorage>
+                </substate>
+
+                <gasPrice> _ </gasPrice>
+                <origin> ORIGIN_ID </origin> // who fires tx
+
+                <blockhashes> _ </blockhashes>
+                <block>
+                    <previousHash> _ </previousHash>
+                    <ommersHash> _ </ommersHash>
+                    <coinbase> _ </coinbase>
+                    <stateRoot> _ </stateRoot>
+                    <transactionsRoot> _ </transactionsRoot>
+                    <receiptsRoot> _ </receiptsRoot>
+                    <logsBloom> _ </logsBloom>
+                    <difficulty> _ </difficulty>
+                    <number> _ </number>
+                    <gasLimit> _ </gasLimit>
+                    <gasUsed> _ </gasUsed>
+                    <timestamp> _ </timestamp>
+                    <extraData> _ </extraData>
+                    <mixHash> _ </mixHash>
+                    <blockNonce> _ </blockNonce>
+                    <ommerBlockHeaders> _ </ommerBlockHeaders>
+                    <baseFee> _ </baseFee>
+                </block>
+            </evm>
+
+            <network>
+                <chainID> _ </chainID>
+
+                <activeAccounts> SetItem(ACCT_ID) _:Set </activeAccounts>
+
+                <accounts>
+                    <account>
+                        <acctID> ACCT_ID </acctID>
+                        <balance> _ </balance>
+                        <code> #parseByteStack($ReturnsIn::RUNTIME) </code>
+                        <storage> _ </storage>
+                        <origStorage> _ </origStorage>
+                        <nonce> _ </nonce>
+                    </account>
+                </accounts>
+
+                <txOrder> _ </txOrder>
+                <txPending> _ </txPending>
+                <messages> _ </messages>
+            </network>
+        </ethereum>
+    </kevm>
+
+    requires 0 <=Int ACCT_ID    andBool ACCT_ID    <Int (2 ^Int 160)
+        andBool 0  <=Int CALLER_ID  andBool CALLER_ID  <Int (2 ^Int 160)
+        andBool 0  <=Int ORIGIN_ID  andBool ORIGIN_ID  <Int (2 ^Int 160)
+        andBool 0  <=Int CALL_DEPTH andBool CALL_DEPTH <Int 1024
+        andBool 0  <=Int IN         andBool IN         <Int (2 ^Int 256)
+        andBool IN ==Int OUT
+
+endmodule
+
diff --git a/crates/test-files/fixtures/kspecs/sanity/returns_in_cond1.k b/crates/test-files/fixtures/kspecs/sanity/returns_in_cond1.k
new file mode 100644
index 0000000000..d7d466bf8a
--- /dev/null
+++ b/crates/test-files/fixtures/kspecs/sanity/returns_in_cond1.k
@@ -0,0 +1,108 @@
+module $TEST_NAME
+    imports VERIFICATION
+
+    claim
+
+    <kevm>
+        <k> #execute => #halt </k>
+        <exit-code> 1 </exit-code>
+        <mode> NORMAL </mode>
+        <schedule> ISTANBUL </schedule>
+
+        <ethereum>
+            <evm>
+                <output> _ => #buf(32, OUT) </output>
+                <statusCode> _ => EVMC_SUCCESS </statusCode>
+                <endPC> _ => ?_ </endPC>
+                <callStack> _ </callStack>
+                <interimStates> _ </interimStates>
+                <touchedAccounts> _ => ?_ </touchedAccounts>
+
+                <callState>
+                    <program> #parseByteStack($ReturnsInCond::RUNTIME) </program>
+                    <jumpDests> #computeValidJumpDests(#parseByteStack($ReturnsInCond::RUNTIME)) </jumpDests>
+
+                    <id> ACCT_ID </id> // contract owner
+                    <caller> CALLER_ID </caller> // who called this contract; in the beginning, origin // msg.sender
+
+                    <callData> #buf(32, IN) </callData>
+
+                    <callValue> 0 </callValue>
+                    <wordStack> .WordStack => ?_ </wordStack>
+                    <localMem> .Memory => ?_ </localMem>
+                    <pc> 0 => ?_ </pc>
+                    <gas> #gas(_VGAS) => ?_ </gas>
+                    <memoryUsed> 0 => ?_ </memoryUsed>
+                    <callGas> _ => ?_ </callGas>
+
+                    <static> false </static> // NOTE: non-static call
+                    <callDepth> CALL_DEPTH </callDepth>
+                </callState>
+
+                <substate>
+                    <selfDestruct> _ </selfDestruct>
+                    <log> _ </log>
+                    <refund> _ </refund> // TODO: more detail
+                    <accessedAccounts> _ => ?_ </accessedAccounts>
+                    <accessedStorage> _ => ?_ </accessedStorage>
+                </substate>
+
+                <gasPrice> _ </gasPrice>
+                <origin> ORIGIN_ID </origin> // who fires tx
+
+                <blockhashes> _ </blockhashes>
+                <block>
+                    <previousHash> _ </previousHash>
+                    <ommersHash> _ </ommersHash>
+                    <coinbase> _ </coinbase>
+                    <stateRoot> _ </stateRoot>
+                    <transactionsRoot> _ </transactionsRoot>
+                    <receiptsRoot> _ </receiptsRoot>
+                    <logsBloom> _ </logsBloom>
+                    <difficulty> _ </difficulty>
+                    <number> _ </number>
+                    <gasLimit> _ </gasLimit>
+                    <gasUsed> _ </gasUsed>
+                    <timestamp> _ </timestamp>
+                    <extraData> _ </extraData>
+                    <mixHash> _ </mixHash>
+                    <blockNonce> _ </blockNonce>
+                    <ommerBlockHeaders> _ </ommerBlockHeaders>
+                    <baseFee> _ </baseFee>
+                </block>
+            </evm>
+
+            <network>
+                <chainID> _ </chainID>
+
+                <activeAccounts> SetItem(ACCT_ID) _:Set </activeAccounts>
+
+                <accounts>
+                    <account>
+                        <acctID> ACCT_ID </acctID>
+                        <balance> _ </balance>
+                        <code> #parseByteStack($ReturnsInCond::RUNTIME) </code>
+                        <storage> _ </storage>
+                        <origStorage> _ </origStorage>
+                        <nonce> _ </nonce>
+                    </account>
+                </accounts>
+
+                <txOrder> _ </txOrder>
+                <txPending> _ </txPending>
+                <messages> _ </messages>
+            </network>
+        </ethereum>
+    </kevm>
+
+    requires 0 <=Int ACCT_ID    andBool ACCT_ID    <Int (2 ^Int 160)
+        andBool 0  <=Int CALLER_ID  andBool CALLER_ID  <Int (2 ^Int 160)
+        andBool 0  <=Int ORIGIN_ID  andBool ORIGIN_ID  <Int (2 ^Int 160)
+        andBool 0  <=Int CALL_DEPTH andBool CALL_DEPTH <Int 1024
+        andBool 0  <=Int IN         andBool IN         <Int (2 ^Int 256)
+        andBool 42 =/=Int IN
+        andBool IN ==Int OUT
+
+
+endmodule
+
diff --git a/crates/test-files/fixtures/kspecs/sanity/returns_in_cond2.k b/crates/test-files/fixtures/kspecs/sanity/returns_in_cond2.k
new file mode 100644
index 0000000000..1c299e5fb6
--- /dev/null
+++ b/crates/test-files/fixtures/kspecs/sanity/returns_in_cond2.k
@@ -0,0 +1,106 @@
+module $TEST_NAME
+    imports VERIFICATION
+
+    claim
+
+    <kevm>
+        <k> #execute => #halt </k>
+        <exit-code> 1 </exit-code>
+        <mode> NORMAL </mode>
+        <schedule> ISTANBUL </schedule>
+
+        <ethereum>
+            <evm>
+                <output> _ => #buf(32, OUT) </output>
+                <statusCode> _ => EVMC_SUCCESS </statusCode>
+                <endPC> _ => ?_ </endPC>
+                <callStack> _ </callStack>
+                <interimStates> _ </interimStates>
+                <touchedAccounts> _ => ?_ </touchedAccounts>
+
+                <callState>
+                    <program> #parseByteStack($ReturnsInCond::RUNTIME) </program>
+                    <jumpDests> #computeValidJumpDests(#parseByteStack($ReturnsInCond::RUNTIME)) </jumpDests>
+
+                    <id> ACCT_ID </id> // contract owner
+                    <caller> CALLER_ID </caller> // who called this contract; in the beginning, origin // msg.sender
+
+                    <callData> #buf(32, IN) </callData>
+
+                    <callValue> 0 </callValue>
+                    <wordStack> .WordStack => ?_ </wordStack>
+                    <localMem> .Memory => ?_ </localMem>
+                    <pc> 0 => ?_ </pc>
+                    <gas> #gas(_VGAS) => ?_ </gas>
+                    <memoryUsed> 0 => ?_ </memoryUsed>
+                    <callGas> _ => ?_ </callGas>
+
+                    <static> false </static> // NOTE: non-static call
+                    <callDepth> CALL_DEPTH </callDepth>
+                </callState>
+
+                <substate>
+                    <selfDestruct> _ </selfDestruct>
+                    <log> _ </log>
+                    <refund> _ </refund> // TODO: more detail
+                    <accessedAccounts> _ => ?_ </accessedAccounts>
+                    <accessedStorage> _ => ?_ </accessedStorage>
+                </substate>
+
+                <gasPrice> _ </gasPrice>
+                <origin> ORIGIN_ID </origin> // who fires tx
+
+                <blockhashes> _ </blockhashes>
+                <block>
+                    <previousHash> _ </previousHash>
+                    <ommersHash> _ </ommersHash>
+                    <coinbase> _ </coinbase>
+                    <stateRoot> _ </stateRoot>
+                    <transactionsRoot> _ </transactionsRoot>
+                    <receiptsRoot> _ </receiptsRoot>
+                    <logsBloom> _ </logsBloom>
+                    <difficulty> _ </difficulty>
+                    <number> _ </number>
+                    <gasLimit> _ </gasLimit>
+                    <gasUsed> _ </gasUsed>
+                    <timestamp> _ </timestamp>
+                    <extraData> _ </extraData>
+                    <mixHash> _ </mixHash>
+                    <blockNonce> _ </blockNonce>
+                    <ommerBlockHeaders> _ </ommerBlockHeaders>
+                    <baseFee> _ </baseFee>
+                </block>
+            </evm>
+
+            <network>
+                <chainID> _ </chainID>
+
+                <activeAccounts> SetItem(ACCT_ID) _:Set </activeAccounts>
+
+                <accounts>
+                    <account>
+                        <acctID> ACCT_ID </acctID>
+                        <balance> _ </balance>
+                        <code> #parseByteStack($ReturnsInCond::RUNTIME) </code>
+                        <storage> _ </storage>
+                        <origStorage> _ </origStorage>
+                        <nonce> _ </nonce>
+                    </account>
+                </accounts>
+
+                <txOrder> _ </txOrder>
+                <txPending> _ </txPending>
+                <messages> _ </messages>
+            </network>
+        </ethereum>
+    </kevm>
+
+    requires 0 <=Int ACCT_ID    andBool ACCT_ID    <Int (2 ^Int 160)
+        andBool 0  <=Int CALLER_ID  andBool CALLER_ID  <Int (2 ^Int 160)
+        andBool 0  <=Int ORIGIN_ID  andBool ORIGIN_ID  <Int (2 ^Int 160)
+        andBool 0  <=Int CALL_DEPTH andBool CALL_DEPTH <Int 1024
+        andBool 42 ==Int IN
+        andBool 26 ==Int OUT
+
+endmodule
+
diff --git a/crates/test-files/fixtures/kspecs/sanity/returns_in_cond2_invalid.k b/crates/test-files/fixtures/kspecs/sanity/returns_in_cond2_invalid.k
new file mode 100644
index 0000000000..87c8ded9df
--- /dev/null
+++ b/crates/test-files/fixtures/kspecs/sanity/returns_in_cond2_invalid.k
@@ -0,0 +1,105 @@
+module $TEST_NAME
+    imports VERIFICATION
+
+    claim
+
+    <kevm>
+        <k> #execute => #halt </k>
+        <exit-code> 1 </exit-code>
+        <mode> NORMAL </mode>
+        <schedule> ISTANBUL </schedule>
+
+        <ethereum>
+            <evm>
+                <output> _ => #buf(32, OUT) </output>
+                <statusCode> _ => EVMC_SUCCESS </statusCode>
+                <endPC> _ => ?_ </endPC>
+                <callStack> _ </callStack>
+                <interimStates> _ </interimStates>
+                <touchedAccounts> _ => ?_ </touchedAccounts>
+
+                <callState>
+                    <program> #parseByteStack($ReturnsInCond::RUNTIME) </program>
+                    <jumpDests> #computeValidJumpDests(#parseByteStack($ReturnsInCond::RUNTIME)) </jumpDests>
+
+                    <id> ACCT_ID </id> // contract owner
+                    <caller> CALLER_ID </caller> // who called this contract; in the beginning, origin // msg.sender
+
+                    <callData> #buf(32, IN) </callData>
+
+                    <callValue> 0 </callValue>
+                    <wordStack> .WordStack => ?_ </wordStack>
+                    <localMem> .Memory => ?_ </localMem>
+                    <pc> 0 => ?_ </pc>
+                    <gas> #gas(_VGAS) => ?_ </gas>
+                    <memoryUsed> 0 => ?_ </memoryUsed>
+                    <callGas> _ => ?_ </callGas>
+
+                    <static> false </static> // NOTE: non-static call
+                    <callDepth> CALL_DEPTH </callDepth>
+                </callState>
+
+                <substate>
+                    <selfDestruct> _ </selfDestruct>
+                    <log> _ </log>
+                    <refund> _ </refund> // TODO: more detail
+                    <accessedAccounts> _ => ?_ </accessedAccounts>
+                    <accessedStorage> _ => ?_ </accessedStorage>
+                </substate>
+
+                <gasPrice> _ </gasPrice>
+                <origin> ORIGIN_ID </origin> // who fires tx
+
+                <blockhashes> _ </blockhashes>
+                <block>
+                    <previousHash> _ </previousHash>
+                    <ommersHash> _ </ommersHash>
+                    <coinbase> _ </coinbase>
+                    <stateRoot> _ </stateRoot>
+                    <transactionsRoot> _ </transactionsRoot>
+                    <receiptsRoot> _ </receiptsRoot>
+                    <logsBloom> _ </logsBloom>
+                    <difficulty> _ </difficulty>
+                    <number> _ </number>
+                    <gasLimit> _ </gasLimit>
+                    <gasUsed> _ </gasUsed>
+                    <timestamp> _ </timestamp>
+                    <extraData> _ </extraData>
+                    <mixHash> _ </mixHash>
+                    <blockNonce> _ </blockNonce>
+                    <ommerBlockHeaders> _ </ommerBlockHeaders>
+                    <baseFee> _ </baseFee>
+                </block>
+            </evm>
+
+            <network>
+                <chainID> _ </chainID>
+
+                <activeAccounts> SetItem(ACCT_ID) _:Set </activeAccounts>
+
+                <accounts>
+                    <account>
+                        <acctID> ACCT_ID </acctID>
+                        <balance> _ </balance>
+                        <code> #parseByteStack($ReturnsInCond::RUNTIME) </code>
+                        <storage> _ </storage>
+                        <origStorage> _ </origStorage>
+                        <nonce> _ </nonce>
+                    </account>
+                </accounts>
+
+                <txOrder> _ </txOrder>
+                <txPending> _ </txPending>
+                <messages> _ </messages>
+            </network>
+        </ethereum>
+    </kevm>
+
+    requires 0 <=Int ACCT_ID    andBool ACCT_ID    <Int (2 ^Int 160)
+        andBool 0  <=Int CALLER_ID  andBool CALLER_ID  <Int (2 ^Int 160)
+        andBool 0  <=Int ORIGIN_ID  andBool ORIGIN_ID  <Int (2 ^Int 160)
+        andBool 0  <=Int CALL_DEPTH andBool CALL_DEPTH <Int 1024
+        andBool 43 ==Int IN
+        andBool 26 ==Int OUT
+
+endmodule
\ No newline at end of file
diff --git a/crates/test-files/fixtures/kspecs/sanity/returns_in_invalid.k b/crates/test-files/fixtures/kspecs/sanity/returns_in_invalid.k
new file mode 100644
index 0000000000..1e49b40cdc
--- /dev/null
+++ b/crates/test-files/fixtures/kspecs/sanity/returns_in_invalid.k
@@ -0,0 +1,106 @@
+module $TEST_NAME
+    imports VERIFICATION
+
+    claim
+
+    <kevm>
+        <k> #execute => #halt </k>
+        <exit-code> 1 </exit-code>
+        <mode> NORMAL </mode>
+        <schedule> ISTANBUL </schedule>
+
+        <ethereum>
+            <evm>
+                <output> _ => #buf(32, OUT) </output>
+                <statusCode> _ => EVMC_SUCCESS </statusCode>
+                <endPC> _ => ?_ </endPC>
+                <callStack> _ </callStack>
+                <interimStates> _ </interimStates>
+                <touchedAccounts> _ => ?_ </touchedAccounts>
+
+                <callState>
+                    <program> #parseByteStack($ReturnsIn::RUNTIME) </program>
+                    <jumpDests> #computeValidJumpDests(#parseByteStack($ReturnsIn::RUNTIME)) </jumpDests>
+
+                    <id> ACCT_ID </id> // contract owner
+                    <caller> CALLER_ID </caller> // who called this contract; in the beginning, origin // msg.sender
+
+                    <callData> #buf(32, IN) </callData>
+
+                    <callValue> 0 </callValue>
+                    <wordStack> .WordStack => ?_ </wordStack>
+                    <localMem> .Memory => ?_ </localMem>
+                    <pc> 0 => ?_ </pc>
+                    <gas> #gas(_VGAS) => ?_ </gas>
+                    <memoryUsed> 0 => ?_ </memoryUsed>
+                    <callGas> _ => ?_ </callGas>
+
+                    <static> false </static> // NOTE: non-static call
+                    <callDepth> CALL_DEPTH </callDepth>
+                </callState>
+
+                <substate>
+                    <selfDestruct> _ </selfDestruct>
+                    <log> _ </log>
+                    <refund> _ </refund> // TODO: more detail
+                    <accessedAccounts> _ => ?_ </accessedAccounts>
+                    <accessedStorage> _ => ?_ </accessedStorage>
+                </substate>
+
+                <gasPrice> _ </gasPrice>
+                <origin> ORIGIN_ID </origin> // who fires tx
+
+                <blockhashes> _ </blockhashes>
+                <block>
+                    <previousHash> _ </previousHash>
+                    <ommersHash> _ </ommersHash>
+                    <coinbase> _ </coinbase>
+                    <stateRoot> _ </stateRoot>
+                    <transactionsRoot> _ </transactionsRoot>
+                    <receiptsRoot> _ </receiptsRoot>
+                    <logsBloom> _ </logsBloom>
+                    <difficulty> _ </difficulty>
+                    <number> _ </number>
+                    <gasLimit> _ </gasLimit>
+                    <gasUsed> _ </gasUsed>
+                    <timestamp> _ </timestamp>
+                    <extraData> _ </extraData>
+                    <mixHash> _ </mixHash>
+                    <blockNonce> _ </blockNonce>
+                    <ommerBlockHeaders> _ </ommerBlockHeaders>
+                    <baseFee> _ </baseFee>
+                </block>
+            </evm>
+
+            <network>
+                <chainID> _ </chainID>
+
+                <activeAccounts> SetItem(ACCT_ID) _:Set </activeAccounts>
+
+                <accounts>
+                    <account>
+                        <acctID> ACCT_ID </acctID>
+                        <balance> _ </balance>
+                        <code> #parseByteStack($ReturnsIn::RUNTIME) </code>
+                        <storage> _ </storage>
+                        <origStorage> _ </origStorage>
+                        <nonce> _ </nonce>
+                    </account>
+                </accounts>
+
+                <txOrder> _ </txOrder>
+                <txPending> _ </txPending>
+                <messages> _ </messages>
+            </network>
+        </ethereum>
+    </kevm>
+
+    requires 0 <=Int ACCT_ID    andBool ACCT_ID    <Int (2 ^Int 160)
+        andBool 0  <=Int CALLER_ID  andBool CALLER_ID  <Int (2 ^Int 160)
+        andBool 0  <=Int ORIGIN_ID  andBool ORIGIN_ID  <Int (2 ^Int 160)
+        andBool 0  <=Int CALL_DEPTH andBool CALL_DEPTH <Int 1024
+        andBool 0  <=Int IN         andBool IN         <Int (2 ^Int 256)
+        andBool IN ==Int OUT +Int 1
+
+endmodule
+
diff --git a/crates/test-files/fixtures/kspecs/storage/foo.fe b/crates/test-files/fixtures/kspecs/storage/foo.fe
new file mode 100644
index 0000000000..e14db14319
--- /dev/null
+++ b/crates/test-files/fixtures/kspecs/storage/foo.fe
@@ -0,0 +1,30 @@
+use std::evm
+
+contract StoreU256:
+    my_u256: u256
+
+    pub fn __call__(self):
+        unsafe:
+            evm::mstore(offset: 0, value: self.my_u256)
+            evm::return_mem(offset: 0, len: 32)
+
+
+contract StoreSolMap:
+    pub fn __call__():
+        unsafe:
+            let key: u256 = evm::call_data_load(offset: 0)
+            evm::mstore(offset: 0, value: key)
+            evm::mstore(offset: 32, value: 0)
+            let slot: u256 = evm::keccak256_mem(offset: 0, len: 64)
+            let value: u256 = evm::sload(offset: slot)
+            evm::mstore(offset: 0, value)
+            evm::return_mem(offset: 0, len: 32)
+
+contract StoreFeMap:
+    my_map: Map<u256, u256>
+
+    pub fn __call__(self):
+        unsafe:
+            let key: u256 = evm::call_data_load(offset: 0)
+            evm::mstore(offset: 0, value: self.my_map[key])
+            evm::return_mem(offset: 0, len: 32)
diff --git a/crates/test-files/fixtures/kspecs/storage/store_fe_map.k b/crates/test-files/fixtures/kspecs/storage/store_fe_map.k
new file mode 100644
index 0000000000..cbe274cc25
--- /dev/null
+++ b/crates/test-files/fixtures/kspecs/storage/store_fe_map.k
@@ -0,0 +1,110 @@
+module $TEST_NAME
+    imports VERIFICATION
+
+    claim
+
+    <kevm>
+        <k> #execute => #halt </k>
+        <exit-code> 1 </exit-code>
+        <mode> NORMAL </mode>
+        <schedule> ISTANBUL </schedule>
+
+        <ethereum>
+            <evm>
+                <output> #buf(32, VAL) </output>
+                <statusCode> _ => EVMC_SUCCESS </statusCode>
+                <endPC> _ => ?_ </endPC>
+                <callStack> _ </callStack>
+                <interimStates> _ </interimStates>
+                <touchedAccounts> _ => ?_ </touchedAccounts>
+
+                <callState>
+                    <program> #parseByteStack($StoreFeMap::RUNTIME) </program>
+                    <jumpDests> #computeValidJumpDests(#parseByteStack($StoreFeMap::RUNTIME)) </jumpDests>
+
+                    <id> ACCT_ID </id> // contract owner
+                    <caller> CALLER_ID </caller> // who called this contract; in the beginning, origin // msg.sender
+
+                    <callData> #buf(32, KEY) </callData>
+
+                    <callValue> 0 </callValue>
+                    <wordStack> .WordStack => ?_ </wordStack>
+                    <localMem> .Memory => ?_ </localMem>
+                    <pc> 0 => ?_ </pc>
+                    <gas> #gas(_VGAS) => ?_ </gas>
+                    <memoryUsed> 0 => ?_ </memoryUsed>
+                    <callGas> _ => ?_ </callGas>
+
+                    <static> false </static> // NOTE: non-static call
+                    <callDepth> CALL_DEPTH </callDepth>
+                </callState>
+
+                <substate>
+                    <selfDestruct> _ </selfDestruct>
+                    <log> _ </log>
+                    <refund> _ </refund> // TODO: more detail
+                    <accessedAccounts> _ => ?_ </accessedAccounts>
+                    <accessedStorage> _ => ?_ </accessedStorage>
+                </substate>
+
+                <gasPrice> _ </gasPrice>
+                <origin> ORIGIN_ID </origin> // who fires tx
+
+                <blockhashes> _ </blockhashes>
+                <block>
+                    <previousHash> _ </previousHash>
+                    <ommersHash> _ </ommersHash>
+                    <coinbase> _ </coinbase>
+                    <stateRoot> _ </stateRoot>
+                    <transactionsRoot> _ </transactionsRoot>
+                    <receiptsRoot> _ </receiptsRoot>
+                    <logsBloom> _ </logsBloom>
+                    <difficulty> _ </difficulty>
+                    <number> _ </number>
+                    <gasLimit> _ </gasLimit>
+                    <gasUsed> _ </gasUsed>
+                    <timestamp> _ </timestamp>
+                    <extraData> _ </extraData>
+                    <mixHash> _ </mixHash>
+                    <blockNonce> _ </blockNonce>
+                    <ommerBlockHeaders> _ </ommerBlockHeaders>
+                    <baseFee> _ </baseFee>
+                </block>
+            </evm>
+
+            <network>
+                <chainID> _ </chainID>
+
+                <activeAccounts> SetItem(ACCT_ID) _:Set </activeAccounts>
+
+                <accounts>
+                    <account>
+                        <acctID> ACCT_ID </acctID>
+                        <balance> _ </balance>
+                        <code> #parseByteStack($StoreFeMap::RUNTIME) </code>
+                        <storage> #hashedLocation("Fe", 0, KEY) |-> VAL _:Map </storage>
+                        <origStorage> _ </origStorage>
+                        <nonce> _ </nonce>
+                    </account>
+                </accounts>
+
+                <txOrder> _ </txOrder>
+                <txPending> _ </txPending>
+                <messages> _ </messages>
+            </network>
+        </ethereum>
+    </kevm>
+
+    requires 0 <=Int ACCT_ID    andBool ACCT_ID    <Int (2 ^Int 160)
+        andBool 0 <=Int CALLER_ID  andBool CALLER_ID  <Int (2 ^Int 160)
+        andBool 0 <=Int ORIGIN_ID  andBool ORIGIN_ID  <Int (2 ^Int 160)
+        andBool 0 <=Int CALL_DEPTH andBool CALL_DEPTH <Int 1024
+        andBool 40 <=Int KEY   andBool KEY    <Int 50
+        //andBool 0 <=Int KEY   andBool KEY    <Int (2 ^Int 256)
+        //andBool 42 ==Int KEY
+        andBool 40 <=Int VAL   andBool VAL    <Int 50
+        //andBool 0 <=Int VAL   andBool VAL    <Int (2 ^Int 256)
+        //andBool 26 ==Int VAL
+
+endmodule
+
diff --git a/crates/test-files/fixtures/kspecs/storage/store_sol_map.k b/crates/test-files/fixtures/kspecs/storage/store_sol_map.k
new file mode 100644
index 0000000000..ff3600fdd5
--- /dev/null
+++ b/crates/test-files/fixtures/kspecs/storage/store_sol_map.k
@@ -0,0 +1,106 @@
+module $TEST_NAME
+    imports VERIFICATION
+
+    claim
+
+    <kevm>
+        <k> #execute => #halt </k>
+        <exit-code> 1 </exit-code>
+        <mode> NORMAL </mode>
+        <schedule> ISTANBUL </schedule>
+
+        <ethereum>
+            <evm>
+                <output> #buf(32, VAL) </output>
+                <statusCode> _ => EVMC_SUCCESS </statusCode>
+                <endPC> _ => ?_ </endPC>
+                <callStack> _ </callStack>
+                <interimStates> _ </interimStates>
+                <touchedAccounts> _ => ?_ </touchedAccounts>
+
+                <callState>
+                    <program> #parseByteStack($StoreSolMap::RUNTIME) </program>
+                    <jumpDests> #computeValidJumpDests(#parseByteStack($StoreSolMap::RUNTIME)) </jumpDests>
+
+                    <id> ACCT_ID </id> // contract owner
+                    <caller> CALLER_ID </caller> // who called this contract; in the beginning, origin // msg.sender
+
+                    <callData> #buf(32, KEY) </callData>
+
+                    <callValue> 0 </callValue>
+                    <wordStack> .WordStack => ?_ </wordStack>
+                    <localMem> .Memory => ?_ </localMem>
+                    <pc> 0 => ?_ </pc>
+                    <gas> #gas(_VGAS) => ?_ </gas>
+                    <memoryUsed> 0 => ?_ </memoryUsed>
+                    <callGas> _ => ?_ </callGas>
+
+                    <static> false </static> // NOTE: non-static call
+                    <callDepth> CALL_DEPTH </callDepth>
+                </callState>
+
+                <substate>
+                    <selfDestruct> _ </selfDestruct>
+                    <log> _ </log>
+                    <refund> _ </refund> // TODO: more detail
+                    <accessedAccounts> _ => ?_ </accessedAccounts>
+                    <accessedStorage> _ => ?_ </accessedStorage>
+                </substate>
+
+                <gasPrice> _ </gasPrice>
+                <origin> ORIGIN_ID </origin> // who fires tx
+
+                <blockhashes> _ </blockhashes>
+                <block>
+                    <previousHash> _ </previousHash>
+                    <ommersHash> _ </ommersHash>
+                    <coinbase> _ </coinbase>
+                    <stateRoot> _ </stateRoot>
+                    <transactionsRoot> _ </transactionsRoot>
+                    <receiptsRoot> _ </receiptsRoot>
+                    <logsBloom> _ </logsBloom>
+                    <difficulty> _ </difficulty>
+                    <number> _ </number>
+                    <gasLimit> _ </gasLimit>
+                    <gasUsed> _ </gasUsed>
+                    <timestamp> _ </timestamp>
+                    <extraData> _ </extraData>
+                    <mixHash> _ </mixHash>
+                    <blockNonce> _ </blockNonce>
+                    <ommerBlockHeaders> _ </ommerBlockHeaders>
+                    <baseFee> _ </baseFee>
+                </block>
+            </evm>
+
+            <network>
+                <chainID> _ </chainID>
+
+                <activeAccounts> SetItem(ACCT_ID) _:Set </activeAccounts>
+
+                <accounts>
+                    <account>
+                        <acctID> ACCT_ID </acctID>
+                        <balance> _ </balance>
+                        <code> #parseByteStack($StoreSolMap::RUNTIME) </code>
+                        <storage> #hashedLocation("Solidity", 0, KEY) |-> VAL _:Map </storage>
+                        <origStorage> _ </origStorage>
+                        <nonce> _ </nonce>
+                    </account>
+                </accounts>
+
+                <txOrder> _ </txOrder>
+                <txPending> _ </txPending>
+                <messages> _ </messages>
+            </network>
+        </ethereum>
+    </kevm>
+
+    requires 0 <=Int ACCT_ID    andBool ACCT_ID    <Int (2 ^Int 160)
+        andBool 0 <=Int CALLER_ID  andBool CALLER_ID  <Int (2 ^Int 160)
+        andBool 0 <=Int ORIGIN_ID  andBool ORIGIN_ID  <Int (2 ^Int 160)
+        andBool 0 <=Int CALL_DEPTH andBool CALL_DEPTH <Int 1024
+        andBool 0 <=Int KEY   andBool KEY    <Int (2 ^Int 256)
+        andBool 0 <=Int VAL   andBool VAL    <Int (2 ^Int 256)
+
+endmodule
+
diff --git a/crates/test-files/fixtures/kspecs/storage/store_u256.k b/crates/test-files/fixtures/kspecs/storage/store_u256.k
new file mode 100644
index 0000000000..54ca8e05bf
--- /dev/null
+++ b/crates/test-files/fixtures/kspecs/storage/store_u256.k
@@ -0,0 +1,106 @@
+module $TEST_NAME
+    imports VERIFICATION
+
+    claim
+
+    <kevm>
+        <k> #execute => #halt </k>
+        <exit-code> 1 </exit-code>
+        <mode> NORMAL </mode>
+        <schedule> ISTANBUL </schedule>
+
+        <ethereum>
+            <evm>
+                <output> _ => #buf(32, OUT) </output>
+                <statusCode> _ => EVMC_SUCCESS </statusCode>
+                <endPC> _ => ?_ </endPC>
+                <callStack> _ </callStack>
+                <interimStates> _ </interimStates>
+                <touchedAccounts> _ => ?_ </touchedAccounts>
+
+                <callState>
+                    <program> #parseByteStack($StoreU256::RUNTIME) </program>
+                    <jumpDests> #computeValidJumpDests(#parseByteStack($StoreU256::RUNTIME)) </jumpDests>
+
+                    <id> ACCT_ID </id> // contract owner
+                    <caller> CALLER_ID </caller> // who called this contract; in the beginning, origin // msg.sender
+
+                    <callData> _ </callData>
+
+                    <callValue> 0 </callValue>
+                    <wordStack> .WordStack => ?_ </wordStack>
+                    <localMem> .Memory => ?_ </localMem>
+                    <pc> 0 => ?_ </pc>
+                    <gas> #gas(_VGAS) => ?_ </gas>
+                    <memoryUsed> 0 => ?_ </memoryUsed>
+                    <callGas> _ => ?_ </callGas>
+
+                    <static> false </static> // NOTE: non-static call
+                    <callDepth> CALL_DEPTH </callDepth>
+                </callState>
+
+                <substate>
+                    <selfDestruct> _ </selfDestruct>
+                    <log> _ </log>
+                    <refund> _ </refund> // TODO: more detail
+                    <accessedAccounts> _ => ?_ </accessedAccounts>
+                    <accessedStorage> _ => ?_ </accessedStorage>
+                </substate>
+
+                <gasPrice> _ </gasPrice>
+                <origin> ORIGIN_ID </origin> // who fires tx
+
+                <blockhashes> _ </blockhashes>
+                <block>
+                    <previousHash> _ </previousHash>
+                    <ommersHash> _ </ommersHash>
+                    <coinbase> _ </coinbase>
+                    <stateRoot> _ </stateRoot>
+                    <transactionsRoot> _ </transactionsRoot>
+                    <receiptsRoot> _ </receiptsRoot>
+                    <logsBloom> _ </logsBloom>
+                    <difficulty> _ </difficulty>
+                    <number> _ </number>
+                    <gasLimit> _ </gasLimit>
+                    <gasUsed> _ </gasUsed>
+                    <timestamp> _ </timestamp>
+                    <extraData> _ </extraData>
+                    <mixHash> _ </mixHash>
+                    <blockNonce> _ </blockNonce>
+                    <ommerBlockHeaders> _ </ommerBlockHeaders>
+                    <baseFee> _ </baseFee>
+                </block>
+            </evm>
+
+            <network>
+                <chainID> _ </chainID>
+
+                <activeAccounts> SetItem(ACCT_ID) _:Set </activeAccounts>
+
+                <accounts>
+                    <account>
+                        <acctID> ACCT_ID </acctID>
+                        <balance> _ </balance>
+                        <code> #parseByteStack($StoreU256::RUNTIME) </code>
+                        <storage> 60532348206132712130393038501709678949590013789985963502110323372208181384 |-> MY_U256 _:Map </storage>
+                        <origStorage> _ </origStorage>
+                        <nonce> _ </nonce>
+                    </account>
+                </accounts>
+
+                <txOrder> _ </txOrder>
+                <txPending> _ </txPending>
+                <messages> _ </messages>
+            </network>
+        </ethereum>
+    </kevm>
+
+    requires 0 <=Int ACCT_ID    andBool ACCT_ID    <Int (2 ^Int 160)
+        andBool 0 <=Int CALLER_ID  andBool CALLER_ID  <Int (2 ^Int 160)
+        andBool 0 <=Int ORIGIN_ID  andBool ORIGIN_ID  <Int (2 ^Int 160)
+        andBool 0 <=Int CALL_DEPTH andBool CALL_DEPTH <Int 1024
+        andBool 0 <=Int MY_U256    andBool MY_U256    <Int (2 ^Int 256)
+        andBool MY_U256 ==Int OUT
+
+endmodule
+
diff --git a/specs/simple7-spec.k b/specs/simple7-spec.k
new file mode 100644
index 0000000000..30a47900a4
--- /dev/null
+++ b/specs/simple7-spec.k
@@ -0,0 +1,109 @@
+module SIMPLE7-SPEC
+    imports VERIFICATION
+
+    claim
+
+    <kevm>
+        <k> #execute => #halt </k>
+        <exit-code> 1 </exit-code>
+        <mode> NORMAL </mode>
+        <schedule> ISTANBUL </schedule>
+
+        <ethereum>
+            <evm>
+                <output> _ => #buf(0, 0) </output>
+                <statusCode> _ => EVMC_SUCCESS </statusCode>
+                <callStack> _ </callStack>
+                <interimStates> _ </interimStates>
+                <touchedAccounts> _ => ?_ </touchedAccounts>
+
+                <callState>
+                    // todo: gen this part
+                    <program> #parseByteStack("0x6000604035600160203583356103ff8082118414841460625783818411148414606257841183148314605e57600390603e858002848002838002016066565b14158214605a5760041415146056576054906070565b005b5080f35b8380f35b8480f35b8580f35b1415600114605457565b60051415600114607c57565b600080fd") </program>
+                    <jumpDests> #computeValidJumpDests(#parseByteStack("0x6000604035600160203583356103ff8082118414841460625783818411148414606257841183148314605e57600390603e858002848002838002016066565b14158214605a5760041415146056576054906070565b005b5080f35b8380f35b8480f35b8580f35b1415600114605457565b60051415600114607c57565b600080fd")) </jumpDests>
+
+                    <id> ACCT_ID </id> // contract owner
+                    <caller> CALLER_ID </caller> // who called this contract; in the beginning, origin // msg.sender
+
+                    // todo: gen this part
+                    <callData> #buf(32, ARG_0) +Bytes #buf(32, ARG_1) +Bytes #buf(32, ARG_2) </callData>
+
+                    <callValue> 0 </callValue>
+                    <wordStack> .WordStack => ?_ </wordStack>
+                    <localMem> .Bytes => ?_ </localMem>
+                    <pc> 0 => ?_ </pc>
+                    <gas> #gas(_VGAS) => ?_ </gas>
+                    <memoryUsed> 0 => ?_ </memoryUsed>
+                    <callGas> _ => ?_ </callGas>
+
+                    <static> false </static> // NOTE: non-static call
+                    <callDepth> CALL_DEPTH </callDepth>
+                </callState>
+
+                <substate>
+                    <selfDestruct> _ </selfDestruct>
+                    <log> _ </log>
+                    <refund> _ </refund>
+                    <accessedAccounts> _ => ?_ </accessedAccounts>
+                    <accessedStorage> _ => ?_ </accessedStorage>
+                </substate>
+
+                <gasPrice> _ </gasPrice>
+                <origin> ORIGIN_ID </origin>
+
+                <blockhashes> _ </blockhashes>
+                <block>
+                    <previousHash> _ </previousHash>
+                    <ommersHash> _ </ommersHash>
+                    <coinbase> _ </coinbase>
+                    <stateRoot> _ </stateRoot>
+                    <transactionsRoot> _ </transactionsRoot>
+                    <receiptsRoot> _ </receiptsRoot>
+                    <logsBloom> _ </logsBloom>
+                    <difficulty> _ </difficulty>
+                    <number> _ </number>
+                    <gasLimit> _ </gasLimit>
+                    <gasUsed> _ </gasUsed>
+                    <timestamp> _ </timestamp>
+                    <extraData> _ </extraData>
+                    <mixHash> _ </mixHash>
+                    <blockNonce> _ </blockNonce>
+                    <ommerBlockHeaders> _ </ommerBlockHeaders>
+                    <baseFee> _ </baseFee>
+                </block>
+            </evm>
+
+            <network>
+                <chainID> _ </chainID>
+
+                <activeAccounts> SetItem(ACCT_ID) _:Set </activeAccounts>
+
+                <accounts>
+                    <account>
+                        <acctID> ACCT_ID </acctID>
+                        <balance> _ </balance>
+                        // todo: gen this part
+                        <code> #parseByteStack("0x6000604035600160203583356103ff8082118414841460625783818411148414606257841183148314605e57600390603e858002848002838002016066565b14158214605a5760041415146056576054906070565b005b5080f35b8380f35b8480f35b8580f35b1415600114605457565b60051415600114607c57565b600080fd") </code>
+                        <storage> _ </storage>
+                        <origStorage> _ </origStorage>
+                        <nonce> _ </nonce>
+                    </account>
+                </accounts>
+
+                <txOrder> _ </txOrder>
+                <txPending> _ </txPending>
+                <messages> _ </messages>
+            </network>
+        </ethereum>
+    </kevm>
+
+    requires 0 <=Int ACCT_ID    andBool ACCT_ID    <Int (2 ^Int 160)
+        andBool 0  <=Int CALLER_ID  andBool CALLER_ID  <Int (2 ^Int 160)
+        andBool 0  <=Int ORIGIN_ID  andBool ORIGIN_ID  <Int (2 ^Int 160)
+        andBool 0  <=Int CALL_DEPTH andBool CALL_DEPTH <Int 1024
+        andBool 0  <=Int ARG_0 andBool ARG_0 <Int (2 ^Int 256)
+andBool 0  <=Int ARG_1 andBool ARG_1 <Int (2 ^Int 256)
+andBool 0  <=Int ARG_2 andBool ARG_2 <Int (2 ^Int 256)
+
+endmodule
+