diff --git a/Cargo.lock b/Cargo.lock
index 3651bb3b..f218fa45 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -2,6 +2,24 @@
 # It is not intended for manual editing.
 version = 3
 
+[[package]]
+name = "a-mir-formality"
+version = "0.1.0"
+dependencies = [
+ "anyhow",
+ "clap 4.3.19",
+ "expect-test",
+ "formality-check",
+ "formality-core",
+ "formality-macros",
+ "formality-prove",
+ "formality-rust",
+ "formality-smir",
+ "formality-types",
+ "pretty_assertions",
+ "ui_test",
+]
+
 [[package]]
 name = "addr2line"
 version = "0.20.0"
@@ -442,12 +460,12 @@ checksum = "34aa73646ffb006b8f5147f3dc182bd4bcb190227ce861fc4a4844bf8e3cb2c0"
 
 [[package]]
 name = "env_logger"
-version = "0.9.1"
+version = "0.10.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "c90bf5f19754d10198ccb95b70664fc925bd1fc090a0fd9a6ebc54acc8cd6272"
+checksum = "85cdab6a89accf66733ad5a1693a4dcced6aeff64602b634530dd73c1f3ee9f0"
 dependencies = [
- "atty",
  "humantime",
+ "is-terminal",
  "log",
  "regex",
  "termcolor",
@@ -522,24 +540,6 @@ dependencies = [
  "syn 1.0.102",
 ]
 
-[[package]]
-name = "formality"
-version = "0.1.0"
-dependencies = [
- "anyhow",
- "clap 4.3.19",
- "expect-test",
- "formality-check",
- "formality-core",
- "formality-macros",
- "formality-prove",
- "formality-rust",
- "formality-smir",
- "formality-types",
- "pretty_assertions",
- "ui_test",
-]
-
 [[package]]
 name = "formality-check"
 version = "0.1.0"
@@ -559,7 +559,7 @@ dependencies = [
 
 [[package]]
 name = "formality-core"
-version = "0.1.0"
+version = "0.1.1"
 dependencies = [
  "anyhow",
  "contracts",
@@ -581,7 +581,7 @@ dependencies = [
  "expect-test",
  "proc-macro2",
  "quote",
- "syn 1.0.102",
+ "syn 2.0.27",
  "synstructure",
  "tracing",
 ]
@@ -1173,13 +1173,13 @@ dependencies = [
 
 [[package]]
 name = "synstructure"
-version = "0.12.6"
+version = "0.13.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f36bdaa60a83aca3921b5259d5400cbf5e90fc51931376a9bd4a0eb79aa7210f"
+checksum = "285ba80e733fac80aa4270fbcdf83772a79b80aa35c97075320abfee4a915b06"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn 1.0.102",
+ "syn 2.0.27",
  "unicode-xid",
 ]
 
diff --git a/Cargo.toml b/Cargo.toml
index bb8a83db..c58f3ec4 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -1,7 +1,12 @@
 [package]
-name = "formality"
+name = "a-mir-formality"
 version = "0.1.0"
 edition = "2021"
+license = "MIT OR Apache-2.0"
+description = "Model of the Rust type system maintained by the Rust types team (in development)"
+homepage = "https://rust-lang.github.io/a-mir-formality/"
+repository = "https://github.com/rust-lang/a-mir-formality/"
+readme = "README.md"
 
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 
diff --git a/crates/formality-core/Cargo.toml b/crates/formality-core/Cargo.toml
index 3e589107..8908712c 100644
--- a/crates/formality-core/Cargo.toml
+++ b/crates/formality-core/Cargo.toml
@@ -1,18 +1,23 @@
 [package]
 name = "formality-core"
-version = "0.1.0"
+version = "0.1.1"
 edition = "2021"
+license = "MIT OR Apache-2.0"
+description = "Language-independent formality system used by a-mir-formality"
+homepage = "https://rust-lang.github.io/a-mir-formality/"
+repository = "https://github.com/rust-lang/a-mir-formality/"
+readme = "README.md"
 
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 
 [dependencies]
 lazy_static = "1.4.0"
-env_logger = "*"
+env_logger = "0.10.0"
 stacker = "0.1.15"
 tracing = "0.1"
 tracing-subscriber = {version = "0.3", default-features = false, features = ["env-filter", "fmt"]}
 tracing-tree = { version = "0.2" }
-formality-macros = { path = "../formality-macros" }
+formality-macros = { version = "0.1.0", path = "../formality-macros" }
 anyhow = "1.0.75"
 contracts = "0.6.3"
 
diff --git a/crates/formality-core/README.md b/crates/formality-core/README.md
new file mode 100644
index 00000000..35494e4d
--- /dev/null
+++ b/crates/formality-core/README.md
@@ -0,0 +1,4 @@
+# formality-core
+
+`formality_core` is the language independent part of a-mir-formality.
+It can be reused by other projects looking to model formal semantics of languages besides Rust.
\ No newline at end of file
diff --git a/crates/formality-macros/Cargo.toml b/crates/formality-macros/Cargo.toml
index a75a6847..0d2346ae 100644
--- a/crates/formality-macros/Cargo.toml
+++ b/crates/formality-macros/Cargo.toml
@@ -2,6 +2,10 @@
 name = "formality-macros"
 version = "0.1.0"
 edition = "2021"
+license = "MIT OR Apache-2.0"
+description = "Macros used by a-mir-formality and formality-core"
+homepage = "https://rust-lang.github.io/a-mir-formality/"
+repository = "https://github.com/rust-lang/a-mir-formality/"
 
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 
@@ -11,8 +15,8 @@ proc-macro = true
 [dependencies]
 quote = "1.0.21"
 proc-macro2 = "1.0"
-syn = "1.0.102"
-synstructure = "0.12.6"
+syn = { version = "2.0", features = ["full"] }
+synstructure = "0.13.0"
 tracing = "0.1"
 convert_case = "0.6.0"
 
diff --git a/crates/formality-macros/READE.md b/crates/formality-macros/READE.md
new file mode 100644
index 00000000..23e51871
--- /dev/null
+++ b/crates/formality-macros/READE.md
@@ -0,0 +1,5 @@
+# formality-macros
+
+Procedural macros used by the formality system.
+Don't import this crate directly.
+Check out formality-core instead.
\ No newline at end of file
diff --git a/crates/formality-macros/src/cast.rs b/crates/formality-macros/src/cast.rs
index ef05b221..10efa4cb 100644
--- a/crates/formality-macros/src/cast.rs
+++ b/crates/formality-macros/src/cast.rs
@@ -91,5 +91,5 @@ fn downcast_to_variant(s: &synstructure::Structure, v: &VariantInfo) -> TokenStr
 }
 
 pub(crate) fn has_cast_attr(attrs: &[Attribute]) -> bool {
-    attrs.iter().any(|a| a.path.is_ident("cast"))
+    attrs.iter().any(|a| a.path().is_ident("cast"))
 }
diff --git a/crates/formality-macros/src/debug.rs b/crates/formality-macros/src/debug.rs
index e29fa0f0..2f7de119 100644
--- a/crates/formality-macros/src/debug.rs
+++ b/crates/formality-macros/src/debug.rs
@@ -237,7 +237,7 @@ fn debug_variant_with_attr(
 }
 
 fn get_grammar_attr(attrs: &[Attribute]) -> Option<syn::Result<FormalitySpec>> {
-    let attr = attrs.iter().find(|a| a.path.is_ident("grammar"))?;
+    let attr = attrs.iter().find(|a| a.path().is_ident("grammar"))?;
     Some(attr.parse_args())
 }
 
diff --git a/crates/formality-macros/src/parse.rs b/crates/formality-macros/src/parse.rs
index a3fa1f16..7e7f5b5e 100644
--- a/crates/formality-macros/src/parse.rs
+++ b/crates/formality-macros/src/parse.rs
@@ -206,7 +206,7 @@ fn lookahead(for_field: &Ident, op: Option<&FormalitySpecOp>) -> syn::Result<Lit
 }
 
 fn get_grammar_attr(attrs: &[Attribute]) -> Option<syn::Result<FormalitySpec>> {
-    let attr = attrs.iter().find(|a| a.path.is_ident("grammar"))?;
+    let attr = attrs.iter().find(|a| a.path().is_ident("grammar"))?;
     Some(attr.parse_args())
 }
 
diff --git a/crates/formality-macros/src/term.rs b/crates/formality-macros/src/term.rs
index a34609df..72c65847 100644
--- a/crates/formality-macros/src/term.rs
+++ b/crates/formality-macros/src/term.rs
@@ -40,7 +40,7 @@ fn remove_formality_attributes(input: &mut DeriveInput) {
         for variant in &mut v.variants {
             variant
                 .attrs
-                .retain(|attr| !attr.path.is_ident("grammar") && !attr.path.is_ident("cast"));
+                .retain(|attr| !attr.path().is_ident("grammar") && !attr.path().is_ident("cast"));
         }
     }
 }
diff --git a/src/main.rs b/src/main.rs
index 6e883a15..d5d52038 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -1,3 +1,3 @@
 fn main() -> anyhow::Result<()> {
-    formality_core::with_tracing_logs(formality::main)
+    formality_core::with_tracing_logs(a_mir_formality::main)
 }
diff --git a/tests/associated_type_normalization.rs b/tests/associated_type_normalization.rs
index 9ce3abcd..06461886 100644
--- a/tests/associated_type_normalization.rs
+++ b/tests/associated_type_normalization.rs
@@ -1,4 +1,4 @@
-use formality::test_where_clause;
+use a_mir_formality::test_where_clause;
 
 const MIRROR: &str = "[
     crate core {
diff --git a/tests/coherence_overlap.rs b/tests/coherence_overlap.rs
index b30e9bbb..0efb4db8 100644
--- a/tests/coherence_overlap.rs
+++ b/tests/coherence_overlap.rs
@@ -1,6 +1,6 @@
 #![allow(non_snake_case)] // we embed type names into the names for our test functions
 
-use formality::test_program_ok;
+use a_mir_formality::test_program_ok;
 use formality_macros::test;
 
 #[test]
diff --git a/tests/projection.rs b/tests/projection.rs
index 4b13edcd..eaa68498 100644
--- a/tests/projection.rs
+++ b/tests/projection.rs
@@ -1,4 +1,4 @@
-use formality::test_where_clause;
+use a_mir_formality::test_where_clause;
 
 const NORMALIZE_BASIC: &str = "[
     crate test {
@@ -260,7 +260,6 @@ const PROJECTION_EQUALITY: &str = "[
     }
 ]";
 
-
 #[test]
 fn projection_equality() {
     expect_test::expect![[r#"
diff --git a/tests/ui.rs b/tests/ui.rs
index 9421ab68..05f758e4 100644
--- a/tests/ui.rs
+++ b/tests/ui.rs
@@ -6,7 +6,7 @@ fn main() -> Result<()> {
     let mut config = Config::rustc("tests/ui");
     // Prevent ui_test from trying to query `formality` for the host platform name
     config.host = Some("non of ya bizniz".into());
-    config.program.program = "target/debug/formality".into();
+    config.program.program = "target/debug/a-mir-formality".into();
     config.mode = Mode::Fail {
         require_patterns: false,
     };