diff --git a/tools/load-pvs.lisp b/tools/load-pvs.lisp
new file mode 100644
index 0000000000000000000000000000000000000000..f8dfe4775a1a36cd5727b6199aed9cf0d85aa28e
--- /dev/null
+++ b/tools/load-pvs.lisp
@@ -0,0 +1,15 @@
+;;; Place the following definitions into "~/.sbclrc" to be able to load PVS into
+;;; any sbcl session.
+(defmacro load-pvs (&optional pvspath)
+  "Load PVS into the current lisp environment. Argument PVSPATH is the filespec
+to the sources of PVS. If not provided, it is fetched from the environment
+variables PVSPATH."
+  (let (($pvspath (gensym)))
+    `(let ((,$pvspath
+             (cond
+               (,pvspath ,pvspath)
+               ((uiop:getenvp "PVSPATH") (uiop:getenv-pathname "PVSPATH"))
+               (t (error "Cannot load PVS: PVSPATH not set.")))))
+       (uiop:with-current-directory (,$pvspath)
+         (load "pvs.system")
+         (uiop:symbol-call :make "OPERATE-ON-SYSTEM" :pvs :load)))))