diff --git a/llmfv/.envrc b/.envrc
similarity index 100%
rename from llmfv/.envrc
rename to .envrc
diff --git a/.gitignore b/.gitignore
index 1d74e21..bbc15c1 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1 +1,23 @@
-.vscode/
+# test outputs
+artefacts/hypothesis/*.py
+artefacts/lean/*.lean
+
+# hypotheses
+.hypothesis/
+
+# env
+.env
+
+# python generated files
+__pycache__/
+*.py[oc]
+build/
+dist/
+wheels/
+*.egg-info
+
+
+# venv
+.venv
+
+.ipynb_checkpoints/
diff --git a/llmfv/.python-version b/.python-version
similarity index 100%
rename from llmfv/.python-version
rename to .python-version
diff --git a/README.md b/README.md
index 70870b1..c4dc928 100644
--- a/README.md
+++ b/README.md
@@ -1,3 +1,24 @@
+# LLM-FV: Toward Scaling Formal Verification Schemes via LLMs
+
+Describe your project here.
+
+
+# Setup
+
+```
+rye sync
+```
+
+Create a `.env` file in `nb/` next to this README with the following:
+```
+ANTHROPIC_API_KEY="YOUR_KEY_HERE"
+```
+
+
+# Basic Run
+You can try to run `python example_agent_run.py`. This will attempt to create tests using claude for the example function in `test/example_func.py`.
+
+Once it completes (successfully), you can re-test the final output with `pytest test/test_example_func.py`. 
 # Formally Verified APPS
 
 ## Conceptually 1
diff --git a/llmfv/artefacts/hypothesis/.gitkeep b/artefacts/hypothesis/.gitkeep
similarity index 100%
rename from llmfv/artefacts/hypothesis/.gitkeep
rename to artefacts/hypothesis/.gitkeep
diff --git a/llmfv/artefacts/lean/.gitkeep b/artefacts/lean/.gitkeep
similarity index 100%
rename from llmfv/artefacts/lean/.gitkeep
rename to artefacts/lean/.gitkeep
diff --git a/imp/.gitignore b/imp/.gitignore
deleted file mode 100644
index bfb30ec..0000000
--- a/imp/.gitignore
+++ /dev/null
@@ -1 +0,0 @@
-/.lake
diff --git a/imp/Imp.lean b/imp/Imp.lean
deleted file mode 100644
index 1d90f2a..0000000
--- a/imp/Imp.lean
+++ /dev/null
@@ -1,2 +0,0 @@
-import Imp.Expr
-import Imp.Stmt
diff --git a/imp/Imp/Expr.lean b/imp/Imp/Expr.lean
deleted file mode 100644
index e21183f..0000000
--- a/imp/Imp/Expr.lean
+++ /dev/null
@@ -1,7 +0,0 @@
-/-
-This file exists only to re-export the contents of the `Imp.Expr` module hierarchy.
--/
-import Imp.Expr.Basic
-import Imp.Expr.Delab
-import Imp.Expr.Eval
-import Imp.Expr.Syntax
diff --git a/imp/Imp/Expr/Basic.lean b/imp/Imp/Expr/Basic.lean
deleted file mode 100644
index a2d7723..0000000
--- a/imp/Imp/Expr/Basic.lean
+++ /dev/null
@@ -1,26 +0,0 @@
-namespace Imp.Expr
-
-/-- Unary operators -/
-inductive UnOp where
-  | neg
-  | not
-deriving Repr, DecidableEq
-
-/-- Binary operators -/
-inductive BinOp where
-  | plus | minus | times | div
-  | and | or
-  | lt | le | eq
-  | append
-deriving Repr, DecidableEq
-
-end Expr
-
-/-- Expressions -/
-inductive Expr where
-  | constInt (i : Int)
-  | constStr (x : String)
-  | var (name : String)
-  | un (op : Expr.UnOp) (e : Expr)
-  | bin (op : Expr.BinOp) (e1 e2 : Expr)
-deriving Repr, DecidableEq
diff --git a/imp/Imp/Expr/Delab.lean b/imp/Imp/Expr/Delab.lean
deleted file mode 100644
index 284b93d..0000000
--- a/imp/Imp/Expr/Delab.lean
+++ /dev/null
@@ -1,125 +0,0 @@
-/-
-This file makes the convenient syntax from `Imp.Expr.Syntax` show up in Lean's output. It's not part
-of what's being taught in the lectures.
--/
-import Lean.PrettyPrinter.Delaborator
-import Imp.Expr.Basic
-import Imp.Expr.Syntax
-
-open Lean PrettyPrinter Delaborator SubExpr Parenthesizer
-
-namespace Imp.Expr.Delab
-
-def annAsTerm {any} (stx : TSyntax any) : DelabM (TSyntax any) :=
-  (⟨·⟩) <$> annotateTermInfo ⟨stx.raw⟩
-
-def delabNameInner : DelabM (TSyntax `varname) := do
-  let e ← getExpr
-  match e with
-  | .lit (.strVal s) =>
-    let x := mkIdent <| .mkSimple s
-    pure <| ⟨x.raw⟩
-  | _ => `(varname|~($(← delab))) >>= annAsTerm
-
--- def delabStrInner : DelabM (TSyntax `str) := do
---   let e ← getExpr
---   match e with
---   | .lit (.strVal s) =>
---     let x := mkIdent <| .mkSimple s
-
-partial def delabExprInner : DelabM (TSyntax `exp) := do
-  let e ← getExpr
-  let stx ←
-    match_expr e with
-    | Expr.constInt x =>
-      match_expr x with
-      | OfNat.ofNat _ n _ =>
-        if let some n' := n.nat? then
-          pure <| ⟨Syntax.mkNumLit (toString n') |>.raw⟩
-        else if let .lit (.natVal n') := n then
-          pure <| ⟨Syntax.mkNumLit (toString n') |>.raw⟩
-        else withAppArg `(exp| ~$(← delab))
-      | Int.ofNat n =>
-        if let some n' := n.nat? then
-          pure <| ⟨Syntax.mkNumLit (toString n') |>.raw⟩
-        else if let .lit (.natVal n') := n then
-          pure <| ⟨Syntax.mkNumLit (toString n') |>.raw⟩
-        else withAppArg `(exp| ~$(← delab))
-      | BitVec.ofNat _ _ => (⟨·.raw⟩) <$> (withAppArg <| withAppArg <| delab)
-      | _ =>
-        `(exp| ~(Expr.constInt $(← withAppArg delab)))
-    | Expr.var _ => do
-      let x ← withAppArg delabNameInner
-      `(exp|$x:varname)
-    | Expr.bin op _ _ =>
-      let s1 ← withAppFn <| withAppArg delabExprInner
-      let s2 ← withAppArg delabExprInner
-      match_expr op with
-      | BinOp.plus => `(exp| $s1 + $s2)
-      | BinOp.minus => `(exp| $s1 - $s2)
-      | BinOp.times => `(exp| $s1 * $s2)
-      | BinOp.div => `(exp| $s1 / $s2)
-      | BinOp.and => `(exp| $s1 && $s2)
-      | BinOp.or => `(exp| $s1 || $s2)
-      | BinOp.lt => `(exp| $s1 < $s2)
-      | BinOp.le => `(exp| $s1 ≤ $s2)
-      | BinOp.eq => `(exp| $s1 == $s2)
-      | BinOp.append => `(exp| $s1 ++ $s2)
-      | _ => `(exp|~(Expr.bin $(← withAppFn <| withAppFn <| withAppArg delab) $(← withAppFn <| withAppArg delab) $(← withAppArg delab)))
-    | Expr.un op _ =>
-      let s ← withAppArg delabExprInner
-      match_expr op with
-      | UnOp.neg => `(exp| -$s)
-      | UnOp.not => `(exp| !$s)
-      | _ => `(exp| ~(Expr.un $(← withAppFn <| withAppArg delab) $(← withAppArg delab)))
-    | _ =>
-      `(exp| ~$(← delab))
-  annAsTerm stx
-
-@[delab app.Imp.Expr.const, delab app.Imp.Expr.var, delab app.Imp.Expr.un, delab app.Imp.Expr.bin]
-partial def delabExpr : Delab := do
-  -- This delaborator only understands a certain arity - give up if it's incorrect
-  guard <| match_expr ← getExpr with
-    | Expr.const _ => true
-    | Expr.var _ => true
-    | Expr.un _ _ => true
-    | Expr.bin _ _ _ => true
-    | _ => false
-  match ← delabExprInner with
-  | `(exp|~$e) => pure e
-  | e => `(term|expr {$(⟨e⟩)})
-
-/- info: expr { 5 } : Expr -/
--- #guard_msgs in
-#check Expr.constInt 5
-
-/- info: expr { 5 } : Expr -/
--- #guard_msgs in
-#check expr { 5 }
-
-/- info: expr { [a] } : Expr -/
--- #guard_msgs in
-#check Expr.constStr "a"
-
-/- info: expr { [a] } : Expr -/
--- #guard_msgs in
--- #check expr { [a] }
-
-/-- info: expr { x } : Expr -/
-#guard_msgs in
-#check expr { x }
-
-/-- info: expr { 5 + 23 - 10 } : Expr -/
-#guard_msgs in
-#check expr { 5 + 23 - 10 }
-
-/-- info: expr { 5 + (23 - 10) } : Expr -/
-#guard_msgs in
-#check expr { 5 + (23 - 10) }
-
-/-
-info: let x := expr { 23 };
-expr { ~x * ~x } : Expr
--/
--- #guard_msgs in
-#check let x := expr {23}; expr {~x * ~x}
diff --git a/imp/Imp/Expr/Eval.lean b/imp/Imp/Expr/Eval.lean
deleted file mode 100644
index fada173..0000000
--- a/imp/Imp/Expr/Eval.lean
+++ /dev/null
@@ -1,91 +0,0 @@
-import Imp.Expr.Basic
-
-open Lean
-
-namespace Imp
-
-inductive Value where
-| str : String -> Value
-| int : Int -> Value
-
-instance : OfNat Value n := by
-  constructor
-  exact (Value.int n)
-
-/-- An environment maps variables names to their values (no pointers) -/
-def Env := String → Value
-
-namespace Env
-
-/-- Set a value in an environment -/
-def set (x : String) (v : Value) (σ : Env) : Env :=
-  fun y => if x == y then v else σ y
-
-def setOption (x : String) (v : Option Value) (σ : Env) : Env :=
-  match v with
-  | some v => σ.set x v
-  | none => σ
-
-/-- Look up a value in an environment -/
-def get (x : String) (σ : Env) : Value :=
-  σ x
-
-/-- Initialize an environment, setting all uninitialized memory to `i` -/
-def init (i : Value) : Env := fun _ => i
-
-@[simp]
-theorem get_init : (Env.init v).get x = v := by rfl
-
-@[simp]
-theorem get_set_same {σ : Env} : (σ.set x v).get x = v := by
-  simp [get, set]
-
-@[simp]
-theorem get_set_different {σ : Env} : x ≠ y → (σ.set x v).get y = σ.get y := by
-  intros
-  simp [get, set, *]
-
-end Env
-
-namespace Expr
-
-/-- Helper that implements unary operators -/
-def UnOp.apply : UnOp → Value → Option Value
-  | .neg, .int i => (Value.int ∘ Int.neg) <$> some i
-  | .not, .int b => if b == 0 then some (Value.int 1) else some (Value.int 0)
-  | .not, .str s => some $ Value.int (if s.isEmpty then 1 else 0)
-  | _, _ => none
-
-/-- Helper that implements binary operators -/
-def BinOp.apply : BinOp → Value → Value → Option Value
-  | .plus, .int i, .int j => some $ Value.int (i + j)
-  | .minus, .int i, .int j => some $ Value.int (i - j)
-  | .times, .int i, .int j => some $ Value.int (i * j)
-  | .div, .int i, .int j => if j == 0 then none else some $ Value.int (i / j)
-  | .and, .int b, .int c => some $ Value.int (b * c)
-  | .and, .str b, .str c => some $ Value.int (b ++ c).length
-  | .or, .int b, .int c => some $ Value.int (b + c)
-  | .or, .str s, .str t => some $ Value.str (s ++ t)
-  | .eq, .int i, .int j => some $ if i == j then Value.int 1 else Value.int 0
-  | .eq, .str s, .str t => some $ if s == t then (Value.int 1) else (Value.int 0)
-  | .le, .int i, .int j => some (if i <= j then Value.int 1 else Value.int 0)
-  | .lt, .int i, .int j => some $ if i < j then Value.int 1 else Value.int 0
-  | .append, .str s, .str t => some $ Value.str (s ++ t)
-  | _, _, _ => none
-
-/--
-Evaluates an expression, finding the value if it has one.
-
-Expressions that divide by zero don't have values - the result is undefined.
--/
-def eval (σ : Env) : Expr → Option Value
-  | .constInt i => some $ .int i
-  | .constStr s => some $ .str s
-  | .var x => σ.get x
-  | .un op e => do
-    let v ← e.eval σ
-    op.apply v
-  | .bin op e1 e2 => do
-    let v1 ← e1.eval σ
-    let v2 ← e2.eval σ
-    op.apply v1 v2
diff --git a/imp/Imp/Expr/Syntax.lean b/imp/Imp/Expr/Syntax.lean
deleted file mode 100644
index 600a11e..0000000
--- a/imp/Imp/Expr/Syntax.lean
+++ /dev/null
@@ -1,117 +0,0 @@
-import Lean.PrettyPrinter.Parenthesizer
-import Imp.Expr.Basic
-
-namespace Imp.Expr
-
-open Lean PrettyPrinter Parenthesizer
-
-
-/- Add a new nonterminal to Lean's grammar, called `varname` -/
-/-- Variable names in Imp -/
-declare_syntax_cat varname
-
-/- There are two productions: identifiers and antiquoted terms -/
-syntax ident : varname
-syntax:max "~" term:max : varname
-
-/- `varname`s are included in terms using `var { ... }`, which is a hook on which to hang the macros
-that translate the `varname` syntax into ordinary Lean expressions. -/
-syntax "var " "{" varname "}" : term
-
-/- These macros translate each production of the `varname` nonterminal into Lean expressions -/
-macro_rules
-  | `(var { $x:ident }) => `(term|$(quote x.getId.toString))
-  | `(var { ~$stx }) => pure stx
-
-/-- Expressions in Imp -/
-declare_syntax_cat exp
-
-/-- Variable names -/
-syntax varname : exp
-
-/-- Numeric constant -/
-syntax num : exp
-
-/-- Strings -/
-syntax:1 "[" str "]": exp
-
-/-- Arithmetic complement -/
-syntax:75 "-" exp:75 : exp
-
-/-- Multiplication -/
-syntax:70 exp:70 " * " exp:71 : exp
-/-- Division -/
-syntax:70 exp:70 " / " exp:71 : exp
-
-/-- Addition -/
-syntax:65 exp:65 " + " exp:66 : exp
-/-- Subtraction -/
-syntax:65 exp:65 " - " exp:66 : exp
-
-/-- Boolean negation -/
-syntax:75 "!" exp:75 : exp
-/-- Less than -/
-syntax:50 exp:50 " < " exp:51 : exp
-/-- Less than or equal to -/
-syntax:50 exp:50 " ≤ " exp:51 : exp
-/-- Greater than or equal to -/
-syntax:50 exp:50 " ≥ " exp:51 : exp
-/-- Greater than -/
-syntax:50 exp:50 " > " exp:51 : exp
-/-- Equal -/
-syntax:45 exp:45 " == " exp:46 : exp
-
-/-- Boolean conjunction -/
-syntax:35 exp:35 " && " exp:36 : exp
-/-- Boolean disjunction -/
-syntax:35 exp:35 " || " exp:36 : exp
-
-/-- String append -/
-syntax:30 exp:30 " ++ " exp:31 : exp
-
-/-- Parentheses for grouping -/
-syntax "(" exp ")" : exp
-
-/-- Escape to Lean -/
-syntax:max "~" term:max : exp
-
-/-- Embed an Imp expression into a Lean expression -/
-syntax:min "expr " "{ " exp " }" : term
-
-open Lean in
-macro_rules
-  | `(expr{$x:ident}) => `(Expr.var $(quote x.getId.toString))
-  | `(expr{$n:num}) => `(Expr.constInt $(quote n.getNat))
-
-  | `(expr{-$e}) => `(Expr.un .neg (expr{$e}))
-  | `(expr{!$e}) => `(Expr.un .not (expr{$e}))
-
-  | `(expr{$e1 + $e2}) => `(Expr.bin .plus (expr{$e1}) (expr{$e2}))
-  | `(expr{$e1 * $e2}) => `(Expr.bin .times (expr{$e1}) (expr{$e2}))
-  | `(expr{$e1 - $e2}) => `(Expr.bin .minus (expr{$e1}) (expr{$e2}))
-  | `(expr{$e1 / $e2}) => `(Expr.bin .div (expr{$e1}) (expr{$e2}))
-
-  | `(expr{$e1 && $e2}) => `(Expr.bin .and (expr{$e1}) (expr{$e2}))
-  | `(expr{$e1 || $e2}) => `(Expr.bin .or (expr{$e1}) (expr{$e2}))
-
-  | `(expr{$e1 < $e2}) => `(Expr.bin .lt (expr{$e1}) (expr{$e2}))
-  | `(expr{$e1 ≤ $e2}) => `(Expr.bin .le (expr{$e1}) (expr{$e2}))
-  | `(expr{$e1 == $e2}) => `(Expr.bin .eq (expr{$e1}) (expr{$e2}))
-  | `(expr{$e1 ≥ $e2}) => `(Expr.bin .le (expr{$e2}) (expr{$e1}))
-  | `(expr{$e1 > $e2}) => `(Expr.bin .lt (expr{$e2}) (expr{$e1}))
-  | `(expr{$e1 ++ $e2}) => `(Expr.bin .append (expr{$e1}) (expr{$e2}))
-  | `(expr{($e)}) => `(expr{$e})
-  | `(expr{~$stx}) => pure stx
-
-
--- Copied from Lean's term parenthesizer - applies the precedence rules in the grammar to add
--- parentheses as needed. This isn't needed when adding new input syntax to Lean, but because the
--- file `Delab.lean` makes Lean use this syntax in its output, the parentheses are needed.
-@[category_parenthesizer exp]
-def exp.parenthesizer : CategoryParenthesizer | prec => do
-  maybeParenthesize `exp true wrapParens prec $
-    parenthesizeCategoryCore `exp prec
-where
-  wrapParens (stx : Syntax) : Syntax := Unhygienic.run do
-    let pstx ← `(($(⟨stx⟩)))
-    return pstx.raw.setInfo (SourceInfo.fromRef stx)
diff --git a/imp/Imp/Hoare/Basic.lean b/imp/Imp/Hoare/Basic.lean
deleted file mode 100644
index 0e1ddee..0000000
--- a/imp/Imp/Hoare/Basic.lean
+++ /dev/null
@@ -1,49 +0,0 @@
-import Imp.Expr.Eval
-import Imp.Stmt.BigStep
-import Imp.Stmt.Basic
-
-open Imp Stmt
-
-@[simp]
-def ValidHoareTriple (P : Env → Prop) (c : Stmt) (Q : Env → Prop) : Prop :=
-  forall (st st' : Env), P st -> c / st ↓ st' -> Q st'
-
-syntax "{{" term:90 "}} " term:91 " {{" term:92 "}}" : term
-macro_rules
-  | `({{$P}}$c{{$Q}}) => `(ValidHoareTriple $P $c $Q)
-
-theorem hoare_skip : forall P, {{P}}(imp { skip; }){{P}} := by
-  intro P
-  simp [ValidHoareTriple]
-  intros st st' h1 h2
-  cases h2; assumption
-
-theorem hoare_seq : forall P Q R c1 c2, {{P}}c1{{Q}} -> {{Q}}c2{{R}} -> {{P}}(imp { ~c1 ~c2 }){{R}} := by
-  intro P Q R c1 c2
-  simp [ValidHoareTriple]
-  intros h1 h2 st st' hP h3
-  cases h3 with
-  | seq h3 h4 =>
-    apply h2
-    apply h1
-    apply hP
-    apply h3
-    apply h4
-
-def assertionSubstitution (P : Env → Prop) (x : String) (a : Expr) : Env → Prop :=
-  fun st => P (st.setOption x (Expr.eval st a))
-
-syntax term " [ " ident " |-> " term "]" : term
-macro_rules
-  | `($P [$x |-> $a]) => `(assertionSubstitution $P $x $a)
-
-theorem hoare_assign : forall P x a, {{P[x |-> a]}}(imp { ~x := a; }){{P}} := by
-  intros P x a
-  simp [ValidHoareTriple]
-  intros st st' h1 h2
-  cases h2 with
-  | assign h3 =>
-    simp [assertionSubstitution] at h1
-    simp [Expr.eval, Env.get] at h3
-    simp [Env.setOption] at h1
-    sorry
diff --git a/imp/Imp/Stmt.lean b/imp/Imp/Stmt.lean
deleted file mode 100644
index 30fccdb..0000000
--- a/imp/Imp/Stmt.lean
+++ /dev/null
@@ -1,6 +0,0 @@
-/-
-This file exists only to re-export the contents of the `Imp.Stmt` module hierarchy.
--/
-import Imp.Stmt.Basic
-import Imp.Stmt.BigStep
-import Imp.Stmt.Delab
diff --git a/imp/Imp/Stmt/Basic.lean b/imp/Imp/Stmt/Basic.lean
deleted file mode 100644
index c054433..0000000
--- a/imp/Imp/Stmt/Basic.lean
+++ /dev/null
@@ -1,91 +0,0 @@
-import Imp.Expr
-
-namespace Imp
-
-/-- Statements in Imp -/
-inductive Stmt where
-  /-- A statement that does nothing -/
-  | skip
-  /-- Executes `stmt1` then `stmt2` -/
-  | seq (stmt1 stmt2 : Stmt)
-  /-- Modifies a variable in the state -/
-  | assign (name : String) (val : Expr)
-  /--
-  Conditional: executes `ifTrue` when `cond`'s value is nonzero, `ifFalse` otherwise
-  -/
-  | if (cond : Expr) (ifTrue ifFalse : Stmt)
-  /--
-  Repeats `body` as long as `cond` evaluates to a nonzero value
-  -/
-  | while (cond : Expr) (body : Stmt)
-deriving Repr, DecidableEq
-
-/-- Imp statements -/
-declare_syntax_cat stmt
-/-- A statement that does nothing -/
-syntax "skip" ";" : stmt
-/-- Sequencing: one statement after another -/
-syntax stmt ppDedent(ppLine stmt) : stmt
-/-- Assignment -/
-syntax varname " := " exp ";" : stmt
-/-- Conditional statement -/
-syntax "if " "(" exp ")" ppHardSpace "{" ppLine stmt ppDedent(ppLine "}" ppHardSpace "else" ppHardSpace "{") ppLine stmt ppDedent(ppLine "}") : stmt
-/-- Loop -/
-syntax "while " "(" exp ")" ppHardSpace "{" ppLine stmt ppDedent(ppLine "}") : stmt
-/-- Escape to Lean -/
-syntax:max "~" term:max : stmt
-
-/-- Include an Imp statement in Lean code -/
-syntax:min "imp" ppHardSpace "{" ppLine stmt ppDedent(ppLine "}") : term
-
-/-
-The above rules are equivalent to the following, but with nicer-looking compiler output:
-
-syntax "skip" ";" : stmt
-syntax stmt stmt : stmt
-syntax varname " := " exp ";" : stmt
-syntax "if " "(" exp ") " "{" stmt "}" "else" "{" stmt "}" : stmt
-syntax "while " "(" exp ") "  "{" stmt "}" : stmt
-syntax:max "~" term:max : stmt
-
-syntax:min "imp" "{" stmt "}" : term
--/
-
-
-open Lean in
-macro_rules
-  | `(imp { skip; }) =>
-    `(Stmt.skip)
-  | `(imp { $s1 $s2 }) =>
-    `(Stmt.seq (imp {$s1}) (imp {$s2}))
-  | `(imp { $x:varname := $e;}) =>
-    `(Stmt.assign (var {$x}) (expr {$e}))
-  | `(imp { if ($c) {$s1} else {$s2} }) =>
-    `(Stmt.if (expr{$c}) (imp{$s1}) (imp{$s2}))
-  | `(imp { while ($c) {$s} }) =>
-    `(Stmt.while (expr{$c}) (imp{$s}))
-  | `(imp { ~$stx }) =>
-    pure stx
-
-
-def swap : Stmt := imp {
-  temp := x;
-  x := y;
-  y := temp;
-}
-
-def min : Stmt := imp {
-  if (x < y) {
-    min := x;
-  } else {
-    min := y;
-  }
-}
-
-def fact : Stmt := imp {
-  out := 1;
-  while (n > 0) {
-    out := out * n;
-    n := n - 1;
-  }
-}
diff --git a/imp/Imp/Stmt/BigStep.lean b/imp/Imp/Stmt/BigStep.lean
deleted file mode 100644
index a5fbbdb..0000000
--- a/imp/Imp/Stmt/BigStep.lean
+++ /dev/null
@@ -1,276 +0,0 @@
-import Imp.Expr
-
-import Imp.Stmt.Delab
-
-namespace Imp
-
-/--
-Truthiness: the result of evaluating an expression is "truthy" if it's defined and non-zero.
--/
-def Truthy (v : Option Value) : Prop :=
-  match v with
-  | some v => match v with
-    | .int x => x ≠ 0
-    | .str s => ¬ s.isEmpty
-  | none => False
-
-instance : Decidable (Truthy v) :=
-  match v with
-  | some v => match v with
-    | .int x => if h : x ≠ 0 then .isTrue h else .isFalse h
-    | .str s => if h : ¬ s.isEmpty then .isTrue h else .isFalse h
-  | none => .isFalse id
-
-@[simp]
-theorem Truthy.some_nonzero : Truthy (some (.int v)) = (v ≠ 0) := by
-  simp [Truthy]
-
-@[simp]
-theorem Truthy.not_none : Truthy none = False := by
-  simp [Truthy]
-
-@[simp]
-theorem Truthy.eval_const_int : Truthy (Expr.eval σ (.constInt v)) = (v ≠ 0) := by
-  simp [Truthy, Expr.eval]
-
-@[simp]
-theorem Truthy.eval_const_str : Truthy (Expr.eval σ (.constStr v)) = ¬ v.isEmpty := by
-  simp [Truthy, Expr.eval]
-
-/--
-Falsiness: the result of evaluating an expression is "falsy" if it's 0
--/
-def Falsy (v : Option Value) : Prop := match v with
-  | some v => match v with
-    | .int x => x = 0
-    | .str s => s.isEmpty
-  | none => False
-
-@[simp]
-theorem Falsy.eval_const_int : Falsy (Expr.eval σ (.constInt v)) = (v = 0) := by
-  simp [Falsy, Expr.eval]
-
-@[simp]
-theorem Falsy.eval_const_str : Falsy (Expr.eval σ (.constStr v)) = v.isEmpty := by
-  simp [Falsy, Expr.eval]
-
-@[simp]
-theorem Falsy.some_zero : Falsy (some (.int v)) = (v = 0) := by
-  simp [Falsy]
-
-@[simp]
-theorem Falsy.not_none : Falsy none = False := by
-  simp [Falsy]
-
-def Value.truthy : Value → Prop
-  | .int x => x ≠ 0
-  | .str s => ¬ s.isEmpty
-
-instance : Decidable (Falsy v) :=  -- inferInstanceAs (Decidable (v = 0))
-  match v with
-  | some v => match v with
-    | .int x => if h : x = 0 then .isTrue h else .isFalse h
-    | .str s => if h : s.isEmpty then .isTrue h else .isFalse h
-  | none => .isFalse id
-
-theorem Truthy.not_falsy : Truthy v → ¬Falsy v := by
-  intro h1 h2
-  simp [Truthy, Falsy] at *
-  cases v <;> simp at *
-  case some v =>
-    cases v <;> simp at *
-    case int x =>
-      contradiction
-    case str s =>
-      rw [h2] at h1
-      contradiction
-
-namespace Stmt
-
-/--
-Big-step semantics: `BigStep σ s σ'` means that running the program `s` in the starting state `σ` is
-termination with the final state `σ'`.
--/
-inductive BigStep : Env → Stmt → Env → Prop where
-  | skip :
-    BigStep σ (imp {skip;}) σ
-  | seq :
-    BigStep σ s1 σ' → BigStep σ' s2 σ'' →
-    BigStep σ (imp{ ~s1 ~s2}) σ''
-  | assign :
-    e.eval σ = some v →
-    BigStep σ (imp {~x := ~e;}) (σ.set x v)
-  | ifTrue :
-    Truthy (c.eval σ) → BigStep σ s1 σ' →
-    BigStep σ (imp {if (~c) {~s1} else {~s2}}) σ'
-  | ifFalse :
-    Falsy (c.eval σ) → BigStep σ s2 σ' →
-    BigStep σ (imp {if (~c) {~s1} else {~s2}}) σ'
-  | whileTrue :
-    Truthy (c.eval σ) →
-    BigStep σ body σ' →
-    BigStep σ' (imp {while (~c) {~body}}) σ'' →
-    BigStep σ (imp {while (~c) {~body}}) σ''
-  | whileFalse :
-    Falsy (c.eval σ) →
-    BigStep σ (imp {while (~c) {~body}}) σ
-
-attribute [simp] BigStep.skip
-
-syntax term:60 " / " term:61 " ↓ " term:62 : term
-macro_rules
-  | `($s / $σ ↓ $σ') => `(BigStep $σ $s $σ')
-
-/--
-`swap` terminates, and the resulting environment contains swapped inputs.
--/
-example : ∃σ', BigStep (Env.init 0 |>.set "x" 5 |>.set "y" 22) swap σ' ∧ σ'.get "x" = 22 ∧ σ'.get "y" = 5 := by
-  unfold swap
-  apply Exists.intro
-  constructor
-  . apply BigStep.seq
-    . apply BigStep.assign
-      simp [Expr.eval, Env.get, Env.set]
-      rfl
-    . apply BigStep.seq
-      . apply BigStep.assign
-        simp [Expr.eval, Env.get, Env.set]
-        rfl
-      . apply BigStep.assign
-        simp [Expr.eval, Env.get, Env.set]
-        rfl
-  . simp [Env.get, Env.set]
-
-/--
-`swap` terminates, and the resulting environment contains swapped inputs. This proof is shorter.
--/
-example : ∃σ', BigStep (Env.init 0 |>.set "x" 5 |>.set "y" 22) swap σ' ∧ σ'.get "x" = 22 ∧ σ'.get "y" = 5 := by
-  repeat' constructor
-
-/--
-`swap` terminates, and the resulting environment contains swapped inputs. This version works no
-matter what the input values are.
--/
-example : ∃σ', BigStep (Env.init 0 |>.set "x" x |>.set "y" y) swap σ' ∧ σ'.get "x" = y ∧ σ'.get "y" = x  := by
-  repeat' constructor
-
-/--
-`min` computes the minimum of its inputs.
--/
--- example : ∃σ', BigStep (Env.init 0 |>.set "x" x |>.set "y" y) min σ' ∧ if x < y then σ'.get "min" = x else σ'.get "min" = y := by
---   unfold min
---   by_cases h : x < y
---   . apply Exists.intro; constructor
---     . apply BigStep.ifTrue
---       . simp [Expr.eval, Expr.BinOp.apply, Env.get, Env.set, *]
---       . constructor; simp [Expr.eval, Env.get, Env.set]; rfl
---     . simp [Env.get, Env.set]
---       intro; contradiction
---   . apply Exists.intro; constructor
---     . apply BigStep.ifFalse
---       . simp [Expr.eval, Expr.BinOp.apply, Env.get, Env.set, *]
---       . constructor; simp [Expr.eval, Env.get, Env.set]; rfl
---     . simp [Env.get, Env.set]
---       intro; contradiction
-
-def loop := imp {while (1) {skip;}}
-
-/--
-`loop` is really an infinite loop - there is no final state that it can result in.
--/
-theorem infinite_loop : ¬ BigStep σ loop σ' := by
-  generalize h' : loop = l
-  intro h
-  induction h <;> try (simp [loop, *] at *; done)
-  case whileTrue =>
-    simp [*]
-  case whileFalse cFalse =>
-    unfold loop at h'
-    cases h'
-    simp at cFalse
-
-/--
-Run a program, with the depth of the recursive calls limited by the `Nat` parameter. Returns `none`
-if the program doesn't terminate fast enough or if some other problem means the result is undefined
-(e.g. division by zero).
- -/
-def run (σ : Env) (s : Stmt) : Nat → Option Env
-  | 0 => none
-  | n + 1 =>
-    match s with
-    | imp {skip;} =>
-      some σ
-    | imp {~s1 ~s2} => do
-      let σ' ← run σ s1 n
-      run σ' s2 n
-    | imp {~x := ~e;} => do
-      let v ← e.eval σ
-      pure (σ.set x v)
-    | imp {if (~c) {~s1} else {~s2}} => do
-      let grd := Truthy $ c.eval σ
-      if grd then
-        run σ s2 n
-      else
-        run σ s1 n
-    | imp {while (~c) {~s1}} => do
-      let grd := Truthy $ c.eval σ
-      if grd then
-        pure σ
-      else
-        let σ' ← run σ s1 n
-        run σ' (imp {while (~c) {~s1}}) n
-
-/--
-`run` is correct: if it returns an answer, then that final state can be reached by the big-step
-semantics. This is not total correctness - `run` could always return `none` - but it does increase
-confidence.
--/
-theorem run_some_implies_big_step : run σ s n = some σ' → BigStep σ s σ' := by
-  intro term
-  induction σ, s, n using run.induct generalizing σ' <;> unfold run at term <;> simp_all
-  case case3 σ n s1 s2 ih1 ih2 =>
-    sorry
-  sorry
-  sorry
-  sorry
-  sorry
-  sorry
-
---   let ⟨σ'', ⟨st1, st2⟩⟩ := term
---   constructor
---   . apply ih1
---     apply st1
---   . apply ih2
---     apply st2
--- case case4 =>
---   let ⟨σ'', ⟨evEq, setEq⟩⟩ := term
---   subst_eqs
---   constructor; assumption
--- case case5 ih1 ih2 =>
---   let ⟨v, ⟨evEq, step⟩⟩ := term
---   by_cases h : v = 0
---   . subst_eqs; simp at *
---     apply BigStep.ifFalse
---     . simp [Falsy, *]
---     . exact ih1 step
---   . subst_eqs; simp at *
---     apply BigStep.ifTrue
---     . simp [Truthy, *]
---     . simp [*] at step
---       apply ih2; assumption
--- case case6 ih1 ih2 =>
---   let ⟨v, ⟨evEq, step⟩⟩ := term
---   by_cases h : v = 0
---   . subst_eqs; simp at *
---     apply BigStep.whileFalse
---     simp [Falsy, *]
---   . subst_eqs; simp [*] at *
---     simp [h] at step
---     let ⟨σ', ⟨oneStep, loopStep⟩⟩ := step
---     apply BigStep.whileTrue
---     . rw [evEq]
---       simp [*]
---     . apply ih1
---       exact oneStep
---     . apply ih2
---       exact loopStep
diff --git a/imp/Imp/Stmt/Delab.lean b/imp/Imp/Stmt/Delab.lean
deleted file mode 100644
index 2ecf371..0000000
--- a/imp/Imp/Stmt/Delab.lean
+++ /dev/null
@@ -1,140 +0,0 @@
-/-
-This file makes the convenient syntax from `Imp.Stmt.Basic` show up in Lean's output. It's not part
-of what's being taught in the lectures.
--/
-import Lean.PrettyPrinter.Delaborator
-import Imp.Stmt.Basic
-import Imp.Expr
-
-open Lean PrettyPrinter.Delaborator SubExpr
-
-namespace Imp.Stmt.Delab
-
-open Imp.Stmt
-open Imp.Expr.Delab
-
-partial def delabStmtInner : DelabM (TSyntax `stmt) := do
-  let e ← getExpr
-  let stx ←
-    match_expr e with
-    | Stmt.skip => `(stmt| skip;)
-    | Stmt.seq _ _ =>
-      let s1 ← withAppFn <| withAppArg delabStmtInner
-      let s2 ← withAppArg delabStmtInner
-      `(stmt| $s1 $s2)
-    | Stmt.assign _ _ =>
-      let x ← withAppFn <| withAppArg delabNameInner
-      let e ← withAppArg delabExprInner
-      `(stmt| $x:varname := $e;)
-    | Stmt.while _ _ =>
-      let c ← withAppFn <| withAppArg delabExprInner
-      let body ← withAppArg delabStmtInner
-      `(stmt| while ($c) { $body })
-    | Stmt.if _ _ _ =>
-      let c ← withAppFn <| withAppFn <| withAppArg delabExprInner
-      let t ← withAppFn <| withAppArg delabStmtInner
-      let f ← withAppArg delabStmtInner
-      `(stmt| if ($c) { $t } else { $f })
-    | _ =>
-      `(stmt| ~$(← delab))
-  annAsTerm stx
-
-@[delab app.Imp.Stmt.skip, delab app.Imp.Stmt.seq, delab app.Imp.Stmt.while, delab app.Imp.Stmt.assign, delab app.Imp.Stmt.if]
-partial def delabStmt : Delab := do
-  -- This delaborator only understands a certain arity - bail if it's incorrect
-  guard <| match_expr ← getExpr with
-    | Stmt.skip => true
-    | Stmt.seq _ _ => true
-    | Stmt.while _ _ => true
-    | Stmt.assign _ _ => true
-    | Stmt.if _ _ _ => true
-    | _ => false
-  match ← delabStmtInner with
-  | `(stmt|~$e) => pure e
-  | s => `(term|imp{$s})
-
-/-- info: Imp.Stmt.skip : Stmt -/
-#guard_msgs in
-#check Stmt.skip
-
-/--
-info: imp {
-  skip;
-} : Stmt
--/
-#guard_msgs in
-#check imp {skip;}
-
-/--
-info: imp {
-  skip;
-  skip;
-} : Stmt
--/
-#guard_msgs in
-#check imp {skip; skip;}
-
-/--
-info: imp {
-  skip;
-  skip;
-  x := 5;
-} : Stmt
--/
-#guard_msgs in
-#check imp {skip; skip; x := 5;}
-
-/--
-info: imp {
-  skip;
-  if (0 < x) {
-    x := x - 1;
-  } else {
-    skip;
-  }
-} : Stmt
--/
-#guard_msgs in
-#check imp {skip; if (x > 0) { x := x - 1;} else {skip;}}
-
-/--
-info: imp {
-  skip;
-  while (0 < x) {
-      x := x - 1;
-    }
-  if (x) {
-    skip;
-  } else {
-    while (5 < x) {
-      skip;
-      skip;
-    }
-  }
-} : Stmt
--/
-#guard_msgs in
-#check imp {skip; while (x > 0) { x := x - 1;} if (x) {skip;} else {while (x > 5) {skip; skip;}}}
-
-/--
-info: let s :=
-  imp {
-    skip;
-  };
-imp {
-  skip;
-  while (0 < x) {
-      x := x - 1;
-    }
-  if (x) {
-    skip;
-  } else {
-    while (5 < x) {
-      skip;
-      ~s
-    }
-  }
-} : Stmt
--/
-#guard_msgs in
-#check let s := imp {skip;}; imp {skip; while (x > 0) { x := x - 1;} if (x) {skip;} else {while (x > 5) {skip; ~s}}}
diff --git a/imp/README.md b/imp/README.md
deleted file mode 100644
index 7984b87..0000000
--- a/imp/README.md
+++ /dev/null
@@ -1,5 +0,0 @@
-# Imp
-
-Simple imperative programming
-
-Mostly plagiarized from [David Christiansen](https://github.com/david-christiansen/ssft24), removing bits and adding strings and arrays
diff --git a/imp/lake-manifest.json b/imp/lake-manifest.json
deleted file mode 100644
index 8e4c4d0..0000000
--- a/imp/lake-manifest.json
+++ /dev/null
@@ -1,5 +0,0 @@
-{"version": "1.1.0",
- "packagesDir": ".lake/packages",
- "packages": [],
- "name": "APPS",
- "lakeDir": ".lake"}
diff --git a/imp/lakefile.lean b/imp/lakefile.lean
deleted file mode 100644
index bc160c6..0000000
--- a/imp/lakefile.lean
+++ /dev/null
@@ -1,8 +0,0 @@
-import Lake
-open Lake DSL
-
-package "imp" where
-  version := v!"0.1.0"
-
-@[default_target]
-lean_lib Imp where
diff --git a/imp/lean-toolchain b/imp/lean-toolchain
deleted file mode 100644
index bf867e0..0000000
--- a/imp/lean-toolchain
+++ /dev/null
@@ -1 +0,0 @@
-nightly
diff --git a/llmfv/.gitignore b/llmfv/.gitignore
deleted file mode 100644
index bbc15c1..0000000
--- a/llmfv/.gitignore
+++ /dev/null
@@ -1,23 +0,0 @@
-# test outputs
-artefacts/hypothesis/*.py
-artefacts/lean/*.lean
-
-# hypotheses
-.hypothesis/
-
-# env
-.env
-
-# python generated files
-__pycache__/
-*.py[oc]
-build/
-dist/
-wheels/
-*.egg-info
-
-
-# venv
-.venv
-
-.ipynb_checkpoints/
diff --git a/llmfv/README.md b/llmfv/README.md
deleted file mode 100644
index 3146081..0000000
--- a/llmfv/README.md
+++ /dev/null
@@ -1,21 +0,0 @@
-# LLM-FV: Toward Scaling Formal Verification Schemes via LLMs
-
-Describe your project here.
-
-
-# Setup
-
-```
-rye sync
-```
-
-Create a `.env` file in `nb/` next to this README with the following:
-```
-ANTHROPIC_API_KEY="YOUR_KEY_HERE"
-```
-
-
-# Basic Run
-You can try to run `python example_agent_run.py`. This will attempt to create tests using claude for the example function in `test/example_func.py`.
-
-Once it completes (successfully), you can re-test the final output with `pytest test/test_example_func.py`. 
diff --git a/llmfv/pyproject.toml b/pyproject.toml
similarity index 100%
rename from llmfv/pyproject.toml
rename to pyproject.toml
diff --git a/llmfv/requirements-dev.lock b/requirements-dev.lock
similarity index 100%
rename from llmfv/requirements-dev.lock
rename to requirements-dev.lock
diff --git a/llmfv/requirements.lock b/requirements.lock
similarity index 100%
rename from llmfv/requirements.lock
rename to requirements.lock
diff --git a/llmfv/src/benchmark/__init__.py b/src/benchmark/__init__.py
similarity index 100%
rename from llmfv/src/benchmark/__init__.py
rename to src/benchmark/__init__.py
diff --git a/llmfv/src/benchmark/claude_prompting.py b/src/benchmark/claude_prompting.py
similarity index 100%
rename from llmfv/src/benchmark/claude_prompting.py
rename to src/benchmark/claude_prompting.py
diff --git a/llmfv/src/notebooks/APPS-staring.ipynb b/src/notebooks/APPS-staring.ipynb
similarity index 100%
rename from llmfv/src/notebooks/APPS-staring.ipynb
rename to src/notebooks/APPS-staring.ipynb
diff --git a/llmfv/src/scripts/__init__.py b/src/scripts/__init__.py
similarity index 100%
rename from llmfv/src/scripts/__init__.py
rename to src/scripts/__init__.py
diff --git a/llmfv/src/scripts/example_agent_run.py b/src/scripts/example_agent_run.py
similarity index 100%
rename from llmfv/src/scripts/example_agent_run.py
rename to src/scripts/example_agent_run.py
diff --git a/llmfv/test/__init__.py b/test/__init__.py
similarity index 100%
rename from llmfv/test/__init__.py
rename to test/__init__.py