diff --git a/CLAUDE.md b/CLAUDE.md
new file mode 100644
index 00000000..75647d70
--- /dev/null
+++ b/CLAUDE.md
@@ -0,0 +1,86 @@
+# CLAUDE.md
+
+This file provides guidance to Claude Code (claude.ai/code) when working with code in this repository.
+
+## Project Overview
+
+Aeon is a statically-typed programming language with native Liquid Types (refinement types), implemented as a Python interpreter with Python FFI. Developed at LASIGE, University of Lisbon.
+
+## Common Commands
+
+```bash
+# Install for development
+uv pip install -e ".[dev]"
+uvx pre-commit install
+
+# Run tests
+uv run pytest
+
+# Run a single test
+uv run pytest tests/end_to_end_test.py::test_name -x
+
+# Run an .ae file
+uv run python -m aeon [file.ae]
+
+# Run with synthesis (genetic programming, 60s default budget)
+uv run python -m aeon --budget 10 -s gp examples/synthesis/example.ae
+
+# Run all examples (used in CI)
+bash run_examples.sh
+
+# Linting/formatting (via pre-commit hooks)
+uvx pre-commit run --all-files
+
+# Type checking
+uv run mypy aeon
+```
+
+**Synthesizer options:** `gp` (genetic programming, default), `synquid`, `random_search`, `enumerative`, `hc` (hill climbing), `1p1` (one plus one)
+
+## Code Style
+
+- Line length: 120 (ruff + black)
+- Ruff rules: E and F codes (ignoring E741, E501)
+- Strict mypy with custom stubs in `/stubs`
+- pytest-beartype enabled for `aeon.core` package
+- Python 3.10+ target
+
+## Architecture
+
+The codebase follows a compiler pipeline:
+
+```
+Source (.ae) → Parse (lark) → Sugar AST → Desugar/Elaborate → Core AST → ANF → Typecheck (z3 SMT) → Synthesize/Evaluate
+```
+
+### Key Packages
+
+| Package | Role |
+|---|---|
+| `aeon/facade` | Entry point: `AeonDriver` orchestrates the full pipeline, `AeonConfig` holds settings |
+| `aeon/sugar` | Surface language: AST (`STypes`/`STerm` in `program.py`), parser (lark grammar in `aeon_sugar.lark`), desugaring |
+| `aeon/core` | Core language: `Types`/`Term` (internal representation, never user-facing), substitutions, liquid constraints, core term/type parser |
+| `aeon/frontend` | ANF conversion |
+| `aeon/elaboration` | Converts sugar AST to core AST with type elaboration |
+| `aeon/typechecking` | Type inference and liquid type constraint verification |
+| `aeon/verification` | SMT-based verification via z3: horn clauses, constraint solving |
+| `aeon/synthesis` | Program synthesis: multiple backends (genetic programming via geneticengine, synquid, enumerative, LLM/ollama) |
+| `aeon/backend` | Runtime evaluation |
+| `aeon/lsp` | Language Server Protocol implementation (pygls v2.1.0) |
+| `aeon/libraries` | Standard library `.ae` files (List, Math, Image, etc.) |
+| `aeon/prelude` | Built-in functions and type definitions |
+
+### Important Distinction
+
+- **`STypes`/`STerm`** (in `aeon/sugar/program.py`): Surface/sugar language types — safe to expose to users and tooling
+- **`Types`/`Term`** (in `aeon/core/types.py`, `aeon/core/terms.py`): Core language types — internal only, never exposed to users
+
+### Grammars
+
+- `aeon/sugar/aeon_sugar.lark` — surface language grammar
+- `aeon/core/aeon_core.lark` — core language grammar (used internally by tests and verification)
+
+### Entry Points
+
+- CLI: `aeon/__main__.py` → `AeonDriver` (modes: parse/run/synth/lsp/format)
+- Synthesis: `aeon/synthesis/entrypoint.py` identifies holes and routes to synthesizer backends
diff --git a/aeon/__main__.py b/aeon/__main__.py
index 9f7a69ef..af679f80 100644
--- a/aeon/__main__.py
+++ b/aeon/__main__.py
@@ -40,7 +40,6 @@ def parse_arguments():
 
 
 def _parse_common_arguments(parser: ArgumentParser):
-    parser.add_argument("--core", action="store_true", help="synthesize a aeon core file")
     parser.add_argument("--budget", type=int, default=60, help="Time for synthesis (in seconds).")
     parser.add_argument(
         "-l",
@@ -146,10 +145,7 @@ def main() -> None:
         aeon_lsp.start(args.tcp)
         sys.exit(0)
 
-    if args.core:
-        errors = driver.parse_core(args.filename)
-    else:
-        errors = driver.parse(args.filename)
+    errors = driver.parse(args.filename)
 
     if errors:
         for err in errors:
diff --git a/aeon/frontend/aeon_core.lark b/aeon/core/aeon_core.lark
similarity index 100%
rename from aeon/frontend/aeon_core.lark
rename to aeon/core/aeon_core.lark
diff --git a/aeon/frontend/parser.py b/aeon/core/parser.py
similarity index 100%
rename from aeon/frontend/parser.py
rename to aeon/core/parser.py
diff --git a/aeon/facade/driver.py b/aeon/facade/driver.py
index eaee4d0f..ffc5b7a6 100644
--- a/aeon/facade/driver.py
+++ b/aeon/facade/driver.py
@@ -1,7 +1,6 @@
 import sys
 from dataclasses import dataclass
-from functools import reduce
-from typing import Any, Iterable
+from typing import Iterable
 
 from aeon.backend.evaluator import EvaluationContext
 from aeon.backend.evaluator import eval
@@ -13,14 +12,12 @@
 from aeon.elaboration import elaborate
 from aeon.facade.api import AeonError
 from aeon.frontend.anf_converter import ensure_anf
-from aeon.frontend.parser import parse_term
 from aeon.prelude.prelude import evaluation_vars
-from aeon.prelude.prelude import typing_vars
 from aeon.sugar.ast_helpers import st_top
 from aeon.sugar.bind import bind, bind_program
 from aeon.sugar.desugar import DesugaredProgram, desugar
 from aeon.sugar.lifting import lift
-from aeon.sugar.lowering import lower_to_core, lower_to_core_context, type_to_core
+from aeon.sugar.lowering import lower_to_core, lower_to_core_context
 from aeon.sugar.parser import parse_main_program
 from aeon.sugar.program import Program, STerm
 from aeon.synthesis.entrypoint import synthesize_holes
@@ -28,7 +25,6 @@
 from aeon.synthesis.modules.synthesizerfactory import make_synthesizer
 from aeon.synthesis.uis.api import SynthesisUI, SynthesisFormat
 from aeon.typechecking.typeinfer import check_type_errors
-from aeon.utils.ctx_helpers import build_context
 from aeon.utils.name import Name
 from aeon.utils.pprint import pretty_print_node
 from aeon.utils.time_utils import RecordTime
@@ -53,20 +49,6 @@ class AeonDriver:
     def __init__(self, cfg: AeonConfig):
         self.cfg = cfg
 
-    def parse_core(self, filename: str):
-        # TODO: deprecate core parsing
-        aeon_code = read_file(filename)
-
-        core_typing_vars: dict[Name, Any] = reduce(
-            lambda acc, el: acc | {el[0]: type_to_core(el[1], available_vars=[e for e in acc.items()])},
-            typing_vars.items(),
-            {},
-        )
-
-        self.typing_ctx = build_context(core_typing_vars)
-        self.core_ast = parse_term(aeon_code)
-        self.metadata: Metadata = {}
-
     def parse(self, filename: str = None, aeon_code: str = None) -> Iterable[AeonError]:
         if aeon_code is None:
             aeon_code = read_file(filename)
diff --git a/aeon/verification/helpers.py b/aeon/verification/helpers.py
index ae78853f..42220e08 100644
--- a/aeon/verification/helpers.py
+++ b/aeon/verification/helpers.py
@@ -12,7 +12,7 @@
 from aeon.core.substitutions import substitution_in_liquid
 from aeon.core.types import AbstractionType, TypeConstructor, Top, TypeVar
 from aeon.core.types import t_bool
-from aeon.frontend.parser import parse_term
+from aeon.core.parser import parse_term
 from aeon.verification.smt import base_functions
 from aeon.verification.vcs import Conjunction
 from aeon.verification.vcs import Constraint
diff --git a/docs/index.md b/docs/index.md
index 30ec38e3..ebd7d608 100644
--- a/docs/index.md
+++ b/docs/index.md
@@ -181,7 +181,6 @@ There are a few libraries available, but unstable as they are under development:
 | -----: | :---------------------------------------------------------------------------- |
 |     -d | Prints debug information                                                      |
 |     -t | Prints timing information about the different steps of the compiler           |
-| --core | Parses the input file as being the Core language, instead of the surface aeon |
 | -l, --log | Sets the log level (TRACE, DEBUG, INFO, WARNINGS, ERROR, CRITICAL, etc.)  |
 | -f, --logfile | Exports the log to a file                                              |
 | -n, --no-main | Disables introducing hole in main                                     |
diff --git a/examples/core/abs_main.ae b/examples/core/abs_main.ae
deleted file mode 100644
index 72568ca8..00000000
--- a/examples/core/abs_main.ae
+++ /dev/null
@@ -1,9 +0,0 @@
-let assert : (b:{b1:Bool | b1}) -> Int = \b -> 0 in
-let abs : (x:Int) -> {y:Int | ?k } = \x -> if 0 <= x then x else (x-1) in
-
-let main : (x:Int) -> Int = \y ->
-    (let z = abs y in
-        let c = (0 <= z) in
-            assert(c)
-    ) in
-1
diff --git a/examples/core/anf_stress_main.ae b/examples/core/anf_stress_main.ae
deleted file mode 100644
index 315ba6da..00000000
--- a/examples/core/anf_stress_main.ae
+++ /dev/null
@@ -1,3 +0,0 @@
-let f : (x:Int) -> (y:Int) -> {z:Int | z == x } = (\x -> (\y -> x)) in
-let r = f (f 1 2) (f 2 3) in
-print r
diff --git a/examples/core/factorial_main.ae b/examples/core/factorial_main.ae
deleted file mode 100644
index e9262e61..00000000
--- a/examples/core/factorial_main.ae
+++ /dev/null
@@ -1,5 +0,0 @@
-let factorial : (x:Int) -> Int = (\n -> if n == 0 then 1 else n * factorial (n-1)) in
-let _1 = print "Factorial of 5:" in
-let _2 = print (factorial 5) in
-let _2 =  (factorial 5) in
-5
diff --git a/examples/core/fib_main.ae b/examples/core/fib_main.ae
deleted file mode 100644
index ca181cb6..00000000
--- a/examples/core/fib_main.ae
+++ /dev/null
@@ -1,5 +0,0 @@
-let fib : (x:Int) -> Int = \n -> if n < 2 then 1 else (fib (n-1)) + (fib (n-2)) in
-let _1 = print("Fib 7:") in
-let a = print(fib 7) in
-let a = (fib 7) in
-0
diff --git a/examples/core/max.ae_ b/examples/core/max.ae_
deleted file mode 100644
index 60c9efa9..00000000
--- a/examples/core/max.ae_
+++ /dev/null
@@ -1,4 +0,0 @@
-# TODO: resolve AssertationError - TypePolymorphism
-let max : (forall a:B, (x:a) -> (y:a) -> a) = \x -> \y -> if x < y then y else x in
-let client : {v : Int | 0 < v } = let r = max 0 5 in r + 1 in
-client
diff --git a/examples/core/native_main.ae b/examples/core/native_main.ae
deleted file mode 100644
index 6f759476..00000000
--- a/examples/core/native_main.ae
+++ /dev/null
@@ -1,4 +0,0 @@
-let a : (x:Int) -> Int = native "print" ;
-let b : (x:Int) -> Int = \x -> native "x+1";
-let k = 1;
-a (b 3)
diff --git a/tests/backend_test.py b/tests/backend_test.py
index ca73aa54..ee2d2505 100644
--- a/tests/backend_test.py
+++ b/tests/backend_test.py
@@ -7,7 +7,7 @@
 from aeon.backend.evaluator import EvaluationContext, eval
 from aeon.core.terms import Literal, Term, TypeAbstraction, TypeApplication
 from aeon.core.types import BaseKind, TypeConstructor
-from aeon.frontend.parser import parse_term
+from aeon.core.parser import parse_term
 
 
 def weval(t: Term, ctx: EvaluationContext = EvaluationContext()):
diff --git a/tests/driver.py b/tests/driver.py
index 7095bae0..2e8510d2 100644
--- a/tests/driver.py
+++ b/tests/driver.py
@@ -19,7 +19,7 @@
 from aeon.backend.evaluator import eval
 from aeon.decorators import Metadata
 
-from aeon.frontend.parser import parse_term
+from aeon.core.parser import parse_term
 from aeon.core.types import top
 from aeon.utils.name import Name
 
diff --git a/tests/frontend_test.py b/tests/frontend_test.py
index 03097818..ac95ff77 100644
--- a/tests/frontend_test.py
+++ b/tests/frontend_test.py
@@ -20,8 +20,8 @@
 from aeon.core.types import TypePolymorphism
 from aeon.core.types import TypeVar
 from aeon.frontend.anf_converter import ensure_anf
-from aeon.frontend.parser import parse_term
-from aeon.frontend.parser import parse_type
+from aeon.core.parser import parse_term
+from aeon.core.parser import parse_type
 from aeon.utils.ast_helpers import false
 from aeon.utils.ast_helpers import i0
 from aeon.utils.ast_helpers import i1
diff --git a/tests/instantiation_test.py b/tests/instantiation_test.py
index edeb3631..99ee8d60 100644
--- a/tests/instantiation_test.py
+++ b/tests/instantiation_test.py
@@ -3,7 +3,7 @@
 from aeon.core.instantiation import type_substitution
 from aeon.core.types import t_bool
 from aeon.core.types import t_int
-from aeon.frontend.parser import parse_type
+from aeon.core.parser import parse_type
 from aeon.utils.name import Name
 
 
diff --git a/tests/optimization_test.py b/tests/optimization_test.py
index e2f0a324..d659caa5 100644
--- a/tests/optimization_test.py
+++ b/tests/optimization_test.py
@@ -1,7 +1,7 @@
 from __future__ import annotations
 
 from aeon.optimization.normal_form import optimize
-from aeon.frontend.parser import parse_term
+from aeon.core.parser import parse_term
 
 
 def eq(source, expected):
diff --git a/tests/polytypes_test.py b/tests/polytypes_test.py
index 4efeca5d..8654411d 100644
--- a/tests/polytypes_test.py
+++ b/tests/polytypes_test.py
@@ -1,5 +1,5 @@
 from aeon.core.types import TypeConstructor
-from aeon.frontend.parser import parse_type
+from aeon.core.parser import parse_type
 
 from aeon.sugar.ast_helpers import st_top
 from tests.driver import check_compile
diff --git a/tests/sub_test.py b/tests/sub_test.py
index 629ea806..0ecd8a0d 100644
--- a/tests/sub_test.py
+++ b/tests/sub_test.py
@@ -1,5 +1,5 @@
 from aeon.utils.name import Name
-from aeon.frontend.parser import parse_type
+from aeon.core.parser import parse_type
 from aeon.typechecking.context import TypingContext, VariableBinder
 from aeon.typechecking.entailment import entailment
 from aeon.verification.sub import sub
diff --git a/tests/substitutions_test.py b/tests/substitutions_test.py
index 3e9ad825..eeee0008 100644
--- a/tests/substitutions_test.py
+++ b/tests/substitutions_test.py
@@ -2,8 +2,8 @@
 
 from aeon.core.substitutions import substitution
 from aeon.core.substitutions import substitution_in_type
-from aeon.frontend.parser import parse_term
-from aeon.frontend.parser import parse_type
+from aeon.core.parser import parse_term
+from aeon.core.parser import parse_type
 from aeon.utils.name import Name
 
 
diff --git a/tests/typevars_test.py b/tests/typevars_test.py
index 58c9bc36..d69a1648 100644
--- a/tests/typevars_test.py
+++ b/tests/typevars_test.py
@@ -2,7 +2,7 @@
 
 from aeon.core.types import get_type_vars
 from aeon.core.types import TypeVar
-from aeon.frontend.parser import parse_type
+from aeon.core.parser import parse_type
 from aeon.utils.name import Name
 
 
diff --git a/tests/wellformed_test.py b/tests/wellformed_test.py
index efa63714..f5012959 100644
--- a/tests/wellformed_test.py
+++ b/tests/wellformed_test.py
@@ -8,7 +8,7 @@
 from aeon.core.types import t_int
 from aeon.core.types import TypePolymorphism
 from aeon.core.types import TypeVar
-from aeon.frontend.parser import parse_type
+from aeon.core.parser import parse_type
 from aeon.typechecking.context import TypingContext
 from aeon.typechecking.well_formed import wellformed
 from aeon.utils.ctx_helpers import built_std_context