diff --git a/.github/workflows/expensive.yml b/.github/workflows/expensive.yml
index 32d8c6341f..7a5f5acafa 100644
--- a/.github/workflows/expensive.yml
+++ b/.github/workflows/expensive.yml
@@ -29,10 +29,10 @@ jobs:
         uses: Swatinem/rust-cache@v1
 
       - name: Build
-        run: cargo test --workspace --all-features --no-run --locked -- --ignored
+        run: cargo test --workspace --features solc-backend --no-run --locked -- --ignored
       - name: Run expensive tests
         id: expensive_tests
-        run: cargo test --workspace --all-features --verbose -- --ignored
+        run: cargo test --workspace --features solc-backend --verbose -- --ignored
       - name: Report
         if: failure() && steps.expensive_tests.outcome == 'failure'
         run: |
diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
index 131af90254..701983d028 100644
--- a/.github/workflows/main.yml
+++ b/.github/workflows/main.yml
@@ -121,9 +121,9 @@ jobs:
       - name: Cache Dependencies
         uses: Swatinem/rust-cache@v1
       - name: Build
-        run: cargo test --workspace --all-features --no-run --locked
+        run: cargo test --workspace --features solc-backend --no-run --locked
       - name: Run tests
-        run: cargo test --workspace --all-features --verbose
+        run: cargo test --workspace --features solc-backend --verbose
 
   wasm-test:
       runs-on: ubuntu-latest
@@ -179,7 +179,7 @@ jobs:
           toolchain: stable
           override: true
       - name: Build
-        run: cargo build --all-features --release && strip target/release/fe && mv target/release/fe target/release/${{ matrix.BIN_FILE }}
+        run: cargo build --features solc-backend --release && strip target/release/fe && mv target/release/fe target/release/${{ matrix.BIN_FILE }}
       - name: Release
         uses: softprops/action-gh-release@v1
         with:
diff --git a/Cargo.lock b/Cargo.lock
index e89660e8ed..20446b45c0 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -810,6 +810,15 @@ version = "1.1.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "fed34cd105917e91daa4da6b3728c47b068749d6a62c59811f06ed2ac71d9da7"
 
+[[package]]
+name = "fv"
+version = "0.15.0-alpha"
+dependencies = [
+ "fe-driver",
+ "fe-test-files",
+ "fe-yulgen",
+]
+
 [[package]]
 name = "fxhash"
 version = "0.2.1"
diff --git a/Makefile b/Makefile
index 69d12b709f..a115740f82 100644
--- a/Makefile
+++ b/Makefile
@@ -75,11 +75,11 @@ docker-wasm-test:
 
 .PHONY: coverage
 coverage:
-	cargo tarpaulin --workspace --all-features --verbose --timeout 120 --exclude-files 'tests/*' --exclude-files 'main.rs' --out xml html -- --skip differential::
+	cargo tarpaulin --workspace --features solc-backend --verbose --timeout 120 --exclude-files 'tests/*' --exclude-files 'main.rs' --out xml html -- --skip differential::
 
 .PHONY: clippy
 clippy:
-	cargo clippy --workspace --all-targets --all-features -- -D warnings -A clippy::upper-case-acronyms -A clippy::large-enum-variant -W clippy::redundant_closure_for_method_calls
+	cargo clippy --workspace --all-targets --features solc-backend -- -D warnings -A clippy::upper-case-acronyms -A clippy::large-enum-variant -W clippy::redundant_closure_for_method_calls
 
 .PHONY: rustfmt
 rustfmt:
diff --git a/crates/driver/src/lib.rs b/crates/driver/src/lib.rs
index 764bd8ea6c..1599dc85d1 100644
--- a/crates/driver/src/lib.rs
+++ b/crates/driver/src/lib.rs
@@ -30,6 +30,8 @@ pub struct CompiledContract {
     pub yul: String,
     #[cfg(feature = "solc-backend")]
     pub bytecode: String,
+    #[cfg(feature = "solc-backend")]
+    pub runtime_bytecode: String,
 }
 
 #[derive(Debug)]
@@ -128,6 +130,15 @@ fn compile_module_id(
         IndexMap::new()
     };
 
+    // compile runtimes to yul
+    let yul_contract_runtimes = fe_yulgen::compile_runtimes(db, lowered_module_id);
+
+    let _bytecode_contract_runtimes = if _with_bytecode {
+        compile_yul_runtimes(yul_contract_runtimes.iter(), _optimize)
+    } else {
+        IndexMap::new()
+    };
+
     // combine all of the named contract maps
     let contracts = json_abis
         .keys()
@@ -143,6 +154,12 @@ fn compile_module_id(
                     } else {
                         "".to_string()
                     },
+                    #[cfg(feature = "solc-backend")]
+                    runtime_bytecode: if _with_bytecode {
+                        _bytecode_contract_runtimes[name].to_owned()
+                    } else {
+                        "".to_string()
+                    },
                 },
             )
         })
@@ -185,3 +202,34 @@ fn compile_yul(
     #[cfg(not(feature = "solc-backend"))]
     IndexMap::new()
 }
+
+fn compile_yul_runtimes(
+    _contracts: impl Iterator<Item = (impl AsRef<str>, impl AsRef<str>)>,
+    _optimize: bool,
+) -> IndexMap<String, String> {
+    #[cfg(feature = "solc-backend")]
+    {
+        match fe_yulc::compile_runtimes(_contracts, _optimize) {
+            Err(error) => {
+                for error in serde_json::from_str::<Value>(&error.0)
+                    .expect("unable to deserialize json output")["errors"]
+                    .as_array()
+                    .expect("errors not an array")
+                {
+                    eprintln!(
+                        "Error: {}",
+                        error["formattedMessage"]
+                            .as_str()
+                            .expect("error value not a string")
+                            .replace("\\\n", "\n")
+                    )
+                }
+                panic!("Yul compilation failed with the above errors")
+            }
+            Ok(contracts) => contracts,
+        }
+    }
+
+    #[cfg(not(feature = "solc-backend"))]
+    IndexMap::new()
+}
diff --git a/crates/fe/src/main.rs b/crates/fe/src/main.rs
index dd33587dde..c90855b044 100644
--- a/crates/fe/src/main.rs
+++ b/crates/fe/src/main.rs
@@ -22,6 +22,7 @@ arg_enum! {
         Ast,
         LoweredAst,
         Bytecode,
+        RuntimeBytecode,
         Tokens,
         Yul,
     }
@@ -52,7 +53,15 @@ pub fn main() {
                 .short("e")
                 .long("emit")
                 .help("Comma separated compile targets e.g. -e=bytecode,yul")
-                .possible_values(&["abi", "bytecode", "ast", "tokens", "yul", "loweredAst"])
+                .possible_values(&[
+                    "abi",
+                    "bytecode",
+                    "runtimeBytecode",
+                    "ast",
+                    "tokens",
+                    "yul",
+                    "loweredAst",
+                ])
                 .default_value("abi,bytecode")
                 .use_delimiter(true)
                 .takes_value(true),
@@ -240,6 +249,15 @@ fn write_compiled_module(
             let file_name = format!("{}.bin", &name);
             write_output(&contract_output_dir.join(file_name), &contract.bytecode)?;
         }
+
+        #[cfg(feature = "solc-backend")]
+        if targets.contains(&CompilationTarget::RuntimeBytecode) {
+            let file_name = format!("{}.runtime.bin", &name);
+            write_output(
+                &contract_output_dir.join(file_name),
+                &contract.runtime_bytecode,
+            )?;
+        }
     }
 
     Ok(())
diff --git a/crates/fv/Cargo.toml b/crates/fv/Cargo.toml
new file mode 100644
index 0000000000..6f8d03e38d
--- /dev/null
+++ b/crates/fv/Cargo.toml
@@ -0,0 +1,20 @@
+[package]
+authors = ["The Fe Developers <snakecharmers@ethereum.org>"]
+categories = ["cryptography::cryptocurrencies", "command-line-utilities", "development-tools"]
+description = "Fe formal verification utilities"
+edition = "2021"
+keywords = ["ethereum", "fe", "yul", "smart", "contract", "compiler"]
+license = "GPL-3.0-or-later"
+name = "fv"
+readme = "README.md"
+repository = "https://github.com/ethereum/fe"
+version = "0.15.0-alpha"
+
+[features]
+solc-backend = ["fe-driver/solc-backend"]
+kevm-backend = []
+
+[dependencies]
+fe-driver = {path = "../driver", version = "^0.15.0-alpha"}
+fe-yulgen = {path = "../yulgen", version = "^0.15.0-alpha"}
+fe-test-files = {path = "../test-files", version = "^0.15.0-alpha"}
diff --git a/crates/fv/README.md b/crates/fv/README.md
new file mode 100644
index 0000000000..9644552d0d
--- /dev/null
+++ b/crates/fv/README.md
@@ -0,0 +1,41 @@
+# Fe Fv
+
+This crate contains utilities for building and running kevm specs.
+
+## kevm setup
+
+A system installation of [evm-semantics](https://github.com/fe-lang/evm-semantics) is required to run the specs. Please clone the repository and follow the installation directions.
+
+While in the `evm-semantics` project, `kompile` the Fe verification module:
+
+```commandline
+$ export PATH=$PATH:/path/to/evm-semantics/.build/usr/bin
+$ kevm kompile --backend haskell tests/specs/fe/verification.k                                  \
+    --directory tests/specs/fe/verification/haskell                                             \
+    --main-module VERIFICATION                                                                  \
+    --syntax-module VERIFICATION                                                                \
+    --concrete-rules-file tests/specs/fe/concrete-rules.txt                                     \
+    -I /usr/lib/kevm/include/kframework -I /usr/lib/kevm/blockchain-k-plugin/include/kframework
+```
+
+## running the proofs
+
+Once the evm-semantics project has been built, set the `KEVM_PATH` environment variable:
+
+```commandline
+$ export KEVM_PATH=/path/to/evm-semantics
+```
+
+and then run the tests: 
+
+```commandline
+$ cargo test --features "solc-backend, kevm-backend"
+```
+
+*Note: If you are working on a resource constrained device, you may not be able to run all tests simultaneously. If issues are encountered, run tests in smaller groups.*
+
+e.g.
+
+```commandline
+$ cargo test sanity_returns_42 --features "solc-backend, kevm-backend"
+```
diff --git a/crates/fv/src/lib.rs b/crates/fv/src/lib.rs
new file mode 100644
index 0000000000..128dd49bec
--- /dev/null
+++ b/crates/fv/src/lib.rs
@@ -0,0 +1,63 @@
+#![cfg(feature = "kevm-backend")]
+use fe_yulgen::Db;
+use std::path::Path;
+use std::process::Command;
+use std::{env, fs};
+
+const SPECS_DIR: &str = "tests/specs/fe/";
+
+pub fn kevm_path() -> String {
+    env::var("KEVM_PATH").expect("`KEVM_PATH` not set")
+}
+
+pub fn run_spec(name: &str, src_path: &str, src: &str, spec: &str) -> Result<(), String> {
+    let kevm_path = kevm_path();
+
+    let spec = build_spec(name, src_path, src, spec);
+    let spec_path = Path::new(&kevm_path)
+        .join(SPECS_DIR)
+        .join(name)
+        .with_extension("k");
+    fs::write(spec_path.clone(), spec).expect("unable to write file");
+
+    let path = env::var("PATH").expect("PATH is not set");
+
+    let out = Command::new("kevm")
+        .arg("prove")
+        .arg(spec_path.to_str().unwrap())
+        .arg("--backend")
+        .arg("haskell")
+        .arg("--format-failures")
+        .arg("--directory")
+        .arg("tests/specs/fe/verification/haskell")
+        .env("PATH", format!(".build/usr/bin:{}", path))
+        .current_dir(&kevm_path)
+        .output()
+        .expect("failed to execute process");
+
+    if out.status.code() != Some(0) {
+        Err(format!(
+            "{}\n{}",
+            String::from_utf8_lossy(&out.stderr),
+            String::from_utf8_lossy(&out.stdout)
+        ))
+    } else {
+        Ok(())
+    }
+}
+
+pub fn build_spec(name: &str, src_path: &str, src: &str, spec: &str) -> String {
+    let mut db = Db::default();
+    let module = fe_driver::compile_single_file(&mut db, src_path, src, true, true).unwrap();
+
+    // replace placeholders
+    let mut new_spec = spec.to_owned().replace("$TEST_NAME", &name.to_uppercase());
+    for (name, contract) in module.contracts.iter() {
+        new_spec = new_spec.replace(
+            &format!("${}::RUNTIME", name),
+            &format!("\"0x{}\"", contract.runtime_bytecode),
+        )
+    }
+
+    new_spec
+}
diff --git a/crates/fv/tests/specs.rs b/crates/fv/tests/specs.rs
new file mode 100644
index 0000000000..6190b31458
--- /dev/null
+++ b/crates/fv/tests/specs.rs
@@ -0,0 +1,68 @@
+#![cfg(feature = "kevm-backend")]
+
+/// Checks if a contract spec is valid.
+macro_rules! test_spec {
+    ($name:ident, $src_path:expr, $spec_path:expr) => {
+        #[test]
+        fn $name() {
+            let src = fe_test_files::fixture(concat!("kspecs/", $src_path));
+            let spec = fe_test_files::fixture(concat!("kspecs/", $spec_path));
+
+            if let Err(output) = fv::run_spec(
+                &stringify!($name).replace("_", "-"),
+                $src_path,
+                &src,
+                &spec
+            ) {
+                panic!("{}", output)
+            }
+        }
+    };
+}
+
+/// Checks if a contract spec is invalid.
+macro_rules! test_spec_invalid {
+    ($name:ident, $src_path:expr, $spec_path:expr) => {
+        #[test]
+        fn $name() {
+            let src = fe_test_files::fixture(concat!("kspecs/", $src_path));
+            let spec = fe_test_files::fixture(concat!("kspecs/", $spec_path));
+
+            match fv::run_spec(&stringify!($name).replace("_", "-"), $src_path, &src, &spec) {
+                Ok(()) => panic!("spec is valid"),
+                Err(output) => {
+                    // we want to make sure it didn't fail for some other reason
+                    if !output.contains("the claimed implication is not valid") {
+                        panic!("spec claim was not checked {}", output)
+                    }
+                }
+            }
+        }
+    };
+}
+
+test_spec! { sanity_returns_42, "sanity/foo.fe", "sanity/returns_42.k" }
+test_spec! { sanity_returns_in, "sanity/foo.fe", "sanity/returns_in.k" }
+test_spec! { sanity_returns_in_cond1, "sanity/foo.fe", "sanity/returns_in_cond1.k" }
+test_spec! { sanity_returns_in_cond2, "sanity/foo.fe", "sanity/returns_in_cond2.k" }
+
+// these are just for extra sanity
+test_spec_invalid! { sanity_returns_42_invalid, "sanity/foo.fe", "sanity/returns_42_invalid.k" }
+test_spec_invalid! { sanity_returns_in_invalid, "sanity/foo.fe", "sanity/returns_in_invalid.k" }
+test_spec_invalid! { sanity_returns_in_cond2_invalid, "sanity/foo.fe", "sanity/returns_in_cond2_invalid.k" }
+
+// encode/decode success
+test_spec! { abi_u256, "abi/foo.fe", "abi/u256.k" }
+test_spec! { abi_u8, "abi/foo.fe", "abi/u8.k" }
+test_spec! { abi_address, "abi/foo.fe", "abi/address.k" }
+test_spec! { abi_address_u16, "abi/foo.fe", "abi/address_u16.k" }
+
+// decode revert
+test_spec! { abi_address_revert, "abi/foo.fe", "abi/address_revert.k" }
+test_spec! { abi_address_u16_revert_0, "abi/foo.fe", "abi/address_u16_revert_0.k" }
+test_spec! { abi_address_u16_revert_1, "abi/foo.fe", "abi/address_u16_revert_1.k" }
+
+// storage
+test_spec! { store_u256, "storage/foo.fe", "storage/store_u256.k" }
+test_spec! { store_sol_map, "storage/foo.fe", "storage/store_sol_map.k" }
+test_spec! { store_fe_map, "storage/foo.fe", "storage/store_fe_map.k" }
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/crates/yulc/src/lib.rs b/crates/yulc/src/lib.rs
index a98980f85f..60e1aea5b5 100644
--- a/crates/yulc/src/lib.rs
+++ b/crates/yulc/src/lib.rs
@@ -18,6 +18,18 @@ pub fn compile(
         .collect()
 }
 
+pub fn compile_runtimes(
+    contracts: impl Iterator<Item = (impl AsRef<str>, impl AsRef<str>)>,
+    optimize: bool,
+) -> Result<IndexMap<String, String>, YulcError> {
+    contracts
+        .map(|(name, yul_src)| {
+            compile_single_contract("runtime", yul_src.as_ref(), optimize)
+                .map(|bytecode| (name.as_ref().to_string(), bytecode))
+        })
+        .collect()
+}
+
 #[cfg(feature = "solc-backend")]
 /// Compiles a single Yul contract to bytecode.
 pub fn compile_single_contract(
diff --git a/crates/yulgen/src/db.rs b/crates/yulgen/src/db.rs
index 4764d67c5e..46c2064d95 100644
--- a/crates/yulgen/src/db.rs
+++ b/crates/yulgen/src/db.rs
@@ -23,9 +23,13 @@ pub trait YulgenDb:
 {
     #[salsa::invoke(queries::compile_module)]
     fn compile_module(&self, module_id: ModuleId) -> IndexMap<String, String>;
+    #[salsa::invoke(queries::compile_module_runtimes)]
+    fn compile_module_runtimes(&self, module_id: ModuleId) -> IndexMap<String, String>;
 
     #[salsa::invoke(queries::contracts::contract_object)]
     fn contract_object(&self, contract: ContractId) -> yul::Object;
+    #[salsa::invoke(queries::contracts::contract_runtime_object)]
+    fn contract_runtime_object(&self, contract: ContractId) -> yul::Object;
     #[salsa::invoke(queries::contracts::contract_abi_dispatcher)]
     fn contract_abi_dispatcher(&self, contract: ContractId) -> Vec<yul::Statement>;
 
diff --git a/crates/yulgen/src/db/queries.rs b/crates/yulgen/src/db/queries.rs
index 887525f020..38c6a8111e 100644
--- a/crates/yulgen/src/db/queries.rs
+++ b/crates/yulgen/src/db/queries.rs
@@ -16,6 +16,13 @@ pub fn compile_module(db: &dyn YulgenDb, module: ModuleId) -> IndexMap<String, S
         .collect()
 }
 
+pub fn compile_module_runtimes(db: &dyn YulgenDb, module: ModuleId) -> IndexMap<String, String> {
+    mappers::module::module_runtimes(db, module)
+        .drain()
+        .map(|(name, object)| (name, to_safe_json(object)))
+        .collect()
+}
+
 fn to_safe_json(obj: yul::Object) -> String {
     normalize_object(obj).to_string().replace('"', "\\\"")
 }
diff --git a/crates/yulgen/src/db/queries/contracts.rs b/crates/yulgen/src/db/queries/contracts.rs
index 9a6043554d..6abdf1bf43 100644
--- a/crates/yulgen/src/db/queries/contracts.rs
+++ b/crates/yulgen/src/db/queries/contracts.rs
@@ -16,55 +16,7 @@ use yultsur::*;
 pub fn contract_object(db: &dyn YulgenDb, contract: ContractId) -> yul::Object {
     let adb = db.upcast();
 
-    let runtime_object = {
-        let (mut functions, data, objects) = build_dependency_graph(
-            db,
-            &contract.runtime_dependency_graph(adb),
-            Item::Type(TypeDef::Contract(contract)),
-        );
-
-        // This can all be replaced with a call to the contract's `__call__` function once the
-        // dispatching code has been moved into lowering.
-        //
-        // For now, we must do the following:
-        // - check if a `__call__` function has been defined in the contract and, if so, we map its
-        // body into a Yul function named `$$__call__`
-        // - if a `__call__` function is not defined in the contract, we generate a `$$__call__`
-        // function that dispatches calls using the Solidity ABI
-        // - call the `$$__call__` function
-        let call_fn_ident = identifier! { ("$$__call__") };
-        if let Some(call_fn) = contract.call_function(adb) {
-            let mut fn_context = FnContext::new(db, call_fn.body(adb));
-            let function_statements =
-                multiple_func_stmt(&mut fn_context, &call_fn.data(adb).ast.kind.body);
-            let call_fn_yul = function_definition! {
-                function [call_fn_ident.clone()]() {
-                    // the function body will contain one or more `return_val` assignments
-                    (let return_val := 0)
-                    [function_statements...]
-                }
-            };
-            functions.push(call_fn_yul);
-        } else {
-            functions.extend(db.contract_abi_dispatcher(contract));
-        }
-        functions.sort();
-        functions.dedup();
-
-        yul::Object {
-            name: identifier! { runtime },
-            code: yul::Code {
-                block: yul::Block {
-                    statements: statements! {
-                        [functions...]
-                        ([call_fn_ident]())
-                    },
-                },
-            },
-            objects,
-            data,
-        }
-    };
+    let runtime_object = db.contract_runtime_object(contract);
 
     let contract_name = contract.name(adb);
     if let Some(init_fn) = contract.init_function(adb) {
@@ -97,6 +49,58 @@ pub fn contract_object(db: &dyn YulgenDb, contract: ContractId) -> yul::Object {
     }
 }
 
+pub fn contract_runtime_object(db: &dyn YulgenDb, contract: ContractId) -> yul::Object {
+    let adb = db.upcast();
+
+    let (mut functions, data, objects) = build_dependency_graph(
+        db,
+        &contract.runtime_dependency_graph(adb),
+        Item::Type(TypeDef::Contract(contract)),
+    );
+
+    // This can all be replaced with a call to the contract's `__call__` function once the
+    // dispatching code has been moved into lowering.
+    //
+    // For now, we must do the following:
+    // - check if a `__call__` function has been defined in the contract and, if so, we map its
+    // body into a Yul function named `$$__call__`
+    // - if a `__call__` function is not defined in the contract, we generate a `$$__call__`
+    // function that dispatches calls using the Solidity ABI
+    // - call the `$$__call__` function
+    let call_fn_ident = identifier! { ("$$__call__") };
+    if let Some(call_fn) = contract.call_function(adb) {
+        let mut fn_context = FnContext::new(db, call_fn.body(adb));
+        let function_statements =
+            multiple_func_stmt(&mut fn_context, &call_fn.data(adb).ast.kind.body);
+        let call_fn_yul = function_definition! {
+            function [call_fn_ident.clone()]() {
+                // the function body will contain one or more `return_val` assignments
+                (let return_val := 0)
+                [function_statements...]
+            }
+        };
+        functions.push(call_fn_yul);
+    } else {
+        functions.extend(db.contract_abi_dispatcher(contract));
+    }
+    functions.sort();
+    functions.dedup();
+
+    yul::Object {
+        name: identifier! { runtime },
+        code: yul::Code {
+            block: yul::Block {
+                statements: statements! {
+                    [functions...]
+                    ([call_fn_ident]())
+                },
+            },
+        },
+        objects,
+        data,
+    }
+}
+
 /// Dispatch function and required encode/decode functions.
 pub fn contract_abi_dispatcher(db: &dyn YulgenDb, contract: ContractId) -> Vec<yul::Statement> {
     let adb = db.upcast();
diff --git a/crates/yulgen/src/lib.rs b/crates/yulgen/src/lib.rs
index efa3304aba..118ea3016b 100644
--- a/crates/yulgen/src/lib.rs
+++ b/crates/yulgen/src/lib.rs
@@ -27,3 +27,7 @@ mod utils;
 pub fn compile(db: &dyn YulgenDb, module: ModuleId) -> IndexMap<String, String> {
     db.compile_module(module)
 }
+
+pub fn compile_runtimes(db: &dyn YulgenDb, module: ModuleId) -> IndexMap<String, String> {
+    db.compile_module_runtimes(module)
+}
diff --git a/crates/yulgen/src/mappers/expressions.rs b/crates/yulgen/src/mappers/expressions.rs
index ebce3c5029..ca6a2096e5 100644
--- a/crates/yulgen/src/mappers/expressions.rs
+++ b/crates/yulgen/src/mappers/expressions.rs
@@ -456,5 +456,6 @@ fn expr_attribute(context: &mut FnContext, exp: &Node<fe::Expr>) -> yul::Express
 pub fn nonce_to_ptr(nonce: usize) -> yul::Expression {
     // set the last byte to `0x00` to ensure our pointer sits at the start of a word
     let ptr = keccak::partial_right_padded(nonce.to_string().as_bytes(), 31);
+    println!("{}", ptr);
     literal_expression! { (ptr) }
 }
diff --git a/crates/yulgen/src/mappers/module.rs b/crates/yulgen/src/mappers/module.rs
index 119b9e1b94..08f9a52c8d 100644
--- a/crates/yulgen/src/mappers/module.rs
+++ b/crates/yulgen/src/mappers/module.rs
@@ -21,3 +21,20 @@ pub fn module(db: &dyn YulgenDb, module: ModuleId) -> YulContracts {
             contracts
         })
 }
+
+pub fn module_runtimes(db: &dyn YulgenDb, module: ModuleId) -> YulContracts {
+    module
+        .all_contracts(db.upcast())
+        .iter()
+        .fold(YulContracts::new(), |mut contracts, id| {
+            let yul_contract = db.contract_runtime_object(*id);
+
+            if contracts
+                .insert(id.name(db.upcast()).to_string(), yul_contract)
+                .is_some()
+            {
+                panic!("duplicate contract definition");
+            }
+            contracts
+        })
+}
diff --git a/crates/yulgen/src/runtime/functions/abi.rs b/crates/yulgen/src/runtime/functions/abi.rs
index 9ad5312d99..a0f0653fac 100644
--- a/crates/yulgen/src/runtime/functions/abi.rs
+++ b/crates/yulgen/src/runtime/functions/abi.rs
@@ -409,9 +409,13 @@ pub fn decode_component_string(max_size: usize, location: AbiDecodeLocation) ->
 pub fn is_left_padded() -> yul::Statement {
     function_definition! {
         function is_left_padded(size_bits, val) -> return_val {
-            (let bits_shifted := sub(256, size_bits))
-            (let shifted_val := shr(bits_shifted, val))
-            (return_val := iszero(shifted_val))
+            (if (eq(size_bits, 0)) {
+                (return_val := 1)
+                (leave)
+            })
+
+            (let right_size := sub(256, size_bits))
+            (return_val := lt(val, (exp(2, right_size))))
         }
     }
 }
diff --git a/crates/yulgen/src/runtime/functions/data.rs b/crates/yulgen/src/runtime/functions/data.rs
index 929f88a012..fad11e11d0 100644
--- a/crates/yulgen/src/runtime/functions/data.rs
+++ b/crates/yulgen/src/runtime/functions/data.rs
@@ -33,7 +33,7 @@ pub fn all() -> Vec<yul::Statement> {
     ]
 }
 
-/// Returns the highest available pointer.
+/// Returns the highest available pointerhttps://buy.gazelle.com/collections/ipads?_=pf&pf_v_model=iPad%20Pro%2012.9%204th%20Gen.
 pub fn avail() -> yul::Statement {
     function_definition! {
         function avail() -> ptr {
@@ -315,7 +315,7 @@ pub fn bytes_sloadn() -> yul::Statement {
         function bytes_sloadn(sptr, size) -> val {
             (let word_ptr := div(sptr, 32))
             (let bytes_offset := mod(sptr, 32))
-            (val := sloadn(word_ptr, bytes_offset, size))
+            (val := sload(word_ptr))
         }
     }
 }
@@ -354,7 +354,7 @@ pub fn map_value_ptr() -> yul::Statement {
             (mstore(ptr, a))
             (mstore((add(ptr, 32)), b))
             (let hash := keccak256(ptr, 64))
-            (return_val := set_zero(248, 256, hash))
+            (return_val := mul((div(hash, 256)), 256))
         }
     }
 }
diff --git a/newsfragments/683.feature.md b/newsfragments/683.feature.md
new file mode 100644
index 0000000000..2d6b753219
--- /dev/null
+++ b/newsfragments/683.feature.md
@@ -0,0 +1,3 @@
+The `fe` binary can now emit runtime bytecode.
+
+e.g. `fe foo.fe --emit runtimeBytecode`
diff --git a/newsfragments/683.internal.md b/newsfragments/683.internal.md
new file mode 100644
index 0000000000..c748d4aca6
--- /dev/null
+++ b/newsfragments/683.internal.md
@@ -0,0 +1,3 @@
+Added an `fv` crate with several kevm spec tests. 
+
+See the README in `crates/fv` for more information.