diff --git a/Strata/Languages/Core/DDMTransform/FormatCore.lean b/Strata/Languages/Core/DDMTransform/FormatCore.lean
index 6015bb1832..d4c54ea6c9 100644
--- a/Strata/Languages/Core/DDMTransform/FormatCore.lean
+++ b/Strata/Languages/Core/DDMTransform/FormatCore.lean
@@ -281,6 +281,7 @@ def lconstToExpr {M} [Inhabited M] (c : Lambda.LConst) :
   | .bitvecConst 16 n => pure (.bv16Lit default ⟨default, n.toNat⟩)
   | .bitvecConst 32 n => pure (.bv32Lit default ⟨default, n.toNat⟩)
   | .bitvecConst 64 n => pure (.bv64Lit default ⟨default, n.toNat⟩)
+  | .bitvecConst 128 n => pure (.bv128Lit default ⟨default, n.toNat⟩)
   | .bitvecConst w _ => do
     ToCSTM.logError "lconstToExpr" "unsupported bitvec width" (toString w)
     pure (.bv64Lit default ⟨default, w⟩)
diff --git a/Strata/Languages/Core/DDMTransform/Translate.lean b/Strata/Languages/Core/DDMTransform/Translate.lean
index f46dd95cc3..1f8ddc798d 100644
--- a/Strata/Languages/Core/DDMTransform/Translate.lean
+++ b/Strata/Languages/Core/DDMTransform/Translate.lean
@@ -860,6 +860,9 @@ partial def translateExpr (p : Program) (bindings : TransBindings) (arg : Arg) :
   | .fn _ q`Core.bv64Lit, [xa] =>
     let n ← translateBitVec 64 xa
     return .bitvecConst () 64 n
+  | .fn _ q`Core.bv128Lit, [xa] =>
+    let n ← translateBitVec 128 xa
+    return .bitvecConst () 128 n
   | .fn _ q`Core.strLit, [xa] =>
     let x ← translateStr xa
     return .strConst () x