diff --git a/Cargo.lock b/Cargo.lock
index 6be8934..063c718 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -168,8 +168,17 @@ name = "metamath-knife"
 version = "0.3.6"
 dependencies = [
  "annotate-snippets",
- "assert_matches",
  "clap",
+ "metamath-rs",
+ "simple_logger",
+]
+
+[[package]]
+name = "metamath-rs"
+version = "0.3.6"
+dependencies = [
+ "annotate-snippets",
+ "assert_matches",
  "dot-writer",
  "filetime",
  "fnv",
@@ -177,7 +186,6 @@ dependencies = [
  "lazy_static",
  "log",
  "regex",
- "simple_logger",
  "tinyvec",
  "typed-arena",
  "xml-rs",
diff --git a/Cargo.toml b/Cargo.toml
index 92713c2..4e1682e 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -1,42 +1,20 @@
-[package]
+[workspace]
+members = [
+    "metamath-rs",
+    "metamath-knife",
+]
+resolver = "2"
+
+[workspace.package]
 authors = ["David A. Wheeler <dwheeler@dwheeler.com>", "Stefan O'Rear <sorear2@gmail.com>"]
 license = "MIT OR Apache-2.0"
-name = "metamath-knife"
 readme = "README.md"
-version = "0.3.6"
 description = "A parallel and incremental verifier for Metamath databases"
-repository = "https://github.com/david-a-wheeler/metamath-knife"
+repository = "https://github.com/metamath/metamath-knife"
 keywords = ["theorem", "proving", "verifier", "proof", "assistant"]
 categories = ["command-line-utilities", "development-tools", "mathematics"]
 edition = "2021"
 
-[dependencies]
-lazy_static = "1.4"
-itertools = "0.10"
-filetime = "0.2"
-fnv = "1.0"
-regex = { version = "1.5", default-features = false, features = ["std", "perf"] }
-tinyvec = "1.5"
-log = "0.4"
-annotate-snippets = "0.9"
-typed-arena = "2.0"
-
-# Dependencies for standalone executable, not needed for a library
-clap = "2.33"
-simple_logger = "1.13"
-
-# Optional dependencies
-dot-writer = { version = "0.1.2", optional = true }
-xml-rs = { version = "0.8.14", optional = true }
-
-[dev-dependencies]
-assert_matches = "1.5"
-
-[features]
-default = ["annotate-snippets/color"]
-dot = ["dot-writer"]
-xml = ["xml-rs"]
-
 [profile]
 
 [profile.release]
@@ -49,8 +27,3 @@ codegen-units = 4
 
 [profile.test]
 codegen-units = 4
-
-[[bin]]
-name = "metamath-knife"
-path = "src/main.rs"
-doc = false
diff --git a/metamath-knife/Cargo.toml b/metamath-knife/Cargo.toml
new file mode 100644
index 0000000..ae205ba
--- /dev/null
+++ b/metamath-knife/Cargo.toml
@@ -0,0 +1,22 @@
+[package]
+name = "metamath-knife"
+readme = "metamath-knife/README.md"
+description = "A command-line tool for Metamath, including parallel and incremental verifier for Metamath databases"
+version = "0.3.6"
+authors.workspace = true
+license.workspace = true
+repository.workspace = true
+keywords.workspace = true
+categories.workspace = true
+edition = "2021"
+
+[dependencies]
+clap = "2.33"
+simple_logger = "1.13"
+annotate-snippets = "0.9"
+metamath-rs = { path = "../metamath-rs" }
+
+[[bin]]
+name = "metamath-knife"
+path = "src/main.rs"
+doc = false
diff --git a/src/main.rs b/metamath-knife/src/main.rs
similarity index 97%
rename from src/main.rs
rename to metamath-knife/src/main.rs
index 44404fb..920aba1 100644
--- a/src/main.rs
+++ b/metamath-knife/src/main.rs
@@ -4,12 +4,12 @@
 
 use annotate_snippets::display_list::DisplayList;
 use clap::{clap_app, crate_version};
-use metamath_knife::database::{Database, DbOptions};
-use metamath_knife::diag::BibError;
-use metamath_knife::parser::is_valid_label;
-use metamath_knife::statement::StatementAddress;
-use metamath_knife::verify_markup::{Bibliography, Bibliography2};
-use metamath_knife::SourceInfo;
+use metamath_rs::database::{Database, DbOptions};
+use metamath_rs::diag::BibError;
+use metamath_rs::parser::is_valid_label;
+use metamath_rs::statement::StatementAddress;
+use metamath_rs::verify_markup::{Bibliography, Bibliography2};
+use metamath_rs::SourceInfo;
 use simple_logger::SimpleLogger;
 use std::fs::File;
 use std::io::{self, BufWriter};
diff --git a/metamath-rs/Cargo.toml b/metamath-rs/Cargo.toml
new file mode 100644
index 0000000..7d4a4fa
--- /dev/null
+++ b/metamath-rs/Cargo.toml
@@ -0,0 +1,34 @@
+[package]
+name = "metamath-rs"
+readme = "metamath-rs/README.md"
+description = "A library manipulating Metamath databases, including a parallel and incremental verifier for Metamath databases"
+version = "0.3.6"
+authors.workspace = true
+license.workspace = true
+repository.workspace = true
+keywords.workspace = true
+categories.workspace = true
+edition = "2021"
+
+[dependencies]
+lazy_static = "1.4"
+itertools = "0.10"
+filetime = "0.2"
+fnv = "1.0"
+regex = { version = "1.5", default-features = false, features = ["std", "perf"] }
+tinyvec = "1.5"
+log = "0.4"
+annotate-snippets = "0.9"
+typed-arena = "2.0"
+
+# Optional dependencies
+dot-writer = { version = "0.1.2", optional = true }
+xml-rs = { version = "0.8.14", optional = true }
+
+[dev-dependencies]
+assert_matches = "1.5"
+
+[features]
+default = ["annotate-snippets/color"]
+dot = ["dot-writer"]
+xml = ["xml-rs"]
diff --git a/src/axiom_use.rs b/metamath-rs/src/axiom_use.rs
similarity index 100%
rename from src/axiom_use.rs
rename to metamath-rs/src/axiom_use.rs
diff --git a/src/bit_set.rs b/metamath-rs/src/bit_set.rs
similarity index 100%
rename from src/bit_set.rs
rename to metamath-rs/src/bit_set.rs
diff --git a/src/comment_parser.rs b/metamath-rs/src/comment_parser.rs
similarity index 100%
rename from src/comment_parser.rs
rename to metamath-rs/src/comment_parser.rs
diff --git a/src/comment_parser_tests.rs b/metamath-rs/src/comment_parser_tests.rs
similarity index 100%
rename from src/comment_parser_tests.rs
rename to metamath-rs/src/comment_parser_tests.rs
diff --git a/src/database.rs b/metamath-rs/src/database.rs
similarity index 100%
rename from src/database.rs
rename to metamath-rs/src/database.rs
diff --git a/src/diag.rs b/metamath-rs/src/diag.rs
similarity index 100%
rename from src/diag.rs
rename to metamath-rs/src/diag.rs
diff --git a/src/discouraged.rs b/metamath-rs/src/discouraged.rs
similarity index 100%
rename from src/discouraged.rs
rename to metamath-rs/src/discouraged.rs
diff --git a/src/export.rs b/metamath-rs/src/export.rs
similarity index 100%
rename from src/export.rs
rename to metamath-rs/src/export.rs
diff --git a/src/export_deps.rs b/metamath-rs/src/export_deps.rs
similarity index 100%
rename from src/export_deps.rs
rename to metamath-rs/src/export_deps.rs
diff --git a/src/formula.rs b/metamath-rs/src/formula.rs
similarity index 100%
rename from src/formula.rs
rename to metamath-rs/src/formula.rs
diff --git a/src/formula_tests.rs b/metamath-rs/src/formula_tests.rs
similarity index 100%
rename from src/formula_tests.rs
rename to metamath-rs/src/formula_tests.rs
diff --git a/src/grammar.rs b/metamath-rs/src/grammar.rs
similarity index 99%
rename from src/grammar.rs
rename to metamath-rs/src/grammar.rs
index cb6f901..5aa03a0 100644
--- a/src/grammar.rs
+++ b/metamath-rs/src/grammar.rs
@@ -139,7 +139,7 @@ impl GrammarTree {
 ///
 /// Example:
 /// ```
-/// use metamath_knife::database::{Database, DbOptions};
+/// use metamath_rs::database::{Database, DbOptions};
 ///
 /// // Setup the required options
 /// let mut options = DbOptions::default();
@@ -1675,7 +1675,7 @@ impl Grammar {
 ///
 /// Example:
 /// ```
-/// use metamath_knife::database::{Database, DbOptions};
+/// use metamath_rs::database::{Database, DbOptions};
 ///
 /// // Setup the required options
 /// let mut options = DbOptions::default();
diff --git a/src/grammar_tests.rs b/metamath-rs/src/grammar_tests.rs
similarity index 100%
rename from src/grammar_tests.rs
rename to metamath-rs/src/grammar_tests.rs
diff --git a/src/lib.rs b/metamath-rs/src/lib.rs
similarity index 100%
rename from src/lib.rs
rename to metamath-rs/src/lib.rs
diff --git a/src/line_cache.rs b/metamath-rs/src/line_cache.rs
similarity index 100%
rename from src/line_cache.rs
rename to metamath-rs/src/line_cache.rs
diff --git a/src/nameck.rs b/metamath-rs/src/nameck.rs
similarity index 100%
rename from src/nameck.rs
rename to metamath-rs/src/nameck.rs
diff --git a/src/outline.rs b/metamath-rs/src/outline.rs
similarity index 100%
rename from src/outline.rs
rename to metamath-rs/src/outline.rs
diff --git a/src/parser.rs b/metamath-rs/src/parser.rs
similarity index 100%
rename from src/parser.rs
rename to metamath-rs/src/parser.rs
diff --git a/src/parser_tests.rs b/metamath-rs/src/parser_tests.rs
similarity index 100%
rename from src/parser_tests.rs
rename to metamath-rs/src/parser_tests.rs
diff --git a/src/proof.rs b/metamath-rs/src/proof.rs
similarity index 100%
rename from src/proof.rs
rename to metamath-rs/src/proof.rs
diff --git a/src/scopeck.rs b/metamath-rs/src/scopeck.rs
similarity index 100%
rename from src/scopeck.rs
rename to metamath-rs/src/scopeck.rs
diff --git a/src/segment.rs b/metamath-rs/src/segment.rs
similarity index 100%
rename from src/segment.rs
rename to metamath-rs/src/segment.rs
diff --git a/src/segment_set.rs b/metamath-rs/src/segment_set.rs
similarity index 100%
rename from src/segment_set.rs
rename to metamath-rs/src/segment_set.rs
diff --git a/src/statement.rs b/metamath-rs/src/statement.rs
similarity index 100%
rename from src/statement.rs
rename to metamath-rs/src/statement.rs
diff --git a/src/tree.rs b/metamath-rs/src/tree.rs
similarity index 100%
rename from src/tree.rs
rename to metamath-rs/src/tree.rs
diff --git a/src/typesetting.rs b/metamath-rs/src/typesetting.rs
similarity index 99%
rename from src/typesetting.rs
rename to metamath-rs/src/typesetting.rs
index 799c106..4e3b7e9 100644
--- a/src/typesetting.rs
+++ b/metamath-rs/src/typesetting.rs
@@ -1,7 +1,7 @@
 //! The typesetting data.
 //!
 //! This is the result of parsing a `$t` metamath comment, which contains information
-//! used by the metamath website generator. Although `metamath-knife` tries to be
+//! used by the metamath website generator. Although `metamath-rs` tries to be
 //! generic and so it does not itself contain a website generator, this pass can be
 //! used to collect information for generating HTML in the style of
 //! [`metamath.exe`](https://github.com/metamath/metamath-exe).
diff --git a/src/usage_tests.rs b/metamath-rs/src/usage_tests.rs
similarity index 100%
rename from src/usage_tests.rs
rename to metamath-rs/src/usage_tests.rs
diff --git a/src/util.rs b/metamath-rs/src/util.rs
similarity index 100%
rename from src/util.rs
rename to metamath-rs/src/util.rs
diff --git a/src/util_tests.rs b/metamath-rs/src/util_tests.rs
similarity index 100%
rename from src/util_tests.rs
rename to metamath-rs/src/util_tests.rs
diff --git a/src/verify.rs b/metamath-rs/src/verify.rs
similarity index 100%
rename from src/verify.rs
rename to metamath-rs/src/verify.rs
diff --git a/src/verify_markup.rs b/metamath-rs/src/verify_markup.rs
similarity index 100%
rename from src/verify_markup.rs
rename to metamath-rs/src/verify_markup.rs