diff --git a/gnu/packages/java.scm b/gnu/packages/java.scm
index 4d6befe511..087f411258 100644
--- a/gnu/packages/java.scm
+++ b/gnu/packages/java.scm
@@ -14040,3 +14040,137 @@ can be interpreted by IDEs and static analysis tools to improve code analysis.")
                ;; either lgpl or asl
                license:lgpl3+
                license:asl2.0))))
+
+(define-public tla2tools
+  (let* ((version "1.8.0")
+         (tag (string-append "v" version)))
+    (package
+      (name "tla2tools")
+      (version version)
+      (source (origin
+                (method git-fetch)
+                (uri (git-reference
+                      (url "https://github.com/tlaplus/tlaplus")
+                      (commit tag)))
+                (file-name (git-file-name name version))
+                (sha256
+                 (base32
+                  "1503ljw32mbgw1mzkyk31sxdyggli9jf5sa31chfy5g5ccaphz9b"))
+                (patches
+                 (search-patches "tla2tools-build-xml.patch"))
+                (modules '((guix build utils)))
+                (snippet
+                 '(begin
+                    ;; Remove packaged libraries (see 'replace-libs below)
+                    (for-each delete-file (find-files "." ".*.jar$"))
+                    #t))))
+      (build-system ant-build-system)
+      (arguments
+       (let* ((tlatools "tlatools/org.lamport.tlatools/")
+              (build-xml (string-append tlatools "customBuild.xml")))
+         `(#:jdk ,openjdk11
+           #:modules ((guix build ant-build-system)
+                      (guix build utils)
+                      (ice-9 match)
+                      (srfi srfi-26))
+           #:make-flags '("-f" ,build-xml)
+           #:phases
+           (modify-phases %standard-phases
+            ;; Replace packed libs with references to jars in store
+             (add-after 'unpack 'replace-libs
+               (lambda* (#:key inputs #:allow-other-keys)
+                 (define (input-jar input)
+                   (car (find-files (assoc-ref inputs input) "\\.jar$")))
+                 (for-each
+                  (match-lambda
+                    ((file . input)
+                     (symlink (input-jar input)
+                              (string-append ,tlatools "/lib/" file))))
+                  '(("gson/gson-2.8.6.jar" . "java-gson")
+                    ("javax.mail/mailapi-1.6.3.jar" . "java-javax-mail")
+                    ("jline/jline-terminal-3.14.1.jar" . "java-jline-terminal")
+                    ("jline/jline-reader-3.14.1.jar" . "java-jline-reader")
+                    ("lsp/org.eclipse.lsp4j.debug-0.10.0.jar" .
+                     "java-eclipse-lsp4j-debug")
+                    ("lsp/org.eclipse.lsp4j.jsonrpc-0.10.0.jar" .
+                     "java-eclipse-lsp4j-jsonrpc")
+                    ("lsp/org.eclipse.lsp4j.jsonrpc.debug-0.10.0.jar" .
+                     "java-eclipse-lsp4j-jsonrpc-debug")
+                    ("junit-4.12.jar" . "java-junit")
+                    ("easymock-3.3.1.jar" . "java-easymock")))
+                 ;; Retain a tiny subset of the original X-Git-*
+                 ;; manifest values just to aid in debugging
+                 (substitute* ,build-xml
+                   (("\\$\\{git.tag\\}") ,tag))
+                 #t))
+             (add-before 'check 'prepare-tests
+               (lambda _
+                 ;; pcal tests write to cfg files
+                 (for-each (cut chmod <> #o644)
+                           (find-files (string-append ,tlatools
+                                                      "/test-model/pcal")
+                                       "\\.cfg$"))
+                 #t))
+             (replace 'install
+               (lambda _
+                 (let* ((share (string-append %output "/share/java"))
+                        (jar-name "tla2tools.jar"); set in project.properties
+                        (jar (string-append ,tlatools
+                                            "/dist/" jar-name))
+                        (java-cp (string-append share "/" jar-name))
+                        (bin (string-append %output "/bin")))
+                   (install-file jar share)
+                   (mkdir-p bin)
+                   ;; Generate wrapper scripts for bin/, which invoke common
+                   ;; commands within tla2tools.jar.  Users can still invoke
+                   ;; tla2tools.jar for the rest.
+                   (for-each
+                    (match-lambda
+                      ((wrapper . class)
+                       (let ((file (string-append bin "/" wrapper)))
+                         (begin
+                           (with-output-to-file file
+                             (lambda _
+                               (display
+                                (string-append
+                                 "#!" (which "sh") "\n"
+                                 "java -cp " java-cp " " class " \"$@\""))))
+                           (chmod file #o755)))))
+                    ;; bin/wrapper . java-class
+                    '(("pcal" . "pcal.trans")
+                      ("tlatex" . "tla2tex.TLA")
+                      ("tla2sany" . "tla2sany.SANY")
+                      ("tlc2" . "tlc2.TLC")
+                      ("tlc2-repl" . "tlc2.REPL"))))
+                 #t))))))
+      (native-inputs
+       `(("java-junit" ,java-junit)
+         ("java-easymock" ,java-easymock)))
+      (inputs
+       `(("java-javax-mail" ,java-javax-mail)
+         ("java-gson" ,java-gson-2.8.6)
+         ("java-jline-terminal" ,java-jline-terminal)
+         ("java-jline-reader" ,java-jline-reader)
+         ("java-eclipse-lsp4j-jsonrpc" ,java-eclipse-lsp4j-jsonrpc)
+         ("java-eclipse-lsp4j-jsonrpc-debug" ,java-eclipse-lsp4j-jsonrpc-debug)
+         ("java-eclipse-lsp4j-debug" ,java-eclipse-lsp4j-debug)))
+      (home-page "https://lamport.azurewebsites.net/tla/tools.html")
+      (synopsis "TLA+ tools (analyzer, TLC, TLATeX, PlusCal translator)")
+      (description "TLA+ is a high-level language for modeling programs and
+systems---especially concurrent and distributed ones.  It's based on the idea
+that the best way to describe things precisely is with simple
+mathematics.  TLA+ and its tools are useful for eliminating fundamental design
+errors, which are hard to find and expensive to correct in code.
+
+The following TLA+ tools are available in this distribution:
+
+@itemize
+@item The Syntactic Analyzer: A parser and syntax checker for
+  TLA+ specifications;
+@item TLC: A model checker and simulator for a subclass of \"executable\" TLA+
+  specifications;
+@item TLATeX: A program for typesetting TLA+ specifications;
+@item Beta test versions of 1-3 for the TLA+2 language; and
+@item The PlusCal translator.
+@end itemize")
+      (license license:expat))))
diff --git a/gnu/packages/patches/tla2tools-build-xml.patch b/gnu/packages/patches/tla2tools-build-xml.patch
new file mode 100644
index 0000000000..0bba82072a
--- /dev/null
+++ b/gnu/packages/patches/tla2tools-build-xml.patch
@@ -0,0 +1,109 @@
+tla2tools comes packaged with three separate javax.mail JARs, which it
+expects to be available to include in the JAR produced by the `dist' target.
+However, the `java-javax-mail' packaged with Guix contains all of these
+dependencies in a single JAR, so the other two are unneeded.  This patch
+removes references to them.
+
+The JAR also was expected to contain classes that are built as part of the
+test suite.  That does not seem useful, nor is it available during the
+`compile' phase, so that portion is removed.
+
+There are a number of Git attributes that are set in the final manifest.
+The branch name is kept, but the others are removed.  The build user is set
+statically to "guix".
+
+Finally, since we already have a patch, two targets `jar' and `check' are
+added to satisfy `ant-build-system' and keep the package definition more
+lean.
+
+diff --git a/tlatools/org.lamport.tlatools/customBuild.xml b/tlatools/org.lamport.tlatools/customBuild.xml
+index f0ba77cb7..748e60d95 100644
+--- a/tlatools/org.lamport.tlatools/customBuild.xml
++++ b/tlatools/org.lamport.tlatools/customBuild.xml
+@@ -36,6 +36,17 @@
+ 		<istrue value="${maven.test.halt}"/>
+ 	</condition>
+ 
++  <!-- `jar' and `check' added for Guix -->
++  <target name="jar">
++		<antcall target="compile" inheritall="true" inheritrefs="true" />
++		<antcall target="compile-aj" inheritall="true" inheritrefs="true" />
++		<antcall target="dist" inheritall="true" inheritrefs="true" />
++  </target>
++  <target name="check">
++		<antcall target="compile-test" inheritall="true" inheritrefs="true" />
++		<antcall target="test" inheritall="true" inheritrefs="true" />
++  </target>
++
+ 	<!-- https://github.com/alx3apps/jgit-buildnumber -->
+ 	<target name="git-revision">
+ 	    <taskdef name="jgit-buildnumber" classname="ru.concerteza.util.buildnumber.JGitBuildNumberAntTask">
+@@ -217,17 +228,7 @@
+ 				<exclude name="javax/mail/search/**"/>
+ 			</patternset>
+ 		</unzip>
+-		<unzip src="lib/javax.mail/smtp-1.6.3.jar" dest="${class.dir}">
+-			<patternset>
+-		        <include name="**/*.class"/>
+-			</patternset>
+-		</unzip>
+-		<unzip src="lib/javax.mail/javax.activation_1.1.0.v201211130549.jar" dest="${class.dir}">
+-			<patternset>
+-		        <include name="**/*.class"/>
+-				<exclude name="org/**"/>
+-			</patternset>
+-		</unzip>
++		<mkdir dir="${class.dir}/META-INF" />
+ 		<touch file="${class.dir}/META-INF/javamail.default.address.map"/>
+ 		<unzip src="lib/jline/jline-terminal-3.14.1.jar" dest="${class.dir}">
+ 			<patternset>
+@@ -259,17 +260,7 @@
+ 				<exclude name="javax/mail/search/**"/>
+ 			</patternset>
+ 		</unzip>
+-		<unzip src="lib/javax.mail/smtp-1.6.3.jar" dest="target/classes">
+-			<patternset>
+-		        <include name="**/*.class"/>
+-			</patternset>
+-		</unzip>
+-		<unzip src="lib/javax.mail/javax.activation_1.1.0.v201211130549.jar" dest="target/classes">
+-			<patternset>
+-		        <include name="**/*.class"/>
+-				<exclude name="org/**"/>
+-			</patternset>
+-		</unzip>
++		<mkdir dir="target/classes/META-INF" />
+ 		<touch file="target/classes/META-INF/javamail.default.address.map"/>
+ 
+ 		<unzip src="lib/jline/jline-terminal-3.14.1.jar" dest="target/classes">
+@@ -373,14 +364,8 @@
+ 					src/tla2sany/parser/Token.09-09-07,
+ 					src/tla2sany/parser/TokenMgrError.09-09-07"/>
+ 			<fileset dir="${doc.dir}" includes="License.txt"/>
+-			<fileset dir="${test.class.dir}">
+-				<include name="**/tlc2/tool/CommonTestCase*.class" />
+-				<include name="**/tlc2/tool/liveness/ModelCheckerTestCase*.class" />
+-				<include name="**/tlc2/TestMPRecorder*.class" />
+-				<include name="**/util/IsolatedTestCaseRunner*.class" />
+-			</fileset>
+ 			<manifest>
+-				<attribute name="Built-By" value="${user.name}" />
++				<attribute name="Built-By" value="guix" />
+ 				<attribute name="Build-Tag" value="${env.BUILD_TAG}" />
+ 				<attribute name="Build-Rev" value="${Build-Rev}" />
+ 				<attribute name="Implementation-Title" value="TLA+ Tools" />
+@@ -389,14 +374,8 @@
+ 				<!-- The jar files contains many main classes (SANY, TEX, pcal, ...) --> 
+                 <!-- but lets consider TLC the one users primarily use. --> 
+ 				<attribute name="Main-class" value="tlc2.TLC" />
+-				<attribute name="Class-Path" value="CommunityModules-deps.jar CommunityModules.jar" />
+ 				<!-- Git revision -->
+-				<attribute name="X-Git-Branch" value="${git.branch}" />
+ 				<attribute name="X-Git-Tag" value="${git.tag}" />
+-				<attribute name="X-Git-Revision" value="${git.revision}" />
+-				<attribute name="X-Git-ShortRevision" value="${git.shortRevision}" />
+-				<attribute name="X-Git-BuildNumber" value="${git.branch}_${git.tag}_${git.shortRevision}" />
+-				<attribute name="X-Git-Commits-Count" value="${git.commitsCount}" />
+ 				<!-- App-Name and Permissions is required by Java Webstart used by distributed TLC -->
+ 				<!-- Depending on security level, the user will see a warning otherwise. -->
+ 				<!-- http://docs.oracle.com/javase/7/docs/technotes/guides/jweb/security/manifest.html -->
