diff --git a/Formula/ebmc.rb@5.0 b/Formula/ebmc@5.0.rb
similarity index 96%
rename from Formula/ebmc.rb@5.0
rename to Formula/ebmc@5.0.rb
index 6408cf205..026cbf82e 100644
--- a/Formula/ebmc.rb@5.0
+++ b/Formula/ebmc@5.0.rb
@@ -2,7 +2,7 @@ class Ebmc < Formula
   desc "Model Checker for SystemVerilog"
   homepage "https://www.cprover.org/ebmc/"
   url "https://github.com/diffblue/hw-cbmc.git",
-    tag: "ebmc-5.0"
+    tag: "ebmc-5.0",
     revision: "61e797fa61f8c207b2bc4ad391c6982e6798dd4d"
   version "5.0"
   license "BSD-3-Clause"
diff --git a/Formula/ebmc.rb@5.1 b/Formula/ebmc@5.1.rb
similarity index 96%
rename from Formula/ebmc.rb@5.1
rename to Formula/ebmc@5.1.rb
index dda7dedf1..8e39c90ae 100644
--- a/Formula/ebmc.rb@5.1
+++ b/Formula/ebmc@5.1.rb
@@ -2,7 +2,7 @@ class Ebmc < Formula
   desc "Model Checker for SystemVerilog"
   homepage "https://www.cprover.org/ebmc/"
   url "https://github.com/diffblue/hw-cbmc.git",
-    tag: "ebmc-5.1"
+    tag: "ebmc-5.1",
     revision: "3296ed5b6e40f91702273b5503bcbfc92487c2fc"
   version "5.1"
   license "BSD-3-Clause"
diff --git a/Formula/ebmc.rb@5.2 b/Formula/ebmc@5.2.rb
similarity index 96%
rename from Formula/ebmc.rb@5.2
rename to Formula/ebmc@5.2.rb
index 3a7fd7143..c7f10421c 100644
--- a/Formula/ebmc.rb@5.2
+++ b/Formula/ebmc@5.2.rb
@@ -2,7 +2,7 @@ class Ebmc < Formula
   desc "Model Checker for SystemVerilog"
   homepage "https://www.cprover.org/ebmc/"
   url "https://github.com/diffblue/hw-cbmc.git",
-    tag: "ebmc-5.2"
+    tag: "ebmc-5.2",
     revision: "d308e0934a635a3e16a332284d41c43eda7a4133"
   version "5.2"
   license "BSD-3-Clause"
diff --git a/Formula/ebmc.rb@5.3 b/Formula/ebmc@5.3.rb
similarity index 96%
rename from Formula/ebmc.rb@5.3
rename to Formula/ebmc@5.3.rb
index 485780dc3..f167c5449 100644
--- a/Formula/ebmc.rb@5.3
+++ b/Formula/ebmc@5.3.rb
@@ -2,7 +2,7 @@ class Ebmc < Formula
   desc "Model Checker for SystemVerilog"
   homepage "https://www.cprover.org/ebmc/"
   url "https://github.com/diffblue/hw-cbmc.git",
-    tag: "ebmc-5.3"
+    tag: "ebmc-5.3",
     revision: "a7bf36c2fba8f7658932b5d83a0e1752668cd091"
   version "5.3"
   license "BSD-3-Clause"
diff --git a/Formula/ebmc@5.4.rb b/Formula/ebmc@5.4.rb
new file mode 100644
index 000000000..81059cd1d
--- /dev/null
+++ b/Formula/ebmc@5.4.rb
@@ -0,0 +1,24 @@
+class Ebmc < Formula
+  desc "Model Checker for SystemVerilog"
+  homepage "https://www.cprover.org/ebmc/"
+  url "https://github.com/diffblue/hw-cbmc.git",
+    tag: "ebmc-5.4",
+    revision: "a7e28cda0bc5ac1a17afa574e2d4fb88a8778b5d"
+  version "5.4"
+  license "BSD-3-Clause"
+
+  uses_from_macos "flex" => :build
+  uses_from_macos "curl" => :build
+  depends_on "bison" => :build
+
+  def install
+    system "make", "-C", "lib/cbmc/src", "minisat2-download"
+    system "make", "-C", "src"
+    system "mkdir", "-p", "#{prefix}/usr/bin"
+    system "cp", "src/ebmc/ebmc", "#{prefix}/usr/bin/"
+  end
+
+  test do
+    system "make", "-C", "regression/ebmc", "test"
+  end
+end