diff --git a/proofs/examples/.gitignore b/proofs/examples/.gitignore
new file mode 100644
index 0000000000000000000000000000000000000000..6ddd9b708d143cc3411bf22a6e8988f74adc7e80
--- /dev/null
+++ b/proofs/examples/.gitignore
@@ -0,0 +1,5 @@
+*.log
+*~
+*.summary
+pvsbin/
+.pvscontext
diff --git a/proofs/examples/Makefile b/proofs/examples/Makefile
new file mode 100644
index 0000000000000000000000000000000000000000..8fb1da17d736e28db96ce95accf64aac1275989c
--- /dev/null
+++ b/proofs/examples/Makefile
@@ -0,0 +1,6 @@
+PROVEIT ?=
+
+.SUFFIXES: .log .pvs .prf
+
+.pvs.log: 
+	${PROVEIT} --traces -l $<
diff --git a/proofs/examples/hello.prf b/proofs/examples/hello.prf
new file mode 100644
index 0000000000000000000000000000000000000000..ae89e03078b2848547a53d8d240f3ff3b0294a4f
--- /dev/null
+++ b/proofs/examples/hello.prf
@@ -0,0 +1,8 @@
+(hello
+ (hello 0
+  (hello-1 nil 3843292355
+   ("" (flatten)
+    (("" (split) (("1" (propax) nil nil) ("2" (propax) nil nil)) nil))
+    nil)
+   nil shostak)))
+
diff --git a/proofs/examples/hello.pvs b/proofs/examples/hello.pvs
new file mode 100644
index 0000000000000000000000000000000000000000..fb4908a0f18677938decaf25e96af2bb82c11417
--- /dev/null
+++ b/proofs/examples/hello.pvs
@@ -0,0 +1,5 @@
+hello: THEORY
+BEGIN
+	P, Q: bool
+	hello: LEMMA P IMPLIES Q IMPLIES P AND Q
+END hello