diff --git a/devel/tla+/Makefile b/devel/tla+/Makefile
new file mode 100644
index 000000000000..4c7134ca76e3
--- /dev/null
+++ b/devel/tla+/Makefile
@@ -0,0 +1,49 @@
+PORTNAME=	tla+
+DISTVERSIONPREFIX=	v
+DISTVERSION=	1.7.4
+CATEGORIES=	devel java
+
+MAINTAINER=	patmaddox@FreeBSD.org
+COMMENT=	TLC is a model checker for specifications written in TLA+
+WWW=		https://www.tlapl.us
+
+LICENSE=	MIT
+LICENSE_FILE=	${WRKSRC}/LICENSE
+
+USES=		java:ant,run
+USE_GITHUB=	yes
+GH_ACCOUNT=	tlaplus
+GH_PROJECT=	tlaplus
+JAVA_VERSION=	11
+
+MAKE_ARGS=	-f customBuild.xml
+ALL_TARGET=	compile dist
+
+NO_ARCH=	yes
+
+_TLA_CMD=	exec ${JAVA} -classpath ${JAVAJARDIR}/tla2tools.jar
+
+BUILD_WRKSRC=	${WRKSRC}/tlatools/org.lamport.tlatools
+
+PLIST_FILES=	${JAVAJARDIR}/tla2tools.jar \
+		bin/tla-pcal \
+		bin/tla-sany \
+		bin/tla-tla2sany \
+		bin/tla-tla2tex \
+		bin/tla-tlc
+
+do-install:
+	@${MKDIR} ${STAGEDIR}${JAVAJARDIR}
+	${INSTALL_DATA} ${BUILD_WRKSRC}/dist/tla2tools.jar ${STAGEDIR}${JAVAJARDIR}/tla2tools.jar
+	@${PRINTF} '#!/bin/sh\n${_TLA_CMD} pcal.trans "$$@"\n' > ${WRKDIR}/tla-pcal
+	${INSTALL_SCRIPT} ${WRKDIR}/tla-pcal ${STAGEDIR}${PREFIX}/bin/tla-pcal
+	@${PRINTF} '#!/bin/sh\n${_TLA_CMD} tla2sany.SANY "$$@"\n' > ${WRKDIR}/tla-sany
+	${INSTALL_SCRIPT} ${WRKDIR}/tla-sany ${STAGEDIR}${PREFIX}/bin/tla-sany
+	@${PRINTF} '#!/bin/sh\n${_TLA_CMD} tla2sany.xml.XMLExporter "$$@"\n' > ${WRKDIR}/tla-tla2sany
+	${INSTALL_SCRIPT} ${WRKDIR}/tla-tla2sany ${STAGEDIR}${PREFIX}/bin/tla-tla2sany
+	@${PRINTF} '#!/bin/sh\n${_TLA_CMD} tla2tex.TLA "$$@"\n' > ${WRKDIR}/tla-tla2tex
+	${INSTALL_SCRIPT} ${WRKDIR}/tla-tla2tex ${STAGEDIR}${PREFIX}/bin/tla-tla2tex
+	@${PRINTF} '#!/bin/sh\n${_TLA_CMD} -XX:+UseParallelGC tlc2.TLC "$$@"\n' > ${WRKDIR}/tla-tlc
+	${INSTALL_SCRIPT} ${WRKDIR}/tla-tlc ${STAGEDIR}${PREFIX}/bin/tla-tlc
+
+.include <bsd.port.mk>
diff --git a/devel/tla+/distinfo b/devel/tla+/distinfo
new file mode 100644
index 000000000000..1fedd79b4907
--- /dev/null
+++ b/devel/tla+/distinfo
@@ -0,0 +1,3 @@
+TIMESTAMP = 1783641600
+SHA256 (tlaplus-tlaplus-v1.7.4_GH0.tar.gz) = eb4e54b6c8dc4945cbd697dbfe55819b6fc3f13fe9561afd7d6523c18ea4c350
+SIZE (tlaplus-tlaplus-v1.7.4_GH0.tar.gz) = 72966127
diff --git a/devel/tla+/pkg-descr b/devel/tla+/pkg-descr
new file mode 100644
index 000000000000..30227407b32a
--- /dev/null
+++ b/devel/tla+/pkg-descr
@@ -0,0 +1,17 @@
+TLA+ is a language for modeling software above the code level and
+hardware above the circuit level. The tool most commonly used by
+engineers is the TLC model checker, but there is also a proof
+checker. TLA+ is based on mathematics and does not resemble any
+programming language. Most engineers will find PlusCal to be the
+easiest way to start using TLA+.
+
+This port installs the TLA+ command-line tools packaged as
+tla2tools.jar, with wrapper scripts for each:
+
+  tla-tlc      - the TLC model checker, which explores a
+                 specification's state space to check safety and
+                 liveness properties
+  tla-sany     - the SANY syntactic and semantic analyzer (parser)
+  tla-tla2sany - export a parsed TLA+ module as an XML parse tree
+  tla-pcal     - the PlusCal-to-TLA+ translator
+  tla-tla2tex  - the LaTeX pretty printer for TLA+ specifications