diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp
index 1cdbe5ada7a..8f73944fb20 100644
--- a/src/cbmc/bmc.cpp
+++ b/src/cbmc/bmc.cpp
@@ -639,6 +639,12 @@ void bmct::perform_symbolic_execution(
   goto_symext::get_goto_functiont get_goto_function)
 {
   symex.symex_from_entry_point_of(get_goto_function, symex_symbol_table);
+
+  if(options.get_bool_option("validate-ssa-equation"))
+  {
+    symex.validate(ns, validation_modet::INVARIANT);
+  }
+
   INVARIANT(
     options.get_bool_option("paths") || path_storage.empty(),
     "Branch points were saved even though we should have been "
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index 4731e476661..8b01624d82c 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -398,6 +398,11 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
       "symex-coverage-report",
       cmdline.get_value("symex-coverage-report"));
 
+  if(cmdline.isset("validate-ssa-equation"))
+  {
+    options.set_option("validate-ssa-equation", true);
+  }
+
   PARSE_OPTIONS_GOTO_TRACE(cmdline, options);
 }
 
diff --git a/src/goto-programs/goto_program.cpp b/src/goto-programs/goto_program.cpp
index 79a86c41d1d..f9eecb2238f 100644
--- a/src/goto-programs/goto_program.cpp
+++ b/src/goto-programs/goto_program.cpp
@@ -706,9 +706,11 @@ void goto_programt::instructiont::validate(
     break;
   case ASSIGN:
     DATA_CHECK(
+      vm,
       code.get_statement() == ID_assign,
       "assign instruction should contain an assign statement");
-    DATA_CHECK(targets.empty(), "assign instruction should not have a target");
+    DATA_CHECK(
+      vm, targets.empty(), "assign instruction should not have a target");
     break;
   case DECL:
     break;
diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h
index a27827ec7d7..d9678aa4096 100644
--- a/src/goto-symex/goto_symex.h
+++ b/src/goto-symex/goto_symex.h
@@ -61,6 +61,12 @@ struct symex_configt final
   bool partial_loops;
   mp_integer debug_level;
 
+  /// \brief Should the additional validation checks be run?
+  ///
+  /// If this flag is set the checks for renaming (both level1 and level2) are
+  /// executed in the goto_symex_statet (in the assignment method).
+  bool run_validation_checks;
+
   explicit symex_configt(const optionst &options);
 };
 
@@ -455,6 +461,11 @@ class goto_symext
       "attempting to read remaining_vccs");
     return _remaining_vccs;
   }
+
+  void validate(const namespacet &ns, const validation_modet vm) const
+  {
+    target.validate(ns, vm);
+  }
 };
 
 void symex_transition(goto_symext::statet &state);
diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp
index 125042ff065..bed62f95b28 100644
--- a/src/goto-symex/goto_symex_state.cpp
+++ b/src/goto-symex/goto_symex_state.cpp
@@ -121,32 +121,6 @@ static bool check_renaming(const exprt &expr)
   return false;
 }
 
-static void assert_l1_renaming(const exprt &expr)
-{
-  #if 1
-  if(check_renaming_l1(expr))
-  {
-    std::cerr << expr.pretty() << '\n';
-    UNREACHABLE;
-  }
-  #else
-  (void)expr;
-  #endif
-}
-
-static void assert_l2_renaming(const exprt &expr)
-{
-  #if 1
-  if(check_renaming(expr))
-  {
-    std::cerr << expr.pretty() << '\n';
-    UNREACHABLE;
-  }
-  #else
-  (void)expr;
-  #endif
-}
-
 class goto_symex_is_constantt : public is_constantt
 {
 protected:
@@ -197,15 +171,18 @@ void goto_symex_statet::assignment(
   // the type might need renaming
   rename(lhs.type(), l1_identifier, ns);
   lhs.update_type();
-  assert_l1_renaming(lhs);
+  if(run_validation_checks)
+  {
+    DATA_INVARIANT(!check_renaming_l1(lhs), "lhs renaming failed on l1");
+  }
 
-  #if 0
+#if 0
   PRECONDITION(l1_identifier != get_original_name(l1_identifier)
       || l1_identifier=="goto_symex::\\guard"
       || ns.lookup(l1_identifier).is_shared()
       || has_prefix(id2string(l1_identifier), "symex::invalid_object")
       || has_prefix(id2string(l1_identifier), "symex_dynamic::dynamic_object"));
-  #endif
+#endif
 
   // do the l2 renaming
   if(level2.current_names.find(l1_identifier)==level2.current_names.end())
@@ -216,8 +193,11 @@ void goto_symex_statet::assignment(
   // in case we happen to be multi-threaded, record the memory access
   bool is_shared=l2_thread_write_encoding(lhs, ns);
 
-  assert_l2_renaming(lhs);
-  assert_l2_renaming(rhs);
+  if(run_validation_checks)
+  {
+    DATA_INVARIANT(!check_renaming(lhs), "lhs renaming failed on l2");
+    DATA_INVARIANT(!check_renaming(rhs), "rhs renaming failed on l2");
+  }
 
   // see #305 on GitHub for a simple example and possible discussion
   if(is_shared && lhs.type().id() == ID_pointer && !allow_pointer_unsoundness)
@@ -240,8 +220,11 @@ void goto_symex_statet::assignment(
     ssa_exprt l1_lhs(lhs);
     get_l1_name(l1_lhs);
 
-    assert_l1_renaming(l1_lhs);
-    assert_l1_renaming(l1_rhs);
+    if(run_validation_checks)
+    {
+      DATA_INVARIANT(!check_renaming_l1(l1_lhs), "lhs renaming failed on l1");
+      DATA_INVARIANT(!check_renaming_l1(l1_rhs), "rhs renaming failed on l1");
+    }
 
     value_set.assign(l1_lhs, l1_rhs, ns, rhs_is_simplified, is_shared);
   }
diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h
index 77c7b343cf5..74381d907de 100644
--- a/src/goto-symex/goto_symex_state.h
+++ b/src/goto-symex/goto_symex_state.h
@@ -268,6 +268,9 @@ class goto_symex_statet final
   /// of a GOTO
   bool has_saved_next_instruction;
 
+  /// \brief Should the additional validation checks be run?
+  bool run_validation_checks;
+
 private:
   /// \brief Dangerous, do not use
   ///
diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp
index 0a5112a48c9..92872a94f9c 100644
--- a/src/goto-symex/symex_main.cpp
+++ b/src/goto-symex/symex_main.cpp
@@ -34,7 +34,8 @@ symex_configt::symex_configt(const optionst &options)
     simplify_opt(options.get_bool_option("simplify")),
     unwinding_assertions(options.get_bool_option("unwinding-assertions")),
     partial_loops(options.get_bool_option("partial-loops")),
-    debug_level(unsafe_string2int(options.get_option("debug-level")))
+    debug_level(unsafe_string2int(options.get_option("debug-level"))),
+    run_validation_checks(options.get_bool_option("validate-ssa-equation"))
 {
 }
 
@@ -307,6 +308,8 @@ void goto_symext::symex_from_entry_point_of(
 
   statet state;
 
+  state.run_validation_checks = symex_config.run_validation_checks;
+
   initialize_entry_point(
     state,
     get_goto_function,
diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp
index 513bbe61109..2198c08641c 100644
--- a/src/goto-symex/symex_target_equation.cpp
+++ b/src/goto-symex/symex_target_equation.cpp
@@ -978,3 +978,63 @@ void symex_target_equationt::SSA_stept::output(std::ostream &out) const
 
   out << "Guard: " << format(guard) << '\n';
 }
+
+/// Check that the SSA step is well-formed
+/// \param ns namespace to lookup identifiers
+/// \param vm validation mode to be used for reporting failures
+void symex_target_equationt::SSA_stept::validate(
+  const namespacet &ns,
+  const validation_modet vm) const
+{
+  validate_full_expr(guard, ns, vm);
+
+  switch(type)
+  {
+  case goto_trace_stept::typet::ASSERT:
+  case goto_trace_stept::typet::ASSUME:
+  case goto_trace_stept::typet::GOTO:
+  case goto_trace_stept::typet::CONSTRAINT:
+    validate_full_expr(cond_expr, ns, vm);
+    break;
+  case goto_trace_stept::typet::ASSIGNMENT:
+  case goto_trace_stept::typet::DECL:
+    validate_full_expr(ssa_lhs, ns, vm);
+    validate_full_expr(ssa_full_lhs, ns, vm);
+    validate_full_expr(original_full_lhs, ns, vm);
+    validate_full_expr(ssa_rhs, ns, vm);
+    DATA_CHECK(
+      vm,
+      base_type_eq(ssa_lhs.get_original_expr(), ssa_rhs, ns),
+      "Type inequality in SSA assignment\nlhs-type: " +
+        ssa_lhs.get_original_expr().type().id_string() +
+        "\nrhs-type: " + ssa_rhs.type().id_string());
+    break;
+  case goto_trace_stept::typet::INPUT:
+  case goto_trace_stept::typet::OUTPUT:
+    for(const auto &expr : io_args)
+      validate_full_expr(expr, ns, vm);
+    break;
+  case goto_trace_stept::typet::FUNCTION_CALL:
+    for(const auto &expr : ssa_function_arguments)
+      validate_full_expr(expr, ns, vm);
+  case goto_trace_stept::typet::FUNCTION_RETURN:
+  {
+    const symbolt *symbol;
+    DATA_CHECK(
+      vm,
+      called_function.empty() || !ns.lookup(called_function, symbol),
+      "unknown function identifier " + id2string(called_function));
+  }
+  break;
+  case goto_trace_stept::typet::NONE:
+  case goto_trace_stept::typet::LOCATION:
+  case goto_trace_stept::typet::DEAD:
+  case goto_trace_stept::typet::SHARED_READ:
+  case goto_trace_stept::typet::SHARED_WRITE:
+  case goto_trace_stept::typet::SPAWN:
+  case goto_trace_stept::typet::MEMORY_BARRIER:
+  case goto_trace_stept::typet::ATOMIC_BEGIN:
+  case goto_trace_stept::typet::ATOMIC_END:
+    break;
+  }
+}
diff --git a/src/goto-symex/symex_target_equation.h b/src/goto-symex/symex_target_equation.h
index cdce8c80b6d..34d5058c8f6 100644
--- a/src/goto-symex/symex_target_equation.h
+++ b/src/goto-symex/symex_target_equation.h
@@ -267,6 +267,8 @@ class symex_target_equationt:public symex_targett
       std::ostream &out) const;
 
     void output(std::ostream &out) const;
+
+    void validate(const namespacet &ns, const validation_modet vm) const;
   };
 
   std::size_t count_assertions() const
@@ -323,6 +325,12 @@ class symex_target_equationt:public symex_targett
     return false;
   }
 
+  void validate(const namespacet &ns, const validation_modet vm) const
+  {
+    for(const SSA_stept &step : SSA_steps)
+      step.validate(ns, vm);
+  }
+
 protected:
   // for enforcing sharing in the expressions stored
   merge_irept merge_irep;
diff --git a/src/util/ssa_expr.h b/src/util/ssa_expr.h
index 02f50537c69..56d4f627d8a 100644
--- a/src/util/ssa_expr.h
+++ b/src/util/ssa_expr.h
@@ -139,6 +139,27 @@ class ssa_exprt:public symbol_exprt
   /* Used to determine whether or not an identifier can be built
    * before trying and getting an exception */
   static bool can_build_identifier(const exprt &src);
+
+  static void check(
+    const exprt &expr,
+    const validation_modet vm = validation_modet::INVARIANT)
+  {
+    DATA_CHECK(
+      vm, !expr.has_operands(), "SSA expression should not have operands");
+    DATA_CHECK(
+      vm, expr.id() == ID_symbol, "SSA expression symbols are symbols");
+    DATA_CHECK(vm, expr.get_bool(ID_C_SSA_symbol), "wrong SSA expression ID");
+  }
+
+  static void validate(
+    const exprt &expr,
+    const namespacet &ns,
+    const validation_modet vm = validation_modet::INVARIANT)
+  {
+    check(expr, vm);
+    validate_full_expr(
+      static_cast<const exprt &>(expr.find(ID_expression)), ns, vm);
+  }
 };
 
 /*! \brief Cast a generic exprt to an \ref ssa_exprt
diff --git a/src/util/std_code.h b/src/util/std_code.h
index b92e933074a..0ac06412e1a 100644
--- a/src/util/std_code.h
+++ b/src/util/std_code.h
@@ -291,7 +291,7 @@ class code_assignt:public codet
     const validation_modet vm = validation_modet::INVARIANT)
   {
     DATA_CHECK(
-      code.operands().size() == 2, "assignment must have two operands");
+      vm, code.operands().size() == 2, "assignment must have two operands");
   }
 
   static void validate(
@@ -302,6 +302,7 @@ class code_assignt:public codet
     check(code, vm);
 
     DATA_CHECK(
+      vm,
       base_type_eq(code.op0().type(), code.op1().type(), ns),
       "lhs and rhs of assignment must have same type");
   }
diff --git a/src/util/std_expr.h b/src/util/std_expr.h
index b008a64d012..ec9a35fa853 100644
--- a/src/util/std_expr.h
+++ b/src/util/std_expr.h
@@ -777,7 +777,9 @@ class binary_exprt:public exprt
     const validation_modet vm = validation_modet::INVARIANT)
   {
     DATA_CHECK(
-      expr.operands().size() == 2, "binary expression must have two operands");
+      vm,
+      expr.operands().size() == 2,
+      "binary expression must have two operands");
   }
 
   static void validate(
@@ -859,6 +861,7 @@ class binary_predicate_exprt:public binary_exprt
     binary_exprt::validate(expr, ns, vm);
 
     DATA_CHECK(
+      vm,
       expr.type().id() == ID_bool,
       "result of binary predicate expression should be of type bool");
   }
@@ -901,6 +904,7 @@ class binary_relation_exprt:public binary_predicate_exprt
 
     // check types
     DATA_CHECK(
+      vm,
       base_type_eq(expr.op0().type(), expr.op1().type(), ns),
       "lhs and rhs of binary relation expression should have same type");
   }
diff --git a/src/util/std_types.h b/src/util/std_types.h
index 970549694be..99cb0be3df5 100644
--- a/src/util/std_types.h
+++ b/src/util/std_types.h
@@ -1149,7 +1149,8 @@ class bitvector_typet : public typet
     const typet &type,
     const validation_modet vm = validation_modet::INVARIANT)
   {
-    DATA_CHECK(!type.get(ID_width).empty(), "bitvector type must have width");
+    DATA_CHECK(
+      vm, !type.get(ID_width).empty(), "bitvector type must have width");
   }
 };
 
diff --git a/src/util/symbol_table.cpp b/src/util/symbol_table.cpp
index e6d058286ec..23ef1e327d7 100644
--- a/src/util/symbol_table.cpp
+++ b/src/util/symbol_table.cpp
@@ -130,6 +130,7 @@ void symbol_tablet::validate(const validation_modet vm) const
 
     // Check that symbols[id].name == id
     DATA_CHECK_WITH_DIAGNOSTICS(
+      vm,
       symbol.name == symbol_key,
       "Symbol table entry must map to a symbol with the correct identifier",
       "Symbol table key '",
@@ -152,6 +153,7 @@ void symbol_tablet::validate(const validation_modet vm) const
           }) != symbol_base_map.end();
 
       DATA_CHECK_WITH_DIAGNOSTICS(
+        vm,
         base_map_matches_symbol,
         "The base_name of a symbol should map to itself",
         "Symbol table key '",
@@ -174,6 +176,7 @@ void symbol_tablet::validate(const validation_modet vm) const
           }) != symbol_module_map.end();
 
       DATA_CHECK_WITH_DIAGNOSTICS(
+        vm,
         module_map_matches_symbol,
         "Symbol table module map should map to symbol",
         "Symbol table key '",
@@ -188,6 +191,7 @@ void symbol_tablet::validate(const validation_modet vm) const
   for(auto base_map_entry : symbol_base_map)
   {
     DATA_CHECK_WITH_DIAGNOSTICS(
+      vm,
       has_symbol(base_map_entry.second),
       "Symbol table base_name map entries must map to a symbol name",
       "base_name map entry '",
@@ -201,6 +205,7 @@ void symbol_tablet::validate(const validation_modet vm) const
   for(auto module_map_entry : symbol_module_map)
   {
     DATA_CHECK_WITH_DIAGNOSTICS(
+      vm,
       has_symbol(module_map_entry.second),
       "Symbol table module map entries must map to a symbol name",
       "base_name map entry '",
diff --git a/src/util/validate.h b/src/util/validate.h
index eaf62c0576c..dc48c601e3d 100644
--- a/src/util/validate.h
+++ b/src/util/validate.h
@@ -15,18 +15,13 @@ Author: Daniel Poetzl
 #include "validation_mode.h"
 
 /// This macro takes a condition which denotes a well-formedness criterion on
-/// goto programs, expressions, instructions, etc. When invoking the macro, a
-/// variable named `vm` of type `const validation_modet` should be in scope. It
-/// indicates whether DATA_INVARIANT() is used to check the condition, or if an
-/// exception is thrown when the condition does not hold.
-#define DATA_CHECK(condition, message)                                         \
+/// goto programs, expressions, instructions, etc. The first parameter should be
+/// of type `validate_modet` and indicates whether DATA_INVARIANT() is used to
+/// check the condition, or if an exception is thrown when the condition does
+/// not hold.
+#define DATA_CHECK(vm, condition, message)                                     \
   do                                                                           \
   {                                                                            \
-    static_assert(                                                             \
-      std::is_same<decltype(vm), const validation_modet>::value,               \
-      "when invoking the macro DATA_CHECK(), a variable named `vm` of type "   \
-      "`const validation_modet` should be in scope which indicates the "       \
-      "validation mode (see `validate.h`");                                    \
     switch(vm)                                                                 \
     {                                                                          \
     case validation_modet::INVARIANT:                                          \
@@ -39,14 +34,9 @@ Author: Daniel Poetzl
     }                                                                          \
   } while(0)
 
-#define DATA_CHECK_WITH_DIAGNOSTICS(condition, message, ...)                   \
+#define DATA_CHECK_WITH_DIAGNOSTICS(vm, condition, message, ...)               \
   do                                                                           \
   {                                                                            \
-    static_assert(                                                             \
-      std::is_same<decltype(vm), const validation_modet>::value,               \
-      "when invoking the macro DATA_CHECK_WITH_DIAGNOSTICS(), a variable "     \
-      "named `vm` of type `const validation_modet` should be in scope which "  \
-      "indicates the validation mode (see `validate.h`");                      \
     switch(vm)                                                                 \
     {                                                                          \
     case validation_modet::INVARIANT:                                          \
diff --git a/src/util/validate_expressions.cpp b/src/util/validate_expressions.cpp
index 6de0c1ca2e1..162533afdbd 100644
--- a/src/util/validate_expressions.cpp
+++ b/src/util/validate_expressions.cpp
@@ -15,6 +15,7 @@ Author: Daniel Poetzl
 
 #include "expr.h"
 #include "namespace.h"
+#include "ssa_expr.h"
 #include "std_expr.h"
 #include "validate.h"
 
@@ -32,6 +33,10 @@ void call_on_expr(const exprt &expr, Args &&... args)
   {
     CALL_ON_EXPR(plus_exprt);
   }
+  else if(expr.get_bool(ID_C_SSA_symbol))
+  {
+    CALL_ON_EXPR(ssa_exprt);
+  }
   else
   {
 #ifdef REPORT_UNIMPLEMENTED_EXPRESSION_CHECKS
diff --git a/src/util/validation_interface.h b/src/util/validation_interface.h
index 47771bf63b9..7543de2e45f 100644
--- a/src/util/validation_interface.h
+++ b/src/util/validation_interface.h
@@ -9,11 +9,16 @@ Author: Daniel Poetzl
 #ifndef CPROVER_UTIL_VALIDATION_INTERFACE_H
 #define CPROVER_UTIL_VALIDATION_INTERFACE_H
 
-#define OPT_VALIDATE "(validate-goto-model)"
+#define OPT_VALIDATE                                                           \
+  "(validate-goto-model)"                                                      \
+  "(validate-ssa-equation)"
 
 #define HELP_VALIDATE                                                          \
   " --validate-goto-model        enable additional well-formedness checks on " \
   "the\n"                                                                      \
-  "                              goto program\n"
+  "                              goto program\n"                               \
+  " --validate-ssa-equation      enable additional well-formedness checks on " \
+  "the\n"                                                                      \
+  "                              SSA representation\n"
 
 #endif /* CPROVER_UTIL_VALIDATION_INTERFACE_H */
diff --git a/unit/Makefile b/unit/Makefile
index 60d4f36ac0e..9fb55603578 100644
--- a/unit/Makefile
+++ b/unit/Makefile
@@ -16,6 +16,7 @@ SRC += analyses/ai/ai.cpp \
        analyses/does_remove_const/is_type_at_least_as_const_as.cpp \
        compound_block_locations.cpp \
        goto-programs/goto_trace_output.cpp \
+       goto-symex/ssa_equation.cpp \
        interpreter/interpreter.cpp \
        json/json_parser.cpp \
        path_strategies.cpp \
diff --git a/unit/goto-symex/module_dependencies.txt b/unit/goto-symex/module_dependencies.txt
new file mode 100644
index 00000000000..e4e1bf05065
--- /dev/null
+++ b/unit/goto-symex/module_dependencies.txt
@@ -0,0 +1,3 @@
+goto-symex
+testing-utils
+util
diff --git a/unit/goto-symex/ssa_equation.cpp b/unit/goto-symex/ssa_equation.cpp
new file mode 100644
index 00000000000..7b4041ba013
--- /dev/null
+++ b/unit/goto-symex/ssa_equation.cpp
@@ -0,0 +1,53 @@
+/*******************************************************************\
+
+   Module: Unit tests for symex_target_equation::validate
+
+   Author: Diffblue Ltd.
+
+ \*******************************************************************/
+
+#include <goto-symex/symex_target_equation.h>
+#include <testing-utils/catch.hpp>
+#include <util/arith_tools.h>
+
+SCENARIO("Validation of well-formed SSA steps", "[core][goto-symex][validate]")
+{
+  GIVEN("A program with one function return")
+  {
+    symbol_tablet symbol_table;
+    const typet type1 = signedbv_typet(32);
+    const code_typet code_type({}, type1);
+
+    symbolt fun_symbol;
+    irep_idt fun_name = "foo";
+    fun_symbol.name = fun_name;
+    symbol_exprt fun_foo(fun_name, code_type);
+
+    symex_target_equationt equation;
+    equation.SSA_steps.push_back(symex_target_equationt::SSA_stept());
+    auto &step = equation.SSA_steps.back();
+    step.type = goto_trace_stept::typet::FUNCTION_RETURN;
+    step.called_function = fun_name;
+
+    WHEN("Called function is in symbol table")
+    {
+      symbol_table.insert(fun_symbol);
+      namespacet ns(symbol_table);
+
+      THEN("The consistency check succeeds")
+      {
+        REQUIRE_NOTHROW(equation.validate(ns, validation_modet::INVARIANT));
+      }
+    }
+
+    WHEN("Called function is not in symbol table")
+    {
+      namespacet ns(symbol_table);
+
+      THEN("The consistency check fails")
+      {
+        REQUIRE_THROWS(equation.validate(ns, validation_modet::EXCEPTION));
+      }
+    }
+  }
+}