diff --git a/srcpkgs/verifast-vfide b/srcpkgs/verifast-vfide
new file mode 120000
index 0000000000..7eed098f84
--- /dev/null
+++ b/srcpkgs/verifast-vfide
@@ -0,0 +1 @@
+verifast
\ No newline at end of file
diff --git a/srcpkgs/verifast/template b/srcpkgs/verifast/template
new file mode 100644
index 0000000000..bc70aa98e2
--- /dev/null
+++ b/srcpkgs/verifast/template
@@ -0,0 +1,29 @@
+# Template file for 'verifast'
+pkgname=verifast
+version=17.06
+revision=1
+build_style=gnu-makefile
+make_build_args="-C src Z3V4DOT5=yes LD_LIBRARY_PATH=/usr/lib/ocaml/stublibs OCAMLCFLAGS=-unsafe-string build"
+hostmakedepends="vala unzip ocaml ocaml-findlib m4 camlp4 pkg-config"
+makedepends="ocaml-lablgtk2-gtksourceview2 ocaml-num z3-ocaml glib-devel gtksourceview2-devel"
+short_desc="VeriFast code verifier in separation logic"
+maintainer="Tai Chi Minh Ralph Eastwood <tcmreastwood@gmail.com>"
+license="MIT"
+homepage="https://github.com/verifast"
+distfiles="https://github.com/verifast/${pkgname}/archive/v${version}.tar.gz"
+checksum=2cadc3d39730b5422373ebc642009d3efb84373a8fc61b1d51877063a1e4191a
+nocross="yes"
+
+do_install() {
+	vbin bin/verifast
+	vbin bin/vfide
+	vlicense LICENSE.md
+}
+
+verifast-vfide_package() {
+	short_desc+=" - vfide"
+	depends="verifast>=${version}_${revision}"
+	pkg_install() {
+		vmove usr/bin/vfide
+	}
+}