diff --git a/CHANGELOG.md b/CHANGELOG.md
index 42c498c..66e0ae5 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -7,6 +7,31 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
 
 ## [Unreleased]
 
+## [0.9.0] - 2026-05-27
+
+**Theme: i64 T1 result-correspondence lifts against the aligned model.**
+
+v0.9.0 picks up what v0.8.0 set up. v0.8.0 (the "honest foundation") aligned
+`Compilation.v` with the real Rust codegen and shipped 26 type-only pseudo-op
+axioms + tactics + flag-correspondence lemmas. v0.9.0 layers the value-correspondence
+on top: 26 new `_spec` axioms equate every i64 pseudo-op's result to the WASM-spec
+function, then 30 existence-only (T2) i64 proofs are lifted to result-correspondence
+(T1), and the 5 strategically-`Admitted` theorems #150 carried over are discharged.
+
+**Net delta:** previously had 36 i64 theorems Qed at T2 plus 5 admits.
+Now has **30 new T1 Qeds + 5 discharged T1 Qeds = 35 i64 T1 Qeds**, with 5 honest
+admit carry-overs (Add/Sub/And/Or/Xor) whose proofs depend on missing helper
+lemmas (ADDS/ADC carry-propagation; SUBS/SBC borrow-propagation; halves-distribute
+over bitwise, blocked by Rocq 9 `Z.mod_mod`).
+
+**Falsification statement.** v0.9.0 is wrong if (a) any of the 35 newly-T1 i64
+theorems is shown to disagree with the WASM reference for a value pair the
+theorem covers (the `_spec` axioms are inconsistent with `Compilation.v`),
+(b) any of the 5 honest-Admitted carry-overs is claimed `Qed.` anywhere in the
+release artifacts, (c) `bazel test //coq:verify_proofs` goes red on a clean
+v0.9.0 checkout, or (d) any newly-added `_spec` axiom claims a result the Rust
+codegen does not actually produce (cross-checked against `docs/analysis/I64_CODEGEN_SURVEY.md`).
+
 ### Added
 
 - **i64 pseudo-op result-correspondence axioms (v0.9.0 PR 1 precursor).**
diff --git a/Cargo.toml b/Cargo.toml
index 6ed4c20..ff46bd8 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -27,7 +27,7 @@ resolver = "2"
 # semver to publish, so the convention now catches up: workspace
 # version follows the release tag, bumped pre-tag in the release
 # checklist. See docs/release-process.md.
-version = "0.8.0"
+version = "0.9.0"
 edition = "2024"
 rust-version = "1.88"
 authors = ["PulseEngine Team"]
diff --git a/MODULE.bazel b/MODULE.bazel
index 6d54d2a..b0b6d51 100644
--- a/MODULE.bazel
+++ b/MODULE.bazel
@@ -7,7 +7,7 @@ module(
     name = "synth",
     # Kept in lockstep with [workspace.package] version in Cargo.toml.
     # Both are bumped pre-tag — see docs/release-process.md.
-    version = "0.8.0",
+    version = "0.9.0",
 )
 
 # Bazel dependencies
diff --git a/crates/synth-backend-awsm/Cargo.toml b/crates/synth-backend-awsm/Cargo.toml
index e935d8e..f6d1aab 100644
--- a/crates/synth-backend-awsm/Cargo.toml
+++ b/crates/synth-backend-awsm/Cargo.toml
@@ -11,6 +11,6 @@ categories.workspace = true
 description = "aWsm backend integration for the Synth compiler"
 
 [dependencies]
-synth-core = { path = "../synth-core", version = "0.8.0" }
+synth-core = { path = "../synth-core", version = "0.9.0" }
 anyhow.workspace = true
 thiserror.workspace = true
diff --git a/crates/synth-backend-riscv/Cargo.toml b/crates/synth-backend-riscv/Cargo.toml
index c8986be..d61107f 100644
--- a/crates/synth-backend-riscv/Cargo.toml
+++ b/crates/synth-backend-riscv/Cargo.toml
@@ -11,8 +11,8 @@ categories.workspace = true
 description = "RISC-V encoder, ELF builder, PMP allocator, and bare-metal startup for synth"
 
 [dependencies]
-synth-core = { path = "../synth-core", version = "0.8.0" }
-synth-synthesis = { path = "../synth-synthesis", version = "0.8.0" }
+synth-core = { path = "../synth-core", version = "0.9.0" }
+synth-synthesis = { path = "../synth-synthesis", version = "0.9.0" }
 anyhow.workspace = true
 thiserror.workspace = true
 tracing.workspace = true
diff --git a/crates/synth-backend-wasker/Cargo.toml b/crates/synth-backend-wasker/Cargo.toml
index 18b953c..780c02e 100644
--- a/crates/synth-backend-wasker/Cargo.toml
+++ b/crates/synth-backend-wasker/Cargo.toml
@@ -11,6 +11,6 @@ categories.workspace = true
 description = "Wasker backend integration for the Synth compiler"
 
 [dependencies]
-synth-core = { path = "../synth-core", version = "0.8.0" }
+synth-core = { path = "../synth-core", version = "0.9.0" }
 anyhow.workspace = true
 thiserror.workspace = true
diff --git a/crates/synth-backend/Cargo.toml b/crates/synth-backend/Cargo.toml
index 4758a4a..56b0ada 100644
--- a/crates/synth-backend/Cargo.toml
+++ b/crates/synth-backend/Cargo.toml
@@ -15,7 +15,7 @@ default = ["arm-cortex-m"]
 arm-cortex-m = ["synth-synthesis"]
 
 [dependencies]
-synth-core = { path = "../synth-core", version = "0.8.0" }
-synth-synthesis = { path = "../synth-synthesis", version = "0.8.0", optional = true }
+synth-core = { path = "../synth-core", version = "0.9.0" }
+synth-synthesis = { path = "../synth-synthesis", version = "0.9.0", optional = true }
 anyhow.workspace = true
 thiserror.workspace = true
diff --git a/crates/synth-cli/Cargo.toml b/crates/synth-cli/Cargo.toml
index 19337d3..a9f0c33 100644
--- a/crates/synth-cli/Cargo.toml
+++ b/crates/synth-cli/Cargo.toml
@@ -27,18 +27,18 @@ verify = ["synth-verify"]
 # Path deps carry `version` so `cargo publish` rewrites them to the
 # crates.io coordinate. Bumping the workspace version requires
 # updating these in lockstep — see docs/release-process.md.
-synth-core = { path = "../synth-core", version = "0.8.0" }
-synth-frontend = { path = "../synth-frontend", version = "0.8.0" }
-synth-synthesis = { path = "../synth-synthesis", version = "0.8.0" }
-synth-backend = { path = "../synth-backend", version = "0.8.0" }
+synth-core = { path = "../synth-core", version = "0.9.0" }
+synth-frontend = { path = "../synth-frontend", version = "0.9.0" }
+synth-synthesis = { path = "../synth-synthesis", version = "0.9.0" }
+synth-backend = { path = "../synth-backend", version = "0.9.0" }
 
 # Optional external backends
-synth-backend-awsm = { path = "../synth-backend-awsm", version = "0.8.0", optional = true }
-synth-backend-wasker = { path = "../synth-backend-wasker", version = "0.8.0", optional = true }
-synth-backend-riscv = { path = "../synth-backend-riscv", version = "0.8.0", optional = true }
+synth-backend-awsm = { path = "../synth-backend-awsm", version = "0.9.0", optional = true }
+synth-backend-wasker = { path = "../synth-backend-wasker", version = "0.9.0", optional = true }
+synth-backend-riscv = { path = "../synth-backend-riscv", version = "0.9.0", optional = true }
 
 # Optional verification (requires z3)
-synth-verify = { path = "../synth-verify", version = "0.8.0", optional = true, features = ["z3-solver", "arm"] }
+synth-verify = { path = "../synth-verify", version = "0.9.0", optional = true, features = ["z3-solver", "arm"] }
 
 # Optional PulseEngine WASM optimizer
 # Uncomment when loom crate is available:
diff --git a/crates/synth-frontend/Cargo.toml b/crates/synth-frontend/Cargo.toml
index d6e36df..e1ec8b4 100644
--- a/crates/synth-frontend/Cargo.toml
+++ b/crates/synth-frontend/Cargo.toml
@@ -14,7 +14,7 @@ description = "WASM/WAT parser and module decoder frontend for the Synth compile
 # Internal path deps carry an explicit version so `cargo publish`
 # can rewrite to the crates.io coordinate. `path` is used for
 # in-workspace builds; `version` is what crates.io sees.
-synth-core = { path = "../synth-core", version = "0.8.0" }
+synth-core = { path = "../synth-core", version = "0.9.0" }
 
 wasmparser.workspace = true
 wasm-encoder.workspace = true
diff --git a/crates/synth-opt/Cargo.toml b/crates/synth-opt/Cargo.toml
index ff521bf..5f946ce 100644
--- a/crates/synth-opt/Cargo.toml
+++ b/crates/synth-opt/Cargo.toml
@@ -11,7 +11,7 @@ categories.workspace = true
 description = "Peephole optimization passes for the Synth compiler"
 
 [dependencies]
-synth-cfg = { path = "../synth-cfg", version = "0.8.0" }
+synth-cfg = { path = "../synth-cfg", version = "0.9.0" }
 
 [dev-dependencies]
 criterion = { version = "0.5", features = ["html_reports"] }
diff --git a/crates/synth-synthesis/Cargo.toml b/crates/synth-synthesis/Cargo.toml
index 868fc18..4794ba4 100644
--- a/crates/synth-synthesis/Cargo.toml
+++ b/crates/synth-synthesis/Cargo.toml
@@ -11,9 +11,9 @@ categories.workspace = true
 description = "WASM-to-ARM instruction selection and peephole optimizer"
 
 [dependencies]
-synth-core = { path = "../synth-core", version = "0.8.0" }
-synth-cfg = { path = "../synth-cfg", version = "0.8.0" }
-synth-opt = { path = "../synth-opt", version = "0.8.0" }
+synth-core = { path = "../synth-core", version = "0.9.0" }
+synth-cfg = { path = "../synth-cfg", version = "0.9.0" }
+synth-opt = { path = "../synth-opt", version = "0.9.0" }
 serde.workspace = true
 anyhow.workspace = true
 thiserror.workspace = true
diff --git a/crates/synth-verify/Cargo.toml b/crates/synth-verify/Cargo.toml
index 6f10345..8c2dd38 100644
--- a/crates/synth-verify/Cargo.toml
+++ b/crates/synth-verify/Cargo.toml
@@ -17,12 +17,12 @@ arm = ["synth-synthesis"]
 
 [dependencies]
 # Core dependencies (always required)
-synth-core = { path = "../synth-core", version = "0.8.0" }
-synth-cfg = { path = "../synth-cfg", version = "0.8.0" }
-synth-opt = { path = "../synth-opt", version = "0.8.0" }
+synth-core = { path = "../synth-core", version = "0.9.0" }
+synth-cfg = { path = "../synth-cfg", version = "0.9.0" }
+synth-opt = { path = "../synth-opt", version = "0.9.0" }
 
 # ARM synthesis (optional, behind 'arm' feature)
-synth-synthesis = { path = "../synth-synthesis", version = "0.8.0", optional = true }
+synth-synthesis = { path = "../synth-synthesis", version = "0.9.0", optional = true }
 
 # SMT solver for formal verification
 z3 = { version = "0.19", features = ["static-link-z3"], optional = true }