diff --git a/regression/cbmc/json-interface1/main.c b/regression/cbmc/json-interface1/main.c
new file mode 100644
index 00000000000..5fc3c2860bb
--- /dev/null
+++ b/regression/cbmc/json-interface1/main.c
@@ -0,0 +1,12 @@
+#include <assert.h>
+
+void foo(int x)
+{
+  for(int i = 0; i < 5; ++i)
+  {
+    if(x)
+      assert(0);
+    assert(0);
+  }
+  assert(0);
+}
diff --git a/regression/cbmc/json-interface1/test.desc b/regression/cbmc/json-interface1/test.desc
new file mode 100644
index 00000000000..5ea8fe3d74c
--- /dev/null
+++ b/regression/cbmc/json-interface1/test.desc
@@ -0,0 +1,12 @@
+CORE broken-smt-backend
+--json-interface
+< test.json
+activate-multi-line-match
+^EXIT=10$
+^SIGNAL=0$
+Not unwinding loop foo\.0 iteration 3 file main\.c line 5 function foo thread 0
+\{\n\s*"description": "assertion 0",\n\s*"property": "foo\.assertion\.(1|3)",\n\s*"status": "SUCCESS"\n\s*\}
+\{\n\s*"description": "assertion 0",\n\s*"property": "foo\.assertion\.(1|3)",\n\s*"status": "FAILURE",\n\s*"trace": \[
+VERIFICATION FAILED
+--
+"property": "foo\.assertion\.2"
diff --git a/regression/cbmc/json-interface1/test.json b/regression/cbmc/json-interface1/test.json
new file mode 100644
index 00000000000..1b68a04d4ca
--- /dev/null
+++ b/regression/cbmc/json-interface1/test.json
@@ -0,0 +1,15 @@
+{
+  "arguments": [
+    "main.c"
+  ],
+  "options": {
+    "function": "foo",
+    "unwind": 3,
+    "property": [
+      "foo.assertion.1",
+      "foo.assertion.3"
+    ],
+    "trace": true,
+    "show-properties": false
+  }	
+}
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index df074359dbf..cc6846805c2 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -79,6 +79,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <langapi/mode.h>
 
+#include <json/json_interface.h>
 #include <xmllang/xml_interface.h>
 
 #include "c_test_input_generator.h"
@@ -90,6 +91,7 @@ cbmc_parse_optionst::cbmc_parse_optionst(int argc, const char **argv)
       argv,
       std::string("CBMC ") + CBMC_VERSION)
 {
+  json_interface(cmdline, ui_message_handler);
   xml_interface(cmdline, ui_message_handler);
 }
 
@@ -103,6 +105,7 @@ ::cbmc_parse_optionst::cbmc_parse_optionst(
       argv,
       std::string("CBMC ") + CBMC_VERSION)
 {
+  json_interface(cmdline, ui_message_handler);
   xml_interface(cmdline, ui_message_handler);
 }
 
@@ -1021,6 +1024,7 @@ void cbmc_parse_optionst::help()
     " --xml-ui                     use XML-formatted output\n"
     " --xml-interface              bi-directional XML interface\n"
     " --json-ui                    use JSON-formatted output\n"
+    " --json-interface             bi-directional JSON interface\n"
     // NOLINTNEXTLINE(whitespace/line_length)
     HELP_VALIDATE
     HELP_GOTO_TRACE
diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h
index bab6bf61f0e..8df79aec96c 100644
--- a/src/cbmc/cbmc_parse_options.h
+++ b/src/cbmc/cbmc_parse_options.h
@@ -47,7 +47,9 @@ class optionst;
   "(object-bits):" \
   OPT_GOTO_CHECK \
   "(no-assertions)(no-assumptions)" \
-  "(xml-ui)(xml-interface)(json-ui)" \
+  "(xml-ui)(xml-interface)" \
+  "(json-interface)" \
+  "(json-ui)" \
   "(smt1)(smt2)(fpa)(cvc3)(cvc4)(boolector)(yices)(z3)(mathsat)" \
   "(cprover-smt2)" \
   "(no-sat-preprocessor)" \
diff --git a/src/cbmc/module_dependencies.txt b/src/cbmc/module_dependencies.txt
index 791561138b6..ca9b882227d 100644
--- a/src/cbmc/module_dependencies.txt
+++ b/src/cbmc/module_dependencies.txt
@@ -7,6 +7,7 @@ goto-instrument
 goto-programs
 goto-symex
 jsil
+json
 json-symtab-language
 langapi # should go away
 linking
diff --git a/src/json/Makefile b/src/json/Makefile
index 95d6b9bf558..4da2cdc21a9 100644
--- a/src/json/Makefile
+++ b/src/json/Makefile
@@ -1,4 +1,5 @@
-SRC = json_lex.yy.cpp \
+SRC = json_interface.cpp \
+      json_lex.yy.cpp \
       json_parser.cpp \
       json_y.tab.cpp \
       # Empty last line
diff --git a/src/json/json_interface.cpp b/src/json/json_interface.cpp
new file mode 100644
index 00000000000..da9eb512dd2
--- /dev/null
+++ b/src/json/json_interface.cpp
@@ -0,0 +1,120 @@
+/*******************************************************************\
+
+Module: JSON Commandline Interface
+
+Author: Peter Schrammel
+
+\*******************************************************************/
+
+/// \file
+/// JSON Commandline Interface
+
+#include "json_interface.h"
+
+#include <util/cmdline.h>
+#include <util/exception_utils.h>
+#include <util/json.h>
+#include <util/message.h>
+
+#include "json_parser.h"
+
+#include <iostream>
+
+/// Parse commandline options from \p json into \p cmdline
+static void get_json_options(const json_objectt &json, cmdlinet &cmdline)
+{
+  const jsont &arguments = json["arguments"];
+  if(!arguments.is_array())
+  {
+    throw invalid_command_line_argument_exceptiont(
+      "array expected", "'arguments'");
+  }
+
+  for(const auto &argument : to_json_array(arguments))
+  {
+    if(!argument.is_string())
+    {
+      throw invalid_command_line_argument_exceptiont(
+        "string expected", "argument");
+    }
+
+    cmdline.args.push_back(argument.value);
+  }
+
+  const jsont &options = json["options"];
+  if(!options.is_object())
+  {
+    throw invalid_command_line_argument_exceptiont(
+      "array expected", "'options'");
+  }
+
+  for(const auto &option_pair : to_json_object(options))
+  {
+    if(option_pair.second.is_string() || option_pair.second.is_number())
+    {
+      // e.g. --option x
+      cmdline.set(option_pair.first, option_pair.second.value);
+    }
+    else if(option_pair.second.is_boolean())
+    {
+      // e.g. --flag
+      if(option_pair.second.is_true())
+        cmdline.set(option_pair.first);
+    }
+    else if(option_pair.second.is_array())
+    {
+      // e.g. --option x --option y
+      for(const auto &element : to_json_array(option_pair.second))
+      {
+        if(element.is_string())
+          cmdline.set(option_pair.first, element.value);
+        else
+        {
+          throw invalid_command_line_argument_exceptiont(
+            "string expected", option_pair.first);
+        }
+      }
+    }
+    else
+    {
+      throw invalid_command_line_argument_exceptiont(
+        "unrecognized commandline option format",
+        option_pair.first,
+        "Boolean, string, number, or string array expected");
+    }
+  }
+}
+
+void json_interface(cmdlinet &cmdline, message_handlert &message_handler)
+{
+  if(cmdline.isset("json-interface"))
+  {
+    jsont json;
+
+    parse_json(std::cin, "", message_handler, json);
+
+    try
+    {
+      if(!json.is_object())
+      {
+        throw invalid_command_line_argument_exceptiont(
+          "JSON object expected at top-level", "command-line JSON input");
+      }
+
+      get_json_options(to_json_object(json), cmdline);
+
+      // Add this so that it gets propagated into optionst;
+      // the ui_message_handlert::uit has already been set on the basis
+      // of the json-interface flag.
+      cmdline.set("json-ui");
+    }
+    catch(const invalid_command_line_argument_exceptiont &e)
+    {
+      messaget log(message_handler);
+      log.error() << e.what() << messaget::eom;
+
+      // make sure we fail with a usage error
+      cmdline.clear();
+    }
+  }
+}
diff --git a/src/json/json_interface.h b/src/json/json_interface.h
new file mode 100644
index 00000000000..f6460a31384
--- /dev/null
+++ b/src/json/json_interface.h
@@ -0,0 +1,40 @@
+/*******************************************************************\
+
+Module: JSON Commandline Interface
+
+Author: Peter Schrammel
+
+\*******************************************************************/
+
+/// \file
+/// JSON Commandline Interface
+
+#ifndef CPROVER_JSON_JSON_INTERFACE_H
+#define CPROVER_JSON_JSON_INTERFACE_H
+
+class cmdlinet;
+class message_handlert;
+
+/// Parses the JSON-formatted command line from stdin
+///
+/// Example:
+/// \code{.json}
+/// {
+///   "arguments": [
+///     "main.c"
+///   ],
+///   "options": {
+///     "function": "foo",
+///     "unwind": 3,
+///     "property": [
+///       "foo.assertion.1",
+///       "foo.assertion.3"
+///     ],
+///     "trace": true,
+///     "show-properties": false
+///   }
+/// }
+/// \endcode
+void json_interface(cmdlinet &, message_handlert &);
+
+#endif // CPROVER_JSON_JSON_INTERFACE_H
diff --git a/src/util/json.h b/src/util/json.h
index 529b13a8ddd..55f59d6b62c 100644
--- a/src/util/json.h
+++ b/src/util/json.h
@@ -61,6 +61,11 @@ class jsont
     return kind==kindt::J_ARRAY;
   }
 
+  bool is_boolean() const
+  {
+    return kind == kindt::J_TRUE || kind == kindt::J_FALSE;
+  }
+
   bool is_true() const
   {
     return kind==kindt::J_TRUE;
diff --git a/src/util/ui_message.cpp b/src/util/ui_message.cpp
index 12418178c33..bb3135adc9e 100644
--- a/src/util/ui_message.cpp
+++ b/src/util/ui_message.cpp
@@ -67,7 +67,9 @@ ui_message_handlert::ui_message_handlert(
       nullptr,
       cmdline.isset("xml-ui") || cmdline.isset("xml-interface")
         ? uit::XML_UI
-        : cmdline.isset("json-ui") ? uit::JSON_UI : uit::PLAIN,
+        : cmdline.isset("json-ui") || cmdline.isset("json-interface")
+            ? uit::JSON_UI
+            : uit::PLAIN,
       program,
       cmdline.isset("flush"),
       cmdline.isset("timestamp") ? cmdline.get_value("timestamp") == "monotonic"