diff --git a/.gitignore b/.gitignore
index 9ea0f13..01fc188 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,2 +1,3 @@
 .*
+*.olean
 !.gitignore
diff --git a/Cargo.lock b/Cargo.lock
index d33082b..6a1a17f 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -11,12 +11,23 @@ dependencies = [
  "memchr",
 ]
 
+[[package]]
+name = "annotate-snippets"
+version = "0.9.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ccaf7e9dfbb6ab22c82e473cd1a8a7bd313c19a5b7e40970f3d89ef5a5c9e81e"
+dependencies = [
+ "unicode-width",
+ "yansi-term",
+]
+
 [[package]]
 name = "bindgen"
 version = "0.69.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "a00dc851838a2120612785d195287475a3ac45514741da670b735818822129a0"
 dependencies = [
+ "annotate-snippets",
  "bitflags",
  "cexpr",
  "clang-sys",
@@ -242,6 +253,7 @@ name = "rustcalllean"
 version = "0.1.0"
 dependencies = [
  "bindgen",
+ "libc",
 ]
 
 [[package]]
@@ -280,6 +292,12 @@ version = "1.0.12"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "3354b9ac3fae1ff6755cb6db53683adb661634f67557942dea4facebec0fee4b"
 
+[[package]]
+name = "unicode-width"
+version = "0.1.11"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e51733f11c9c4f72aa0c160008246859e340b00807569a0da0e7a1079b27ba85"
+
 [[package]]
 name = "which"
 version = "4.4.2"
@@ -292,6 +310,28 @@ dependencies = [
  "rustix",
 ]
 
+[[package]]
+name = "winapi"
+version = "0.3.9"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5c839a674fcd7a98952e593242ea400abe93992746761e38641405d28b00f419"
+dependencies = [
+ "winapi-i686-pc-windows-gnu",
+ "winapi-x86_64-pc-windows-gnu",
+]
+
+[[package]]
+name = "winapi-i686-pc-windows-gnu"
+version = "0.4.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ac3b87c63620426dd9b991e5ce0329eff545bccbbb34f3be09ff6fb6ab51b7b6"
+
+[[package]]
+name = "winapi-x86_64-pc-windows-gnu"
+version = "0.4.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "712e227841d057c1ee1cd2fb22fa7e5a5461ae8e48fa2ca79ec42cfc1931183f"
+
 [[package]]
 name = "windows-sys"
 version = "0.52.0"
@@ -357,3 +397,12 @@ name = "windows_x86_64_msvc"
 version = "0.52.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "32b752e52a2da0ddfbdbcc6fceadfeede4c939ed16d13e648833a61dfb611ed8"
+
+[[package]]
+name = "yansi-term"
+version = "0.1.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "fe5c30ade05e61656247b2e334a031dfd0cc466fadef865bdcdea8d537951bf1"
+dependencies = [
+ "winapi",
+]
diff --git a/Cargo.toml b/Cargo.toml
index 9de7b0a..c6d3a93 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -9,6 +9,8 @@ edition = "2021"
 rust-version = "1.73"
 
 [dependencies]
+libc = "0.2.153"
 
 [build-dependencies]
-bindgen = "0.69.4"
+# the experimental flag must be enabled
+bindgen = { version = "0.69.4", features = ["experimental"] }
diff --git a/README.md b/README.md
index fc2fa99..476bb27 100644
--- a/README.md
+++ b/README.md
@@ -7,3 +7,4 @@ This is based on:
 * [Lean4 FFI](https://lean-lang.org/lean4/doc/dev/ffi.html#initialization)
 * [Rustonomicon FFI](https://doc.rust-lang.org/nomicon/ffi.html)
 * [Rust Bindgen](https://rust-lang.github.io/rust-bindgen/introduction.html)
+* [Rust Bindgen Static Functions](https://github.com/rust-lang/rust-bindgen/discussions/2405)
diff --git a/build.rs b/build.rs
index da9e4a2..573fa3b 100644
--- a/build.rs
+++ b/build.rs
@@ -7,6 +7,7 @@ fn main()
 {
 	let callee_root = env::var("CALLEE_PATH").expect("Callee path variable must be available");
 	let lean_root = env::var("LEAN_ROOT").expect("Lean root must exist");
+	let input = format!("{lean_root}/include/lean/lean.h");
 	println!("cargo:rustc-link-search={callee_root}");
 	println!("cargo:rustc-link-search={lean_root}/lib/lean");
 	println!("cargo:rustc-link-lib={CALLEE_NAME}");
@@ -19,18 +20,81 @@ fn main()
 	let bindings = bindgen::Builder::default()
 		// The input header we would like to generate
 		// bindings for.
-		.header(format!("{lean_root}/include/lean/lean.h"))
+		.header(&input)
 		// Tell cargo to invalidate the built crate whenever any of the
 		// included header files changed.
 		.parse_callbacks(Box::new(bindgen::CargoCallbacks::new()))
+		// The following is specific to `lean.h`: There are a lot of static
+		// function
+		.wrap_static_fns(true)
+		// but some functions use `_Atomic(int)` types that bindgen cannot handle,
+		// so they are blocklisted. The types which use `_Atomic` are treated as
+		// opaque.
+		.blocklist_function("lean_get_rc_mt_addr")
+		.opaque_type("lean_thunk_object")
+		.opaque_type("lean_task_object")
 		// Finish the builder and generate the bindings.
 		.generate()
 		// Unwrap the Result and panic on failure.
 		.expect("Unable to generate bindings");
 
+	let extern_src_path = std::env::temp_dir().join("bindgen").join("extern.c");
+	let extern_obj_path = std::env::temp_dir().join("bindgen").join("extern.o");
+	let output_path = PathBuf::from(std::env::var("OUT_DIR").unwrap());
 	// Write the bindings to the $OUT_DIR/bindings.rs file.
 	let out_path = PathBuf::from(env::var("OUT_DIR").unwrap());
 	bindings
 		.write_to_file(out_path.join("lean.rs"))
 		.expect("Couldn't write bindings!");
+
+	// This is the path to the object file.
+	let obj_path = output_path.join("extern.o");
+	// This is the path to the static library file.
+	let lib_path = output_path.join("libextern.a");
+
+	// Compile the generated wrappers into an object file.
+	let clang_output = std::process::Command::new("clang")
+		.arg("-O")
+		.arg("-c")
+		.arg("-o")
+		.arg(extern_obj_path)
+		.arg(extern_src_path)
+		.arg("-include")
+		.arg(&input)
+		.output()
+		.unwrap();
+	if !clang_output.status.success() {
+		panic!(
+			"Could not compile object file:\n{}",
+			String::from_utf8_lossy(&clang_output.stderr)
+		);
+	}
+
+	// Turn the object file into a static library
+	#[cfg(not(target_os = "windows"))]
+	let lib_output = std::process::Command::new("ar")
+		.arg("rcs")
+		.arg(output_path.join(&lib_path))
+		.arg(obj_path)
+		.output()
+		.unwrap();
+	#[cfg(target_os = "windows")]
+	let lib_output = std::process::Command::new("LIB")
+		.arg(obj_path)
+		.arg(format!(
+			"/OUT:{}",
+			out_dir_path.join("libextern.lib").display()
+		))
+		.output()
+		.unwrap();
+	if !lib_output.status.success() {
+		panic!(
+			"Could not emit library file:\n{}",
+			String::from_utf8_lossy(&lib_output.stderr)
+		);
+	}
+
+	// Statically link against the generated lib
+	println!("cargo:rustc-link-search={}", output_path.display());
+	println!("cargo:rustc-link-lib=static=extern");
 }
diff --git a/flake.nix b/flake.nix
index 6ee59d4..bc67e74 100644
--- a/flake.nix
+++ b/flake.nix
@@ -41,6 +41,8 @@
         LEAN_ROOT = leanPkgs.lean-all;
         buildInputs = common ++ [
           pkgs.rustc
+          # This is not needed for compilation. It is here for diagnostic purposes
+          pkgs.rust-bindgen
         ];
       };
     };
diff --git a/rust-toolchain.toml b/rust-toolchain.toml
new file mode 100644
index 0000000..5d56faf
--- /dev/null
+++ b/rust-toolchain.toml
@@ -0,0 +1,2 @@
+[toolchain]
+channel = "nightly"
diff --git a/src/main.rs b/src/main.rs
index ef3c08f..79a52c5 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -1,21 +1,51 @@
 #[allow(non_upper_case_globals)]
 #[allow(non_camel_case_types)]
 #[allow(non_snake_case)]
-mod lean {
+#[allow(dead_code)]
+mod lean
+{
 	include!(concat!(env!("OUT_DIR"), "/lean.rs"));
 
-	#[link(name="lean")]
-	extern {
+	#[link(name = "lean")]
+	extern "C" {
 		pub fn lean_initialize_runtime_module();
 		pub fn lean_initialize();
 		// lean_io_mark_end_initialization is already defined.
 	}
+	#[link(name = "Callee")]
+	extern "C" {
+		pub fn initialize_Callee(builtin: u8, world: *mut lean_object) -> *mut lean_object;
+		pub fn my_function(s: lean_obj_arg) -> lean_obj_arg;
+	}
 }
-fn main() {
+fn main()
+{
 	unsafe {
 		lean::lean_initialize_runtime_module();
 		lean::lean_initialize();
+		let builtin: u8 = 1;
+		let res = lean::initialize_Callee(builtin, lean::lean_io_mk_world());
+		if lean::lean_io_result_is_ok(res) {
+			lean::lean_dec_ref(res);
+		} else {
+			lean::lean_io_result_show_error(res);
+			lean::lean_dec(res);
+			panic!("Failed to load callee");
+		}
 		lean::lean_io_mark_end_initialization();
 	}
-   println!("Lean initialization complete!");
+	println!("Lean initialization complete!");
+
+	let c_str = std::ffi::CString::new("hello ").unwrap();
+	let result = unsafe {
+		let native_str = lean::lean_mk_string(c_str.as_ptr());
+		let result_obj = lean::my_function(native_str);
+		let result_c_str = std::ffi::CStr::from_ptr(lean::lean_string_cstr(result_obj));
+		let str = result_c_str.to_str().unwrap().to_string();
+		// Clean up the resultant objects
+		lean::lean_dec(result_obj);
+		str
+	};
+
+	println!("result: {result}");
 }