diff --git a/src/tests/util/CMakeLists.txt b/src/tests/util/CMakeLists.txt
index 0e7eb6f68b..31466def78 100644
--- a/src/tests/util/CMakeLists.txt
+++ b/src/tests/util/CMakeLists.txt
@@ -1,6 +1,9 @@
 add_executable(name name.cpp $<TARGET_OBJECTS:util> $<TARGET_OBJECTS:runtime>)
 target_link_libraries(name ${EXTRA_LIBS})
 add_exec_test(name "name")
+add_executable(nat nat.cpp $<TARGET_OBJECTS:util> $<TARGET_OBJECTS:runtime>)
+target_link_libraries(nat ${EXTRA_LIBS})
+add_exec_test(nat "nat")
 add_executable(sexpr_tst sexpr.cpp $<TARGET_OBJECTS:util> $<TARGET_OBJECTS:runtime> $<TARGET_OBJECTS:sexpr>)
 target_link_libraries(sexpr_tst ${EXTRA_LIBS})
 add_exec_test(sexpr "sexpr_tst")
diff --git a/src/tests/util/nat.cpp b/src/tests/util/nat.cpp
new file mode 100644
index 0000000000..cf15f8ab2b
--- /dev/null
+++ b/src/tests/util/nat.cpp
@@ -0,0 +1,52 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include <cstring>
+#include <sstream>
+#include "util/test.h"
+#include "util/nat.h"
+#include "util/init_module.h"
+using namespace lean;
+
+static void tst1() {
+    lean_assert(nat("10000000000000000000") + nat("10000000000000000000") == nat("20000000000000000000"));
+    lean_assert(nat(1) == nat(2) - nat(1));
+    lean_assert(nat(30) * nat(10) == nat(300));
+    lean_assert(nat(7) / nat(2) == nat(3));
+    lean_assert(nat(11) % nat(3) == nat(2));
+    lean_assert(nat("-10") == nat(0));
+    lean_assert(nat(-1) == nat(0));
+    nat v(10);
+    v = v + nat(1);
+    lean_assert(v == nat(11));
+    lean_assert(nat(12) != nat("11"));
+    lean_assert(nat(10) < nat(100));
+    lean_assert(nat(10) <= nat(100));
+    lean_assert(nat(10) <= nat(10));
+    lean_assert(!(nat(10) < nat(10)));
+    lean_assert(!(nat(11) < nat(10)));
+    lean_assert(!(nat(10) > nat(100)));
+    lean_assert(!(nat(10) >= nat(100)));
+    lean_assert(nat(10) >= nat(10));
+    lean_assert(!(nat(10) > nat(10)));
+    lean_assert(nat(11) > nat(10));
+    lean_assert(nat(20) > nat(10));
+    lean_assert(nat(20) >= nat(10));
+    lean_assert(nat(20).is_small());
+    lean_assert(nat(1).get_small_value() == 1);
+    lean_assert(!nat("10000000000000000000").is_small());
+    lean_assert(nat("10000000000000000000").get_big_value() == mpz("10000000000000000000"));
+    lean_assert(nat(1).to_mpz() == mpz(1));
+    lean_assert(nat("10000000000000000000").to_mpz() == mpz("10000000000000000000"));
+}
+
+int main() {
+    save_stack_info();
+    initialize_util_module();
+    tst1();
+    finalize_util_module();
+    return has_violations() ? 1 : 0;
+}
diff --git a/src/util/nat.h b/src/util/nat.h
new file mode 100644
index 0000000000..e7fda39b57
--- /dev/null
+++ b/src/util/nat.h
@@ -0,0 +1,50 @@
+/*
+Copyright (c) 2018 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "util/object_ref.h"
+
+namespace lean {
+/* Wrapper for manipulating Lean runtime nat values in C++. */
+class nat : public object_ref {
+    nat(object * o, bool):object_ref(o) {}
+    static nat wrap(object * o) { return nat(o, true); }
+public:
+    nat():object_ref(box(0)) {}
+    explicit nat(int v):object_ref(mk_nat_obj(v < 0 ? 0u : static_cast<unsigned>(v))) {}
+    explicit nat(unsigned v):object_ref(mk_nat_obj(v)) {}
+    explicit nat(mpz const & v):object_ref(mk_nat_obj(v)) {}
+    explicit nat(char const * v):object_ref(box(0)) {
+        mpz m(v);
+        if (m > 0)
+            *this = nat(mk_nat_obj(m));
+    }
+    nat(nat const & other):object_ref(other) {}
+    nat(nat && other):object_ref(other) {}
+    explicit nat(object * o):object_ref(o) { inc(o); }
+
+    nat & operator=(nat const & other) { object_ref::operator=(other); return *this; }
+    nat & operator=(nat && other) { object_ref::operator=(other); return *this; }
+
+    bool is_small() const { return is_scalar(raw()); }
+    unsigned get_small_value() const { lean_assert(is_small()); return unbox(raw()); }
+    mpz const & get_big_value() const { lean_assert(!is_small()); return mpz_value(raw()); }
+    mpz to_mpz() const { return is_small() ? mpz(unbox(raw())) : mpz_value(raw()); }
+    std::string to_string() const { return to_mpz().to_string(); }
+
+    friend bool operator==(nat const & a, nat const & b) { return nat_eq(a.raw(), b.raw()); }
+    friend bool operator!=(nat const & a, nat const & b) { return !(a == b); }
+    friend bool operator<=(nat const & a, nat const & b) { return nat_le(a.raw(), b.raw()); }
+    friend bool operator<(nat const & a, nat const & b) { return nat_lt(a.raw(), b.raw()); }
+    friend bool operator>=(nat const & a, nat const & b) { return b <= a; }
+    friend bool operator>(nat const & a, nat const & b) { return b < a; }
+    friend nat operator+(nat const & a, nat const & b) { return wrap(nat_add(a.raw(), b.raw())); }
+    friend nat operator-(nat const & a, nat const & b) { return wrap(nat_sub(a.raw(), b.raw())); }
+    friend nat operator*(nat const & a, nat const & b) { return wrap(nat_mul(a.raw(), b.raw())); }
+    friend nat operator/(nat const & a, nat const & b) { return wrap(nat_div(a.raw(), b.raw())); }
+    friend nat operator%(nat const & a, nat const & b) { return wrap(nat_mod(a.raw(), b.raw())); }
+};
+};