diff --git a/README.md b/README.md
index 64e294e..20703b8 100644
--- a/README.md
+++ b/README.md
@@ -17,4 +17,6 @@ This package is registered with General, so to install do
 pkg> add PropCheck
 ```
 
+PropCheck.jl currently supports Julia versions 1.6 and up. CI runs on nightly and is expected to pass, but no guarantee about stability on unreleased versions of Julia is given.
+
 Please check out the [documentation](https://seelengrab.github.io/PropCheck.jl/) to learn how you can use PropCheck.jl to fuzz your code.
diff --git a/docs/make.jl b/docs/make.jl
index 1375c65..6d0efad 100644
--- a/docs/make.jl
+++ b/docs/make.jl
@@ -27,6 +27,7 @@ function builddocs(clear=false)
                 "Composing Generators" => "Examples/properties.md"
             ],
             "Shrinking with `Tree`s" => "shrinktrees.md",
+            "FAQ" => "faq.md",
             "Interfaces" => "interfaces.md",
             "API Reference" => "api.md"
         ]
diff --git a/docs/src/api.md b/docs/src/api.md
index f187b26..414fdb6 100644
--- a/docs/src/api.md
+++ b/docs/src/api.md
@@ -1,3 +1,5 @@
+# API
+
 ## Function Index
 
 !!! warning "Stability"
@@ -13,7 +15,7 @@
 ```@index
 ```
 
-### Function reference
+## Function reference
 
 ```@autodocs
 Modules = [PropCheck]
diff --git a/docs/src/faq.md b/docs/src/faq.md
new file mode 100644
index 0000000..a808fdf
--- /dev/null
+++ b/docs/src/faq.md
@@ -0,0 +1,20 @@
+# FAQ
+
+## What about formal specifications?
+
+While efforts regarding formal specifications & machine checkable proofs are comendable, I think we can get quite far with property based testing & fuzzing
+before we need to tackle the dragon that is formal methods & verification. PropCheck.jl is decidedly not in the formal verification camp - it's not an interface
+to SAT or SMT solvers, but a fuzzer. Said differently, property based testing + fuzzing are a fuzzy, statistical subset of full formal verification. You can think of
+running fuzzing tests as increasing confidence in the correctness of your code each time you run your testsuite, due to different inputs being chosen.
+
+That being said, if this package becomes obsolete due to tremendous advances in formal methods & verification in Julia, I'll happily retire this package to the annals of history :)
+
+## What about package XYZ?
+
+There are a number of other codebases related to property based testing (for example, [JCheck.jl](https://github.com/ps-pat/JCheck.jl), [QuickCheck.jl](https://github.com/pao/QuickCheck.jl)
+or [RandomizedPropertyTest.jl](https://git.sr.ht/~quf/RandomizedPropertyTest.jl)) but to my eyes, they are either very old (10+ years!) and don't support modern Julia, don't support
+shrinking or don't really compose their generators well, due to being based on QuickCheck. PropCheck.jl, while certainly taking inspiration from QuickCheck, is using a mixed approach,
+focusing on integrated shrinking. This has advantages and disadvantages, but from my experience with the package so far, the current architecture is pretty extensible and works much
+better than a plain implementation of QuickCheck (Julia is much less focused on types than Haskell is, after all; much of the information we have about a type is implicit & not guaranteed,
+and even with that, some type based shrinks are just plain bad, due to even their types not capturing the full semantics of the produced values). Most of the features currently in
+PropCheck.jl came about because I ran into an issue that I wanted to solve when testing a different codebase - a workflow I don't expect to change too much in the future.
diff --git a/docs/src/index.md b/docs/src/index.md
index f6cf044..155cff6 100644
--- a/docs/src/index.md
+++ b/docs/src/index.md
@@ -5,10 +5,12 @@ This is the documentation for *PropCheck.jl*, a property based testing framework
 It features integrated shrinkers, which can smartly shrink initial failures to smaller examples while preserving
 the invariants the original input was generated under.
 
-Check out the Examples to get an introduction to property based testing and to learn how to write your own tests!
+Check out the Examples in the sidebar to get an introduction to property based testing and to learn how to write your own tests!
+
+Here's also a sitemap for the rest of the documentation:
 
 ```@contents
-Pages = ["index.md", "intro.md", "Examples/basic.md", "Examples/structs.md", "Examples/containers.md", "Examples/properties.md"]
+Pages = ["index.md", "intro.md", "shrinktrees.md", "faq.md", "interfaces.md", "api.md"]
 Depth = 3
 ```