diff --git a/LICENSE b/LICENSE
new file mode 100644
index 0000000..de00807
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,28 @@
+BSD 3-Clause License
+
+Copyright (c) 2024-2026, Runtime Verification Inc.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+1. Redistributions of source code must retain the above copyright notice, this
+   list of conditions and the following disclaimer.
+
+2. Redistributions in binary form must reproduce the above copyright notice,
+   this list of conditions and the following disclaimer in the documentation
+   and/or other materials provided with the distribution.
+
+3. Neither the name of the copyright holder nor the names of its
+   contributors may be used to endorse or promote products derived from
+   this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
+AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
+IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
+FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
+SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
+CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
+OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/README.md b/README.md
index bcbc9fb..fda8ffd 100644
--- a/README.md
+++ b/README.md
@@ -1 +1,121 @@
 # kframework-rs
+
+Rust bindings for the [K Framework](https://github.com/runtimeverification/k): a KORE pattern parser/serializer and FFI wrappers for the KLLVM execution backend.
+
+
+## Crates
+
+### `kframework`
+
+Parses and manipulates KORE (K's intermediate representation) in pure Rust, with no native dependencies.
+
+- Lexer and parser for textual KORE patterns, sorts, sentences, and definitions
+- Full AST for KORE (`Pattern`, `Sort`, `App`, `Sentence`, `Definition`, ...)
+- JSON serialization and deserialization via `serde`
+- `PatternVisitor` trait for custom traversals
+- `kore-to-json` binary: reads a `.kore` file and prints JSON to stdout
+
+
+### `kframework_ffi`
+
+Rust wrappers around the KLLVM C API (`interpreter.so`). Lets you execute K semantics compiled with `kompile --llvm-kompile-type c` from Rust.
+
+- `Pattern`: owns a `kore_pattern *`; parse from a KORE string or build from a `Symbol`
+- `Block`: wraps KLLVM's interned term representation; runs execution via `take_steps`
+- `Sort` / `Symbol`: RAII wrappers with `Drop` implementations
+- `Marshaller<H>`: converts a `kore::Pattern` tree to kllvm, substituting typed variables through a user-supplied `VarHandler`; caches variable-free subtrees across calls
+
+
+## Getting Started
+
+### Prerequisites
+
+- Rust 1.85.0+
+- `libclang` (`kframework_ffi` only)
+- A `kompile`-built `interpreter.so` on `LD_LIBRARY_PATH` (`kframework_ffi` only)
+
+
+### Build
+
+```sh
+# Build the pure-Rust kframework crate only
+cargo build -p kframework
+
+# Build everything (requires interpreter.so)
+cargo build
+```
+
+
+### Test
+
+```sh
+cargo test
+```
+
+
+### Format & Lint
+
+```sh
+cargo fmt
+cargo clippy --all-targets -- --deny warnings
+```
+
+Or run all checks at once:
+
+```sh
+make
+```
+
+
+## Usage
+
+### Parsing a KORE Pattern
+
+```rust
+use kframework::kore::Parser;
+
+let mut parser = Parser::new(r#"\dv{SortInt{}}("42")"#)?;
+let pattern = parser.pattern()?;
+println!("{:?}", pattern);
+```
+
+
+### Converting a `.kore` File to JSON
+
+```sh
+cargo run --bin kore-to-json -- path/to/file.kore
+```
+
+
+### Executing K Semantics via KLLVM
+
+```rust
+use kframework_ffi::kllvm;
+
+kllvm::init();
+
+let pattern: kllvm::Pattern = KORE_STRING.parse().expect("parse failed");
+let mut block: kllvm::Block = pattern.into();
+block.take_steps(-1); // run to completion
+
+let result: kllvm::Pattern = block.into();
+println!("{result}");
+
+kllvm::free_all_memory();
+```
+
+See [`kframework_ffi/src/kllvm.rs`](kframework_ffi/src/kllvm.rs) for the full API.
+
+
+## Examples
+
+### Fuzzer (`examples/fuzzer`)
+
+Uses `kframework_ffi` with [honggfuzz](https://github.com/rust-fuzz/honggfuzz-rs) to fuzz K semantics compiled from the bundled Imp language definition.
+
+See [`examples/fuzzer/README.md`](examples/fuzzer/README.md) for setup instructions.
+
+
+## License
+
+BSD 3-Clause. Copyright (c) 2024-2026 Runtime Verification Inc. See [LICENSE](LICENSE) for details.