diff --git a/src/Std.lean b/src/Std.lean
index 0a2f53c641b6..f427d00b8a8f 100644
--- a/src/Std.lean
+++ b/src/Std.lean
@@ -10,3 +10,4 @@ import Std.Sync
 import Std.Time
 import Std.Tactic
 import Std.Internal
+import Std.Net
diff --git a/src/Std/Net.lean b/src/Std/Net.lean
new file mode 100644
index 000000000000..3d96dac34807
--- /dev/null
+++ b/src/Std/Net.lean
@@ -0,0 +1,7 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+prelude
+import Std.Net.Addr
diff --git a/src/Std/Net/Addr.lean b/src/Std/Net/Addr.lean
new file mode 100644
index 000000000000..dffa107465fc
--- /dev/null
+++ b/src/Std/Net/Addr.lean
@@ -0,0 +1,197 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Henrik Böving
+-/
+prelude
+import Init.Data.Vector.Basic
+
+/-!
+This module contains Lean representations of IP and socket addresses:
+- `IPv4Addr`: Representing IPv4 addresses.
+- `SocketAddressV4`: Representing a pair of IPv4 address and port.
+- `IPv6Addr`: Representing IPv6 addresses.
+- `SocketAddressV6`: Representing a pair of IPv6 address and port.
+- `IPAddr`: Can either be an `IPv4Addr` or an `IPv6Addr`.
+- `SocketAddress`: Can either be a `SocketAddressV4` or `SocketAddressV6`.
+-/
+
+namespace Std
+namespace Net
+
+/--
+Representation of an IPv4 address.
+-/
+structure IPv4Addr where
+  /--
+  This structure represents the address: `octets[0].octets[1].octets[2].octets[3]`.
+  -/
+  octets : Vector UInt8 4
+  deriving Inhabited, DecidableEq
+
+/--
+A pair of an `IPv4Addr` and a port.
+-/
+structure SocketAddressV4 where
+  addr : IPv4Addr
+  port : UInt16
+  deriving Inhabited, DecidableEq
+
+/--
+Representation of an IPv6 address.
+-/
+structure IPv6Addr where
+  /--
+  This structure represents the address: `segments[0]:segments[1]:...`.
+  -/
+  segments : Vector UInt16 8
+  deriving Inhabited, DecidableEq
+
+/--
+A pair of an `IPv6Addr` and a port.
+-/
+structure SocketAddressV6 where
+  addr : IPv6Addr
+  port : UInt16
+  deriving Inhabited, DecidableEq
+
+/--
+An IP address, either IPv4 or IPv6.
+-/
+inductive IPAddr where
+  | v4 (addr : IPv4Addr)
+  | v6 (addr : IPv6Addr)
+  deriving Inhabited, DecidableEq
+
+/--
+Either a `SocketAddressV4` or `SocketAddressV6`.
+-/
+inductive SocketAddress where
+  | v4 (addr : SocketAddressV4)
+  | v6 (addr : SocketAddressV6)
+  deriving Inhabited, DecidableEq
+
+/--
+The kinds of address families supported by Lean, currently only IP variants.
+-/
+inductive AddressFamily where
+  | ipv4
+  | ipv6
+  deriving Inhabited, DecidableEq
+
+namespace IPv4Addr
+
+/--
+Build the IPv4 address `a.b.c.d`.
+-/
+def ofParts (a b c d : UInt8) : IPv4Addr :=
+  { octets := #v[a, b, c, d] }
+
+/--
+Try to parse `s` as an IPv4 address, returning `none` on failure.
+-/
+@[extern "lean_uv_pton_v4"]
+opaque ofString (s : @&String) : Option IPv4Addr
+
+/--
+Turn `addr` into a `String` in the usual IPv4 format.
+-/
+@[extern "lean_uv_ntop_v4"]
+opaque toString (addr : @&IPv4Addr) : String
+
+instance : ToString IPv4Addr where
+  toString := toString
+
+instance : Coe IPv4Addr IPAddr where
+  coe addr := .v4 addr
+
+end IPv4Addr
+
+namespace SocketAddressV4
+
+instance : Coe SocketAddressV4 SocketAddress where
+  coe addr := .v4 addr
+
+end SocketAddressV4
+
+namespace IPv6Addr
+
+/--
+Build the IPv6 address `a:b:c:d:e:f:g:h`.
+-/
+def ofParts (a b c d e f g h : UInt16) : IPv6Addr :=
+  { segments := #v[a, b, c, d, e, f, g, h] }
+
+/--
+Try to parse `s` as an IPv6 address according to
+[RFC 2373](https://datatracker.ietf.org/doc/html/rfc2373), returning `none` on failure.
+-/
+@[extern "lean_uv_pton_v6"]
+opaque ofString (s : @&String) : Option IPv6Addr
+
+/--
+Turn `addr` into a `String` in the IPv6 format described in
+[RFC 2373](https://datatracker.ietf.org/doc/html/rfc2373).
+-/
+@[extern "lean_uv_ntop_v6"]
+opaque toString (addr : @&IPv6Addr) : String
+
+instance : ToString IPv6Addr where
+  toString := toString
+
+instance : Coe IPv6Addr IPAddr where
+  coe addr := .v6 addr
+
+end IPv6Addr
+
+namespace SocketAddressV6
+
+instance : Coe SocketAddressV6 SocketAddress where
+  coe addr := .v6 addr
+
+end SocketAddressV6
+
+namespace IPAddr
+
+/--
+Obtain the `AddressFamily` associated with an `IPAddr`.
+-/
+def family : IPAddr → AddressFamily
+  | .v4 .. => .ipv4
+  | .v6 .. => .ipv6
+
+def toString : IPAddr → String
+  | .v4 addr => addr.toString
+  | .v6 addr => addr.toString
+
+instance : ToString IPAddr where
+  toString := toString
+
+end IPAddr
+
+namespace SocketAddress
+
+/--
+Obtain the `AddressFamily` associated with a `SocketAddress`.
+-/
+def family : SocketAddress → AddressFamily
+  | .v4 .. => .ipv4
+  | .v6 .. => .ipv6
+
+/--
+Obtain the `IPAddr` contained in a `SocketAddress`.
+-/
+def ipAddr : SocketAddress → IPAddr
+  | .v4 sa  => .v4 sa.addr
+  | .v6 sa  => .v6 sa.addr
+
+/--
+Obtain the port contained in a `SocketAddress`.
+-/
+def port : SocketAddress → UInt16
+  | .v4 sa | .v6 sa => sa.port
+
+end SocketAddress
+
+end Net
+end Std
diff --git a/src/runtime/CMakeLists.txt b/src/runtime/CMakeLists.txt
index 367c7c298038..d6d8b50b395d 100644
--- a/src/runtime/CMakeLists.txt
+++ b/src/runtime/CMakeLists.txt
@@ -2,7 +2,7 @@ set(RUNTIME_OBJS debug.cpp thread.cpp mpz.cpp utf8.cpp
 object.cpp apply.cpp exception.cpp interrupt.cpp memory.cpp
 stackinfo.cpp compact.cpp init_module.cpp load_dynlib.cpp io.cpp hash.cpp
 platform.cpp alloc.cpp allocprof.cpp sharecommon.cpp stack_overflow.cpp
-process.cpp object_ref.cpp mpn.cpp mutex.cpp libuv.cpp)
+process.cpp object_ref.cpp mpn.cpp mutex.cpp libuv.cpp uv/net_addr.cpp)
 add_library(leanrt_initial-exec STATIC ${RUNTIME_OBJS})
 set_target_properties(leanrt_initial-exec PROPERTIES
   ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_CURRENT_BINARY_DIR})
diff --git a/src/runtime/uv/net_addr.cpp b/src/runtime/uv/net_addr.cpp
new file mode 100644
index 000000000000..f06a078f6874
--- /dev/null
+++ b/src/runtime/uv/net_addr.cpp
@@ -0,0 +1,131 @@
+/*
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Henrik Böving
+*/
+
+#include "runtime/uv/net_addr.h"
+#include <cstring>
+
+namespace lean {
+
+#ifndef LEAN_EMSCRIPTEN
+
+void lean_ipv4_addr_to_in_addr(b_obj_arg ipv4_addr, in_addr* out) {
+    out->s_addr = 0;
+    for (int i = 0; i < 4; i++) {
+        uint32_t octet = (uint32_t)(uint8_t)lean_unbox(array_uget(ipv4_addr, i));
+        out->s_addr |= octet << (3 - i) * 8;
+    }
+    out->s_addr = htonl(out->s_addr);
+}
+
+void lean_ipv6_addr_to_in6_addr(b_obj_arg ipv6_addr, in6_addr* out) {
+    for (int i = 0; i < 8; i++) {
+        uint16_t segment = htons((uint16_t)lean_unbox(array_uget(ipv6_addr, i)));
+        out->s6_addr[2 * i] = (uint8_t)segment;
+        out->s6_addr[2 * i + 1] = (uint8_t)(segment >> 8);
+    }
+}
+
+lean_obj_res lean_in_addr_to_ipv4_addr(const in_addr* ipv4_addr) {
+    obj_res ret = alloc_array(0, 4);
+    uint32_t hostaddr = ntohl(ipv4_addr->s_addr);
+
+    for (int i = 0; i < 4; i++) {
+        uint8_t octet = (uint8_t)(hostaddr >> (3 - i) * 8);
+        array_push(ret, lean_box(octet));
+    }
+
+    lean_assert(array_size(ret) == 4);
+    return ret;
+}
+
+lean_obj_res lean_in6_addr_to_ipv6_addr(const in6_addr* ipv6_addr) {
+    obj_res ret = alloc_array(0, 8);
+
+    for (int i = 0; i < 16; i += 2) {
+        uint16_t part1 = (uint16_t)ipv6_addr->s6_addr[i];
+        uint16_t part2 = (uint16_t)ipv6_addr->s6_addr[i + 1];
+        uint16_t segment = ntohs((part2 << 8) | part1);
+        array_push(ret, lean_box(segment));
+    }
+
+    lean_assert(array_size(ret) == 8);
+    return ret;
+}
+
+/* Std.Net.IPV4Addr.ofString (s : @&String) : Option IPV4Addr */
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_pton_v4(b_obj_arg str_obj) {
+    const char* str = string_cstr(str_obj);
+    in_addr internal;
+    if (uv_inet_pton(AF_INET, str, &internal) == 0) {
+        return mk_option_some(lean_in_addr_to_ipv4_addr(&internal));
+    } else {
+        return mk_option_none();
+    }
+}
+
+/* Std.Net.IPV4Addr.toString (addr : @&IPV4Addr) : String */
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ntop_v4(b_obj_arg ipv4_addr) {
+    in_addr internal;
+    lean_ipv4_addr_to_in_addr(ipv4_addr, &internal);
+    char dst[INET_ADDRSTRLEN];
+    int ret = uv_inet_ntop(AF_INET, &internal, dst, sizeof(dst));
+    lean_always_assert(ret == 0);
+    return lean_mk_string(dst);
+}
+
+/* Std.Net.IPV6Addr.ofString (s : @&String) : Option IPV6Addr */
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_pton_v6(b_obj_arg str_obj) {
+    const char* str = string_cstr(str_obj);
+    in6_addr internal;
+    if (uv_inet_pton(AF_INET6, str, &internal) == 0) {
+        return mk_option_some(lean_in6_addr_to_ipv6_addr(&internal));
+    } else {
+        return mk_option_none();
+    }
+}
+
+/* Std.Net.IPV6Addr.toString (addr : @&IPV6Addr) : String */
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ntop_v6(b_obj_arg ipv6_addr) {
+    in6_addr internal;
+    lean_ipv6_addr_to_in6_addr(ipv6_addr, &internal);
+    char dst[INET6_ADDRSTRLEN];
+    int ret = uv_inet_ntop(AF_INET6, &internal, dst, sizeof(dst));
+    lean_always_assert(ret == 0);
+    return lean_mk_string(dst);
+}
+
+#else
+
+/* Std.Net.IPV4Addr.ofString (s : @&String) : Option IPV4Addr */
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_pton_v4(b_obj_arg str_obj) {
+    lean_always_assert(
+        false && ("Please build a version of Lean4 with libuv to invoke this.")
+    );
+}
+
+/* Std.Net.IPV4Addr.toString (addr : @&IPV4Addr) : String */
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ntop_v4(b_obj_arg ipv4_addr) {
+    lean_always_assert(
+        false && ("Please build a version of Lean4 with libuv to invoke this.")
+    );
+}
+
+/* Std.Net.IPV6Addr.ofString (s : @&String) : Option IPV6Addr */
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_pton_v6(b_obj_arg str_obj) {
+    lean_always_assert(
+        false && ("Please build a version of Lean4 with libuv to invoke this.")
+    );
+}
+
+/* Std.Net.IPV6Addr.toString (addr : @&IPV6Addr) : String */
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ntop_v6(b_obj_arg ipv6_addr) {
+    lean_always_assert(
+        false && ("Please build a version of Lean4 with libuv to invoke this.")
+    );
+}
+
+#endif
+}
diff --git a/src/runtime/uv/net_addr.h b/src/runtime/uv/net_addr.h
new file mode 100644
index 000000000000..2d6783beb50b
--- /dev/null
+++ b/src/runtime/uv/net_addr.h
@@ -0,0 +1,28 @@
+/*
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Henrik Böving
+*/
+#pragma once
+#include <lean/lean.h>
+#include "runtime/object.h"
+
+
+namespace lean {
+
+#ifndef LEAN_EMSCRIPTEN
+#include <uv.h>
+
+void lean_ipv4_addr_to_in_addr(b_obj_arg ipv4_addr, struct in_addr* out);
+void lean_ipv6_addr_to_in6_addr(b_obj_arg ipv6_addr, struct in6_addr* out);
+lean_obj_res lean_in_addr_to_ipv4_addr(const struct in_addr* ipv4_addr);
+lean_obj_res lean_in6_addr_to_ipv6_addr(const struct in6_addr* ipv6_addr);
+
+#endif
+
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_pton_v4(b_obj_arg str_obj);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ntop_v4(b_obj_arg ipv4_addr);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_pton_v6(b_obj_arg str_obj);
+extern "C" LEAN_EXPORT lean_obj_res lean_uv_ntop_v6(b_obj_arg ipv6_addr);
+
+}
diff --git a/tests/lean/run/net_addr.lean b/tests/lean/run/net_addr.lean
new file mode 100644
index 000000000000..5503e880310f
--- /dev/null
+++ b/tests/lean/run/net_addr.lean
@@ -0,0 +1,39 @@
+import Std.Net.Addr
+
+open Std.Net
+
+/-- info: true -/
+#guard_msgs in
+#eval (IPv4Addr.ofParts 192 168 178 120).toString == "192.168.178.120"
+
+/-- info: true -/
+#guard_msgs in
+#eval (IPv4Addr.ofParts 1 2 3 4).toString == "1.2.3.4"
+
+/-- info: true -/
+#guard_msgs in
+#eval (IPv6Addr.ofParts 0xdead 0xbeef 0 0 0 0 0 0).toString == "dead:beef::"
+
+/-- info: true -/
+#guard_msgs in
+#eval (IPv6Addr.ofParts 0x1234 0x5678 0x9abc 0xdef1 0x4321 0x8765 0xcba9 0x1fed).toString == "1234:5678:9abc:def1:4321:8765:cba9:1fed"
+
+/-- info: true -/
+#guard_msgs in
+#eval IPv4Addr.ofString "1.2.3.4" == some (IPv4Addr.ofParts 1 2 3 4)
+
+/-- info: true -/
+#guard_msgs in
+#eval IPv4Addr.ofString "192.168.300.120" |>.isNone
+
+/-- info: true -/
+#guard_msgs in
+#eval IPv6Addr.ofString "dead:beef::" == some (IPv6Addr.ofParts 0xdead 0xbeef 0 0 0 0 0 0)
+
+/-- info: true -/
+#guard_msgs in
+#eval IPv6Addr.ofString "1234:5678:9abc:def1:4321:8765:cba9:1fed" == some (IPv6Addr.ofParts 0x1234 0x5678 0x9abc 0xdef1 0x4321 0x8765 0xcba9 0x1fed)
+
+/-- info: true -/
+#guard_msgs in
+#eval IPv6Addr.ofString "dead:beef::badaddress" |>.isNone