diff --git a/library/init/meta/exceptional.lean b/library/init/meta/exceptional.lean
new file mode 100644
index 0000000000..9561d8962c
--- /dev/null
+++ b/library/init/meta/exceptional.lean
@@ -0,0 +1,50 @@
+/-
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import init.monad init.meta.format
+/-
+Remark: we use a function that produces a format object as the exception information.
+Motivation: the formatting object may be big, and we may create it on demand.
+-/
+inductive exceptional (A : Type) :=
+| success   : A → exceptional A
+| exception : (options → format) → exceptional A
+
+section
+open exceptional
+variables {A : Type}
+variables [has_to_string A]
+
+protected meta_definition exceptional.to_string : exceptional A → string
+| (success a)     := to_string a
+| (exception A e) := "Exception: " + to_string (e options.mk)
+
+protected meta_definition exceptional.has_to_string [instance] : has_to_string (exceptional A) :=
+has_to_string.mk exceptional.to_string
+end
+
+namespace exceptional
+variables {A B : Type}
+
+inline protected meta_definition fmap (f : A → B) (e : exceptional A) : exceptional B :=
+exceptional.cases_on e
+  (λ a, success (f a))
+  (λ f, !exception f)
+
+inline protected meta_definition bind (e₁ : exceptional A) (e₂ : A → exceptional B) : exceptional B :=
+exceptional.cases_on e₁
+  (λ a, e₂ a)
+  (λ f, !exception f)
+
+inline protected meta_definition return (a : A) : exceptional A :=
+success a
+
+meta_definition fail (f : format) : exceptional A :=
+!exception (λ u, f)
+end exceptional
+
+meta_definition exceptional.is_monad [instance] : monad exceptional :=
+monad.mk @exceptional.fmap @exceptional.return @exceptional.bind
diff --git a/src/library/trace.cpp b/src/library/trace.cpp
index 9181827c3b..dab8a3244d 100644
--- a/src/library/trace.cpp
+++ b/src/library/trace.cpp
@@ -91,16 +91,18 @@ bool is_trace_class_enabled(name const & n) {
     return is_trace_class_set(get_enabled_trace_classes(), n);
 }
 
-scope_trace_env::scope_trace_env(environment const & env, io_state const & ios, abstract_type_context & ctx) {
+
+void scope_trace_env::init(environment * env, io_state * ios, abstract_type_context * ctx, bool ios_owner) {
     m_enable_sz  = get_enabled_trace_classes().size();
     m_disable_sz = get_disabled_trace_classes().size();
     m_old_env    = g_env;
     m_old_ios    = g_ios;
     m_old_ctx    = g_ctx;
-    g_env        = const_cast<environment*>(&env);
-    g_ios        = const_cast<io_state*>(&ios);
-    g_ctx        = &ctx;
-    options const & opts = ios.get_options();
+    g_env        = env;
+    g_ios        = ios;
+    g_ctx        = ctx;
+    m_ios_owner  = ios_owner;
+    options const & opts = ios->get_options();
     name trace("trace");
     opts.for_each([&](name const & n) {
             if (is_prefix_of(trace, n)) {
@@ -113,7 +115,24 @@ scope_trace_env::scope_trace_env(environment const & env, io_state const & ios,
         });
 }
 
+scope_trace_env::scope_trace_env(environment const & env, io_state const & ios, abstract_type_context & ctx) {
+    init(const_cast<environment*>(&env), const_cast<io_state*>(&ios), &ctx, false);
+}
+
+scope_trace_env::scope_trace_env(options const & o) {
+    if (!g_ios) {
+        m_ios_owner  = false;
+        m_enable_sz  = 0;
+        m_disable_sz = 0;
+    } else {
+        io_state * tmp_ios = new io_state(*g_ios, o);
+        init(g_env, tmp_ios, g_ctx, true);
+    }
+}
+
 scope_trace_env::~scope_trace_env() {
+    if (m_ios_owner)
+        delete g_ios;
     g_env = const_cast<environment*>(m_old_env);
     g_ios = const_cast<io_state*>(m_old_ios);
     g_ctx = m_old_ctx;
diff --git a/src/library/trace.h b/src/library/trace.h
index dede5597f6..a36abaedc3 100644
--- a/src/library/trace.h
+++ b/src/library/trace.h
@@ -22,8 +22,11 @@ class scope_trace_env {
     environment const *     m_old_env;
     io_state    const *     m_old_ios;
     abstract_type_context * m_old_ctx;
+    bool                    m_ios_owner;
+    void init(environment * env, io_state * ios, abstract_type_context * ctx, bool ios_owner);
 public:
     scope_trace_env(environment const & env, io_state const & ios, abstract_type_context & ctx);
+    scope_trace_env(options const & opts);
     ~scope_trace_env();
 };
 
diff --git a/src/library/vm/CMakeLists.txt b/src/library/vm/CMakeLists.txt
index dbb3799d00..be4508389f 100644
--- a/src/library/vm/CMakeLists.txt
+++ b/src/library/vm/CMakeLists.txt
@@ -1,3 +1,3 @@
-add_library(vm OBJECT vm.cpp vm_nat.cpp vm_string.cpp vm_aux.cpp vm_io.cpp vm_name.cpp
-  vm_options.cpp vm_format.cpp vm_rb_map.cpp vm_level.cpp vm_expr.cpp
-  optimize.cpp init_module.cpp)
\ No newline at end of file
+add_library(vm OBJECT vm.cpp optimize.cpp vm_nat.cpp vm_string.cpp vm_aux.cpp vm_io.cpp vm_name.cpp
+  vm_options.cpp vm_format.cpp vm_rb_map.cpp vm_level.cpp vm_expr.cpp vm_exceptional.cpp
+  init_module.cpp)
\ No newline at end of file
diff --git a/src/library/vm/init_module.cpp b/src/library/vm/init_module.cpp
index 14efe18661..d5f8c8fb45 100644
--- a/src/library/vm/init_module.cpp
+++ b/src/library/vm/init_module.cpp
@@ -14,6 +14,7 @@ Author: Leonardo de Moura
 #include "library/vm/vm_rb_map.h"
 #include "library/vm/vm_level.h"
 #include "library/vm/vm_expr.h"
+#include "library/vm/vm_exceptional.h"
 
 namespace lean {
 void initialize_vm_core_module() {
@@ -27,8 +28,10 @@ void initialize_vm_core_module() {
     initialize_vm_rb_map();
     initialize_vm_level();
     initialize_vm_expr();
+    initialize_vm_exceptional();
 }
 void finalize_vm_core_module() {
+    finalize_vm_exceptional();
     finalize_vm_expr();
     finalize_vm_level();
     finalize_vm_rb_map();
@@ -44,6 +47,7 @@ void finalize_vm_core_module() {
 void initialize_vm_module() {
     initialize_vm();
     initialize_vm_expr_builtin_idxs();
+    initialize_vm_exceptional_builtin_idxs();
 }
 void finalize_vm_module() {
     finalize_vm();
diff --git a/src/library/vm/vm_exceptional.cpp b/src/library/vm/vm_exceptional.cpp
new file mode 100644
index 0000000000..b0d8496b8b
--- /dev/null
+++ b/src/library/vm/vm_exceptional.cpp
@@ -0,0 +1,70 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "kernel/kernel_exception.h"
+#include "library/trace.h"
+#include "library/vm/vm_exceptional.h"
+#include "library/vm/vm_options.h"
+#include "library/vm/vm_format.h"
+
+namespace lean {
+struct vm_throwable : public vm_external {
+    throwable * m_val;
+    vm_throwable(throwable const & ex):m_val(ex.clone()) {}
+    ~vm_throwable() { delete m_val; }
+    virtual void dealloc() override { this->~vm_throwable(); get_vm_allocator().deallocate(sizeof(vm_throwable), this); }
+};
+
+throwable * to_throwable(vm_obj const & o) {
+    lean_assert(is_external(o));
+    lean_assert(dynamic_cast<vm_throwable*>(to_external(o)));
+    return static_cast<vm_throwable*>(to_external(o))->m_val;
+}
+
+vm_obj to_obj(throwable const & ex) {
+    return mk_vm_external(new (get_vm_allocator().allocate(sizeof(vm_throwable))) vm_throwable(ex));
+}
+
+vm_obj throwable_to_format(vm_obj const & _ex, vm_obj const & _opts) {
+    throwable * ex = to_throwable(_ex);
+    if (!ex)
+        return to_obj(format("null-exception"));
+    options const & opts = to_options(_opts);
+
+    if (auto kex = dynamic_cast<ext_exception*>(ex)) {
+        scope_trace_env scope1(opts);
+        io_state_stream ios = tout();
+        formatter fmt = ios.get_formatter();
+        return to_obj(kex->pp(fmt));
+    }
+
+    /* TODO(Leo): add support for other exception types that may generate interesting format */
+
+    return to_obj(format(ex->what()));
+}
+
+static unsigned g_throwable_to_format_fun_idx = -1;
+
+vm_obj mk_vm_exceptional_success(vm_obj const & a) {
+    return mk_vm_constructor(0, a);
+}
+
+vm_obj mk_vm_exceptional_exception(throwable const & ex) {
+    vm_obj _ex = to_obj(ex);
+    return mk_vm_closure(g_throwable_to_format_fun_idx, 1, &_ex);
+}
+
+void initialize_vm_exceptional() {
+    DECLARE_VM_BUILTIN("_throwable_to_format", throwable_to_format);
+}
+
+void finalize_vm_exceptional() {
+}
+
+void initialize_vm_exceptional_builtin_idxs() {
+    g_throwable_to_format_fun_idx = *get_vm_builtin_idx(name("_throwable_to_format"));
+}
+}
diff --git a/src/library/vm/vm_exceptional.h b/src/library/vm/vm_exceptional.h
new file mode 100644
index 0000000000..fb51f9a9f6
--- /dev/null
+++ b/src/library/vm/vm_exceptional.h
@@ -0,0 +1,17 @@
+/*
+Copyright (c) 2016 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/exception.h"
+#include "library/vm/vm.h"
+
+namespace lean {
+vm_obj mk_vm_exceptional_success(vm_obj const & a);
+vm_obj mk_vm_exceptional_exception(throwable const & ex);
+void initialize_vm_exceptional();
+void finalize_vm_exceptional();
+void initialize_vm_exceptional_builtin_idxs();
+}