diff --git a/explorer/interpreter/BUILD b/explorer/interpreter/BUILD
index 490b92ef5c6d..6aa3baa4b2c8 100644
--- a/explorer/interpreter/BUILD
+++ b/explorer/interpreter/BUILD
@@ -74,6 +74,7 @@ cc_library(
         ":interpreter",
         ":resolve_control_flow",
         ":resolve_names",
+        ":resolve_unformed",
         ":type_checker",
         "//common:check",
         "//common:ostream",
@@ -202,3 +203,21 @@ cc_library(
         "@llvm-project//llvm:Support",
     ],
 )
+
+cc_library(
+    name = "resolve_unformed",
+    srcs = [
+        "resolve_unformed.cpp",
+    ],
+    hdrs = [
+        "resolve_unformed.h",
+    ],
+    deps = [
+        "//common:check",
+        "//explorer/ast",
+        "//explorer/ast:static_scope",
+        "//explorer/common:error_builders",
+        "//explorer/common:nonnull",
+        "@llvm-project//llvm:Support",
+    ],
+)
diff --git a/explorer/interpreter/exec_program.cpp b/explorer/interpreter/exec_program.cpp
index 9e40cca64fae..60b08af121d6 100644
--- a/explorer/interpreter/exec_program.cpp
+++ b/explorer/interpreter/exec_program.cpp
@@ -12,6 +12,7 @@
 #include "explorer/interpreter/interpreter.h"
 #include "explorer/interpreter/resolve_control_flow.h"
 #include "explorer/interpreter/resolve_names.h"
+#include "explorer/interpreter/resolve_unformed.h"
 #include "explorer/interpreter/type_checker.h"
 #include "llvm/Support/Error.h"
 
@@ -45,8 +46,11 @@ auto ExecProgram(Nonnull<Arena*> arena, AST ast,
   }
   CARBON_RETURN_IF_ERROR(TypeChecker(arena, trace_stream).TypeCheck(ast));
   if (trace_stream) {
-    **trace_stream << "\n";
-    **trace_stream << "********** type checking complete **********\n";
+    **trace_stream << "********** resolving unformed variables **********\n";
+  }
+  CARBON_RETURN_IF_ERROR(ResolveUnformed(ast));
+  if (trace_stream) {
+    **trace_stream << "********** printing declarations **********\n";
     for (const auto decl : ast.declarations) {
       **trace_stream << *decl;
     }
diff --git a/explorer/interpreter/resolve_unformed.cpp b/explorer/interpreter/resolve_unformed.cpp
new file mode 100644
index 000000000000..7e093c9d8523
--- /dev/null
+++ b/explorer/interpreter/resolve_unformed.cpp
@@ -0,0 +1,240 @@
+// Part of the Carbon Language project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+
+#include "explorer/interpreter/resolve_unformed.h"
+
+#include <unordered_map>
+
+#include "common/check.h"
+#include "explorer/ast/ast.h"
+#include "explorer/ast/expression.h"
+#include "explorer/ast/pattern.h"
+#include "explorer/common/error_builders.h"
+#include "explorer/common/nonnull.h"
+
+using llvm::cast;
+
+namespace Carbon {
+
+// Aggregate information about a AstNode being analyzed.
+struct FlowFact {
+  bool may_be_formed;
+};
+
+// Traverses the sub-AST rooted at the given node, resolving the formed/unformed
+// states of local variables within it and updating the flow facts.
+static auto ResolveUnformed(
+    Nonnull<const Expression*> expression,
+    std::unordered_map<Nonnull<const AstNode*>, FlowFact>& flow_facts,
+    bool set_formed) -> ErrorOr<Success>;
+static auto ResolveUnformed(
+    Nonnull<const Pattern*> pattern,
+    std::unordered_map<Nonnull<const AstNode*>, FlowFact>& flow_facts,
+    bool has_init) -> ErrorOr<Success>;
+static auto ResolveUnformed(
+    Nonnull<const Statement*> statement,
+    std::unordered_map<Nonnull<const AstNode*>, FlowFact>& flow_facts)
+    -> ErrorOr<Success>;
+static auto ResolveUnformed(Nonnull<const Declaration*> declaration)
+    -> ErrorOr<Success>;
+
+static auto ResolveUnformed(
+    Nonnull<const Expression*> expression,
+    std::unordered_map<Nonnull<const AstNode*>, FlowFact>& flow_facts,
+    const bool set_formed) -> ErrorOr<Success> {
+  switch (expression->kind()) {
+    case ExpressionKind::IdentifierExpression: {
+      auto& identifier = cast<IdentifierExpression>(*expression);
+      auto fact = flow_facts.find(&identifier.value_node().base());
+      // TODO: @slaterlatiao add all available value nodes to flow facts and use
+      // CARBON_CHECK on the following line.
+      if (fact == flow_facts.end()) {
+        break;
+      }
+      if (set_formed) {
+        fact->second.may_be_formed = true;
+      } else if (!fact->second.may_be_formed) {
+        return CompilationError(identifier.source_loc())
+               << "use of uninitialized variable " << identifier.name();
+      }
+      break;
+    }
+    case ExpressionKind::CallExpression: {
+      auto& call = cast<CallExpression>(*expression);
+      CARBON_RETURN_IF_ERROR(
+          ResolveUnformed(&call.argument(), flow_facts, /*set_formed=*/false));
+      break;
+    }
+    case ExpressionKind::TupleLiteral:
+      for (Nonnull<const Expression*> field :
+           cast<TupleLiteral>(*expression).fields()) {
+        CARBON_RETURN_IF_ERROR(
+            ResolveUnformed(field, flow_facts, /*set_formed=*/false));
+      }
+      break;
+    case ExpressionKind::OperatorExpression: {
+      auto& opt_exp = cast<OperatorExpression>(*expression);
+      if (opt_exp.op() == Operator::AddressOf) {
+        CARBON_CHECK(opt_exp.arguments().size() == 1)
+            << "OperatorExpression with op & can only have 1 argument";
+        CARBON_RETURN_IF_ERROR(
+            // When a variable is taken address of, defer the unformed check to
+            // runtime. A more sound analysis can be implemented when a
+            // points-to analysis is available.
+            ResolveUnformed(opt_exp.arguments().front(), flow_facts,
+                            /*set_formed=*/true));
+      } else {
+        for (Nonnull<const Expression*> operand : opt_exp.arguments()) {
+          CARBON_RETURN_IF_ERROR(
+              ResolveUnformed(operand, flow_facts, /*set_formed=*/false));
+        }
+      }
+      break;
+    }
+    case ExpressionKind::DotSelfExpression:
+    case ExpressionKind::IntLiteral:
+    case ExpressionKind::BoolLiteral:
+    case ExpressionKind::BoolTypeLiteral:
+    case ExpressionKind::IntTypeLiteral:
+    case ExpressionKind::StringLiteral:
+    case ExpressionKind::StringTypeLiteral:
+    case ExpressionKind::TypeTypeLiteral:
+    case ExpressionKind::ContinuationTypeLiteral:
+    case ExpressionKind::ValueLiteral:
+    case ExpressionKind::IndexExpression:
+    case ExpressionKind::SimpleMemberAccessExpression:
+    case ExpressionKind::CompoundMemberAccessExpression:
+    case ExpressionKind::IfExpression:
+    case ExpressionKind::WhereExpression:
+    case ExpressionKind::StructLiteral:
+    case ExpressionKind::StructTypeLiteral:
+    case ExpressionKind::IntrinsicExpression:
+    case ExpressionKind::UnimplementedExpression:
+    case ExpressionKind::FunctionTypeLiteral:
+    case ExpressionKind::ArrayTypeLiteral:
+    case ExpressionKind::InstantiateImpl:
+      break;
+  }
+  return Success();
+}
+
+static auto ResolveUnformed(
+    Nonnull<const Pattern*> pattern,
+    std::unordered_map<Nonnull<const AstNode*>, FlowFact>& flow_facts,
+    const bool has_init) -> ErrorOr<Success> {
+  switch (pattern->kind()) {
+    case PatternKind::BindingPattern:
+      flow_facts.insert(
+          {Nonnull<const AstNode*>(&cast<BindingPattern>(*pattern)),
+           {has_init}});
+      break;
+    case PatternKind::TuplePattern:
+      for (Nonnull<const Pattern*> field :
+           cast<TuplePattern>(*pattern).fields()) {
+        CARBON_RETURN_IF_ERROR(ResolveUnformed(field, flow_facts, has_init));
+      }
+      break;
+    case PatternKind::GenericBinding:
+    case PatternKind::AlternativePattern:
+    case PatternKind::ExpressionPattern:
+    case PatternKind::AutoPattern:
+    case PatternKind::VarPattern:
+    case PatternKind::AddrPattern:
+      // do nothing
+      break;
+  }
+  return Success();
+}
+
+static auto ResolveUnformed(
+    Nonnull<const Statement*> statement,
+    std::unordered_map<Nonnull<const AstNode*>, FlowFact>& flow_facts)
+    -> ErrorOr<Success> {
+  switch (statement->kind()) {
+    case StatementKind::Block: {
+      auto& block = cast<Block>(*statement);
+      for (auto* block_statement : block.statements()) {
+        CARBON_RETURN_IF_ERROR(ResolveUnformed(block_statement, flow_facts));
+      }
+      break;
+    }
+    case StatementKind::VariableDefinition: {
+      auto& def = cast<VariableDefinition>(*statement);
+      CARBON_RETURN_IF_ERROR(ResolveUnformed(&def.pattern(), flow_facts,
+                                             /*has_init=*/def.has_init()));
+      break;
+    }
+    case StatementKind::ReturnVar:
+      // TODO: @slaterlatiao: Implement this flow.
+      break;
+    case StatementKind::ReturnExpression: {
+      auto& ret_exp_stmt = cast<ReturnExpression>(*statement);
+      CARBON_RETURN_IF_ERROR(ResolveUnformed(&ret_exp_stmt.expression(),
+                                             flow_facts, /*set_formed=*/false));
+      break;
+    }
+    case StatementKind::Assign: {
+      auto& assign = cast<Assign>(*statement);
+      CARBON_RETURN_IF_ERROR(
+          ResolveUnformed(&assign.lhs(), flow_facts, /*set_formed=*/true));
+      CARBON_RETURN_IF_ERROR(
+          ResolveUnformed(&assign.rhs(), flow_facts, /*set_formed=*/false));
+      break;
+    }
+    case StatementKind::ExpressionStatement: {
+      auto& exp_stmt = cast<ExpressionStatement>(*statement);
+      CARBON_RETURN_IF_ERROR(ResolveUnformed(&exp_stmt.expression(), flow_facts,
+                                             /*set_formed=*/false));
+      break;
+    }
+    case StatementKind::Break:
+    case StatementKind::Continue:
+    case StatementKind::If:
+    case StatementKind::While:
+    case StatementKind::Match:
+    case StatementKind::Continuation:
+    case StatementKind::Run:
+    case StatementKind::Await:
+      // do nothing
+      break;
+  }
+  return Success();
+}
+
+static auto ResolveUnformed(Nonnull<const Declaration*> declaration)
+    -> ErrorOr<Success> {
+  switch (declaration->kind()) {
+    // Checks formed/unformed state intraprocedurally.
+    // Can be extended to an interprocedural analysis when a call graph is
+    // available.
+    case DeclarationKind::FunctionDeclaration: {
+      auto& function = cast<FunctionDeclaration>(*declaration);
+      if (function.body().has_value()) {
+        std::unordered_map<Nonnull<const AstNode*>, FlowFact> flow_facts;
+        CARBON_RETURN_IF_ERROR(ResolveUnformed(*function.body(), flow_facts));
+      }
+      break;
+    }
+    case DeclarationKind::ClassDeclaration:
+    case DeclarationKind::InterfaceDeclaration:
+    case DeclarationKind::ImplDeclaration:
+    case DeclarationKind::ChoiceDeclaration:
+    case DeclarationKind::VariableDeclaration:
+    case DeclarationKind::AssociatedConstantDeclaration:
+    case DeclarationKind::SelfDeclaration:
+    case DeclarationKind::AliasDeclaration:
+      // do nothing
+      break;
+  }
+  return Success();
+}
+
+auto ResolveUnformed(const AST& ast) -> ErrorOr<Success> {
+  for (auto declaration : ast.declarations) {
+    CARBON_RETURN_IF_ERROR(ResolveUnformed(declaration));
+  }
+  return Success();
+}
+
+}  // namespace Carbon
diff --git a/explorer/interpreter/resolve_unformed.h b/explorer/interpreter/resolve_unformed.h
new file mode 100644
index 000000000000..3e65b2be62ce
--- /dev/null
+++ b/explorer/interpreter/resolve_unformed.h
@@ -0,0 +1,20 @@
+// Part of the Carbon Language project, under the Apache License v2.0 with LLVM
+// Exceptions. See /LICENSE for license information.
+// SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
+
+#ifndef CARBON_EXPLORER_INTERPRETER_RESOLVE_UNFORMED_H_
+#define CARBON_EXPLORER_INTERPRETER_RESOLVE_UNFORMED_H_
+
+#include "explorer/ast/ast.h"
+#include "explorer/common/nonnull.h"
+
+namespace Carbon {
+
+// An intraprocedural forward analysis that checks the may-be-formed states on
+// local variables. Returns compilation error on usage of must-be-unformed
+// variables.
+auto ResolveUnformed(const AST& ast) -> ErrorOr<Success>;
+
+}  // namespace Carbon
+
+#endif  // CARBON_EXPLORER_INTERPRETER_RESOLVE_UNFORMED_H_
diff --git a/explorer/testdata/basic_syntax/trace.carbon b/explorer/testdata/basic_syntax/trace.carbon
index 2dfca109f58c..b38caa4626ee 100644
--- a/explorer/testdata/basic_syntax/trace.carbon
+++ b/explorer/testdata/basic_syntax/trace.carbon
@@ -13,7 +13,8 @@
 // CHECK: interface ImplicitAs {
 // CHECK: ********** type checking **********
 // CHECK: ** declaring interface ImplicitAs
-// CHECK: ********** type checking complete **********
+// CHECK: ********** resolving unformed variables **********
+// CHECK: ********** printing declarations **********
 // CHECK: interface ImplicitAs {
 // CHECK: ********** starting execution **********
 // CHECK: ********** initializing globals **********
diff --git a/explorer/testdata/uninitialized/fail_local_uninitialized_assign.carbon b/explorer/testdata/uninitialized/fail_local_uninitialized_assign.carbon
index 732c5764ad8e..1109176e9aea 100644
--- a/explorer/testdata/uninitialized/fail_local_uninitialized_assign.carbon
+++ b/explorer/testdata/uninitialized/fail_local_uninitialized_assign.carbon
@@ -13,7 +13,7 @@ package ExplorerTest api;
 fn Main() -> i32 {
   var x: i32;
   var y: i32;
-  // CHECK: RUNTIME ERROR: {{.*}}/explorer/testdata/uninitialized/fail_local_uninitialized_assign.carbon:[[@LINE+1]]: undefined behavior: access to uninitialized value Uninit<Placeholder<x>>
+  // CHECK: COMPILATION ERROR: {{.*}}/explorer/testdata/uninitialized/fail_local_uninitialized_assign.carbon:[[@LINE+1]]: use of uninitialized variable x
   y = x;
   return y;
 }
diff --git a/explorer/testdata/uninitialized/fail_local_uninitialized_init.carbon b/explorer/testdata/uninitialized/fail_local_uninitialized_init.carbon
index f34756b34bcb..50e5b31c2319 100644
--- a/explorer/testdata/uninitialized/fail_local_uninitialized_init.carbon
+++ b/explorer/testdata/uninitialized/fail_local_uninitialized_init.carbon
@@ -12,7 +12,7 @@ package ExplorerTest api;
 
 fn Main() -> i32 {
   var x: i32;
-  // CHECK: RUNTIME ERROR: {{.*}}/explorer/testdata/uninitialized/fail_local_uninitialized_init.carbon:[[@LINE+1]]: undefined behavior: access to uninitialized value Uninit<Placeholder<x>>
   var y: i32 = x;
+  // CHECK: COMPILATION ERROR: {{.*}}/explorer/testdata/uninitialized/fail_local_uninitialized_init.carbon:[[@LINE+1]]: use of uninitialized variable x
   return x;
 }
diff --git a/explorer/testdata/uninitialized/fail_local_uninitialized_param.carbon b/explorer/testdata/uninitialized/fail_local_uninitialized_param.carbon
index 612bf341d178..2e2530ed15cc 100644
--- a/explorer/testdata/uninitialized/fail_local_uninitialized_param.carbon
+++ b/explorer/testdata/uninitialized/fail_local_uninitialized_param.carbon
@@ -16,6 +16,6 @@ fn AddInt(a: i32, b: i32) -> auto {
 
 fn Main() -> i32 {
   var x: i32;
-  // CHECK: RUNTIME ERROR: {{.*}}/explorer/testdata/uninitialized/fail_local_uninitialized_param.carbon:[[@LINE+1]]: undefined behavior: access to uninitialized value Uninit<Placeholder<x>>
+  // CHECK: COMPILATION ERROR: {{.*}}/explorer/testdata/uninitialized/fail_local_uninitialized_param.carbon:[[@LINE+1]]: use of uninitialized variable x
   return AddInt(x, 2);
 }
diff --git a/explorer/testdata/uninitialized/fail_local_uninitialized_pattern.carbon b/explorer/testdata/uninitialized/fail_local_uninitialized_pattern.carbon
index eaeb22bc60c8..c9ecc3e5d72b 100644
--- a/explorer/testdata/uninitialized/fail_local_uninitialized_pattern.carbon
+++ b/explorer/testdata/uninitialized/fail_local_uninitialized_pattern.carbon
@@ -13,6 +13,6 @@ package ExplorerTest api;
 fn Main() -> i32 {
   var (x: i32, y: i32);
   x = 1;
-  // CHECK: RUNTIME ERROR: {{.*}}/explorer/testdata/uninitialized/fail_local_uninitialized_pattern.carbon:[[@LINE+1]]: undefined behavior: access to uninitialized value Uninit<Placeholder<y>>
+  // CHECK: COMPILATION ERROR: {{.*}}/explorer/testdata/uninitialized/fail_local_uninitialized_pattern.carbon:[[@LINE+1]]: use of uninitialized variable y
   return y;
 }
diff --git a/explorer/testdata/uninitialized/fail_local_uninitialized_return.carbon b/explorer/testdata/uninitialized/fail_local_uninitialized_return.carbon
index dd3e6bea0ca9..59670821eab5 100644
--- a/explorer/testdata/uninitialized/fail_local_uninitialized_return.carbon
+++ b/explorer/testdata/uninitialized/fail_local_uninitialized_return.carbon
@@ -12,6 +12,6 @@ package ExplorerTest api;
 
 fn Main() -> i32 {
   var x: i32;
-  // CHECK: RUNTIME ERROR: {{.*}}/explorer/testdata/uninitialized/fail_local_uninitialized_return.carbon:[[@LINE+1]]: undefined behavior: access to uninitialized value Uninit<Placeholder<x>>
+  // CHECK: COMPILATION ERROR: {{.*}}/explorer/testdata/uninitialized/fail_local_uninitialized_return.carbon:[[@LINE+1]]: use of uninitialized variable x
   return x;
 }