diff --git a/kore/kore.cabal b/kore/kore.cabal
index 45d3f06813..7f56d23b14 100644
--- a/kore/kore.cabal
+++ b/kore/kore.cabal
@@ -268,6 +268,8 @@ library
     Kore.Builtin.Endianness.Endianness
     Kore.Builtin.EqTerm
     Kore.Builtin.Error
+    Kore.Builtin.Float
+    Kore.Builtin.Float.Float
     Kore.Builtin.Inj
     Kore.Builtin.Int
     Kore.Builtin.Int.Int
@@ -316,6 +318,7 @@ library
     Kore.Internal.Inj
     Kore.Internal.InternalBool
     Kore.Internal.InternalBytes
+    Kore.Internal.InternalFloat
     Kore.Internal.InternalInt
     Kore.Internal.InternalList
     Kore.Internal.InternalMap
@@ -473,6 +476,7 @@ library
     Kore.Simplify.InjSimplifier
     Kore.Simplify.InternalBool
     Kore.Simplify.InternalBytes
+    Kore.Simplify.InternalFloat
     Kore.Simplify.InternalInt
     Kore.Simplify.InternalList
     Kore.Simplify.InternalMap
@@ -697,6 +701,7 @@ test-suite kore-test
     Test.Kore.Builtin.Encoding
     Test.Kore.Builtin.Endianness
     Test.Kore.Builtin.External
+    Test.Kore.Builtin.Float
     Test.Kore.Builtin.Inj
     Test.Kore.Builtin.Int
     Test.Kore.Builtin.InternalBytes
diff --git a/kore/src/Kore/Builtin.hs b/kore/src/Kore/Builtin.hs
index 293e2100fc..f699f48dca 100644
--- a/kore/src/Kore/Builtin.hs
+++ b/kore/src/Kore/Builtin.hs
@@ -38,6 +38,7 @@ import Kore.Attribute.Symbol qualified as Attribute
 import Kore.Builtin.Bool qualified as Bool
 import Kore.Builtin.Builtin qualified as Builtin
 import Kore.Builtin.Endianness qualified as Endianness
+import Kore.Builtin.Float qualified as Float
 import Kore.Builtin.IO qualified as IO
 import Kore.Builtin.Inj qualified as Inj
 import Kore.Builtin.Int qualified as Int
@@ -68,6 +69,7 @@ koreVerifiers =
     mempty
         <> Bool.verifiers
         <> Endianness.verifiers
+        <> Float.verifiers
         <> Inj.verifiers
         <> Int.verifiers
         <> InternalBytes.verifiers
@@ -92,6 +94,7 @@ koreEvaluators :: Text -> Maybe BuiltinAndAxiomSimplifier
 koreEvaluators key =
     asum
         [ Bool.builtinFunctions key
+        , Float.builtinFunctions key
         , Int.builtinFunctions key
         , IO.builtinFunctions key
         , KEqual.builtinFunctions key
diff --git a/kore/src/Kore/Builtin/Float.hs b/kore/src/Kore/Builtin/Float.hs
new file mode 100644
index 0000000000..51a4ff29c0
--- /dev/null
+++ b/kore/src/Kore/Builtin/Float.hs
@@ -0,0 +1,507 @@
+{- |
+Module      : Kore.Builtin.Float
+Description : Built-in IEEE floating-point sort
+Copyright   : (c) Runtime Verification, 2026
+License     : BSD-3-Clause
+-}
+module Kore.Builtin.Float (
+    sort,
+    assertSort,
+    verifiers,
+    builtinFunctions,
+    extractFloatDomainValue,
+    asInternal,
+    asPattern,
+    asPartialPattern,
+    parseText,
+    unifyFloat,
+    matchFloat,
+    matchUnifyFloatEq,
+
+    -- * keys
+    precisionKey,
+    exponentBitsKey,
+    exponentKey,
+    signKey,
+    isNaNKey,
+    negKey,
+    addKey,
+    subKey,
+    mulKey,
+    divKey,
+    remKey,
+    absKey,
+    ceilKey,
+    floorKey,
+    truncKey,
+    roundKey,
+    minKey,
+    maxKey,
+    eqKey,
+    ltKey,
+    leKey,
+    gtKey,
+    geKey,
+    maxValueKey,
+    minValueKey,
+    int2FloatKey,
+    float2IntKey,
+    float2StringKey,
+    string2FloatKey,
+) where
+
+import Data.Functor.Const
+import Data.HashMap.Strict qualified as HashMap
+import Data.Text (
+    Text,
+ )
+import Data.Text qualified as Text
+import GHC.Float (
+    castDoubleToWord64,
+    castFloatToWord32,
+    castWord32ToFloat,
+    castWord64ToDouble,
+ )
+import Kore.Builtin.Bool qualified as Bool
+import Kore.Builtin.Builtin (
+    UnifyEq (..),
+ )
+import Kore.Builtin.Builtin qualified as Builtin
+import Kore.Builtin.Float.Float
+import Kore.Builtin.Int qualified as Int
+import Kore.Builtin.String qualified as String
+import Kore.Error qualified
+import Kore.Internal.InternalFloat
+import Kore.Internal.InternalString
+import Kore.Internal.Pattern (
+    Pattern,
+ )
+import Kore.Internal.Pattern qualified as Pattern
+import Kore.Internal.TermLike as TermLike
+import Kore.Log.DebugUnifyBottom (
+    debugUnifyBottomAndReturnBottom,
+ )
+import Kore.Rewrite.RewritingVariable (
+    RewritingVariableName,
+ )
+import Kore.Simplify.Simplify (
+    BuiltinAndAxiomSimplifier,
+ )
+import Kore.Unification.Unify as Unify
+import Prelude.Kore
+
+assertSort :: Builtin.SortVerifier
+assertSort = Builtin.verifySort sort
+
+verifiers :: Builtin.Verifiers
+verifiers =
+    Builtin.Verifiers
+        { sortDeclVerifiers
+        , symbolVerifiers
+        , patternVerifierHook
+        }
+
+sortDeclVerifiers :: Builtin.SortDeclVerifiers
+sortDeclVerifiers = HashMap.fromList [(sort, Builtin.verifySortDecl)]
+
+symbolVerifiers :: Builtin.SymbolVerifiers
+symbolVerifiers =
+    HashMap.fromList
+        [ (precisionKey, Builtin.verifySymbol Int.assertSort [assertSort])
+        , (exponentBitsKey, Builtin.verifySymbol Int.assertSort [assertSort])
+        , (exponentKey, Builtin.verifySymbol Int.assertSort [assertSort])
+        , (signKey, Builtin.verifySymbol Bool.assertSort [assertSort])
+        , (isNaNKey, Builtin.verifySymbol Bool.assertSort [assertSort])
+        , (negKey, Builtin.verifySymbol assertSort [assertSort])
+        , (addKey, Builtin.verifySymbol assertSort [assertSort, assertSort])
+        , (subKey, Builtin.verifySymbol assertSort [assertSort, assertSort])
+        , (mulKey, Builtin.verifySymbol assertSort [assertSort, assertSort])
+        , (divKey, Builtin.verifySymbol assertSort [assertSort, assertSort])
+        , (remKey, Builtin.verifySymbol assertSort [assertSort, assertSort])
+        , (absKey, Builtin.verifySymbol assertSort [assertSort])
+        , (ceilKey, Builtin.verifySymbol assertSort [assertSort])
+        , (floorKey, Builtin.verifySymbol assertSort [assertSort])
+        , (truncKey, Builtin.verifySymbol assertSort [assertSort])
+        ,
+            ( roundKey
+            , Builtin.verifySymbol assertSort [assertSort, Int.assertSort, Int.assertSort]
+            )
+        , (minKey, Builtin.verifySymbol assertSort [assertSort, assertSort])
+        , (maxKey, Builtin.verifySymbol assertSort [assertSort, assertSort])
+        , (eqKey, Builtin.verifySymbol Bool.assertSort [assertSort, assertSort])
+        , (ltKey, Builtin.verifySymbol Bool.assertSort [assertSort, assertSort])
+        , (leKey, Builtin.verifySymbol Bool.assertSort [assertSort, assertSort])
+        , (gtKey, Builtin.verifySymbol Bool.assertSort [assertSort, assertSort])
+        , (geKey, Builtin.verifySymbol Bool.assertSort [assertSort, assertSort])
+        ,
+            ( maxValueKey
+            , Builtin.verifySymbol assertSort [Int.assertSort, Int.assertSort]
+            )
+        ,
+            ( minValueKey
+            , Builtin.verifySymbol assertSort [Int.assertSort, Int.assertSort]
+            )
+        ,
+            ( int2FloatKey
+            , Builtin.verifySymbol assertSort [Int.assertSort, Int.assertSort, Int.assertSort]
+            )
+        , (float2IntKey, Builtin.verifySymbol Int.assertSort [assertSort])
+        , (float2StringKey, Builtin.verifySymbol String.assertSort [assertSort])
+        , (string2FloatKey, Builtin.verifySymbol assertSort [String.assertSort])
+        ]
+
+patternVerifierHook :: Builtin.PatternVerifierHook
+patternVerifierHook =
+    Builtin.domainValuePatternVerifierHook sort patternVerifierWorker
+  where
+    patternVerifierWorker external =
+        case externalChild of
+            StringLiteral_ literal ->
+                case parseText literal of
+                    Just internalFloatValue ->
+                        (return . InternalFloatF . Const)
+                            InternalFloat
+                                { internalFloatSort
+                                , internalFloatValue
+                                }
+                    Nothing ->
+                        Kore.Error.koreFail "Expected IEEE float literal"
+            _ -> Kore.Error.koreFail "Expected literal string"
+      where
+        DomainValue{domainValueSort = internalFloatSort} = external
+        DomainValue{domainValueChild = externalChild} = external
+
+extractFloatDomainValue ::
+    Text ->
+    TermLike variable ->
+    Maybe FloatValue
+extractFloatDomainValue _ = \case
+    InternalFloat_ InternalFloat{internalFloatValue} -> Just internalFloatValue
+    _ -> Nothing
+
+builtinFunctions :: Text -> Maybe BuiltinAndAxiomSimplifier
+builtinFunctions key
+    | key == precisionKey =
+        Just $
+            Builtin.unaryOperator
+                extractFloatDomainValue
+                Int.asPattern
+                precisionKey
+                precisionValue
+    | key == exponentBitsKey =
+        Just $
+            Builtin.unaryOperator
+                extractFloatDomainValue
+                Int.asPattern
+                exponentBitsKey
+                exponentBitsValue
+    | key == exponentKey =
+        Just $
+            Builtin.unaryOperator
+                extractFloatDomainValue
+                Int.asPattern
+                exponentKey
+                exponentValue
+    | key == signKey =
+        Just $
+            Builtin.unaryOperator
+                extractFloatDomainValue
+                Bool.asPattern
+                signKey
+                signValue
+    | key == isNaNKey =
+        Just $
+            Builtin.unaryOperator
+                extractFloatDomainValue
+                Bool.asPattern
+                isNaNKey
+                isNaNValue
+    | key == negKey = Just $ unaryFloatOperator negKey negate negate
+    | key == addKey = Just $ binaryFloatOperator addKey (+) (+)
+    | key == subKey = Just $ binaryFloatOperator subKey (-) (-)
+    | key == mulKey = Just $ binaryFloatOperator mulKey (*) (*)
+    | key == divKey = Just $ binaryFloatOperator divKey (/) (/)
+    | key == remKey = Just evalRem
+    | key == absKey = Just $ unaryFloatOperator absKey abs abs
+    | key == ceilKey = Just evalCeil
+    | key == floorKey = Just evalFloor
+    | key == truncKey = Just evalTrunc
+    | key == roundKey = Just evalRound
+    | key == minKey = Just evalMin
+    | key == maxKey = Just evalMax
+    | key == eqKey = Just $ comparator eqKey (==) (==)
+    | key == ltKey = Just $ comparator ltKey (<) (<)
+    | key == leKey = Just $ comparator leKey (<=) (<=)
+    | key == gtKey = Just $ comparator gtKey (>) (>)
+    | key == geKey = Just $ comparator geKey (>=) (>=)
+    | key == maxValueKey = Just evalMaxValue
+    | key == minValueKey = Just evalMinValue
+    | key == int2FloatKey = Just evalInt2Float
+    | key == float2IntKey = Just evalFloat2Int
+    | key == float2StringKey = Just evalFloat2String
+    | key == string2FloatKey = Just evalString2Float
+    | otherwise = Nothing
+  where
+    unaryFloatOperator name onFloat onDouble =
+        Builtin.unaryOperator
+            extractFloatDomainValue
+            asPattern
+            name
+            (unarySameFormat onFloat onDouble)
+
+    comparator name onFloat onDouble =
+        Builtin.binaryOperator
+            extractFloatDomainValue
+            asPartialBoolPattern
+            name
+            (binaryCompareSameFormat onFloat onDouble)
+
+    binaryFloatOperator name onFloat onDouble =
+        Builtin.binaryOperator
+            extractFloatDomainValue
+            asPartialPattern
+            name
+            (binarySameFormat onFloat onDouble)
+
+    evalRem = Builtin.functionEvaluator evalRem0
+    evalRem0 _ resultSort children =
+        case children of
+            [extractFloatDomainValue remKey -> Just first, extractFloatDomainValue remKey -> Just second] ->
+                pure . asPartialPattern resultSort $ evalRemainder first second
+            [_, _] -> empty
+            _ -> Builtin.wrongArity (Text.unpack remKey)
+
+    evalCeil = Builtin.functionEvaluator evalCeil0
+    evalCeil0 _ resultSort children =
+        case children of
+            [extractFloatDomainValue ceilKey -> Just value] ->
+                pure . asPattern resultSort $ integralUnary ceilInteger value
+            [_] -> empty
+            _ -> Builtin.wrongArity (Text.unpack ceilKey)
+
+    evalFloor = Builtin.functionEvaluator evalFloor0
+    evalFloor0 _ resultSort children =
+        case children of
+            [extractFloatDomainValue floorKey -> Just value] ->
+                pure . asPattern resultSort $ integralUnary floorInteger value
+            [_] -> empty
+            _ -> Builtin.wrongArity (Text.unpack floorKey)
+
+    evalTrunc = Builtin.functionEvaluator evalTrunc0
+    evalTrunc0 _ resultSort children =
+        case children of
+            [extractFloatDomainValue truncKey -> Just value] ->
+                pure . asPattern resultSort $ integralUnary truncateInteger value
+            [_] -> empty
+            _ -> Builtin.wrongArity (Text.unpack truncKey)
+
+    evalRound = Builtin.functionEvaluator evalRound0
+    evalRound0 _ resultSort children =
+        case children of
+            [ extractFloatDomainValue roundKey -> Just value
+                , Int.extractIntDomainValue roundKey -> Just precisionBits'
+                , Int.extractIntDomainValue roundKey -> Just exponentBits'
+                ] ->
+                    pure . asPartialPattern resultSort $
+                        do
+                            format <- formatFromBits precisionBits' exponentBits'
+                            pure (convertFormat format value)
+            [_, _, _] -> empty
+            _ -> Builtin.wrongArity (Text.unpack roundKey)
+
+    evalMin = Builtin.functionEvaluator evalMin0
+    evalMin0 _ resultSort children =
+        case children of
+            [extractFloatDomainValue minKey -> Just first, extractFloatDomainValue minKey -> Just second] ->
+                pure . asPartialPattern resultSort $ minFloat first second
+            [_, _] -> empty
+            _ -> Builtin.wrongArity (Text.unpack minKey)
+
+    evalMax = Builtin.functionEvaluator evalMax0
+    evalMax0 _ resultSort children =
+        case children of
+            [extractFloatDomainValue maxKey -> Just first, extractFloatDomainValue maxKey -> Just second] ->
+                pure . asPartialPattern resultSort $ maxFloat first second
+            [_, _] -> empty
+            _ -> Builtin.wrongArity (Text.unpack maxKey)
+
+    evalMaxValue = Builtin.functionEvaluator evalMaxValue0
+    evalMaxValue0 _ resultSort children =
+        case children of
+            [ Int.extractIntDomainValue maxValueKey -> Just precisionBits'
+                , Int.extractIntDomainValue maxValueKey -> Just exponentBits'
+                ] ->
+                    pure . asPartialPattern resultSort $
+                        maxValueForFormat <$> formatFromBits precisionBits' exponentBits'
+            [_, _] -> empty
+            _ -> Builtin.wrongArity (Text.unpack maxValueKey)
+
+    evalMinValue = Builtin.functionEvaluator evalMinValue0
+    evalMinValue0 _ resultSort children =
+        case children of
+            [ Int.extractIntDomainValue minValueKey -> Just precisionBits'
+                , Int.extractIntDomainValue minValueKey -> Just exponentBits'
+                ] ->
+                    pure . asPartialPattern resultSort $
+                        minValueForFormat <$> formatFromBits precisionBits' exponentBits'
+            [_, _] -> empty
+            _ -> Builtin.wrongArity (Text.unpack minValueKey)
+
+    evalInt2Float = Builtin.functionEvaluator evalInt2Float0
+    evalInt2Float0 _ resultSort children =
+        case children of
+            [ Int.extractIntDomainValue int2FloatKey -> Just integerValue
+                , Int.extractIntDomainValue int2FloatKey -> Just precisionBits'
+                , Int.extractIntDomainValue int2FloatKey -> Just exponentBits'
+                ] ->
+                    pure . asPartialPattern resultSort $
+                        integerToFormat <$> formatFromBits precisionBits' exponentBits' <*> pure integerValue
+            [_, _, _] -> empty
+            _ -> Builtin.wrongArity (Text.unpack int2FloatKey)
+
+    evalFloat2Int = Builtin.functionEvaluator evalFloat2Int0
+    evalFloat2Int0 _ resultSort children =
+        case children of
+            [extractFloatDomainValue float2IntKey -> Just value] ->
+                pure . Int.asPartialPattern resultSort $ floatToInteger value
+            [_] -> empty
+            _ -> Builtin.wrongArity (Text.unpack float2IntKey)
+
+    evalFloat2String = Builtin.functionEvaluator evalFloat2String0
+    evalFloat2String0 _ resultSort children =
+        case children of
+            [extractFloatDomainValue float2StringKey -> Just value] ->
+                pure . String.asPattern resultSort $ renderFloatValue value
+            [_] -> empty
+            _ -> Builtin.wrongArity (Text.unpack float2StringKey)
+
+    evalString2Float = Builtin.functionEvaluator evalString2Float0
+    evalString2Float0 _ resultSort children =
+        case children of
+            [extractStringDomainValue string2FloatKey -> Just input] ->
+                pure . asPartialPattern resultSort $ parseText input
+            [_] -> empty
+            _ -> Builtin.wrongArity (Text.unpack string2FloatKey)
+
+    integralUnary ::
+        (forall b. RealFrac b => b -> Integer) ->
+        FloatValue ->
+        FloatValue
+    integralUnary rounder = \case
+        Float32 wordValue ->
+            let value = castWord32ToFloat wordValue
+             in if isNaN value || isInfinite value
+                    then Float32 wordValue
+                    else integerToFormat Binary32 (rounder value)
+        Float64 wordValue ->
+            let value = castWord64ToDouble wordValue
+             in if isNaN value || isInfinite value
+                    then Float64 wordValue
+                    else integerToFormat Binary64 (rounder value)
+
+    evalRemainder first second =
+        case (first, second) of
+            (Float32 word1, Float32 word2) ->
+                pure . Float32 . castFloatToWord32 $
+                    remainderLike (castWord32ToFloat word1) (castWord32ToFloat word2)
+            (Float64 word1, Float64 word2) ->
+                pure . Float64 . castDoubleToWord64 $
+                    remainderLike (castWord64ToDouble word1) (castWord64ToDouble word2)
+            _ -> Nothing
+
+    remainderLike ::
+        forall a.
+        RealFloat a =>
+        a ->
+        a ->
+        a
+    remainderLike numerator denominator
+        | isNaN numerator || isNaN denominator = 0 / 0
+        | isInfinite numerator = 0 / 0
+        | denominator == 0 = 0 / 0
+        | isInfinite denominator = numerator
+        | otherwise =
+            let quotient = numerator / denominator
+                nearestInteger = fromInteger (round quotient)
+             in numerator - nearestInteger * denominator
+
+    minFloat first second
+        | isNaNValue first || isNaNValue second = Nothing
+        | otherwise =
+            case binaryCompareSameFormat compareMin compareMin first second of
+                Just True -> Just first
+                Just False -> Just second
+                Nothing -> Nothing
+      where
+        compareMin x y = x < y
+
+    maxFloat first second
+        | isNaNValue first || isNaNValue second = Nothing
+        | otherwise =
+            case binaryCompareSameFormat compareMax compareMax first second of
+                Just True -> Just first
+                Just False -> Just second
+                Nothing -> Nothing
+      where
+        compareMax x y = x > y
+
+data UnifyFloat = UnifyFloat
+    { float1, float2 :: !InternalFloat
+    , term1, term2 :: !(TermLike RewritingVariableName)
+    }
+
+matchFloat ::
+    TermLike RewritingVariableName ->
+    TermLike RewritingVariableName ->
+    Maybe UnifyFloat
+matchFloat term1 term2
+    | InternalFloat_ float1 <- term1
+    , InternalFloat_ float2 <- term2 =
+        Just UnifyFloat{float1, float2, term1, term2}
+    | otherwise = Nothing
+
+unifyFloat ::
+    forall unifier.
+    MonadUnify unifier =>
+    UnifyFloat ->
+    unifier (Pattern RewritingVariableName)
+unifyFloat unifyData =
+    assert (on (==) internalFloatSort float1 float2) worker
+  where
+    worker
+        | on (==) internalFloatValue float1 float2 =
+            pure (Pattern.fromTermLike term1)
+        | otherwise =
+            debugUnifyBottomAndReturnBottom "distinct floating-point values" term1 term2
+    UnifyFloat{float1, float2, term1, term2} = unifyData
+
+matchUnifyFloatEq ::
+    TermLike RewritingVariableName ->
+    TermLike RewritingVariableName ->
+    Maybe UnifyEq
+matchUnifyFloatEq = Builtin.matchUnifyEq eqKey
+
+asPartialBoolPattern ::
+    InternalVariable variable =>
+    Sort ->
+    Maybe Bool ->
+    Pattern variable
+asPartialBoolPattern resultSort =
+    maybe (Pattern.bottomOf resultSort) (Bool.asPattern resultSort)
+
+extractStringDomainValue ::
+    Text ->
+    TermLike variable ->
+    Maybe Text
+extractStringDomainValue _ = \case
+    TermLike.InternalString_ InternalString{internalStringValue} -> Just internalStringValue
+    _ -> Nothing
+
+ceilInteger :: RealFrac a => a -> Integer
+ceilInteger = ceiling
+
+floorInteger :: RealFrac a => a -> Integer
+floorInteger = floor
+
+truncateInteger :: RealFrac a => a -> Integer
+truncateInteger = truncate
diff --git a/kore/src/Kore/Builtin/Float/Float.hs b/kore/src/Kore/Builtin/Float/Float.hs
new file mode 100644
index 0000000000..4cc484def1
--- /dev/null
+++ b/kore/src/Kore/Builtin/Float/Float.hs
@@ -0,0 +1,352 @@
+{- |
+Copyright   : (c) Runtime Verification, 2026
+License     : BSD-3-Clause
+-}
+module Kore.Builtin.Float.Float (
+    FloatFormat (..),
+    sort,
+    asBuiltin,
+    asInternal,
+    asPattern,
+    asPartialPattern,
+    parseText,
+    convertFormat,
+    formatFromBits,
+    precisionValue,
+    exponentBitsValue,
+    exponentValue,
+    signValue,
+    isNaNValue,
+    unarySameFormat,
+    binarySameFormat,
+    binaryCompareSameFormat,
+    minValueForFormat,
+    maxValueForFormat,
+    floatToInteger,
+    integerToFormat,
+    roundToIntegral,
+
+    -- * Keys
+    precisionKey,
+    exponentBitsKey,
+    exponentKey,
+    signKey,
+    isNaNKey,
+    negKey,
+    addKey,
+    subKey,
+    mulKey,
+    divKey,
+    remKey,
+    absKey,
+    ceilKey,
+    floorKey,
+    truncKey,
+    roundKey,
+    minKey,
+    maxKey,
+    eqKey,
+    ltKey,
+    leKey,
+    gtKey,
+    geKey,
+    maxValueKey,
+    minValueKey,
+    int2FloatKey,
+    float2IntKey,
+    float2StringKey,
+    string2FloatKey,
+) where
+
+import Control.Monad (
+    guard,
+ )
+import Data.Bits (
+    shiftR,
+    (.&.),
+ )
+import Data.Char qualified as Char
+import Data.String (
+    IsString,
+ )
+import Data.Text (
+    Text,
+ )
+import Data.Text qualified as Text
+import GHC.Float (
+    castDoubleToWord64,
+    castFloatToWord32,
+    castWord32ToFloat,
+    castWord64ToDouble,
+ )
+import Kore.Internal.InternalFloat
+import Kore.Internal.Pattern (
+    Pattern,
+ )
+import Kore.Internal.Pattern qualified as Pattern
+import Kore.Internal.TermLike as TermLike
+import Prelude.Kore
+import Text.Read (
+    readMaybe,
+ )
+
+data FloatFormat = Binary32 | Binary64
+    deriving stock (Eq, Ord, Show)
+
+sort :: Text
+sort = "FLOAT.Float"
+
+asBuiltin :: Sort -> FloatValue -> InternalFloat
+asBuiltin = InternalFloat
+
+asInternal ::
+    Sort ->
+    FloatValue ->
+    TermLike variable
+asInternal internalFloatSort internalFloatValue =
+    TermLike.fromConcrete . mkInternalFloat $
+        asBuiltin internalFloatSort internalFloatValue
+
+asPattern ::
+    InternalVariable variable =>
+    Sort ->
+    FloatValue ->
+    Pattern variable
+asPattern resultSort =
+    Pattern.fromTermLike . asInternal resultSort
+
+asPartialPattern ::
+    InternalVariable variable =>
+    Sort ->
+    Maybe FloatValue ->
+    Pattern variable
+asPartialPattern resultSort =
+    maybe (Pattern.bottomOf resultSort) (asPattern resultSort)
+
+formatOf :: FloatValue -> FloatFormat
+formatOf = \case
+    Float32 _ -> Binary32
+    Float64 _ -> Binary64
+
+formatFromBits :: Integer -> Integer -> Maybe FloatFormat
+formatFromBits precisionBits' exponentBits'
+    | (precisionBits', exponentBits') == (24, 8) = Just Binary32
+    | (precisionBits', exponentBits') == (53, 11) = Just Binary64
+    | otherwise = Nothing
+
+precisionValue :: FloatValue -> Integer
+precisionValue = precisionBits
+
+exponentBitsValue :: FloatValue -> Integer
+exponentBitsValue = exponentBits
+
+exponentValue :: FloatValue -> Integer
+exponentValue = \case
+    Float32 wordValue -> toInteger ((wordValue `shiftR` 23) .&. 0xff)
+    Float64 wordValue -> toInteger ((wordValue `shiftR` 52) .&. 0x7ff)
+
+signValue :: FloatValue -> Bool
+signValue = \case
+    Float32 wordValue -> ((wordValue `shiftR` 31) .&. 0x1) == 1
+    Float64 wordValue -> ((wordValue `shiftR` 63) .&. 0x1) == 1
+
+isNaNValue :: FloatValue -> Bool
+isNaNValue = \case
+    Float32 wordValue -> isNaN (castWord32ToFloat wordValue)
+    Float64 wordValue -> isNaN (castWord64ToDouble wordValue)
+
+maxValueForFormat :: FloatFormat -> FloatValue
+maxValueForFormat = \case
+    Binary32 -> Float32 0x7f7fffff
+    Binary64 -> Float64 0x7fefffffffffffff
+
+minValueForFormat :: FloatFormat -> FloatValue
+minValueForFormat = \case
+    Binary32 -> Float32 0x00000001
+    Binary64 -> Float64 0x0000000000000001
+
+integerToFormat :: FloatFormat -> Integer -> FloatValue
+integerToFormat = \case
+    Binary32 -> Float32 . castFloatToWord32 . fromInteger
+    Binary64 -> Float64 . castDoubleToWord64 . fromInteger
+
+floatToInteger :: FloatValue -> Maybe Integer
+floatToInteger = \case
+    Float32 wordValue ->
+        let value = castWord32ToFloat wordValue
+         in if isNaN value || isInfinite value
+                then Nothing
+                else Just (round value)
+    Float64 wordValue ->
+        let value = castWord64ToDouble wordValue
+         in if isNaN value || isInfinite value
+                then Nothing
+                else Just (round value)
+
+roundToIntegral :: FloatValue -> FloatValue
+roundToIntegral = \case
+    Float32 wordValue ->
+        let value = castWord32ToFloat wordValue
+         in if isNaN value || isInfinite value
+                then Float32 wordValue
+                else Float32 (castFloatToWord32 (fromInteger (round value)))
+    Float64 wordValue ->
+        let value = castWord64ToDouble wordValue
+         in if isNaN value || isInfinite value
+                then Float64 wordValue
+                else Float64 (castDoubleToWord64 (fromInteger (round value)))
+
+convertFormat :: FloatFormat -> FloatValue -> FloatValue
+convertFormat target value
+    | target == formatOf value = value
+convertFormat Binary32 (Float64 wordValue) =
+    Float32 (castFloatToWord32 (realToFrac (castWord64ToDouble wordValue)))
+convertFormat Binary64 (Float32 wordValue) =
+    Float64 (castDoubleToWord64 (realToFrac (castWord32ToFloat wordValue)))
+convertFormat Binary32 (Float32 wordValue) = Float32 wordValue
+convertFormat Binary64 (Float64 wordValue) = Float64 wordValue
+
+unarySameFormat ::
+    (Float -> Float) ->
+    (Double -> Double) ->
+    FloatValue ->
+    FloatValue
+unarySameFormat onFloat onDouble = \case
+    Float32 wordValue ->
+        Float32 (castFloatToWord32 (onFloat (castWord32ToFloat wordValue)))
+    Float64 wordValue ->
+        Float64 (castDoubleToWord64 (onDouble (castWord64ToDouble wordValue)))
+
+binarySameFormat ::
+    (Float -> Float -> Float) ->
+    (Double -> Double -> Double) ->
+    FloatValue ->
+    FloatValue ->
+    Maybe FloatValue
+binarySameFormat onFloat onDouble first second =
+    case (first, second) of
+        (Float32 word1, Float32 word2) ->
+            Just . Float32 $
+                castFloatToWord32
+                    (onFloat (castWord32ToFloat word1) (castWord32ToFloat word2))
+        (Float64 word1, Float64 word2) ->
+            Just . Float64 $
+                castDoubleToWord64
+                    (onDouble (castWord64ToDouble word1) (castWord64ToDouble word2))
+        _ -> Nothing
+
+binaryCompareSameFormat ::
+    (Float -> Float -> Bool) ->
+    (Double -> Double -> Bool) ->
+    FloatValue ->
+    FloatValue ->
+    Maybe Bool
+binaryCompareSameFormat onFloat onDouble first second =
+    case (first, second) of
+        (Float32 word1, Float32 word2) ->
+            Just (onFloat (castWord32ToFloat word1) (castWord32ToFloat word2))
+        (Float64 word1, Float64 word2) ->
+            Just (onDouble (castWord64ToDouble word1) (castWord64ToDouble word2))
+        _ -> Nothing
+
+parseText :: Text -> Maybe FloatValue
+parseText input = do
+    case parseExactBits input of
+        Just exact -> Just exact
+        Nothing -> do
+            (body, format) <- parseFormat input
+            case format of
+                Binary32 ->
+                    Float32 . castFloatToWord32 <$> readMaybe (Text.unpack body)
+                Binary64 ->
+                    Float64 . castDoubleToWord64 <$> readMaybe (Text.unpack body)
+
+parseExactBits :: Text -> Maybe FloatValue
+parseExactBits input =
+    parseBits "bits32(" Float32 input
+        <|> parseBits "bits64(" Float64 input
+  where
+    parseBits ::
+        Read word =>
+        Text ->
+        (word -> FloatValue) ->
+        Text ->
+        Maybe FloatValue
+    parseBits prefix wrap text = do
+        body <- Text.stripPrefix prefix text
+        digits <- Text.stripSuffix ")" body
+        wrap <$> readMaybe (Text.unpack digits)
+
+parseFormat :: Text -> Maybe (Text, FloatFormat)
+parseFormat input =
+    case Text.unsnoc input of
+        Just (body, suffix)
+            | suffix == 'f' || suffix == 'F' -> Just (body, Binary32)
+            | suffix == 'd' || suffix == 'D' -> Just (body, Binary64)
+        _ ->
+            case parseExplicitFormat input of
+                Just explicit -> Just explicit
+                Nothing -> Just (input, Binary64)
+
+parseExplicitFormat :: Text -> Maybe (Text, FloatFormat)
+parseExplicitFormat input = do
+    let (rest1, expBitsText) = splitTrailingDigits input
+    (rest2, xChar) <- Text.unsnoc rest1
+    guard (xChar == 'x' || xChar == 'X')
+    guard (not (Text.null expBitsText))
+    let (rest3, precisionText) = splitTrailingDigits rest2
+    (body, pChar) <- Text.unsnoc rest3
+    guard (pChar == 'p' || pChar == 'P')
+    guard (not (Text.null precisionText))
+    precisionBits' <- readMaybe (Text.unpack precisionText)
+    exponentBits' <- readMaybe (Text.unpack expBitsText)
+    format <- formatFromBits precisionBits' exponentBits'
+    pure (body, format)
+  where
+    splitTrailingDigits text =
+        let reversed = Text.reverse text
+            trailingDigitsReversed = Text.takeWhile Char.isDigit reversed
+            trailingDigits = Text.reverse trailingDigitsReversed
+            prefix = Text.dropEnd (Text.length trailingDigits) text
+         in (prefix, trailingDigits)
+
+precisionKey, exponentBitsKey, exponentKey, signKey, isNaNKey :: IsString s => s
+precisionKey = "FLOAT.precision"
+exponentBitsKey = "FLOAT.exponentBits"
+exponentKey = "FLOAT.exponent"
+signKey = "FLOAT.sign"
+isNaNKey = "FLOAT.isNaN"
+
+negKey, addKey, subKey, mulKey, divKey, remKey :: IsString s => s
+negKey = "FLOAT.neg"
+addKey = "FLOAT.add"
+subKey = "FLOAT.sub"
+mulKey = "FLOAT.mul"
+divKey = "FLOAT.div"
+remKey = "FLOAT.rem"
+
+absKey, ceilKey, floorKey, truncKey, roundKey, minKey, maxKey :: IsString s => s
+absKey = "FLOAT.abs"
+ceilKey = "FLOAT.ceil"
+floorKey = "FLOAT.floor"
+truncKey = "FLOAT.trunc"
+roundKey = "FLOAT.round"
+minKey = "FLOAT.min"
+maxKey = "FLOAT.max"
+
+eqKey, ltKey, leKey, gtKey, geKey :: IsString s => s
+eqKey = "FLOAT.eq"
+ltKey = "FLOAT.lt"
+leKey = "FLOAT.le"
+gtKey = "FLOAT.gt"
+geKey = "FLOAT.ge"
+
+maxValueKey, minValueKey, int2FloatKey, float2IntKey :: IsString s => s
+maxValueKey = "FLOAT.maxValue"
+minValueKey = "FLOAT.minValue"
+int2FloatKey = "FLOAT.int2float"
+float2IntKey = "FLOAT.float2int"
+
+float2StringKey, string2FloatKey :: IsString s => s
+float2StringKey = "STRING.float2string"
+string2FloatKey = "STRING.string2float"
diff --git a/kore/src/Kore/Internal/InternalFloat.hs b/kore/src/Kore/Internal/InternalFloat.hs
new file mode 100644
index 0000000000..5502b6fe6a
--- /dev/null
+++ b/kore/src/Kore/Internal/InternalFloat.hs
@@ -0,0 +1,133 @@
+{- |
+Copyright   : (c) Runtime Verification, 2026
+License     : BSD-3-Clause
+-}
+module Kore.Internal.InternalFloat (
+    FloatValue (..),
+    InternalFloat (..),
+    precisionBits,
+    exponentBits,
+    renderExactFloatValue,
+    renderFloatValue,
+) where
+
+import Data.Functor.Const
+import Data.Text (
+    Text,
+ )
+import Data.Text qualified as Text
+import Data.Word (
+    Word32,
+    Word64,
+ )
+import GHC.Float (
+    castWord32ToFloat,
+    castWord64ToDouble,
+ )
+import GHC.Generics qualified as GHC
+import Generics.SOP qualified as SOP
+import Kore.Attribute.Pattern.ConstructorLike
+import Kore.Attribute.Pattern.Defined
+import Kore.Attribute.Pattern.FreeVariables
+import Kore.Attribute.Pattern.Function
+import Kore.Attribute.Pattern.Simplified
+import Kore.Attribute.Pattern.Total
+import Kore.Attribute.Synthetic
+import Kore.Debug
+import Kore.Sort
+import Kore.Unparser
+import Numeric (
+    showGFloat,
+ )
+import Prelude.Kore
+import Pretty qualified
+
+data FloatValue
+    = Float32 !Word32
+    | Float64 !Word64
+    deriving stock (Eq, Ord, Show)
+    deriving stock (GHC.Generic)
+    deriving anyclass (Hashable, NFData)
+    deriving anyclass (SOP.Generic, SOP.HasDatatypeInfo)
+    deriving anyclass (Debug, Diff)
+
+precisionBits :: FloatValue -> Integer
+precisionBits = \case
+    Float32 _ -> 24
+    Float64 _ -> 53
+
+exponentBits :: FloatValue -> Integer
+exponentBits = \case
+    Float32 _ -> 8
+    Float64 _ -> 11
+
+renderFloatValue :: FloatValue -> Text
+renderFloatValue = \case
+    value | isNaNValue value -> renderExactFloatValue value
+    Float32 value ->
+        prettyRealFloat (castWord32ToFloat value) <> "f"
+    Float64 value ->
+        prettyRealFloat (castWord64ToDouble value)
+  where
+    prettyRealFloat :: RealFloat a => a -> Text
+    prettyRealFloat value = Text.pack (showGFloat Nothing value "")
+
+    isNaNValue = \case
+        Float32 value -> isNaN (castWord32ToFloat value)
+        Float64 value -> isNaN (castWord64ToDouble value)
+
+renderExactFloatValue :: FloatValue -> Text
+renderExactFloatValue = \case
+    Float32 value -> "bits32(" <> showDecimal value <> ")"
+    Float64 value -> "bits64(" <> showDecimal value <> ")"
+  where
+    showDecimal :: Show a => a -> Text
+    showDecimal = Text.pack . show
+
+-- | Internal representation of the builtin @FLOAT.Float@ domain.
+data InternalFloat = InternalFloat
+    { internalFloatSort :: !Sort
+    , internalFloatValue :: !FloatValue
+    }
+    deriving stock (Eq, Ord, Show)
+    deriving stock (GHC.Generic)
+    deriving anyclass (Hashable, NFData)
+    deriving anyclass (SOP.Generic, SOP.HasDatatypeInfo)
+    deriving anyclass (Debug, Diff)
+
+instance Unparse InternalFloat where
+    unparse InternalFloat{internalFloatSort, internalFloatValue} =
+        "\\dv"
+            <> parameters [internalFloatSort]
+            <> Pretty.parens (Pretty.dquotes $ Pretty.pretty $ renderFloatValue internalFloatValue)
+
+    unparse2 InternalFloat{internalFloatSort, internalFloatValue} =
+        "\\dv2"
+            <> parameters2 [internalFloatSort]
+            <> arguments' [Pretty.dquotes $ Pretty.pretty $ renderFloatValue internalFloatValue]
+
+instance Synthetic Sort (Const InternalFloat) where
+    synthetic (Const InternalFloat{internalFloatSort}) = internalFloatSort
+
+instance Synthetic (FreeVariables variable) (Const InternalFloat) where
+    synthetic _ = emptyFreeVariables
+
+instance Synthetic ConstructorLike (Const InternalFloat) where
+    synthetic = const (ConstructorLike . Just $ ConstructorLikeHead)
+    {-# INLINE synthetic #-}
+
+instance Synthetic Defined (Const InternalFloat) where
+    synthetic = alwaysDefined
+    {-# INLINE synthetic #-}
+
+instance Synthetic Function (Const InternalFloat) where
+    synthetic = alwaysFunction
+    {-# INLINE synthetic #-}
+
+instance Synthetic Total (Const InternalFloat) where
+    synthetic = alwaysTotal
+    {-# INLINE synthetic #-}
+
+instance Synthetic Simplified (Const InternalFloat) where
+    synthetic = alwaysSimplified
+    {-# INLINE synthetic #-}
diff --git a/kore/src/Kore/Internal/Key.hs b/kore/src/Kore/Internal/Key.hs
index 7a74285e48..53a16c69df 100644
--- a/kore/src/Kore/Internal/Key.hs
+++ b/kore/src/Kore/Internal/Key.hs
@@ -31,6 +31,7 @@ import Kore.Internal.Inj (
  )
 import Kore.Internal.InternalBool
 import Kore.Internal.InternalBytes
+import Kore.Internal.InternalFloat
 import Kore.Internal.InternalInt
 import Kore.Internal.InternalList
 import Kore.Internal.InternalMap
@@ -156,6 +157,10 @@ instance From InternalString Key where
     from = synthesize . from
     {-# INLINE from #-}
 
+instance From InternalFloat Key where
+    from = synthesize . from
+    {-# INLINE from #-}
+
 -- | The base functor of 'Key'; the branching structure of the syntax tree.
 data KeyF child
     = ApplySymbolF !(Application Symbol child)
@@ -169,6 +174,7 @@ data KeyF child
     | InternalSetF !(InternalSet Key child)
     | InternalStringF !(Const InternalString child)
     | StringLiteralF !(Const StringLiteral child)
+    | InternalFloatF !(Const InternalFloat child)
     deriving stock (Eq, Ord, Show)
     deriving stock (Foldable, Functor, Traversable)
     deriving stock (GHC.Generic)
@@ -191,6 +197,7 @@ instance Synthetic Sort KeyF where
         DomainValueF domainValue -> synthetic domainValue
         InternalBoolF internalBool -> synthetic internalBool
         InternalBytesF internalBytes -> synthetic internalBytes
+        InternalFloatF internalFloat -> synthetic internalFloat
         InternalIntF internalInt -> synthetic internalInt
         InternalListF internalList -> synthetic internalList
         InternalMapF internalMap -> synthetic internalMap
@@ -206,6 +213,10 @@ instance From InternalBytes (KeyF child) where
     from = InternalBytesF . Const
     {-# INLINE from #-}
 
+instance From InternalFloat (KeyF child) where
+    from = InternalFloatF . Const
+    {-# INLINE from #-}
+
 instance From InternalInt (KeyF child) where
     from = InternalIntF . Const
     {-# INLINE from #-}
diff --git a/kore/src/Kore/Internal/SideCondition.hs b/kore/src/Kore/Internal/SideCondition.hs
index 9653f28f51..43ac920d4c 100644
--- a/kore/src/Kore/Internal/SideCondition.hs
+++ b/kore/src/Kore/Internal/SideCondition.hs
@@ -117,6 +117,7 @@ import Kore.Internal.TermLike (
     pattern Inj_,
     pattern InternalBool_,
     pattern InternalBytes_,
+    pattern InternalFloat_,
     pattern InternalInt_,
     pattern InternalList_,
     pattern InternalMap_,
@@ -714,6 +715,7 @@ retractLocalFunction =
                 Inj_ _ -> Just (Pair term1 term2)
                 InternalInt_ _ -> Just (Pair term1 term2)
                 InternalBytes_ _ _ -> Just (Pair term1 term2)
+                InternalFloat_ _ -> Just (Pair term1 term2)
                 InternalString_ _ -> Just (Pair term1 term2)
                 InternalBool_ _ -> Just (Pair term1 term2)
                 InternalList_ _ -> Just (Pair term1 term2)
@@ -1068,6 +1070,8 @@ cacheSimplifiedFunctions =
                 foldMap extractSimplifiedFunctions bool
             TermLike.InternalBytesF bytes ->
                 foldMap extractSimplifiedFunctions bytes
+            TermLike.InternalFloatF float ->
+                foldMap extractSimplifiedFunctions float
             TermLike.InternalIntF int ->
                 foldMap extractSimplifiedFunctions int
             TermLike.InternalStringF string ->
diff --git a/kore/src/Kore/Internal/TermLike.hs b/kore/src/Kore/Internal/TermLike.hs
index d59436b942..963e6c5774 100644
--- a/kore/src/Kore/Internal/TermLike.hs
+++ b/kore/src/Kore/Internal/TermLike.hs
@@ -58,6 +58,7 @@ module Kore.Internal.TermLike (
     mkInternalBytes,
     mkInternalBytes',
     mkInternalBool,
+    mkInternalFloat,
     mkInternalInt,
     mkInternalString,
     mkInternalList,
@@ -114,6 +115,7 @@ module Kore.Internal.TermLike (
     pattern Bottom_,
     pattern InternalBytes_,
     pattern InternalBool_,
+    pattern InternalFloat_,
     pattern InternalInt_,
     pattern InternalList_,
     pattern InternalMap_,
@@ -236,6 +238,7 @@ import Kore.Internal.Alias
 import Kore.Internal.Inj
 import Kore.Internal.InternalBool
 import Kore.Internal.InternalBytes
+import Kore.Internal.InternalFloat
 import Kore.Internal.InternalInt
 import Kore.Internal.InternalList
 import Kore.Internal.InternalMap
@@ -336,6 +339,7 @@ hasConstructorLikeTop = \case
     App_ symbol _ -> Symbol.isConstructor symbol
     DV_ _ _ -> True
     InternalBool_ _ -> True
+    InternalFloat_ _ -> True
     InternalInt_ _ -> True
     InternalList_ _ -> True
     InternalMap_ _ -> True
@@ -475,6 +479,8 @@ forgetSimplifiedIgnorePredicates term@(Recursive.project -> (_ :< termF)) =
             Recursive.embed (newAttrs :< StringLiteralF (recursiveCall stringLiteral))
         InternalBoolF internalBool ->
             Recursive.embed (newAttrs :< InternalBoolF (recursiveCall internalBool))
+        InternalFloatF internalFloat ->
+            Recursive.embed (newAttrs :< InternalFloatF (recursiveCall internalFloat))
         InternalIntF internalInt ->
             Recursive.embed (newAttrs :< InternalIntF (recursiveCall internalInt))
         InternalBytesF internalBytes ->
@@ -757,6 +763,7 @@ forceSortPredicate
             ApplyAliasF _ -> illSorted forcedSort original
             InternalBoolF _ -> illSorted forcedSort original
             InternalBytesF _ -> illSorted forcedSort original
+            InternalFloatF _ -> illSorted forcedSort original
             InternalIntF _ -> illSorted forcedSort original
             InternalStringF _ -> illSorted forcedSort original
             InternalListF _ -> illSorted forcedSort original
@@ -1034,6 +1041,14 @@ mkInternalInt ::
     TermLike variable
 mkInternalInt = updateCallStack . synthesize . InternalIntF . Const
 
+-- | Construct an internal float pattern.
+mkInternalFloat ::
+    HasCallStack =>
+    InternalVariable variable =>
+    InternalFloat ->
+    TermLike variable
+mkInternalFloat = updateCallStack . synthesize . InternalFloatF . Const
+
 -- | Construct an internal string pattern.
 mkInternalString ::
     HasCallStack =>
@@ -1497,6 +1512,10 @@ pattern InternalBool_ ::
     InternalBool ->
     TermLike variable
 
+pattern InternalFloat_ ::
+    InternalFloat ->
+    TermLike variable
+
 pattern InternalInt_ ::
     InternalInt ->
     TermLike variable
@@ -1653,6 +1672,9 @@ pattern DV_ domainValueSort domainValueChild <-
 pattern InternalBool_ internalBool <-
     (Recursive.project -> _ :< InternalBoolF (Const internalBool))
 
+pattern InternalFloat_ internalFloat <-
+    (Recursive.project -> _ :< InternalFloatF (Const internalFloat))
+
 pattern InternalInt_ internalInt <-
     (Recursive.project -> _ :< InternalIntF (Const internalInt))
 
diff --git a/kore/src/Kore/Internal/TermLike/TermLike.hs b/kore/src/Kore/Internal/TermLike/TermLike.hs
index f0df3916b4..f8eca21135 100644
--- a/kore/src/Kore/Internal/TermLike/TermLike.hs
+++ b/kore/src/Kore/Internal/TermLike/TermLike.hs
@@ -97,6 +97,7 @@ import Kore.Internal.Inj
 import Kore.Internal.Inj qualified as Inj
 import Kore.Internal.InternalBool
 import Kore.Internal.InternalBytes
+import Kore.Internal.InternalFloat
 import Kore.Internal.InternalInt
 import Kore.Internal.InternalList
 import Kore.Internal.InternalMap
@@ -186,6 +187,7 @@ data TermLikeF variable child
     | StringLiteralF !(Const StringLiteral child)
     | InternalBoolF !(Const InternalBool child)
     | InternalBytesF !(Const InternalBytes child)
+    | InternalFloatF !(Const InternalFloat child)
     | InternalIntF !(Const InternalInt child)
     | InternalStringF !(Const InternalString child)
     | InternalListF !(InternalList child)
@@ -236,6 +238,7 @@ instance
             StringLiteralF stringLiteral -> synthetic stringLiteral
             InternalBoolF internalBool -> synthetic internalBool
             InternalBytesF internalBytes -> synthetic internalBytes
+            InternalFloatF internalFloat -> synthetic internalFloat
             InternalIntF internalInt -> synthetic internalInt
             InternalStringF internalString -> synthetic internalString
             InternalListF internalList -> synthetic internalList
@@ -273,6 +276,7 @@ instance Synthetic Sort (TermLikeF variable) where
             StringLiteralF stringLiteral -> synthetic stringLiteral
             InternalBoolF internalBool -> synthetic internalBool
             InternalBytesF internalBytes -> synthetic internalBytes
+            InternalFloatF internalFloat -> synthetic internalFloat
             InternalIntF internalInt -> synthetic internalInt
             InternalStringF internalString -> synthetic internalString
             InternalListF internalList -> synthetic internalList
@@ -310,6 +314,7 @@ instance Synthetic Attribute.Total (TermLikeF variable) where
             StringLiteralF stringLiteral -> synthetic stringLiteral
             InternalBoolF internalBool -> synthetic internalBool
             InternalBytesF internalBytes -> synthetic internalBytes
+            InternalFloatF internalFloat -> synthetic internalFloat
             InternalIntF internalInt -> synthetic internalInt
             InternalStringF internalString -> synthetic internalString
             InternalListF internalList -> synthetic internalList
@@ -347,6 +352,7 @@ instance Synthetic Attribute.Function (TermLikeF variable) where
             StringLiteralF stringLiteral -> synthetic stringLiteral
             InternalBoolF internalBool -> synthetic internalBool
             InternalBytesF internalBytes -> synthetic internalBytes
+            InternalFloatF internalFloat -> synthetic internalFloat
             InternalIntF internalInt -> synthetic internalInt
             InternalStringF internalString -> synthetic internalString
             InternalListF internalList -> synthetic internalList
@@ -384,6 +390,7 @@ instance Synthetic Attribute.Defined (TermLikeF variable) where
             StringLiteralF stringLiteral -> synthetic stringLiteral
             InternalBoolF internalBool -> synthetic internalBool
             InternalBytesF internalBytes -> synthetic internalBytes
+            InternalFloatF internalFloat -> synthetic internalFloat
             InternalIntF internalInt -> synthetic internalInt
             InternalStringF internalString -> synthetic internalString
             InternalListF internalList -> synthetic internalList
@@ -421,6 +428,7 @@ instance Synthetic Attribute.Simplified (TermLikeF variable) where
             StringLiteralF stringLiteral -> synthetic stringLiteral
             InternalBoolF internalBool -> synthetic internalBool
             InternalBytesF internalBytes -> synthetic internalBytes
+            InternalFloatF internalFloat -> synthetic internalFloat
             InternalIntF internalInt -> synthetic internalInt
             InternalStringF internalString -> synthetic internalString
             InternalListF internalList -> synthetic internalList
@@ -458,6 +466,7 @@ instance Synthetic Attribute.ConstructorLike (TermLikeF variable) where
             StringLiteralF stringLiteral -> synthetic stringLiteral
             InternalBoolF internalBool -> synthetic internalBool
             InternalBytesF internalBytes -> synthetic internalBytes
+            InternalFloatF internalFloat -> synthetic internalFloat
             InternalIntF internalInt -> synthetic internalInt
             InternalStringF internalString -> synthetic internalString
             InternalListF internalList -> synthetic internalList
@@ -474,6 +483,7 @@ instance From (KeyF child) (TermLikeF variable child) where
     from (Key.DomainValueF domainValue) = DomainValueF domainValue
     from (Key.InternalBoolF internalBool) = InternalBoolF internalBool
     from (Key.InternalIntF internalInt) = InternalIntF internalInt
+    from (Key.InternalFloatF internalFloat) = InternalFloatF internalFloat
     from (Key.InternalStringF internalString) = InternalStringF internalString
     from (Key.InternalSetF internalSet) = InternalSetF internalSet
     from (Key.InternalMapF internalMap) = InternalMapF internalMap
@@ -961,6 +971,8 @@ retractKey =
                     sequence (Key.InternalBoolF internalBool)
                 InternalBytesF internalBytes ->
                     sequence (Key.InternalBytesF internalBytes)
+                InternalFloatF internalFloat ->
+                    sequence (Key.InternalFloatF internalFloat)
                 InternalIntF internalInt ->
                     sequence (Key.InternalIntF internalInt)
                 InternalStringF internalString ->
@@ -1026,6 +1038,8 @@ instance
                 locationFromAst internalBoolSort
             InternalBytesF (Const InternalBytes{internalBytesSort}) ->
                 locationFromAst internalBytesSort
+            InternalFloatF (Const InternalFloat{internalFloatSort}) ->
+                locationFromAst internalFloatSort
             InternalIntF (Const InternalInt{internalIntSort}) ->
                 locationFromAst internalIntSort
             InternalStringF (Const InternalString{internalStringSort}) ->
@@ -1077,6 +1091,7 @@ traverseVariablesF adj =
         StringLiteralF strP -> pure (StringLiteralF strP)
         InternalBoolF boolP -> pure (InternalBoolF boolP)
         InternalBytesF bytesP -> pure (InternalBytesF bytesP)
+        InternalFloatF floatP -> pure (InternalFloatF floatP)
         InternalIntF intP -> pure (InternalIntF intP)
         InternalStringF stringP -> pure (InternalStringF stringP)
         InternalListF listP -> pure (InternalListF listP)
@@ -1288,6 +1303,9 @@ uninternalize = Pattern.Pattern . Recursive.cata go
             uninternalizeInternalValue bytesSort $
                 Encoding.decode8Bit $
                     ByteString.fromShort bytesValue
+        InternalFloatF (Const (InternalFloat floatSort floatValue)) ->
+            uninternalizeInternalValue floatSort $
+                renderFloatValue floatValue
         InternalIntF (Const (InternalInt intSort intValue)) ->
             uninternalizeInternalValue intSort $
                 Text.pack $
diff --git a/kore/src/Kore/Simplify/AndTerms.hs b/kore/src/Kore/Simplify/AndTerms.hs
index ef340ea3a8..31a8c92241 100644
--- a/kore/src/Kore/Simplify/AndTerms.hs
+++ b/kore/src/Kore/Simplify/AndTerms.hs
@@ -28,6 +28,7 @@ import Data.Text (
 import Kore.Builtin.Bool qualified as Builtin.Bool
 import Kore.Builtin.Builtin qualified as Builtin
 import Kore.Builtin.Endianness qualified as Builtin.Endianness
+import Kore.Builtin.Float qualified as Builtin.Float
 import Kore.Builtin.Int qualified as Builtin.Int
 import Kore.Builtin.InternalBytes (
     matchBytes,
@@ -152,6 +153,8 @@ maybeTermEquals childTransformers first second = do
     worker injSimplifier overloadSimplifier tools
         | Just unifyData <- Builtin.Int.matchInt first second =
             lift $ Builtin.Int.unifyInt unifyData
+        | Just unifyData <- Builtin.Float.matchFloat first second =
+            lift $ Builtin.Float.unifyFloat unifyData
         | Just unifyData <- Builtin.Bool.matchBools first second =
             lift $ Builtin.Bool.unifyBool unifyData
         | Just unifyData <- Builtin.String.matchString first second =
@@ -190,6 +193,8 @@ maybeTermEquals childTransformers first second = do
             lift $ Builtin.Bool.unifyBoolNot childTransformers boolNotData
         | Just unifyData <- Builtin.Int.matchUnifyIntEq first second =
             lift $ Builtin.unifyEq childTransformers unifyData
+        | Just unifyData <- Builtin.Float.matchUnifyFloatEq first second =
+            lift $ Builtin.unifyEq childTransformers unifyData
         | Just unifyData <- Builtin.String.matchUnifyStringEq first second =
             lift $ Builtin.unifyEq childTransformers unifyData
         | Just unifyData <- Builtin.KEqual.matchUnifyKequalsEq first second =
@@ -244,6 +249,8 @@ maybeTermAnd childTransformers first second = do
             lift $ boolAnd unifyData
         | Just unifyData <- Builtin.Int.matchInt first second =
             lift $ Builtin.Int.unifyInt unifyData
+        | Just unifyData <- Builtin.Float.matchFloat first second =
+            lift $ Builtin.Float.unifyFloat unifyData
         | Just unifyData <- Builtin.Bool.matchBools first second =
             lift $ Builtin.Bool.unifyBool unifyData
         | Just unifyData <- Builtin.String.matchString first second =
diff --git a/kore/src/Kore/Simplify/Ceil.hs b/kore/src/Kore/Simplify/Ceil.hs
index fcba75c0d2..b328f08e30 100644
--- a/kore/src/Kore/Simplify/Ceil.hs
+++ b/kore/src/Kore/Simplify/Ceil.hs
@@ -352,6 +352,7 @@ makeSimplifiedCeil
             StringLiteralF _ -> unexpectedError
             InternalBoolF _ -> unexpectedError
             InternalBytesF _ -> unexpectedError
+            InternalFloatF _ -> unexpectedError
             InternalIntF _ -> unexpectedError
             InternalListF _ -> True
             InternalMapF _ -> True
@@ -411,6 +412,7 @@ enumerateSubtermsNeedingCeil
             StringLiteralF _ -> unexpectedError
             InternalBoolF _ -> unexpectedError
             InternalBytesF _ -> unexpectedError
+            InternalFloatF _ -> unexpectedError
             InternalIntF _ -> unexpectedError
             InternalListF _ -> True
             InternalMapF _ -> True
diff --git a/kore/src/Kore/Simplify/InternalFloat.hs b/kore/src/Kore/Simplify/InternalFloat.hs
new file mode 100644
index 0000000000..e7286cddde
--- /dev/null
+++ b/kore/src/Kore/Simplify/InternalFloat.hs
@@ -0,0 +1,23 @@
+{- |
+Copyright   : (c) Runtime Verification, 2026
+License     : BSD-3-Clause
+-}
+module Kore.Simplify.InternalFloat (
+    simplify,
+) where
+
+import Kore.Internal.InternalFloat
+import Kore.Internal.OrPattern (
+    OrPattern,
+ )
+import Kore.Internal.OrPattern qualified as OrPattern
+import Kore.Internal.TermLike
+import Kore.Rewrite.RewritingVariable (
+    RewritingVariableName,
+ )
+import Prelude.Kore
+
+simplify ::
+    InternalFloat ->
+    OrPattern RewritingVariableName
+simplify = OrPattern.fromPattern . pure . mkInternalFloat
diff --git a/kore/src/Kore/Simplify/TermLike.hs b/kore/src/Kore/Simplify/TermLike.hs
index 19eb02ee7d..ee5c5cdb60 100644
--- a/kore/src/Kore/Simplify/TermLike.hs
+++ b/kore/src/Kore/Simplify/TermLike.hs
@@ -68,6 +68,9 @@ import Kore.Simplify.InternalBool qualified as InternalBool (
 import Kore.Simplify.InternalBytes qualified as InternalBytes (
     simplify,
  )
+import Kore.Simplify.InternalFloat qualified as InternalFloat (
+    simplify,
+ )
 import Kore.Simplify.InternalInt qualified as InternalInt (
     simplify,
  )
@@ -184,6 +187,9 @@ simplify sideCondition =
                 InternalBytesF internalBytesF ->
                     InternalBytes.simplify (getConst internalBytesF)
                         & return
+                InternalFloatF internalFloatF ->
+                    InternalFloat.simplify (getConst internalFloatF)
+                        & return
                 InternalIntF internalIntF ->
                     InternalInt.simplify (getConst internalIntF)
                         & return
diff --git a/kore/src/Kore/Unification/NewUnifier.hs b/kore/src/Kore/Unification/NewUnifier.hs
index be427538f3..fc0f8a3002 100644
--- a/kore/src/Kore/Unification/NewUnifier.hs
+++ b/kore/src/Kore/Unification/NewUnifier.hs
@@ -473,6 +473,7 @@ unifyTerms' rootSort sideCondition origVars vars ((first, second) : rest) bindin
             (_, _) | first == second -> discharge
             (InternalInt_ _, InternalInt_ _) -> failUnify "Distinct integer domain values"
             (InternalBool_ _, InternalBool_ _) -> failUnify "Distinct Boolean domain values"
+            (InternalFloat_ _, InternalFloat_ _) -> failUnify "Distinct floating-point domain values"
             (InternalString_ _, InternalString_ _) -> failUnify "Distinct string domain values"
             (DV_ _ _, DV_ _ _) -> failUnify "Distinct domain values"
             (StringLiteral_ _, StringLiteral_ _) -> failUnify "Distinct string literals"
diff --git a/kore/test/Test/ConsistentKore.hs b/kore/test/Test/ConsistentKore.hs
index 20d1fafac9..07b03d6fad 100644
--- a/kore/test/Test/ConsistentKore.hs
+++ b/kore/test/Test/ConsistentKore.hs
@@ -376,6 +376,7 @@ _checkTermImplemented term@(Recursive.project -> _ :< termF) =
     checkTermF (IffF _) = term
     checkTermF (ImpliesF _) = term
     checkTermF (InF _) = term
+    checkTermF (InternalFloatF _) = term
     checkTermF (MuF _) = term
     checkTermF (NextF _) = term
     checkTermF (NotF _) = term
diff --git a/kore/test/Test/Kore/Builtin/Definition.hs b/kore/test/Test/Kore/Builtin/Definition.hs
index 8a3a9a7a3d..a5c8da6499 100644
--- a/kore/test/Test/Kore/Builtin/Definition.hs
+++ b/kore/test/Test/Kore/Builtin/Definition.hs
@@ -40,10 +40,12 @@ import Kore.Attribute.Synthetic (
  )
 import Kore.Attribute.Total
 import Kore.Builtin.Endianness qualified as Endianness
+import Kore.Builtin.Float qualified as Float
 import Kore.Builtin.Signedness qualified as Signedness
 import Kore.Internal.ApplicationSorts
 import Kore.Internal.InternalBool
 import Kore.Internal.InternalBytes
+import Kore.Internal.InternalFloat
 import Kore.Internal.InternalInt
 import Kore.Internal.InternalList
 import Kore.Internal.InternalMap
@@ -310,6 +312,94 @@ eqInt
         TermLike RewritingVariableName
 eqInt i j = mkApplySymbol eqIntSymbol [i, j]
 ltInt i j = mkApplySymbol ltIntSymbol [i, j]
+-- ** Float
+comparisonFloatSymbol :: Text -> Internal.Symbol
+comparisonFloatSymbol name = comparisonSymbol name floatSort
+unaryFloatSymbol :: Text -> Internal.Symbol
+unaryFloatSymbol name = unarySymbol name floatSort
+binaryFloatSymbol :: Text -> Internal.Symbol
+binaryFloatSymbol name = binarySymbol name floatSort
+eqFloatSymbol :: Internal.Symbol
+eqFloatSymbol =
+    comparisonFloatSymbol "eqFloat"
+        & hook "FLOAT.eq"
+        & function
+        & total
+addFloatSymbol :: Internal.Symbol
+addFloatSymbol =
+    binaryFloatSymbol "addFloat"
+        & hook "FLOAT.add"
+        & function
+        & total
+precisionFloatSymbol :: Internal.Symbol
+precisionFloatSymbol =
+    builtinSymbol "precisionFloat" intSort [floatSort]
+        & hook "FLOAT.precision"
+        & function
+        & total
+signFloatSymbol :: Internal.Symbol
+signFloatSymbol =
+    builtinSymbol "signFloat" boolSort [floatSort]
+        & hook "FLOAT.sign"
+        & function
+        & total
+int2FloatSymbol :: Internal.Symbol
+int2FloatSymbol =
+    builtinSymbol "int2Float" floatSort [intSort, intSort, intSort]
+        & hook "FLOAT.int2float"
+        & function
+float2IntSymbol :: Internal.Symbol
+float2IntSymbol =
+    builtinSymbol "float2Int" intSort [floatSort]
+        & hook "FLOAT.float2int"
+        & function
+float2StringSymbol :: Internal.Symbol
+float2StringSymbol =
+    builtinSymbol "float2String" stringSort [floatSort]
+        & hook "STRING.float2string"
+        & function
+        & total
+string2FloatSymbol :: Internal.Symbol
+string2FloatSymbol =
+    builtinSymbol "string2Float" floatSort [stringSort]
+        & hook "STRING.string2float"
+        & function
+eqFloat ::
+    TermLike RewritingVariableName ->
+    TermLike RewritingVariableName ->
+    TermLike RewritingVariableName
+eqFloat x y = mkApplySymbol eqFloatSymbol [x, y]
+addFloat ::
+    TermLike RewritingVariableName ->
+    TermLike RewritingVariableName ->
+    TermLike RewritingVariableName
+addFloat x y = mkApplySymbol addFloatSymbol [x, y]
+precisionFloat ::
+    TermLike RewritingVariableName ->
+    TermLike RewritingVariableName
+precisionFloat x = mkApplySymbol precisionFloatSymbol [x]
+signFloat ::
+    TermLike RewritingVariableName ->
+    TermLike RewritingVariableName
+signFloat x = mkApplySymbol signFloatSymbol [x]
+int2Float ::
+    TermLike RewritingVariableName ->
+    TermLike RewritingVariableName ->
+    TermLike RewritingVariableName ->
+    TermLike RewritingVariableName
+int2Float x p e = mkApplySymbol int2FloatSymbol [x, p, e]
+float2Int ::
+    TermLike RewritingVariableName ->
+    TermLike RewritingVariableName
+float2Int x = mkApplySymbol float2IntSymbol [x]
+float2String ::
+    TermLike RewritingVariableName ->
+    TermLike RewritingVariableName
+float2String x = mkApplySymbol float2StringSymbol [x]
+string2Float ::
+    TermLike RewritingVariableName ->
+    TermLike RewritingVariableName
+string2Float x = mkApplySymbol string2FloatSymbol [x]
 -- ** KEQUAL
 comparisonKSymbol :: Text -> Internal.Symbol
 comparisonKSymbol name = comparisonSymbol name kSort
@@ -1011,6 +1101,37 @@ builtinInt internalIntValue =
         }
 mkInt :: InternalVariable variable => Integer -> TermLike variable
 mkInt = mkInternalInt . builtinInt
+-- ** Float
+
+floatSort :: Sort
+floatSort =
+    SortActualSort
+        SortActual
+            { sortActualName = testId "Float"
+            , sortActualSorts = []
+            }
+
+floatSortDecl :: ParsedSentence
+floatSortDecl =
+    hookedSortDecl
+        floatSort
+        [hasDomainValuesAttribute, hookAttribute "FLOAT.Float"]
+
+internalFloat :: FloatValue -> InternalFloat
+internalFloat internalFloatValue =
+    InternalFloat
+        { internalFloatSort = floatSort
+        , internalFloatValue
+        }
+
+mkFloat :: InternalVariable variable => FloatValue -> TermLike variable
+mkFloat = mkInternalFloat . internalFloat
+
+mkFloatText :: InternalVariable variable => Text -> TermLike variable
+mkFloatText =
+    mkFloat
+        . fromJust
+        . Float.parseText
 -- ** KEQUAL
 kSort :: Sort
 kSort =
@@ -1700,6 +1821,32 @@ stringModule =
             ]
         }
 
+-- ** FLOAT
+
+floatModuleName :: ModuleName
+floatModuleName = ModuleName "FLOAT"
+
+floatModule :: ParsedModule
+floatModule =
+    Module
+        { moduleName = floatModuleName
+        , moduleAttributes = Attributes []
+        , moduleSentences =
+            [ importParsedModule boolModuleName
+            , importParsedModule intModuleName
+            , importParsedModule stringModuleName
+            , floatSortDecl
+            , hookedSymbolDecl eqFloatSymbol
+            , hookedSymbolDecl addFloatSymbol
+            , hookedSymbolDecl precisionFloatSymbol
+            , hookedSymbolDecl signFloatSymbol
+            , hookedSymbolDecl int2FloatSymbol
+            , hookedSymbolDecl float2IntSymbol
+            , hookedSymbolDecl float2StringSymbol
+            , hookedSymbolDecl string2FloatSymbol
+            ]
+        }
+
 -- ** IO
 
 ioModuleName :: ModuleName
@@ -1799,11 +1946,13 @@ testModule =
             , importParsedModule pairModuleName
             , importParsedModule setModuleName
             , importParsedModule stringModuleName
+            , importParsedModule floatModuleName
             , importParsedModule bytesModuleName
             , importParsedModule kryptoModuleName
             , importParsedModule ioModuleName
             , subsortDecl boolSort kItemSort
             , subsortDecl intSort kItemSort
+            , subsortDecl floatSort kItemSort
             , subsortDecl idSort kItemSort
             , subsortDecl kItemSort kSort
             ]
@@ -1863,6 +2012,7 @@ testDefinition =
             , pairModule
             , setModule
             , stringModule
+            , floatModule
             , ioModule
             , bytesModule
             , kryptoModule
diff --git a/kore/test/Test/Kore/Builtin/External.hs b/kore/test/Test/Kore/Builtin/External.hs
index e370784743..ca66acef01 100644
--- a/kore/test/Test/Kore/Builtin/External.hs
+++ b/kore/test/Test/Kore/Builtin/External.hs
@@ -23,6 +23,7 @@ import Kore.Builtin.Signedness.Signedness qualified as Signedness
 import Kore.Internal.Alias qualified as Alias
 import Kore.Internal.Inj qualified as Inj
 import Kore.Internal.InternalBool
+import Kore.Internal.InternalFloat
 import Kore.Internal.InternalInt
 import Kore.Internal.InternalList
 import Kore.Internal.InternalMap
@@ -97,6 +98,7 @@ externalize = Recursive.futu externalize1
             -- Internals
             InternalBoolF (Const internalBool) -> externalizeBool internalBool
             InternalIntF (Const internalInt) -> externalizeInt internalInt
+            InternalFloatF (Const internalFloat) -> externalizeFloat internalFloat
             InternalBytesF (Const internalBytes) -> externalizeBytes internalBytes
             InternalStringF (Const internalString) -> externalizeString internalString
             InternalListF internalList -> externalizeList internalList
@@ -357,3 +359,20 @@ externalizeInt builtin =
     domainValueChild =
         Free . (:<) Attribute.Null . Syntax.StringLiteralF . Const $
             StringLiteral (Text.pack $ show internalIntValue)
+
+externalizeFloat ::
+    InternalFloat ->
+    FutuPattern variable (TermLike variable)
+externalizeFloat builtin =
+    Attribute.Null
+        :< Syntax.DomainValueF
+            DomainValue
+                { domainValueSort = internalFloatSort
+                , domainValueChild
+                }
+  where
+    InternalFloat{internalFloatSort} = builtin
+    InternalFloat{internalFloatValue} = builtin
+    domainValueChild =
+        Free . (:<) Attribute.Null . Syntax.StringLiteralF . Const $
+            StringLiteral (renderFloatValue internalFloatValue)
diff --git a/kore/test/Test/Kore/Builtin/Float.hs b/kore/test/Test/Kore/Builtin/Float.hs
new file mode 100644
index 0000000000..a958b9fbd0
--- /dev/null
+++ b/kore/test/Test/Kore/Builtin/Float.hs
@@ -0,0 +1,180 @@
+module Test.Kore.Builtin.Float (
+    test_domainValue,
+    test_add,
+    test_eq,
+    test_precision,
+    test_sign,
+    test_int2float,
+    test_float2int,
+    test_float2string,
+    test_string2float,
+    test_nan_roundtrip,
+) where
+
+import Data.Maybe (
+    fromJust,
+ )
+import Data.Text (
+    Text,
+ )
+import Kore.Builtin.Builtin qualified as Builtin
+import Kore.Builtin.Float qualified as Float
+import Kore.Internal.InternalFloat (
+    FloatValue (..),
+    InternalFloat (..),
+ )
+import Kore.Internal.MultiOr qualified as MultiOr
+import Kore.Internal.OrPattern (
+    OrPattern,
+ )
+import Kore.Internal.Pattern (
+    Pattern,
+ )
+import Kore.Internal.TermLike
+import Kore.Rewrite.RewritingVariable (
+    RewritingVariableName,
+ )
+import Prelude.Kore
+import Test.Kore.Builtin.Bool qualified as Test.Bool
+import Test.Kore.Builtin.Builtin
+import Test.Kore.Builtin.Definition
+import Test.Kore.Builtin.Int qualified as Test.Int
+import Test.Kore.Builtin.String qualified as Test.String
+import Test.Tasty
+import Test.Tasty.HUnit.Ext
+
+test_domainValue :: TestTree
+test_domainValue =
+    testCase "FLOAT domain value verifies to InternalFloat" $
+        case verifyPattern (Just floatSort) (Builtin.makeDomainValueTerm floatSort "0.5f") of
+            Right (InternalFloat_ InternalFloat{internalFloatValue = Float32 _}) -> pure ()
+            Right other ->
+                assertFailure ("expected InternalFloat, got: " ++ show other)
+            Left err ->
+                assertFailure (show err)
+
+test_add :: TestTree
+test_add =
+    testFloat
+        "FLOAT.add 1.0f 2.0f"
+        addFloatSymbol
+        [asInternal "1.0f", asInternal "2.0f"]
+        (asOrPattern "3.0f")
+
+test_eq :: [TestTree]
+test_eq =
+    [ testBool
+        "FLOAT.eq treats NaN as unequal"
+        eqFloatSymbol
+        [asInternal "NaNf", asInternal "NaNf"]
+        (Test.Bool.asOrPattern False)
+    , testBool
+        "FLOAT.eq treats signed zeros as equal"
+        eqFloatSymbol
+        [asInternal "0.0f", asInternal "-0.0f"]
+        (Test.Bool.asOrPattern True)
+    ]
+
+test_precision :: TestTree
+test_precision =
+    Test.Int.testInt
+        "FLOAT.precision on binary32"
+        precisionFloatSymbol
+        [asInternal "1.0f"]
+        (Test.Int.asOrPattern 24)
+
+test_sign :: [TestTree]
+test_sign =
+    [ testBool
+        "FLOAT.sign sees negative zero"
+        signFloatSymbol
+        [asInternal "-0.0f"]
+        (Test.Bool.asOrPattern True)
+    , testBool
+        "FLOAT.sign sees positive zero"
+        signFloatSymbol
+        [asInternal "0.0f"]
+        (Test.Bool.asOrPattern False)
+    ]
+
+test_int2float :: TestTree
+test_int2float =
+    testFloat
+        "FLOAT.int2float produces binary32"
+        int2FloatSymbol
+        [Test.Int.asInternal 7, Test.Int.asInternal 24, Test.Int.asInternal 8]
+        (asOrPattern "7.0f")
+
+test_float2int :: TestTree
+test_float2int =
+    Test.Int.testInt
+        "FLOAT.float2int rounds ties to even"
+        float2IntSymbol
+        [asInternal "2.5"]
+        (Test.Int.asOrPattern 2)
+
+test_float2string :: TestTree
+test_float2string =
+    testSymbolWithoutSolver
+        evaluateTerm
+        "STRING.float2string preserves concrete float syntax"
+        float2StringSymbol
+        [asInternal "1.5f"]
+        (Test.String.asOrPattern "1.5f")
+
+test_string2float :: TestTree
+test_string2float =
+    testFloat
+        "STRING.string2float parses IEEE syntax"
+        string2FloatSymbol
+        [Test.String.asInternal "1.5f"]
+        (asOrPattern "1.5f")
+
+test_nan_roundtrip :: [TestTree]
+test_nan_roundtrip =
+    [ testSymbolWithoutSolver
+        evaluateTerm
+        "STRING.float2string preserves NaN payloads via exact bit syntax"
+        float2StringSymbol
+        [Float.asInternal floatSort (Float32 0x7fc00001)]
+        (Test.String.asOrPattern "bits32(2143289345)")
+    , testSymbolWithoutSolver
+        evaluateTerm
+        "STRING.string2float parses exact NaN bit syntax"
+        string2FloatSymbol
+        [Test.String.asInternal "bits32(2143289345)"]
+        (MultiOr.singleton $ Float.asPattern floatSort (Float32 0x7fc00001))
+    ]
+
+asInternal :: Text -> TermLike variable
+asInternal =
+    Float.asInternal floatSort
+        . fromJust
+        . Float.parseText
+
+asPattern :: Text -> Pattern RewritingVariableName
+asPattern =
+    Float.asPattern floatSort
+        . fromJust
+        . Float.parseText
+
+asOrPattern :: Text -> OrPattern RewritingVariableName
+asOrPattern = MultiOr.singleton . asPattern
+
+testFloat ::
+    HasCallStack =>
+    String ->
+    Symbol ->
+    [TermLike RewritingVariableName] ->
+    OrPattern RewritingVariableName ->
+    TestTree
+testFloat name = testSymbolWithoutSolver evaluateTerm name
+
+testBool ::
+    HasCallStack =>
+    String ->
+    Symbol ->
+    [TermLike RewritingVariableName] ->
+    OrPattern RewritingVariableName ->
+    TestTree
+testBool name = testSymbolWithoutSolver evaluateTerm name