diff --git a/toolchain/check/BUILD b/toolchain/check/BUILD
index 8eea88a7c59a..eededb7bff00 100644
--- a/toolchain/check/BUILD
+++ b/toolchain/check/BUILD
@@ -102,6 +102,7 @@ cc_library(
     deps = [
         ":context",
         ":function",
+        ":impl",
         ":import",
         ":interface",
         "//common:check",
@@ -145,6 +146,20 @@ cc_library(
     ],
 )
 
+cc_library(
+    name = "impl",
+    srcs = ["impl.cpp"],
+    hdrs = ["impl.h"],
+    deps = [
+        ":context",
+        "//common:check",
+        "//toolchain/sem_ir:file",
+        "//toolchain/sem_ir:ids",
+        "//toolchain/sem_ir:inst",
+        "//toolchain/sem_ir:inst_kind",
+    ],
+)
+
 cc_library(
     name = "import",
     srcs = ["import.cpp"],
diff --git a/toolchain/check/context.cpp b/toolchain/check/context.cpp
index a6cab7e43795..5141fed0b8b7 100644
--- a/toolchain/check/context.cpp
+++ b/toolchain/check/context.cpp
@@ -699,6 +699,7 @@ class TypeCompleter {
       case SemIR::BuiltinKind::NamespaceType:
       case SemIR::BuiltinKind::FunctionType:
       case SemIR::BuiltinKind::BoundMethodType:
+      case SemIR::BuiltinKind::WitnessType:
         return MakeCopyValueRepr(type_id);
 
       case SemIR::BuiltinKind::StringType:
@@ -842,10 +843,11 @@ class TypeCompleter {
       case SemIR::FunctionDecl::Kind:
       case SemIR::ImplDecl::Kind:
       case SemIR::Import::Kind:
+      case SemIR::ImportRefUnused::Kind:
       case SemIR::InitializeFrom::Kind:
       case SemIR::InterfaceDecl::Kind:
+      case SemIR::InterfaceWitness::Kind:
       case SemIR::IntLiteral::Kind:
-      case SemIR::ImportRefUnused::Kind:
       case SemIR::NameRef::Kind:
       case SemIR::Namespace::Kind:
       case SemIR::Param::Kind:
diff --git a/toolchain/check/eval.cpp b/toolchain/check/eval.cpp
index 5067493e28fa..77c004c46b17 100644
--- a/toolchain/check/eval.cpp
+++ b/toolchain/check/eval.cpp
@@ -329,6 +329,9 @@ auto TryEvalInst(Context& context, SemIR::InstId inst_id, SemIR::Inst inst)
       return RebuildIfFieldsAreConstant(context, inst,
                                         &SemIR::BoundMethod::object_id,
                                         &SemIR::BoundMethod::function_id);
+    case SemIR::InterfaceWitness::Kind:
+      return RebuildIfFieldsAreConstant(context, inst,
+                                        &SemIR::InterfaceWitness::table_id);
     case SemIR::PointerType::Kind:
       return RebuildIfFieldsAreConstant(context, inst,
                                         &SemIR::PointerType::pointee_id);
diff --git a/toolchain/check/handle_impl.cpp b/toolchain/check/handle_impl.cpp
index 560f8fda6a38..c8290255f583 100644
--- a/toolchain/check/handle_impl.cpp
+++ b/toolchain/check/handle_impl.cpp
@@ -5,6 +5,7 @@
 #include "toolchain/check/context.h"
 #include "toolchain/check/convert.h"
 #include "toolchain/check/decl_name_stack.h"
+#include "toolchain/check/impl.h"
 #include "toolchain/check/modifiers.h"
 #include "toolchain/parse/typed_nodes.h"
 #include "toolchain/sem_ir/ids.h"
@@ -270,11 +271,14 @@ auto HandleImplDefinition(Context& context,
                           Parse::ImplDefinitionId /*parse_node*/) -> bool {
   auto impl_id =
       context.node_stack().Pop<Parse::NodeKind::ImplDefinitionStart>();
+
+  if (!context.impls().Get(impl_id).is_defined()) {
+    context.impls().Get(impl_id).witness_id =
+        BuildImplWitness(context, impl_id);
+  }
+
   context.inst_block_stack().Pop();
   context.decl_name_stack().PopScope();
-
-  // The impl is now fully defined.
-  context.impls().Get(impl_id).defined = true;
   return true;
 }
 
diff --git a/toolchain/check/impl.cpp b/toolchain/check/impl.cpp
new file mode 100644
index 000000000000..776cfb789165
--- /dev/null
+++ b/toolchain/check/impl.cpp
@@ -0,0 +1,37 @@
+// 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 "toolchain/check/impl.h"
+
+#include "toolchain/check/context.h"
+#include "toolchain/sem_ir/ids.h"
+#include "toolchain/sem_ir/impl.h"
+
+namespace Carbon::Check {
+
+auto BuildImplWitness(Context& context, SemIR::ImplId impl_id)
+    -> SemIR::InstId {
+  auto& impl = context.impls().Get(impl_id);
+  CARBON_CHECK(impl.is_being_defined());
+
+  // TODO: Handle non-interface constraints.
+  auto interface_type =
+      context.types().TryGetAs<SemIR::InterfaceType>(impl.constraint_id);
+  if (!interface_type) {
+    context.TODO(context.insts().GetParseNode(impl.definition_id),
+                 "impl as non-interface");
+    return SemIR::InstId::BuiltinError;
+  }
+
+  auto interface_id = interface_type->interface_id;
+
+  // TODO: Form the witness table.
+
+  auto table_id = context.inst_blocks().Add({});
+  return context.AddInst(SemIR::InterfaceWitness{
+      context.GetBuiltinType(SemIR::BuiltinKind::WitnessType), interface_id,
+      table_id});
+}
+
+}  // namespace Carbon::Check
diff --git a/toolchain/check/impl.h b/toolchain/check/impl.h
new file mode 100644
index 000000000000..2d5471a0183d
--- /dev/null
+++ b/toolchain/check/impl.h
@@ -0,0 +1,18 @@
+// 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_TOOLCHAIN_CHECK_IMPL_H_
+#define CARBON_TOOLCHAIN_CHECK_IMPL_H_
+
+#include "toolchain/check/context.h"
+#include "toolchain/sem_ir/ids.h"
+
+namespace Carbon::Check {
+
+// Builds and returns a witness for the impl `impl_id`.
+auto BuildImplWitness(Context& context, SemIR::ImplId impl_id) -> SemIR::InstId;
+
+}  // namespace Carbon::Check
+
+#endif  // CARBON_TOOLCHAIN_CHECK_IMPL_H_
diff --git a/toolchain/check/testdata/basics/builtin_insts.carbon b/toolchain/check/testdata/basics/builtin_insts.carbon
index a3aaa7b61cc0..b98225a3b80e 100644
--- a/toolchain/check/testdata/basics/builtin_insts.carbon
+++ b/toolchain/check/testdata/basics/builtin_insts.carbon
@@ -28,6 +28,7 @@
 // CHECK:STDOUT:     instFunctionType: {kind: ImportRefUsed, arg0: ir0, arg1: instFunctionType, type: typeTypeType}
 // CHECK:STDOUT:     instBoundMethodType: {kind: ImportRefUsed, arg0: ir0, arg1: instBoundMethodType, type: typeTypeType}
 // CHECK:STDOUT:     instNamespaceType: {kind: ImportRefUsed, arg0: ir0, arg1: instNamespaceType, type: typeTypeType}
+// CHECK:STDOUT:     instWitnessType: {kind: ImportRefUsed, arg0: ir0, arg1: instWitnessType, type: typeTypeType}
 // CHECK:STDOUT:     inst+0:          {kind: Namespace, arg0: name_scope0, arg1: inst<invalid>, type: type0}
 // CHECK:STDOUT:   constant_values:
 // CHECK:STDOUT:     instTypeType:    template instTypeType
@@ -39,6 +40,7 @@
 // CHECK:STDOUT:     instFunctionType: template instFunctionType
 // CHECK:STDOUT:     instBoundMethodType: template instBoundMethodType
 // CHECK:STDOUT:     instNamespaceType: template instNamespaceType
+// CHECK:STDOUT:     instWitnessType: template instWitnessType
 // CHECK:STDOUT:     inst+0:          template inst+0
 // CHECK:STDOUT:   inst_blocks:
 // CHECK:STDOUT:     empty:           {}
diff --git a/toolchain/check/testdata/impl/basic.carbon b/toolchain/check/testdata/impl/basic.carbon
index d5efc0fab146..549cbcc73f87 100644
--- a/toolchain/check/testdata/impl/basic.carbon
+++ b/toolchain/check/testdata/impl/basic.carbon
@@ -18,6 +18,7 @@ impl i32 as Simple {
 // CHECK:STDOUT:   %.1: type = interface_type @Simple [template]
 // CHECK:STDOUT:   %.2: type = assoc_entity_type @Simple, <function> [template]
 // CHECK:STDOUT:   %.3: <associated <function> in Simple> = assoc_entity element0, @Simple.%F [template]
+// CHECK:STDOUT:   %.4: <witness> = interface_witness @Simple, () [template]
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: file {
@@ -43,9 +44,11 @@ impl i32 as Simple {
 // CHECK:STDOUT:
 // CHECK:STDOUT: impl @impl: i32 as Simple {
 // CHECK:STDOUT:   %F: <function> = fn_decl @F.2 [template] {}
+// CHECK:STDOUT:   %.1: <witness> = interface_witness @Simple, () [template = constants.%.4]
 // CHECK:STDOUT:
 // CHECK:STDOUT: !members:
 // CHECK:STDOUT:   .F = %F
+// CHECK:STDOUT:   witness = %.1
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: fn @F.1();
diff --git a/toolchain/check/testdata/impl/empty.carbon b/toolchain/check/testdata/impl/empty.carbon
index f42759dca791..6020762c4c1e 100644
--- a/toolchain/check/testdata/impl/empty.carbon
+++ b/toolchain/check/testdata/impl/empty.carbon
@@ -14,6 +14,7 @@ impl i32 as Empty {
 // CHECK:STDOUT:
 // CHECK:STDOUT: constants {
 // CHECK:STDOUT:   %.1: type = interface_type @Empty [template]
+// CHECK:STDOUT:   %.2: <witness> = interface_witness @Empty, () [template]
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: file {
@@ -34,5 +35,10 @@ impl i32 as Empty {
 // CHECK:STDOUT:   witness = ()
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: impl @impl: i32 as Empty {}
+// CHECK:STDOUT: impl @impl: i32 as Empty {
+// CHECK:STDOUT:   %.1: <witness> = interface_witness @Empty, () [template = constants.%.2]
+// CHECK:STDOUT:
+// CHECK:STDOUT: !members:
+// CHECK:STDOUT:   witness = %.1
+// CHECK:STDOUT: }
 // CHECK:STDOUT:
diff --git a/toolchain/check/testdata/impl/fail_extend_impl_forall.carbon b/toolchain/check/testdata/impl/fail_extend_impl_forall.carbon
index 938c9c90d6ed..95250bd4b4d8 100644
--- a/toolchain/check/testdata/impl/fail_extend_impl_forall.carbon
+++ b/toolchain/check/testdata/impl/fail_extend_impl_forall.carbon
@@ -12,9 +12,12 @@ interface GenericInterface(T:! type) {
 }
 
 class C {
-  // CHECK:STDERR: fail_extend_impl_forall.carbon:[[@LINE+6]]:3: ERROR: Cannot `extend` a parameterized `impl`.
+  // CHECK:STDERR: fail_extend_impl_forall.carbon:[[@LINE+9]]:3: ERROR: Cannot `extend` a parameterized `impl`.
   // CHECK:STDERR:   extend impl forall [T:! type] as GenericInterface(T) {
   // CHECK:STDERR:   ^~~~~~
+  // CHECK:STDERR: fail_extend_impl_forall.carbon:[[@LINE+6]]:3: ERROR: Semantics TODO: `impl as non-interface`.
+  // CHECK:STDERR:   extend impl forall [T:! type] as GenericInterface(T) {
+  // CHECK:STDERR:   ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
   // CHECK:STDERR: fail_extend_impl_forall.carbon:[[@LINE+3]]:36: ERROR: Value of type `type` is not callable.
   // CHECK:STDERR:   extend impl forall [T:! type] as GenericInterface(T) {
   // CHECK:STDERR:                                    ^~~~~~~~~~~~~~~~~
@@ -62,21 +65,22 @@ class C {
 // CHECK:STDOUT:
 // CHECK:STDOUT: impl @impl: C as <error> {
 // CHECK:STDOUT:   %F: <function> = fn_decl @F.2 [template] {
-// CHECK:STDOUT:     %T.ref: type = name_ref T, @C.%T.loc21_23.2 [symbolic = @C.%T.loc21_23.2]
-// CHECK:STDOUT:     %x.loc22_10.1: T = param x
-// CHECK:STDOUT:     %x.loc22_10.2: T = bind_name x, %x.loc22_10.1
+// CHECK:STDOUT:     %T.ref: type = name_ref T, @C.%T.loc24_23.2 [symbolic = @C.%T.loc24_23.2]
+// CHECK:STDOUT:     %x.loc25_10.1: T = param x
+// CHECK:STDOUT:     %x.loc25_10.2: T = bind_name x, %x.loc25_10.1
 // CHECK:STDOUT:   }
 // CHECK:STDOUT:
 // CHECK:STDOUT: !members:
 // CHECK:STDOUT:   .F = %F
+// CHECK:STDOUT:   witness = <error>
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: class @C {
 // CHECK:STDOUT:   impl_decl @impl {
-// CHECK:STDOUT:     %T.loc21_23.1: type = param T
-// CHECK:STDOUT:     %T.loc21_23.2: type = bind_symbolic_name T, %T.loc21_23.1 [symbolic]
+// CHECK:STDOUT:     %T.loc24_23.1: type = param T
+// CHECK:STDOUT:     %T.loc24_23.2: type = bind_symbolic_name T, %T.loc24_23.1 [symbolic]
 // CHECK:STDOUT:     %GenericInterface.ref: type = name_ref GenericInterface, file.%GenericInterface.decl [template = constants.%.1]
-// CHECK:STDOUT:     %T.ref: type = name_ref T, %T.loc21_23.2 [symbolic = %T.loc21_23.2]
+// CHECK:STDOUT:     %T.ref: type = name_ref T, %T.loc24_23.2 [symbolic = %T.loc24_23.2]
 // CHECK:STDOUT:   }
 // CHECK:STDOUT:
 // CHECK:STDOUT: !members:
@@ -86,7 +90,7 @@ class C {
 // CHECK:STDOUT:
 // CHECK:STDOUT: fn @F.1(@GenericInterface.%x.loc11_8.2: T);
 // CHECK:STDOUT:
-// CHECK:STDOUT: fn @F.2(@impl.%x.loc22_10.2: T) {
+// CHECK:STDOUT: fn @F.2(@impl.%x.loc25_10.2: T) {
 // CHECK:STDOUT: !entry:
 // CHECK:STDOUT:   return
 // CHECK:STDOUT: }
diff --git a/toolchain/check/testdata/impl/fail_extend_impl_scope.carbon b/toolchain/check/testdata/impl/fail_extend_impl_scope.carbon
index 8f60dd9e9526..023c4a38b913 100644
--- a/toolchain/check/testdata/impl/fail_extend_impl_scope.carbon
+++ b/toolchain/check/testdata/impl/fail_extend_impl_scope.carbon
@@ -15,6 +15,7 @@ extend impl i32 as I {}
 // CHECK:STDOUT:
 // CHECK:STDOUT: constants {
 // CHECK:STDOUT:   %.1: type = interface_type @I [template]
+// CHECK:STDOUT:   %.2: <witness> = interface_witness @I, () [template]
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: file {
@@ -35,5 +36,10 @@ extend impl i32 as I {}
 // CHECK:STDOUT:   witness = ()
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: impl @impl: i32 as I {}
+// CHECK:STDOUT: impl @impl: i32 as I {
+// CHECK:STDOUT:   %.1: <witness> = interface_witness @I, () [template = constants.%.2]
+// CHECK:STDOUT:
+// CHECK:STDOUT: !members:
+// CHECK:STDOUT:   witness = %.1
+// CHECK:STDOUT: }
 // CHECK:STDOUT:
diff --git a/toolchain/check/testdata/impl/fail_extend_impl_type_as.carbon b/toolchain/check/testdata/impl/fail_extend_impl_type_as.carbon
index c2a3caa4035b..ea5f7cd054e8 100644
--- a/toolchain/check/testdata/impl/fail_extend_impl_type_as.carbon
+++ b/toolchain/check/testdata/impl/fail_extend_impl_type_as.carbon
@@ -38,7 +38,8 @@ class E {
 // CHECK:STDOUT: constants {
 // CHECK:STDOUT:   %.1: type = interface_type @I [template]
 // CHECK:STDOUT:   %C: type = class_type @C [template]
-// CHECK:STDOUT:   %.2: type = struct_type {} [template]
+// CHECK:STDOUT:   %.2: <witness> = interface_witness @I, () [template]
+// CHECK:STDOUT:   %.3: type = struct_type {} [template]
 // CHECK:STDOUT:   %D: type = class_type @D [template]
 // CHECK:STDOUT:   %E: type = class_type @E [template]
 // CHECK:STDOUT: }
@@ -64,11 +65,21 @@ class E {
 // CHECK:STDOUT:   witness = ()
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: impl @impl.1: i32 as I {}
+// CHECK:STDOUT: impl @impl.1: i32 as I {
+// CHECK:STDOUT:   %.1: <witness> = interface_witness @I, () [template = constants.%.2]
+// CHECK:STDOUT:
+// CHECK:STDOUT: !members:
+// CHECK:STDOUT:   witness = %.1
+// CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: impl @impl.2: D as I;
 // CHECK:STDOUT:
-// CHECK:STDOUT: impl @impl.3: E as I {}
+// CHECK:STDOUT: impl @impl.3: E as I {
+// CHECK:STDOUT:   %.1: <witness> = interface_witness @I, () [template = constants.%.2]
+// CHECK:STDOUT:
+// CHECK:STDOUT: !members:
+// CHECK:STDOUT:   witness = %.1
+// CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: class @C {
 // CHECK:STDOUT:   impl_decl @impl.1 {
diff --git a/toolchain/check/testdata/impl/fail_impl_as_scope.carbon b/toolchain/check/testdata/impl/fail_impl_as_scope.carbon
index feb847aaf171..dc8f64cdb4b3 100644
--- a/toolchain/check/testdata/impl/fail_impl_as_scope.carbon
+++ b/toolchain/check/testdata/impl/fail_impl_as_scope.carbon
@@ -21,6 +21,7 @@ impl as Simple {
 // CHECK:STDOUT:   %.1: type = interface_type @Simple [template]
 // CHECK:STDOUT:   %.2: type = assoc_entity_type @Simple, <function> [template]
 // CHECK:STDOUT:   %.3: <associated <function> in Simple> = assoc_entity element0, @Simple.%F [template]
+// CHECK:STDOUT:   %.4: <witness> = interface_witness @Simple, () [template]
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: file {
@@ -46,9 +47,11 @@ impl as Simple {
 // CHECK:STDOUT:
 // CHECK:STDOUT: impl @impl: <error> as Simple {
 // CHECK:STDOUT:   %F: <function> = fn_decl @F.2 [template] {}
+// CHECK:STDOUT:   %.1: <witness> = interface_witness @Simple, () [template = constants.%.4]
 // CHECK:STDOUT:
 // CHECK:STDOUT: !members:
 // CHECK:STDOUT:   .F = %F
+// CHECK:STDOUT:   witness = %.1
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: fn @F.1();
diff --git a/toolchain/check/testdata/impl/fail_impl_bad_interface.carbon b/toolchain/check/testdata/impl/fail_impl_bad_interface.carbon
index 797a490d592f..ac13e0ed5301 100644
--- a/toolchain/check/testdata/impl/fail_impl_bad_interface.carbon
+++ b/toolchain/check/testdata/impl/fail_impl_bad_interface.carbon
@@ -4,6 +4,9 @@
 //
 // AUTOUPDATE
 
+// CHECK:STDERR: fail_impl_bad_interface.carbon:[[@LINE+6]]:1: ERROR: Semantics TODO: `impl as non-interface`.
+// CHECK:STDERR: impl i32 as false {}
+// CHECK:STDERR: ^~~~~~~~~~~~~~~~~~~
 // CHECK:STDERR: fail_impl_bad_interface.carbon:[[@LINE+3]]:13: ERROR: Cannot implicitly convert from `bool` to `type`.
 // CHECK:STDERR: impl i32 as false {}
 // CHECK:STDERR:             ^~~~~
@@ -18,9 +21,12 @@ impl i32 as false {}
 // CHECK:STDOUT: file {
 // CHECK:STDOUT:   package: <namespace> = namespace [template] {}
 // CHECK:STDOUT:   impl_decl @impl {
-// CHECK:STDOUT:     %.loc10: bool = bool_literal false [template = constants.%.1]
+// CHECK:STDOUT:     %.loc13: bool = bool_literal false [template = constants.%.1]
 // CHECK:STDOUT:   }
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: impl @impl: i32 as <error> {}
+// CHECK:STDOUT: impl @impl: i32 as <error> {
+// CHECK:STDOUT: !members:
+// CHECK:STDOUT:   witness = <error>
+// CHECK:STDOUT: }
 // CHECK:STDOUT:
diff --git a/toolchain/check/testdata/impl/fail_impl_bad_type.carbon b/toolchain/check/testdata/impl/fail_impl_bad_type.carbon
index 1369354f00ac..e16d9a3532f2 100644
--- a/toolchain/check/testdata/impl/fail_impl_bad_type.carbon
+++ b/toolchain/check/testdata/impl/fail_impl_bad_type.carbon
@@ -16,6 +16,7 @@ impl true as I {}
 // CHECK:STDOUT: constants {
 // CHECK:STDOUT:   %.1: type = interface_type @I [template]
 // CHECK:STDOUT:   %.2: bool = bool_literal true [template]
+// CHECK:STDOUT:   %.3: <witness> = interface_witness @I, () [template]
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: file {
@@ -37,5 +38,10 @@ impl true as I {}
 // CHECK:STDOUT:   witness = ()
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: impl @impl: <error> as I {}
+// CHECK:STDOUT: impl @impl: <error> as I {
+// CHECK:STDOUT:   %.1: <witness> = interface_witness @I, () [template = constants.%.3]
+// CHECK:STDOUT:
+// CHECK:STDOUT: !members:
+// CHECK:STDOUT:   witness = %.1
+// CHECK:STDOUT: }
 // CHECK:STDOUT:
diff --git a/toolchain/check/testdata/impl/fail_redefinition.carbon b/toolchain/check/testdata/impl/fail_redefinition.carbon
index 2d20d4e133ea..5ad25e9e2b5b 100644
--- a/toolchain/check/testdata/impl/fail_redefinition.carbon
+++ b/toolchain/check/testdata/impl/fail_redefinition.carbon
@@ -20,6 +20,7 @@ impl i32 as I {}
 // CHECK:STDOUT:
 // CHECK:STDOUT: constants {
 // CHECK:STDOUT:   %.1: type = interface_type @I [template]
+// CHECK:STDOUT:   %.2: <witness> = interface_witness @I, () [template]
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: file {
@@ -43,5 +44,8 @@ impl i32 as I {}
 // CHECK:STDOUT:   witness = ()
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: impl @impl: i32 as I {}
+// CHECK:STDOUT: impl @impl: i32 as I {
+// CHECK:STDOUT: !members:
+// CHECK:STDOUT:   witness = <unexpected instref inst+6>
+// CHECK:STDOUT: }
 // CHECK:STDOUT:
diff --git a/toolchain/check/testdata/impl/fail_todo_extend_impl.carbon b/toolchain/check/testdata/impl/fail_todo_extend_impl.carbon
index d4a5366df4eb..3a22b0301342 100644
--- a/toolchain/check/testdata/impl/fail_todo_extend_impl.carbon
+++ b/toolchain/check/testdata/impl/fail_todo_extend_impl.carbon
@@ -34,9 +34,10 @@ fn G(c: C) {
 // CHECK:STDOUT:   %.2: type = assoc_entity_type @HasF, <function> [template]
 // CHECK:STDOUT:   %.3: <associated <function> in HasF> = assoc_entity element0, @HasF.%F [template]
 // CHECK:STDOUT:   %C: type = class_type @C [template]
-// CHECK:STDOUT:   %.4: type = struct_type {} [template]
-// CHECK:STDOUT:   %.5: type = tuple_type () [template]
-// CHECK:STDOUT:   %.6: type = ptr_type {} [template]
+// CHECK:STDOUT:   %.4: <witness> = interface_witness @HasF, () [template]
+// CHECK:STDOUT:   %.5: type = struct_type {} [template]
+// CHECK:STDOUT:   %.6: type = tuple_type () [template]
+// CHECK:STDOUT:   %.7: type = ptr_type {} [template]
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: file {
@@ -67,9 +68,11 @@ fn G(c: C) {
 // CHECK:STDOUT:
 // CHECK:STDOUT: impl @impl: C as HasF {
 // CHECK:STDOUT:   %F: <function> = fn_decl @F.2 [template] {}
+// CHECK:STDOUT:   %.1: <witness> = interface_witness @HasF, () [template = constants.%.4]
 // CHECK:STDOUT:
 // CHECK:STDOUT: !members:
 // CHECK:STDOUT:   .F = %F
+// CHECK:STDOUT:   witness = %.1
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: class @C {
diff --git a/toolchain/check/testdata/impl/impl_as.carbon b/toolchain/check/testdata/impl/impl_as.carbon
index e07442e5d977..4b43b2ae33be 100644
--- a/toolchain/check/testdata/impl/impl_as.carbon
+++ b/toolchain/check/testdata/impl/impl_as.carbon
@@ -21,7 +21,8 @@ class C {
 // CHECK:STDOUT:   %.2: type = assoc_entity_type @Simple, <function> [template]
 // CHECK:STDOUT:   %.3: <associated <function> in Simple> = assoc_entity element0, @Simple.%F [template]
 // CHECK:STDOUT:   %C: type = class_type @C [template]
-// CHECK:STDOUT:   %.4: type = struct_type {} [template]
+// CHECK:STDOUT:   %.4: <witness> = interface_witness @Simple, () [template]
+// CHECK:STDOUT:   %.5: type = struct_type {} [template]
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: file {
@@ -46,9 +47,11 @@ class C {
 // CHECK:STDOUT:
 // CHECK:STDOUT: impl @impl: C as Simple {
 // CHECK:STDOUT:   %F: <function> = fn_decl @F.2 [template] {}
+// CHECK:STDOUT:   %.1: <witness> = interface_witness @Simple, () [template = constants.%.4]
 // CHECK:STDOUT:
 // CHECK:STDOUT: !members:
 // CHECK:STDOUT:   .F = %F
+// CHECK:STDOUT:   witness = %.1
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: class @C {
diff --git a/toolchain/check/testdata/impl/impl_forall.carbon b/toolchain/check/testdata/impl/impl_forall.carbon
index c61eea6e9172..cd17fa2fafc3 100644
--- a/toolchain/check/testdata/impl/impl_forall.carbon
+++ b/toolchain/check/testdata/impl/impl_forall.carbon
@@ -18,6 +18,7 @@ impl forall [T:! type] T as Simple {
 // CHECK:STDOUT:   %.1: type = interface_type @Simple [template]
 // CHECK:STDOUT:   %.2: type = assoc_entity_type @Simple, <function> [template]
 // CHECK:STDOUT:   %.3: <associated <function> in Simple> = assoc_entity element0, @Simple.%F [template]
+// CHECK:STDOUT:   %.4: <witness> = interface_witness @Simple, () [template]
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: file {
@@ -46,9 +47,11 @@ impl forall [T:! type] T as Simple {
 // CHECK:STDOUT:
 // CHECK:STDOUT: impl @impl: T as Simple {
 // CHECK:STDOUT:   %F: <function> = fn_decl @F.2 [template] {}
+// CHECK:STDOUT:   %.1: <witness> = interface_witness @Simple, () [template = constants.%.4]
 // CHECK:STDOUT:
 // CHECK:STDOUT: !members:
 // CHECK:STDOUT:   .F = %F
+// CHECK:STDOUT:   witness = %.1
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: fn @F.1();
diff --git a/toolchain/check/testdata/impl/redeclaration.carbon b/toolchain/check/testdata/impl/redeclaration.carbon
index dd2ae3e3042b..ad29c44d5091 100644
--- a/toolchain/check/testdata/impl/redeclaration.carbon
+++ b/toolchain/check/testdata/impl/redeclaration.carbon
@@ -20,6 +20,7 @@ impl i32 as I {}
 // CHECK:STDOUT:   %.1: type = interface_type @I [template]
 // CHECK:STDOUT:   %X: type = class_type @X [template]
 // CHECK:STDOUT:   %.2: type = struct_type {} [template]
+// CHECK:STDOUT:   %.3: <witness> = interface_witness @I, () [template]
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: file {
@@ -45,7 +46,12 @@ impl i32 as I {}
 // CHECK:STDOUT:   witness = ()
 // CHECK:STDOUT: }
 // CHECK:STDOUT:
-// CHECK:STDOUT: impl @impl: i32 as I {}
+// CHECK:STDOUT: impl @impl: i32 as I {
+// CHECK:STDOUT:   %.1: <witness> = interface_witness @I, () [template = constants.%.3]
+// CHECK:STDOUT:
+// CHECK:STDOUT: !members:
+// CHECK:STDOUT:   witness = %.1
+// CHECK:STDOUT: }
 // CHECK:STDOUT:
 // CHECK:STDOUT: class @X {
 // CHECK:STDOUT:   impl_decl @impl {
diff --git a/toolchain/lower/handle.cpp b/toolchain/lower/handle.cpp
index 24405795ad6e..e2b9fdf7317a 100644
--- a/toolchain/lower/handle.cpp
+++ b/toolchain/lower/handle.cpp
@@ -246,6 +246,12 @@ auto HandleInterfaceDecl(FunctionContext& /*context*/,
   FatalErrorIfEncountered(inst);
 }
 
+auto HandleInterfaceWitness(FunctionContext& /*context*/,
+                            SemIR::InstId /*inst_id*/,
+                            SemIR::InterfaceWitness inst) -> void {
+  FatalErrorIfEncountered(inst);
+}
+
 auto HandleIntLiteral(FunctionContext& context, SemIR::InstId inst_id,
                       SemIR::IntLiteral inst) -> void {
   const llvm::APInt& i = context.sem_ir().ints().Get(inst.int_id);
diff --git a/toolchain/sem_ir/builtin_kind.def b/toolchain/sem_ir/builtin_kind.def
index f7a0bd7c8c4b..2c57f0a1fe23 100644
--- a/toolchain/sem_ir/builtin_kind.def
+++ b/toolchain/sem_ir/builtin_kind.def
@@ -73,6 +73,9 @@ CARBON_SEM_IR_BUILTIN_KIND(BoundMethodType, "<bound method>")
 // The type of namespace and imported package names.
 CARBON_SEM_IR_BUILTIN_KIND(NamespaceType, "<namespace>")
 
+// The type of witnesses.
+CARBON_SEM_IR_BUILTIN_KIND(WitnessType, "<witness>")
+
 // Keep invalid last, so that we can use values as array indices without needing
 // an invalid entry.
 CARBON_SEM_IR_BUILTIN_KIND_NAME(Invalid)
diff --git a/toolchain/sem_ir/file.cpp b/toolchain/sem_ir/file.cpp
index 48c5e011f219..4f06ff33f0d2 100644
--- a/toolchain/sem_ir/file.cpp
+++ b/toolchain/sem_ir/file.cpp
@@ -238,6 +238,7 @@ static auto GetTypePrecedence(InstKind kind) -> int {
     case ImportRefUnused::Kind:
     case InitializeFrom::Kind:
     case InterfaceDecl::Kind:
+    case InterfaceWitness::Kind:
     case IntLiteral::Kind:
     case Namespace::Kind:
     case Param::Kind:
@@ -485,6 +486,7 @@ static auto StringifyTypeExprImpl(const SemIR::File& outer_sem_ir,
       case ImportRefUnused::Kind:
       case InitializeFrom::Kind:
       case InterfaceDecl::Kind:
+      case InterfaceWitness::Kind:
       case IntLiteral::Kind:
       case Namespace::Kind:
       case Param::Kind:
@@ -591,6 +593,7 @@ auto GetExprCategory(const File& file, InstId inst_id) -> ExprCategory {
       case FacetTypeAccess::Kind:
       case InterfaceDecl::Kind:
       case InterfaceType::Kind:
+      case InterfaceWitness::Kind:
       case IntLiteral::Kind:
       case Param::Kind:
       case PointerType::Kind:
diff --git a/toolchain/sem_ir/formatter.cpp b/toolchain/sem_ir/formatter.cpp
index 882f8b58bf6b..eba0fd38d56b 100644
--- a/toolchain/sem_ir/formatter.cpp
+++ b/toolchain/sem_ir/formatter.cpp
@@ -747,7 +747,18 @@ class Formatter {
       out_ << ' ';
       OpenBrace();
       FormatCodeBlock(impl_info.body_block_id);
-      FormatNameScope(impl_info.scope_id, "!members:\n");
+
+      // Print the !members label even if the name scope is empty because we
+      // always list the witness in this section.
+      IndentLabel();
+      out_ << "!members:\n";
+      FormatNameScope(impl_info.scope_id);
+
+      Indent();
+      out_ << "witness = ";
+      FormatArg(impl_info.witness_id);
+      out_ << "\n";
+
       CloseBrace();
       out_ << '\n';
     } else {
diff --git a/toolchain/sem_ir/impl.h b/toolchain/sem_ir/impl.h
index fa36a5f546b2..c0136f1398f4 100644
--- a/toolchain/sem_ir/impl.h
+++ b/toolchain/sem_ir/impl.h
@@ -18,7 +18,12 @@ struct Impl : public Printable<Impl> {
 
   // Determines whether this impl has been fully defined. This is false until we
   // reach the `}` of the impl definition.
-  auto is_defined() const -> bool { return defined; }
+  auto is_defined() const -> bool { return witness_id.is_valid(); }
+
+  // Determines whether this impl's definition has begun but not yet ended.
+  auto is_being_defined() const -> bool {
+    return definition_id.is_valid() && !is_defined();
+  }
 
   // The following members always have values, and do not change throughout the
   // lifetime of the interface.
@@ -40,7 +45,9 @@ struct Impl : public Printable<Impl> {
   InstBlockId body_block_id = InstBlockId::Invalid;
 
   // The following members are set at the `}` of the impl definition.
-  bool defined = false;
+
+  // The witness for the impl. This can be `BuiltinError`.
+  InstId witness_id = InstId::Invalid;
 };
 
 // A collection of `Impl`s, which can be accessed by the self type and
diff --git a/toolchain/sem_ir/inst_kind.def b/toolchain/sem_ir/inst_kind.def
index 6d7a32a4bf37..7ed5f48444fd 100644
--- a/toolchain/sem_ir/inst_kind.def
+++ b/toolchain/sem_ir/inst_kind.def
@@ -56,6 +56,7 @@ CARBON_SEM_IR_INST_KIND(ImportRefUsed)
 CARBON_SEM_IR_INST_KIND(InitializeFrom)
 CARBON_SEM_IR_INST_KIND(InterfaceDecl)
 CARBON_SEM_IR_INST_KIND(InterfaceType)
+CARBON_SEM_IR_INST_KIND(InterfaceWitness)
 CARBON_SEM_IR_INST_KIND(IntLiteral)
 CARBON_SEM_IR_INST_KIND(NameRef)
 CARBON_SEM_IR_INST_KIND(Namespace)
diff --git a/toolchain/sem_ir/typed_insts.h b/toolchain/sem_ir/typed_insts.h
index 562738604367..3ad3122703c8 100644
--- a/toolchain/sem_ir/typed_insts.h
+++ b/toolchain/sem_ir/typed_insts.h
@@ -540,6 +540,17 @@ struct InterfaceType {
   // here.
 };
 
+// A witness that a type implements an interface.
+struct InterfaceWitness {
+  static constexpr auto Kind =
+      InstKind::InterfaceWitness.Define<Parse::InvalidNodeId>(
+          "interface_witness");
+
+  TypeId type_id;
+  InterfaceId interface_id;
+  InstBlockId table_id;
+};
+
 struct IntLiteral {
   // TODO: Make Parse::NodeId more specific.
   static constexpr auto Kind =