An example of what BEAM code ends up being generated for a simple TypeCheck spec.

addition.beam_disasm.ex

{:beam_file, Addition,
 [
   {:__info__, 1, 2},
   {:"__type_check_spec_for_add/2__", 0, 18},
   {:add, 2, 8},
   {:baseline_add, 2, 16},
   {:module_info, 0, 20},
   {:module_info, 1, 22}
 ], [vsn: [337339698024769425821845159222917769638]],
 [
   version: '7.6',
   options: [:dialyzer, :no_spawn_compiler_process, :from_core,
    :no_core_prepare, :no_auto_import],
   source: '...'
 ],
 [
   {:function, :__info__, 1, 2,
    [
      {:label, 1},
      {:line, 0},
      {:func_info, {:atom, Addition}, {:atom, :__info__}, 1},
      {:label, 2},
      {:select_val, {:x, 0}, {:f, 1},
       {:list,
        [
          atom: :attributes,
          f: 6,
          atom: :compile,
          f: 6,
          atom: :deprecated,
          f: 5,
          atom: :functions,
          f: 4,
          atom: :macros,
          f: 5,
          atom: :md5,
          f: 6,
          atom: :module,
          f: 3
        ]}},
      {:label, 3},
      {:move, {:atom, Addition}, {:x, 0}},
      :return,
      {:label, 4},
      {:move,
       {:literal, ["__type_check_spec_for_add/2__": 0, add: 2, baseline_add: 2]},
       {:x, 0}},
      :return,
      {:label, 5},
      {:move, nil, {:x, 0}},
      :return,
      {:label, 6},
      {:move, {:x, 0}, {:x, 1}},
      {:move, {:atom, Addition}, {:x, 0}},
      {:line, 0},
      {:call_ext_only, 2, {:extfunc, :erlang, :get_module_info, 2}}
    ]},
   {:function, :add, 2, 8,
    [
      {:line, 1},
      {:label, 7},
      {:func_info, {:atom, Addition}, {:atom, :add}, 2},
      {:label, 8},
      {:test, :is_number, {:f, 9}, [x: 0]},
      {:move, {:literal, {:ok, []}}, {:x, 2}},
      {:jump, {:f, 10}},
      {:label, 9},
      {:test_heap, 8, 2},
      {:put_tuple2, {:x, 2},
       {:list,
        [
          literal: #TypeCheck.Type< number() >,
          atom: :no_match,
          literal: %{},
          x: 0
        ]}},
      {:put_tuple2, {:x, 2}, {:list, [atom: :error, x: 2]}},
      {:label, 10},
      {:test, :is_tagged_tuple, {:f, 12}, [{:x, 2}, 2, {:atom, :ok}]},
      {:test, :is_number, {:f, 11}, [x: 1]},
      {:call_only, 2, {Addition, :"add (overridable 1)", 2}},
      {:label, 11},
      {:allocate_heap, 3, 5, 2},
      {:move, {:x, 1}, {:y, 1}},
      {:move, {:x, 0}, {:y, 2}},
      {:put_tuple2, {:y, 0},
       {:list,
        [
          literal: #TypeCheck.Type< number() >,
          atom: :no_match,
          literal: %{},
          x: 1
        ]}},
      {:line, 2},
      {:call, 0, {Addition, :"__type_check_spec_for_add/2__", 0}},
      {:put_map_assoc, {:f, 0}, {:literal, %{index: 1}}, {:x, 1}, 1,
       {:list, [atom: :problem, y: 0]}},
      {:test_heap, 9, 2},
      {:put_list, {:y, 1}, nil, {:x, 2}},
      {:put_list, {:y, 2}, {:x, 2}, {:x, 2}},
      {:put_tuple2, {:x, 0}, {:list, [x: 0, atom: :param_error, x: 1, x: 2]}},
      {:trim, 3, 0},
      {:line, 2},
      {:call_ext, 1, {:extfunc, TypeCheck.TypeError, :exception, 1}},
      {:line, 2},
      {:call_ext_last, 1, {:extfunc, :erlang, :error, 1}, 0},
      {:label, 12},
      {:allocate, 3, 3},
      {:move, {:x, 2}, {:y, 0}},
      {:move, {:x, 1}, {:y, 1}},
      {:move, {:x, 0}, {:y, 2}},
      {:line, 2},
      {:call, 0, {Addition, :"__type_check_spec_for_add/2__", 0}},
      {:get_tuple_element, {:y, 0}, 1, {:x, 1}},
      {:put_map_assoc, {:f, 0}, {:literal, %{index: 0}}, {:x, 1}, 2,
       {:list, [atom: :problem, x: 1]}},
      {:test_heap, 9, 2},
      {:put_list, {:y, 1}, nil, {:x, 2}},
      {:put_list, {:y, 2}, {:x, 2}, {:x, 2}},
      {:put_tuple2, {:x, 0}, {:list, [x: 0, atom: :param_error, x: 1, x: 2]}},
      {:trim, 3, 0},
      {:line, 2},
      {:call_ext, 1, {:extfunc, TypeCheck.TypeError, :exception, 1}},
      {:line, 2},
      {:call_ext_last, 1, {:extfunc, :erlang, :error, 1}, 0}
    ]},
   {:function, :"add (overridable 1)", 2, 14,
    [
      {:line, 3},
      {:label, 13},
      {:func_info, {:atom, Addition}, {:atom, :"add (overridable 1)"}, 2},
      {:label, 14},
      {:line, 4},
      {:gc_bif, :+, {:f, 0}, 2, [x: 0, x: 1], {:x, 0}},
      :return
    ]},
   {:function, :baseline_add, 2, 16,
    [
      {:line, 5},
      {:label, 15},
      {:func_info, {:atom, Addition}, {:atom, :baseline_add}, 2},
      {:label, 16},
      {:line, 6},
      {:gc_bif, :+, {:f, 0}, 2, [x: 0, x: 1], {:x, 0}},
      :return
    ]},
   {:function, :"__type_check_spec_for_add/2__", 0, 18,
    [
      {:line, 7},
      {:label, 17},
      {:func_info, {:atom, Addition}, {:atom, :"__type_check_spec_for_add/2__"},
       0},
      {:label, 18},
      {:allocate_zero, 2, 0},
      {:line, 7},
      {:call_ext, 0, {:extfunc, TypeCheck.Builtin, :number, 0}},
      {:move, {:x, 0}, {:y, 1}},
      {:line, 7},
      {:call_ext, 0, {:extfunc, TypeCheck.Builtin, :number, 0}},
      {:move, {:x, 0}, {:y, 0}},
      {:line, 7},
      {:call_ext, 0, {:extfunc, TypeCheck.Builtin, :number, 0}},
      {:test_heap, 4, 1},
      {:put_list, {:y, 0}, nil, {:x, 1}},
      {:put_list, {:y, 1}, {:x, 1}, {:x, 1}},
      {:put_map_assoc, {:f, 0}, {:literal, %{name: :add}}, {:x, 0}, 2,
       {:list,
        [
          atom: :__struct__,
          atom: TypeCheck.Spec,
          atom: :param_types,
          x: 1,
          atom: :return_type,
          x: 0
        ]}},
      {:deallocate, 2},
      :return
    ]},
   {:function, :module_info, 0, 20,
    [
      {:line, 0},
      {:label, 19},
      {:func_info, {:atom, Addition}, {:atom, :module_info}, 0},
      {:label, 20},
      {:move, {:atom, Addition}, {:x, 0}},
      {:line, 0},
      {:call_ext_only, 1, {:extfunc, :erlang, :get_module_info, 1}}
    ]},
   {:function, :module_info, 1, 22,
    [
      {:line, 0},
      {:label, 21},
      {:func_info, {:atom, Addition}, {:atom, :module_info}, 1},
      {:label, 22},
      {:move, {:x, 0}, {:x, 1}},
      {:move, {:atom, Addition}, {:x, 0}},
      {:line, 0},
      {:call_ext_only, 2, {:extfunc, :erlang, :get_module_info, 2}}
    ]}
 ]}

addition.ex

defmodule Addition do
  use TypeCheck
  spec add(number(), number()) :: number()
  def add(a, b) do
    a + b
  end

  def baseline_add(a, b) do
    a + b
  end
end