diff --git a/README.md b/README.md
index 35a11f1..65e7d9a 100644
--- a/README.md
+++ b/README.md
@@ -1,7 +1,7 @@
-# Juvix Lean formalization library
+# Juvix library for Lean 4
 
 The Juvix Lean library provides primitives for verifying the correctness of Juvix compiler runs, i.e., proving that the semantics of a particular Juvix program is preserved by the compilation process.
 
-The major components of the library include:
-- formalization of Juvix compiler internal representations and their semantics,
-- proof-producing metaprograms for verifying that individual Juvix compiler transformations preserve the semantics.
+The library includes:
+- formalization of Juvix compiler internal representations (IRs) and their semantics,
+- proof-producing metaprograms for verifying that Juvix compiler transformations preserve the semantics of concrete IR programs.