diff --git a/templates/ffi/FFI.lean b/templates/ffi/FFI.lean
new file mode 100644
index 0000000..6e1fc10
--- /dev/null
+++ b/templates/ffi/FFI.lean
@@ -0,0 +1,3 @@
+-- This module serves as the root of the `FFI` library.
+-- Import modules here that should be built as part of the library.
+import FFI.Basic
diff --git a/templates/ffi/FFI/Basic.lean b/templates/ffi/FFI/Basic.lean
new file mode 100644
index 0000000..3840f4e
--- /dev/null
+++ b/templates/ffi/FFI/Basic.lean
@@ -0,0 +1,5 @@
+import Blake3
+
+abbrev input : ByteArray := ⟨#[0]⟩
+
+def myHash := (Blake3.hash input).val.data
diff --git a/templates/ffi/Main.lean b/templates/ffi/Main.lean
new file mode 100644
index 0000000..83168b5
--- /dev/null
+++ b/templates/ffi/Main.lean
@@ -0,0 +1,5 @@
+import FFI
+
+def main : IO Unit :=
+ IO.println s!"Hash of [0]: {myHash}"
+
diff --git a/templates/ffi/flake.lock b/templates/ffi/flake.lock
new file mode 100644
index 0000000..83ab460
--- /dev/null
+++ b/templates/ffi/flake.lock
@@ -0,0 +1,233 @@
+{
+ "nodes": {
+ "blake3": {
+ "flake": false,
+ "locked": {
+ "lastModified": 1740955160,
+ "narHash": "sha256-Z07khB6ABvt6Q6YqOUAi9nFRXLZMfcEnjc3mH1OieUE=",
+ "owner": "BLAKE3-team",
+ "repo": "BLAKE3",
+ "rev": "9edb473fa81c422acc2cb611f55c4df52d1cdbbb",
+ "type": "github"
+ },
+ "original": {
+ "owner": "BLAKE3-team",
+ "repo": "BLAKE3",
+ "type": "github"
+ }
+ },
+ "blake3-lean": {
+ "inputs": {
+ "blake3": "blake3",
+ "flake-parts": "flake-parts",
+ "lean4-nix": "lean4-nix",
+ "nixpkgs": [
+ "nixpkgs"
+ ]
+ },
+ "locked": {
+ "lastModified": 1741315082,
+ "narHash": "sha256-4Azr/5gt+h6ydaza1MEcjDV164qrPQRMXiRRbWXET/k=",
+ "owner": "argumentcomputer",
+ "repo": "Blake3.lean",
+ "rev": "29018d578b043f6638907f3425af839eec345361",
+ "type": "github"
+ },
+ "original": {
+ "owner": "argumentcomputer",
+ "repo": "Blake3.lean",
+ "rev": "29018d578b043f6638907f3425af839eec345361",
+ "type": "github"
+ }
+ },
+ "flake-parts": {
+ "inputs": {
+ "nixpkgs-lib": "nixpkgs-lib"
+ },
+ "locked": {
+ "lastModified": 1740872218,
+ "narHash": "sha256-ZaMw0pdoUKigLpv9HiNDH2Pjnosg7NBYMJlHTIsHEUo=",
+ "owner": "hercules-ci",
+ "repo": "flake-parts",
+ "rev": "3876f6b87db82f33775b1ef5ea343986105db764",
+ "type": "github"
+ },
+ "original": {
+ "owner": "hercules-ci",
+ "repo": "flake-parts",
+ "type": "github"
+ }
+ },
+ "flake-parts_2": {
+ "inputs": {
+ "nixpkgs-lib": "nixpkgs-lib_2"
+ },
+ "locked": {
+ "lastModified": 1740872218,
+ "narHash": "sha256-ZaMw0pdoUKigLpv9HiNDH2Pjnosg7NBYMJlHTIsHEUo=",
+ "owner": "hercules-ci",
+ "repo": "flake-parts",
+ "rev": "3876f6b87db82f33775b1ef5ea343986105db764",
+ "type": "github"
+ },
+ "original": {
+ "owner": "hercules-ci",
+ "repo": "flake-parts",
+ "type": "github"
+ }
+ },
+ "flake-parts_3": {
+ "inputs": {
+ "nixpkgs-lib": "nixpkgs-lib_3"
+ },
+ "locked": {
+ "lastModified": 1740872218,
+ "narHash": "sha256-ZaMw0pdoUKigLpv9HiNDH2Pjnosg7NBYMJlHTIsHEUo=",
+ "owner": "hercules-ci",
+ "repo": "flake-parts",
+ "rev": "3876f6b87db82f33775b1ef5ea343986105db764",
+ "type": "github"
+ },
+ "original": {
+ "owner": "hercules-ci",
+ "repo": "flake-parts",
+ "type": "github"
+ }
+ },
+ "flake-parts_4": {
+ "inputs": {
+ "nixpkgs-lib": "nixpkgs-lib_4"
+ },
+ "locked": {
+ "lastModified": 1740872218,
+ "narHash": "sha256-ZaMw0pdoUKigLpv9HiNDH2Pjnosg7NBYMJlHTIsHEUo=",
+ "owner": "hercules-ci",
+ "repo": "flake-parts",
+ "rev": "3876f6b87db82f33775b1ef5ea343986105db764",
+ "type": "github"
+ },
+ "original": {
+ "owner": "hercules-ci",
+ "repo": "flake-parts",
+ "type": "github"
+ }
+ },
+ "lean4-nix": {
+ "inputs": {
+ "flake-parts": "flake-parts_2",
+ "nixpkgs": [
+ "blake3-lean",
+ "nixpkgs"
+ ]
+ },
+ "locked": {
+ "lastModified": 1741177057,
+ "narHash": "sha256-xcd74c7oDQvEJHeQfJaJt7/HWBcCDrS5Ki0DtOEe1dA=",
+ "owner": "argumentcomputer",
+ "repo": "lean4-nix",
+ "rev": "29b86ca0f5c9db6186311b21fde6a634be3f2d74",
+ "type": "github"
+ },
+ "original": {
+ "owner": "argumentcomputer",
+ "repo": "lean4-nix",
+ "type": "github"
+ }
+ },
+ "lean4-nix_2": {
+ "inputs": {
+ "flake-parts": "flake-parts_4",
+ "nixpkgs": [
+ "nixpkgs"
+ ]
+ },
+ "locked": {
+ "lastModified": 1741177057,
+ "narHash": "sha256-xcd74c7oDQvEJHeQfJaJt7/HWBcCDrS5Ki0DtOEe1dA=",
+ "owner": "argumentcomputer",
+ "repo": "lean4-nix",
+ "rev": "29b86ca0f5c9db6186311b21fde6a634be3f2d74",
+ "type": "github"
+ },
+ "original": {
+ "owner": "argumentcomputer",
+ "repo": "lean4-nix",
+ "type": "github"
+ }
+ },
+ "nixpkgs": {
+ "locked": {
+ "lastModified": 1741173522,
+ "narHash": "sha256-k7VSqvv0r1r53nUI/IfPHCppkUAddeXn843YlAC5DR0=",
+ "owner": "nixos",
+ "repo": "nixpkgs",
+ "rev": "d69ab0d71b22fa1ce3dbeff666e6deb4917db049",
+ "type": "github"
+ },
+ "original": {
+ "owner": "nixos",
+ "ref": "nixos-unstable",
+ "repo": "nixpkgs",
+ "type": "github"
+ }
+ },
+ "nixpkgs-lib": {
+ "locked": {
+ "lastModified": 1740872140,
+ "narHash": "sha256-3wHafybyRfpUCLoE8M+uPVZinImg3xX+Nm6gEfN3G8I=",
+ "type": "tarball",
+ "url": "https://github.com/NixOS/nixpkgs/archive/6d3702243441165a03f699f64416f635220f4f15.tar.gz"
+ },
+ "original": {
+ "type": "tarball",
+ "url": "https://github.com/NixOS/nixpkgs/archive/6d3702243441165a03f699f64416f635220f4f15.tar.gz"
+ }
+ },
+ "nixpkgs-lib_2": {
+ "locked": {
+ "lastModified": 1740872140,
+ "narHash": "sha256-3wHafybyRfpUCLoE8M+uPVZinImg3xX+Nm6gEfN3G8I=",
+ "type": "tarball",
+ "url": "https://github.com/NixOS/nixpkgs/archive/6d3702243441165a03f699f64416f635220f4f15.tar.gz"
+ },
+ "original": {
+ "type": "tarball",
+ "url": "https://github.com/NixOS/nixpkgs/archive/6d3702243441165a03f699f64416f635220f4f15.tar.gz"
+ }
+ },
+ "nixpkgs-lib_3": {
+ "locked": {
+ "lastModified": 1740872140,
+ "narHash": "sha256-3wHafybyRfpUCLoE8M+uPVZinImg3xX+Nm6gEfN3G8I=",
+ "type": "tarball",
+ "url": "https://github.com/NixOS/nixpkgs/archive/6d3702243441165a03f699f64416f635220f4f15.tar.gz"
+ },
+ "original": {
+ "type": "tarball",
+ "url": "https://github.com/NixOS/nixpkgs/archive/6d3702243441165a03f699f64416f635220f4f15.tar.gz"
+ }
+ },
+ "nixpkgs-lib_4": {
+ "locked": {
+ "lastModified": 1740872140,
+ "narHash": "sha256-3wHafybyRfpUCLoE8M+uPVZinImg3xX+Nm6gEfN3G8I=",
+ "type": "tarball",
+ "url": "https://github.com/NixOS/nixpkgs/archive/6d3702243441165a03f699f64416f635220f4f15.tar.gz"
+ },
+ "original": {
+ "type": "tarball",
+ "url": "https://github.com/NixOS/nixpkgs/archive/6d3702243441165a03f699f64416f635220f4f15.tar.gz"
+ }
+ },
+ "root": {
+ "inputs": {
+ "blake3-lean": "blake3-lean",
+ "flake-parts": "flake-parts_3",
+ "lean4-nix": "lean4-nix_2",
+ "nixpkgs": "nixpkgs"
+ }
+ }
+ },
+ "root": "root",
+ "version": 7
+}
diff --git a/templates/ffi/flake.nix b/templates/ffi/flake.nix
new file mode 100644
index 0000000..ab8a67e
--- /dev/null
+++ b/templates/ffi/flake.nix
@@ -0,0 +1,63 @@
+{
+ description = "Lean 4 Example Project";
+
+ inputs = {
+ nixpkgs.url = "github:nixos/nixpkgs/nixos-unstable";
+ flake-parts.url = "github:hercules-ci/flake-parts";
+ lean4-nix = {
+ url = "github:argumentcomputer/lean4-nix";
+ inputs.nixpkgs.follows = "nixpkgs";
+ };
+ blake3-lean = {
+ url = "github:argumentcomputer/Blake3.lean?rev=29018d578b043f6638907f3425af839eec345361";
+ inputs.nixpkgs.follows = "nixpkgs";
+ };
+ };
+
+ outputs = inputs @ {
+ nixpkgs,
+ flake-parts,
+ lean4-nix,
+ blake3-lean,
+ ...
+ }:
+ flake-parts.lib.mkFlake {inherit inputs;} {
+ systems = [
+ "aarch64-darwin"
+ "aarch64-linux"
+ "x86_64-darwin"
+ "x86_64-linux"
+ ];
+
+ perSystem = {
+ system,
+ pkgs,
+ ...
+ }:
+ let
+ blake3 = blake3-lean.inputs.blake3;
+ blake3Mod = (blake3-lean.lib { inherit pkgs lean4-nix blake3; }).lib;
+ blake3Lib = blake3Mod.blake3-lib;
+ blake3C = blake3Mod.blake3-c;
+ in
+ {
+ _module.args.pkgs = import nixpkgs {
+ inherit system;
+ overlays = [(lean4-nix.readToolchainFile ./lean-toolchain)];
+ };
+
+ packages.default = (pkgs.lean.buildLeanPackage {
+ name = "ffi";
+ src = ./.;
+ roots = ["FFI" "Main"];
+ deps = [ blake3Lib ];
+ staticLibDeps = [ blake3C ];
+ linkFlags = [ "-L${blake3C}/lib" "-lblake3" ];
+ }).executable;
+
+ devShells.default = pkgs.mkShell {
+ packages = with pkgs.lean; [lean lean-all];
+ };
+ };
+ };
+}
diff --git a/templates/ffi/lake-manifest.json b/templates/ffi/lake-manifest.json
new file mode 100644
index 0000000..38ca140
--- /dev/null
+++ b/templates/ffi/lake-manifest.json
@@ -0,0 +1,15 @@
+{"version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "https://github.com/argumentcomputer/Blake3.lean",
+ "type": "git",
+ "subDir": null,
+ "scope": "",
+ "rev": "29018d578b043f6638907f3425af839eec345361",
+ "name": "Blake3",
+ "manifestFile": "lake-manifest.json",
+ "inputRev": "29018d578b043f6638907f3425af839eec345361",
+ "inherited": false,
+ "configFile": "lakefile.lean"}],
+ "name": "ffi",
+ "lakeDir": ".lake"}
diff --git a/templates/ffi/lakefile.lean b/templates/ffi/lakefile.lean
new file mode 100644
index 0000000..d4b9e94
--- /dev/null
+++ b/templates/ffi/lakefile.lean
@@ -0,0 +1,15 @@
+import Lake
+open Lake DSL
+
+require Blake3 from git
+ "https://github.com/argumentcomputer/Blake3.lean" @ "29018d578b043f6638907f3425af839eec345361"
+
+package "ffi" where
+ version := v!"0.1.0"
+
+lean_lib «FFI» where
+ -- add library configuration options here
+
+@[default_target]
+lean_exe "ffi" where
+ root := `Main
diff --git a/templates/ffi/lean-toolchain b/templates/ffi/lean-toolchain
new file mode 100644
index 0000000..5499a24
--- /dev/null
+++ b/templates/ffi/lean-toolchain
@@ -0,0 +1 @@
+leanprover/lean4:v4.17.0