diff --git a/.gitignore b/.gitignore
index 9b33a2e64..1ea45490a 100644
--- a/.gitignore
+++ b/.gitignore
@@ -20,3 +20,5 @@ cobertura.xml
 
 **/test_snapshots
 .stellar/
+
+**/.certora_internal
diff --git a/Cargo.lock b/Cargo.lock
index ac416e9df..186554a06 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -1,6 +1,6 @@
 # This file is automatically @generated by Cargo.
 # It is not intended for manual editing.
-version = 3
+version = 4
 
 [[package]]
 name = "ahash"
@@ -186,6 +186,12 @@ version = "1.6.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "8c3c1a368f70d6cf7302d78f8f7093da241fb8e8807c05cc9e51a125895a6d5b"
 
+[[package]]
+name = "bitflags"
+version = "2.9.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5c8214115b7bf84099f1309324e63141d4c5d7cc26862f97a0a857dbefe165bd"
+
 [[package]]
 name = "block-buffer"
 version = "0.10.4"
@@ -228,6 +234,36 @@ dependencies = [
  "shlex",
 ]
 
+[[package]]
+name = "certora"
+version = "0.1.0"
+source = "git+https://github.com/Certora/solana-cvt.git?branch=dev-soroban#18bbc828357ce14a7ca3efdcbc804967493717af"
+dependencies = [
+ "stubs",
+]
+
+[[package]]
+name = "certora-soroban"
+version = "0.1.0"
+source = "git+https://github.com/Certora/solana-cvt.git?branch=dev-soroban#18bbc828357ce14a7ca3efdcbc804967493717af"
+dependencies = [
+ "soroban-sdk",
+]
+
+[[package]]
+name = "certora-soroban-macros"
+version = "0.1.0"
+source = "git+https://github.com/Certora/solana-cvt.git?branch=dev-soroban#18bbc828357ce14a7ca3efdcbc804967493717af"
+dependencies = [
+ "darling",
+ "proc-macro2",
+ "quote",
+ "soroban-sdk",
+ "soroban-sdk-macros",
+ "syn 2.0.87",
+ "uuid",
+]
+
 [[package]]
 name = "cfg-if"
 version = "1.0.0"
@@ -346,6 +382,126 @@ dependencies = [
  "syn 2.0.87",
 ]
 
+[[package]]
+name = "cvlr"
+version = "0.3.1"
+source = "git+https://github.com/Certora/cvlr.git#86e78c705a18efe8854a5c59fe8f94126d3d9d19"
+dependencies = [
+ "cvlr-asserts 0.3.1 (git+https://github.com/Certora/cvlr.git)",
+ "cvlr-early-panic",
+ "cvlr-hook",
+ "cvlr-log 0.3.1 (git+https://github.com/Certora/cvlr.git)",
+ "cvlr-macros",
+ "cvlr-mathint",
+ "cvlr-nondet 0.3.1 (git+https://github.com/Certora/cvlr.git)",
+]
+
+[[package]]
+name = "cvlr-asserts"
+version = "0.3.1"
+source = "git+https://github.com/1arie1/cvlr.git#86e78c705a18efe8854a5c59fe8f94126d3d9d19"
+
+[[package]]
+name = "cvlr-asserts"
+version = "0.3.1"
+source = "git+https://github.com/Certora/cvlr.git#86e78c705a18efe8854a5c59fe8f94126d3d9d19"
+
+[[package]]
+name = "cvlr-early-panic"
+version = "0.3.1"
+source = "git+https://github.com/Certora/cvlr.git#86e78c705a18efe8854a5c59fe8f94126d3d9d19"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn 2.0.87",
+]
+
+[[package]]
+name = "cvlr-hook"
+version = "0.3.1"
+source = "git+https://github.com/Certora/cvlr.git#86e78c705a18efe8854a5c59fe8f94126d3d9d19"
+dependencies = [
+ "quote",
+ "syn 2.0.87",
+]
+
+[[package]]
+name = "cvlr-log"
+version = "0.3.1"
+source = "git+https://github.com/1arie1/cvlr.git#86e78c705a18efe8854a5c59fe8f94126d3d9d19"
+
+[[package]]
+name = "cvlr-log"
+version = "0.3.1"
+source = "git+https://github.com/Certora/cvlr.git#86e78c705a18efe8854a5c59fe8f94126d3d9d19"
+dependencies = [
+ "cvlr-mathint",
+]
+
+[[package]]
+name = "cvlr-macros"
+version = "0.3.1"
+source = "git+https://github.com/Certora/cvlr.git#86e78c705a18efe8854a5c59fe8f94126d3d9d19"
+dependencies = [
+ "darling",
+ "proc-macro2",
+ "quote",
+ "syn 2.0.87",
+]
+
+[[package]]
+name = "cvlr-mathint"
+version = "0.3.1"
+source = "git+https://github.com/Certora/cvlr.git#86e78c705a18efe8854a5c59fe8f94126d3d9d19"
+dependencies = [
+ "cvlr-asserts 0.3.1 (git+https://github.com/Certora/cvlr.git)",
+ "cvlr-nondet 0.3.1 (git+https://github.com/Certora/cvlr.git)",
+]
+
+[[package]]
+name = "cvlr-nondet"
+version = "0.3.1"
+source = "git+https://github.com/1arie1/cvlr.git#86e78c705a18efe8854a5c59fe8f94126d3d9d19"
+dependencies = [
+ "cvlr-asserts 0.3.1 (git+https://github.com/1arie1/cvlr.git)",
+]
+
+[[package]]
+name = "cvlr-nondet"
+version = "0.3.1"
+source = "git+https://github.com/Certora/cvlr.git#86e78c705a18efe8854a5c59fe8f94126d3d9d19"
+dependencies = [
+ "cvlr-asserts 0.3.1 (git+https://github.com/Certora/cvlr.git)",
+]
+
+[[package]]
+name = "cvlr-soroban"
+version = "0.3.0"
+source = "git+https://github.com/Certora/cvlr-soroban.git#f4fab1b6b360159eed0a7582b35ba85b80369460"
+dependencies = [
+ "cvlr-asserts 0.3.1 (git+https://github.com/1arie1/cvlr.git)",
+ "cvlr-log 0.3.1 (git+https://github.com/1arie1/cvlr.git)",
+ "cvlr-nondet 0.3.1 (git+https://github.com/1arie1/cvlr.git)",
+ "soroban-sdk",
+]
+
+[[package]]
+name = "cvlr-soroban-derive"
+version = "0.3.0"
+source = "git+https://github.com/Certora/cvlr-soroban.git#f4fab1b6b360159eed0a7582b35ba85b80369460"
+dependencies = [
+ "darling",
+ "proc-macro2",
+ "quote",
+ "syn 2.0.87",
+ "uuid",
+]
+
+[[package]]
+name = "cvlr-soroban-macros"
+version = "0.3.0"
+source = "git+https://github.com/Certora/cvlr-soroban.git#f4fab1b6b360159eed0a7582b35ba85b80369460"
+
 [[package]]
 name = "darling"
 version = "0.20.10"
@@ -575,10 +731,22 @@ dependencies = [
  "cfg-if",
  "js-sys",
  "libc",
- "wasi",
+ "wasi 0.11.0+wasi-snapshot-preview1",
  "wasm-bindgen",
 ]
 
+[[package]]
+name = "getrandom"
+version = "0.3.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "43a49c392881ce6d5c3b8cb70f98717b7c07aabbdff06687b9030dbfbe2725f8"
+dependencies = [
+ "cfg-if",
+ "libc",
+ "wasi 0.13.3+wasi-0.2.2",
+ "windows-targets",
+]
+
 [[package]]
 name = "group"
 version = "0.13.0"
@@ -859,6 +1027,13 @@ dependencies = [
 name = "phoenix-pool"
 version = "1.1.0"
 dependencies = [
+ "certora",
+ "certora-soroban",
+ "certora-soroban-macros",
+ "cvlr",
+ "cvlr-soroban",
+ "cvlr-soroban-derive",
+ "cvlr-soroban-macros",
  "num-integer",
  "phoenix",
  "pretty_assertions",
@@ -1007,7 +1182,7 @@ version = "0.6.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "ec0be4795e2f6a28069bec0b5ff3e2ac9bafc99e6a9a7dc3547996c5c816922c"
 dependencies = [
- "getrandom",
+ "getrandom 0.2.15",
 ]
 
 [[package]]
@@ -1222,7 +1397,7 @@ dependencies = [
  "ed25519-dalek",
  "elliptic-curve",
  "generic-array",
- "getrandom",
+ "getrandom 0.2.15",
  "hex-literal",
  "hmac",
  "k256",
@@ -1346,6 +1521,13 @@ dependencies = [
 name = "soroban-token-contract"
 version = "0.0.6"
 dependencies = [
+ "certora",
+ "certora-soroban",
+ "certora-soroban-macros",
+ "cvlr",
+ "cvlr-soroban",
+ "cvlr-soroban-derive",
+ "cvlr-soroban-macros",
  "soroban-sdk",
  "soroban-token-sdk",
 ]
@@ -1427,6 +1609,11 @@ version = "0.11.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "7da8b5736845d9f2fcb837ea5d9e2628564b3b043a70948a3f0b778838c5fb4f"
 
+[[package]]
+name = "stubs"
+version = "0.1.0"
+source = "git+https://github.com/Certora/solana-cvt.git?branch=dev-soroban#18bbc828357ce14a7ca3efdcbc804967493717af"
+
 [[package]]
 name = "subtle"
 version = "2.6.1"
@@ -1551,6 +1738,15 @@ version = "1.0.12"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "3354b9ac3fae1ff6755cb6db53683adb661634f67557942dea4facebec0fee4b"
 
+[[package]]
+name = "uuid"
+version = "1.15.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e0f540e3240398cce6128b64ba83fdbdd86129c16a3aa1a3a252efd66eb3d587"
+dependencies = [
+ "getrandom 0.3.1",
+]
+
 [[package]]
 name = "version_check"
 version = "0.9.5"
@@ -1563,6 +1759,15 @@ version = "0.11.0+wasi-snapshot-preview1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "9c8d87e72b64a3b4db28d11ce29237c246188f4f51057d65a7eab63b7987e423"
 
+[[package]]
+name = "wasi"
+version = "0.13.3+wasi-0.2.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "26816d2e1a4a36a2940b96c5296ce403917633dff8f3440e9b236ed6f6bacad2"
+dependencies = [
+ "wit-bindgen-rt",
+]
+
 [[package]]
 name = "wasm-bindgen"
 version = "0.2.93"
@@ -1728,6 +1933,15 @@ version = "0.52.6"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "589f6da84c646204747d1270a2a5661ea66ed1cced2631d546fdfb155959f9ec"
 
+[[package]]
+name = "wit-bindgen-rt"
+version = "0.33.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "3268f3d866458b787f390cf61f4bbb563b922d091359f9608842999eaee3943c"
+dependencies = [
+ "bitflags",
+]
+
 [[package]]
 name = "yansi"
 version = "0.5.1"
diff --git a/Cargo.toml b/Cargo.toml
index 99103bf65..23a92c1af 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -20,6 +20,15 @@ soroban-token-sdk = "22.0.4"
 test-case = "3.3"
 pretty_assertions = "1.4.0"
 
+cvlr = {git = "https://github.com/Certora/cvlr.git",  default-features=false}
+cvlr-soroban = {git = "https://github.com/Certora/cvlr-soroban.git"}
+cvlr-soroban-derive = {git = "https://github.com/Certora/cvlr-soroban.git"}
+cvlr-soroban-macros = {git = "https://github.com/Certora/cvlr-soroban.git"}
+
+certora = {git = "https://github.com/Certora/solana-cvt.git", branch="dev-soroban", default-features=false, features=[]}
+certora-soroban = {git = "https://github.com/Certora/solana-cvt.git", branch="dev-soroban", default-features=false}
+certora-soroban-macros = {git = "https://github.com/Certora/solana-cvt.git", branch="dev-soroban", default-features=false}
+
 [profile.release]
 opt-level = "z"
 overflow-checks = true
@@ -33,3 +42,7 @@ lto = true
 [profile.release-with-logs]
 inherits = "release"
 debug-assertions = true
+
+[profile.certora]
+inherits = "release"
+strip = false
diff --git a/contracts/pool/Cargo.toml b/contracts/pool/Cargo.toml
index 3297d9555..02ac9108b 100644
--- a/contracts/pool/Cargo.toml
+++ b/contracts/pool/Cargo.toml
@@ -11,6 +11,7 @@ crate-type = ["cdylib"]
 
 [features]
 testutils = ["soroban-sdk/testutils"]
+certora = []
 
 [dependencies]
 soroban-decimal = { workspace = true }
@@ -18,6 +19,15 @@ phoenix = { workspace = true }
 num-integer = { workspace = true }
 soroban-sdk = { workspace = true }
 
+cvlr = { workspace = true }
+cvlr-soroban = { workspace = true }
+cvlr-soroban-derive = { workspace = true }
+cvlr-soroban-macros = { workspace = true }
+
+certora = { workspace = true }
+certora-soroban = { workspace = true }
+certora-soroban-macros = { workspace = true }
+
 [dev-dependencies]
 soroban-sdk = { workspace = true, features = ["testutils"] }
 pretty_assertions = { workspace = true }
diff --git a/contracts/pool/confs/setup.conf b/contracts/pool/confs/setup.conf
new file mode 100644
index 000000000..5fd05a1af
--- /dev/null
+++ b/contracts/pool/confs/setup.conf
@@ -0,0 +1,9 @@
+{
+    "files": "../../../target/wasm32-unknown-unknown/certora/phoenix_pool.wasm",
+    "process": "emv",
+    "rule": [
+        "sanity",
+        "certora_only_admin_can_update_config"
+    ],
+    "precise_bitwise_ops": true,
+}
diff --git a/contracts/pool/justfile b/contracts/pool/justfile
new file mode 100644
index 000000000..019d5f25e
--- /dev/null
+++ b/contracts/pool/justfile
@@ -0,0 +1,9 @@
+export RUSTFLAGS := "-C strip=none"
+
+target := "../../target/"
+
+build: 
+    cargo build --profile certora --target=wasm32-unknown-unknown --features certora
+
+clean:
+    rm -rf {{target}}
diff --git a/contracts/pool/src/certora/mod.rs b/contracts/pool/src/certora/mod.rs
new file mode 100644
index 000000000..cc05df3b5
--- /dev/null
+++ b/contracts/pool/src/certora/mod.rs
@@ -0,0 +1 @@
+pub mod spec;
diff --git a/contracts/pool/src/certora/spec.rs b/contracts/pool/src/certora/spec.rs
new file mode 100644
index 000000000..0efaaa9c3
--- /dev/null
+++ b/contracts/pool/src/certora/spec.rs
@@ -0,0 +1,25 @@
+use crate::storage::DataKey;
+use certora_soroban::is_auth;
+use cvlr::{asserts::cvlr_satisfy, cvlr_assume};
+use cvlr_soroban_derive::rule;
+use soroban_sdk::{Address, Env};
+
+use crate::contract::{LiquidityPool, LiquidityPoolTrait};
+
+#[rule]
+fn sanity() {
+    cvlr_satisfy!(true);
+}
+
+#[rule]
+fn certora_only_admin_can_update_config(env: Env, total_fee_bps: i64) {
+    let admin = env
+        .storage()
+        .persistent()
+        .get::<_, Address>(&DataKey::Admin)
+        .unwrap();
+
+    cvlr_assume!(is_auth(admin));
+    LiquidityPool::update_config(env, None, Some(total_fee_bps), None, None, None, None);
+    certora::satisfy!(true);
+}
diff --git a/contracts/pool/src/lib.rs b/contracts/pool/src/lib.rs
index 3984e5c63..632886fad 100644
--- a/contracts/pool/src/lib.rs
+++ b/contracts/pool/src/lib.rs
@@ -1,4 +1,5 @@
 #![no_std]
+mod certora;
 mod contract;
 mod error;
 mod storage;
diff --git a/contracts/pool/src/storage.rs b/contracts/pool/src/storage.rs
index ffda9aaa6..16cac1451 100644
--- a/contracts/pool/src/storage.rs
+++ b/contracts/pool/src/storage.rs
@@ -54,7 +54,7 @@ pub struct Config {
     /// The maximum allowed percentage (in bps) for referral fee
     pub max_referral_bps: i64,
 }
-const CONFIG: Symbol = symbol_short!("CONFIG");
+pub(crate) const CONFIG: Symbol = symbol_short!("CONFIG");
 
 const DEFAULT_SLIPPAGE_BPS: Symbol = symbol_short!("DSLIPBPS");
 pub fn save_default_slippage_bps(env: &Env, bps: i64) {
diff --git a/contracts/token/Cargo.toml b/contracts/token/Cargo.toml
index a39a67d9f..de1c74f81 100644
--- a/contracts/token/Cargo.toml
+++ b/contracts/token/Cargo.toml
@@ -7,9 +7,22 @@ edition = "2021"
 [lib]
 crate-type = ["cdylib"]
 
+[features]
+certora = []
+
 [dependencies]
 soroban-sdk = { workspace = true }
 soroban-token-sdk = { workspace = true }
 
+cvlr = { workspace = true }
+cvlr-soroban = { workspace = true }
+cvlr-soroban-derive = { workspace = true }
+cvlr-soroban-macros = { workspace = true }
+
+certora = { workspace = true }
+certora-soroban = { workspace = true }
+certora-soroban-macros = { workspace = true }
+
+
 [dev-dependencies]
 soroban-sdk = { workspace = true, features = ["testutils"] }
diff --git a/contracts/token/confs/setup.conf b/contracts/token/confs/setup.conf
new file mode 100644
index 000000000..fdf5a3c50
--- /dev/null
+++ b/contracts/token/confs/setup.conf
@@ -0,0 +1,9 @@
+{
+    "files": "../../../target/wasm32-unknown-unknown/certora/soroban_token_contract.wasm",
+    "process": "emv",
+    "rule": [
+        "sanity",
+		"transfer_is_correct"
+    ],
+    "precise_bitwise_ops": true,
+}
diff --git a/contracts/token/justfile b/contracts/token/justfile
new file mode 100644
index 000000000..7f8d77d75
--- /dev/null
+++ b/contracts/token/justfile
@@ -0,0 +1,10 @@
+
+export RUSTFLAGS := "-C strip=none"
+
+target := "../../target/"
+
+build: 
+    cargo build --profile certora --target=wasm32-unknown-unknown --features certora
+
+clean:
+    rm -rf {{target}}
diff --git a/contracts/token/src/certora/mod.rs b/contracts/token/src/certora/mod.rs
new file mode 100644
index 000000000..cc05df3b5
--- /dev/null
+++ b/contracts/token/src/certora/mod.rs
@@ -0,0 +1 @@
+pub mod spec;
diff --git a/contracts/token/src/certora/spec.rs b/contracts/token/src/certora/spec.rs
new file mode 100644
index 000000000..0133e8156
--- /dev/null
+++ b/contracts/token/src/certora/spec.rs
@@ -0,0 +1,29 @@
+use soroban_sdk::{Address, Env};
+
+use crate::contract::Token;
+use soroban_sdk::token::TokenInterface;
+
+use cvlr::asserts::{cvlr_assert, cvlr_assume, cvlr_satisfy};
+use cvlr_soroban_derive::rule;
+
+#[rule]
+fn sanity(e: Env, addr: Address) {
+    let _ = Token::balance(e, addr);
+    cvlr_satisfy!(true);
+}
+
+#[rule]
+fn transfer_is_correct(e: Env, to: Address, from: Address, amount: i128) {
+    cvlr_assume!(
+        e.storage().persistent().has(&from) && e.storage().persistent().has(&to) && to != from
+    );
+    let balance_from_before = Token::balance(e.clone(), from.clone());
+    let balance_to_before = Token::balance(e.clone(), to.clone());
+    Token::transfer(e.clone(), from.clone(), to.clone(), amount);
+    let balance_from_after = Token::balance(e.clone(), from.clone());
+    let balance_to_after = Token::balance(e.clone(), to.clone());
+    cvlr_assert!(
+        (balance_to_after == balance_to_before + amount)
+            && (balance_from_after == balance_from_before - amount)
+    );
+}
diff --git a/contracts/token/src/lib.rs b/contracts/token/src/lib.rs
index b5f04e4dc..4ed76a202 100644
--- a/contracts/token/src/lib.rs
+++ b/contracts/token/src/lib.rs
@@ -3,6 +3,7 @@
 mod admin;
 mod allowance;
 mod balance;
+mod certora;
 mod contract;
 mod metadata;
 mod storage_types;