diff --git a/.github/workflows/maven-2.yml b/.github/workflows/maven-2.yml
index b37aaee..67d31a7 100644
--- a/.github/workflows/maven-2.yml
+++ b/.github/workflows/maven-2.yml
@@ -3,7 +3,7 @@ on:
   push:
     branches: [main]
   pull_request:
-    branches: [main]
+    branches: [main, feat/latte-liquid-typechecking]
 
 jobs:
   verify:
diff --git a/README.md b/README.md
index 12d9e1a..8241ceb 100644
--- a/README.md
+++ b/README.md
@@ -2,7 +2,7 @@
 
 Latte now runs as an ownership and aliasing pass before an independently implemented refinement checker. Both passes use the same Spoon AST. The old mutable checker has been replaced; no LiquidJava verifier implementation was copied.
 
-The verifier now covers floating-point arithmetic, exception and switch flow, deferred bodies, recursive aliases, allocation recency, inherited contracts, field-backed state, arrays and loop/effect analysis. The imported suite has **165 exact matches out of 311 inputs**; this is not full LiquidJava compatibility. All 410 upstream Java fixtures are preserved. See [compatibility status](docs/compatibility.md) for the implemented behavior, policy differences and precision limits.
+The verifier now covers floating-point arithmetic, exception and switch flow, deferred bodies, recursive aliases, allocation recency, inherited contracts, field-backed state, arrays and loop/effect analysis. The imported suite has **180 exact matches out of 311 inputs**; this is not full LiquidJava compatibility. All 410 upstream Java fixtures are preserved. See [compatibility status](docs/compatibility.md) for the implemented behavior, policy differences and precision limits.
 
 ## Build and run
 
@@ -19,7 +19,7 @@ The first example succeeds. The second reports a state refinement failure and ex
 
 The small library jar is `target/latte-0.0.1-SNAPSHOT.jar`. The runnable `latte-cli.jar` also includes Spoon and Z3, including the native solver libraries supplied by `z3-turnkey`.
 
-`mvn test` runs 465 tests, including the focused tests, legacy Latte regressions and 165 promoted upstream regression inputs. A separate imported-fixture test enforces the intentional fresh-reference comparison difference. `mvn verify -Pcompatibility` also runs **every** imported input and writes `target/liquidjava-compatibility.json`. A successful build does not mean that all upstream expectations match.
+`mvn test` runs 522 tests, including the focused tests, legacy Latte regressions and 180 promoted upstream regression inputs. A separate imported-fixture test enforces the intentional fresh-reference comparison difference. `mvn verify -Pcompatibility` also runs **every** imported input and writes `target/liquidjava-compatibility.json`. A successful build does not mean that all upstream expectations match.
 
 ## Ownership policy
 
@@ -65,6 +65,10 @@ class Example {
 
 [Examples](examples/refinements) cover accepted local aliases, unique and borrowed references, rejected shared references, escapes, stale aliases, field-backed state, arrays, floating-point behavior, control flow and inherited/deferred contracts. Their expected diagnostic kinds and lines are checked by the test suite.
 
+## External Java libraries
+
+Use `@ExternalRefinementsFor` to provide ownership and refinement contracts for JDK or third-party library methods, constructors and fields. Both passes resolve the same contracts on the Spoon AST. See the [external contract guide](docs/external-refinements.md) and [checked examples](examples/refinements/ExternalLibraryContracts.java). Use `--classpath` for library JARs; multiple input paths are analyzed together.
+
 ## AST handoff and embedding
 
 ```java
@@ -100,7 +104,7 @@ The state stores, points-to sets, predicates and proof results are immutable Jav
 - `latte.api`: the two-pass pipeline, diagnostics and CLI.
 - `liquidjava.specification`: freshly defined annotation API with familiar LiquidJava syntax.
 
-External refinements are deliberately deferred. Recursive paths, older loop allocations, unknown calls and exceptions are conservatively approximated; loop inference supports a finite set of inductive bounds. Recursive constructor expansion requires a finite heap summary and currently reports `UNSUPPORTED`. Constructors without source bodies retain conservative effects. These approximations can reject valid programs. Unsupported constructs and solver timeouts are failures. The checker remains a prototype, and the complete compatibility report is the source of truth for port coverage.
+External library contracts are supported through `@ExternalRefinementsFor`; see [syntax, ownership rules and classpath usage](docs/external-refinements.md). Recursive paths, older loop allocations, unknown calls and exceptions are conservatively approximated; loop inference supports a finite set of inductive bounds. Recursive constructor expansion requires a finite heap summary and currently reports `UNSUPPORTED`. Constructors without source bodies retain conservative effects. These approximations can reject valid programs. Unsupported constructs and solver timeouts are failures. The checker remains a prototype, and the complete compatibility report is the source of truth for port coverage.
 
 Run `mvn spotless:apply` after editing Java. Formatting is checked by `mvn verify` and CI.
 
diff --git a/docs/compatibility.md b/docs/compatibility.md
index bc25977..86c128d 100644
--- a/docs/compatibility.md
+++ b/docs/compatibility.md
@@ -8,6 +8,8 @@ The pipeline checks refinements on parameters, locals, fields, assignments, call
 
 The follow-up implementation adds:
 
+- External library contracts shared by Latte and LiquidTypeChecking, including ownership, overloads, constructors, inherited members, fields, state transitions and reference predicates. A per-model registry validates Java signatures and publishes bindings on the Spoon AST. The CLI and embedding API accept library classpaths and multiple source inputs. See [external specifications](external-refinements.md).
+
 - IEEE 754 `float` and `double` arithmetic, rounding, signed zero, NaN, infinities, Java remainder, numeric promotion and narrowing conversions. Java integral operations retain finite-width overflow, signed division/remainder and masked shift counts.
 - Explicit normal, return, throw, break, continue and yield completions. Catches and finally blocks preserve the state at the relevant completion; finally can replace an earlier return. Resource closing, switch fall-through, switch expressions and common implicit exceptions are modeled. Deferred lambda bodies and method references are checked against their functional contracts.
 - Compositional return-alias summaries, including local assignments, conditional returns, delegated returns and recursion. A finite path domain widens recursive paths to reachable subgraphs. Allocation recency distinguishes the newest object at a site from older instances. The original `MyNodeComplete` regression now passes.
@@ -28,12 +30,12 @@ Abstract ghost transitions remain specifications. Their consistency, preconditio
 
 At this checkpoint:
 
-- **165 of 311** imported inputs match the upstream expected diagnostics exactly. The earlier checkpoint had 166; fresh-reference reasoning now intentionally differs on one more fixture, described below.
-- All 165 exact matches are required parameterized tests in `supported-inputs.txt`. `ReferenceFreshnessTest` separately requires the corrected diagnostics for the unchanged reference-comparison fixture.
-- **465 tests** cover these imported inputs, focused regressions, examples and the legacy Latte suite.
+- **180 of 311** imported inputs match the upstream expected diagnostics exactly. External specifications add 15 exact matches to the previous 165. Fresh-reference reasoning retains the intentional difference described below.
+- All 180 exact matches are required parameterized tests in `supported-inputs.txt`. `ReferenceFreshnessTest` separately requires the corrected diagnostics for the unchanged reference-comparison fixture.
+- **522 tests** cover these imported inputs, focused regressions, examples and the legacy Latte suite.
 - Every imported input completes without an uncaught analysis exception.
 - Every upstream negative input is rejected, except the two explicit semantic differences below.
-- The only `UNSUPPORTED` diagnostics in the complete imported audit concern external refinements, appearing in 60 inputs. This does not mean that all other inputs match upstream expectations.
+- External declarations are checked instead of rejected wholesale. Exact-match accounting still distinguishes ownership-policy differences, invalid specifications and precision limits.
 
 Run from `latte/`:
 
@@ -52,7 +54,7 @@ mvn exec:java -Dexec.mainClass=latte.compatibility.CompatibilityAudit \
 
 ## Compatibility differences and precision limits
 
-External refinement specifications remain intentionally deferred. Shared reference refinements are rejected under the requested ownership policy. Existing upstream examples with unannotated reference parameters, shared fields or externally managed objects need suitable ownership contracts before their object-state refinements can be retained.
+External refinement specifications now bind to actual Java library declarations for both passes; see [the contract guide](external-refinements.md). Invalid targets and member signatures are errors, including fixtures where upstream expected only a warning. Shared reference refinements are rejected under the requested ownership policy. Existing upstream examples with unannotated reference parameters, shared fields or externally managed objects need suitable ownership contracts before their object-state refinements can be retained.
 
 Some upstream expectations assume mathematical arithmetic for Java expressions. The new checker rejects those claims when overflow or IEEE rounding supplies a counterexample. Examples include `CorrectFunctionDeclarations`, `CorrectOperatorAssignments`, `CorrectSimpleIfElse` and `CorrectChars`. Predicate-only decimal expressions use mathematical reals; when combined with a floating Java value, they are converted to that floating sort.
 
@@ -65,7 +67,7 @@ These are named exceptions to the negative-input gate, not exceptions for entire
 
 `ErrorIfReferenceComparison.java` still reports its two feasible double-close errors (lines 30 and 39). Its third expected error, at line 21, assumes that a preexisting parameter can equal a newly allocated object. Java allocation freshness rules out that branch. The unchanged fixture is checked by a dedicated regression test and remains a mismatch in the upstream diagnostic audit.
 
-Reference-array examples are in `examples/refinements/ReferenceArrayAliases.java`. Known local elements remain refinable, including borrowed and unique objects. Arbitrary index expressions are summarized by Latte and constrained by symbolic select/store operations in LiquidTypeChecking; this can lose ownership precision. Unknown external elements and implicit rows of multidimensional allocations remain shared summaries, with distinct possible values on different reads. Mutations involving unknown element sets conservatively invalidate object state. Explicit nested array initializers retain their individual array identities. Library containers such as `ArrayList` still require external ownership and alias contracts; this array fix does not add those contracts.
+Reference-array examples are in `examples/refinements/ReferenceArrayAliases.java`. Known local elements remain refinable, including borrowed and unique objects. Arbitrary index expressions are summarized by Latte and constrained by symbolic select/store operations in LiquidTypeChecking; this can lose ownership precision. Unknown external elements and implicit rows of multidimensional allocations remain shared summaries, with distinct possible values on different reads. Mutations involving unknown element sets conservatively invalidate object state. Explicit nested array initializers retain their individual array identities. Library containers such as `ArrayList` can now have external ownership and state contracts. These do not infer arbitrary element ownership or aliases from a size specification.
 
 The analysis remains conservative. Recursive return paths widen after four field steps. Older objects at a repeated allocation site are summarized as shared, so refinements requiring their individual identities may be rejected. Loop inference uses a finite set of candidate bounds rather than arbitrary invariants. Exception and unknown-call effects can lose precision. Unspecified field updates are invalidated rather than inferred as exact method postconditions. Multiple inherited cases guarantee the facts common to the applicable alternatives. Solver timeouts are verification failures, never successful proofs.
 
diff --git a/docs/external-refinements.md b/docs/external-refinements.md
new file mode 100644
index 0000000..ae9486a
--- /dev/null
+++ b/docs/external-refinements.md
@@ -0,0 +1,79 @@
+# External library contracts
+
+Place a specification type alongside the application sources, annotated with the library's qualified Java name. The verifier uses the existing annotation syntax for both Latte ownership and LiquidTypeChecking refinements. Library source changes are unnecessary.
+
+```java
+@ExternalRefinementsFor("java.util.ArrayList")
+@RefinementPredicate("int size(ArrayList list)")
+interface ArrayListContracts<E> {
+    @StateRefinement(to = "size(this) == 0")
+    void ArrayList();
+
+    @StateRefinement(to = "size(this) == size(old(this)) + 1")
+    boolean add(E value);
+
+    @StateRefinement(from = "true")
+    @Refinement("_ == size(this)")
+    int size();
+}
+```
+
+A constructor is represented by a `void` method with the target class's simple name. Methods use their Java names, parameter types and result types. Parameter names may differ from the library: predicates use the names in the specification. Overloads are matched by erased Java parameter types, including generic bounds. Static library methods can be written as ordinary interface method declarations. Receiver state annotations require an instance method or constructor.
+
+```java
+java.util.ArrayList<Integer> list = new java.util.ArrayList<>();
+java.util.ArrayList<Integer> alias = list;
+alias.add(42);
+@Refinement("_ == 1") int count = list.size();
+```
+
+Both variables have the same Latte identity, so the transition through `alias` changes the state read through `list`. State predicates and state sets belong to `java.util.ArrayList`, independently of the specification type's name. Contracts on inherited Java members are found through the target's class and interface hierarchy. Constructors are never inherited.
+
+## Ownership and effects
+
+Use `specification.Borrowed`, `Unique`, `Free` and `Shared` on external parameters, results and fields with the same meaning as source contracts. Shared references remain ineligible for refinements. A state contract does not upgrade a shared receiver into an owned one.
+
+```java
+@ExternalRefinementsFor("java.util.Arrays")
+interface ArrayContracts {
+    void fill(@Borrowed int[] values, int value);
+}
+```
+
+Here Latte retains local ownership of `values`; LiquidTypeChecking invalidates its old contents because borrowing permits mutation. A reference argument without an ownership annotation is shared and can escape. A `@Free` parameter consumes all local aliases, and a `@Free` result can carry refinements. Constructor parameters follow the same rules. The checked [examples](../examples/refinements/ExternalLibraryContracts.java) include valid local aliases and rejected stale values, consumed aliases and shared receivers.
+
+A receiver contract with only `from`, including `from = "true"`, promises to preserve its state. A `to` clause describes a transition. Without a receiver state clause, a specified instance method may change the receiver. Reference parameters may change regardless of their ownership annotation. Calls missing from the specification retain conservative unknown-call behavior.
+
+Specifications are trusted public contracts; library bodies, placeholder bodies and field initializers are not verified as implementations. State transitions and reference results must accurately describe the library. External calls also conservatively invalidate potentially affected application fields; ownership and receiver contracts do not promise global purity. Library internals and element identities are not inferred from a container-size contract. For example, this ArrayList specification does not establish an ownership or alias relationship between an inserted object and a later `get` result.
+
+External fields can carry refinements and ownership annotations. Actual Java declarations determine whether fields are static; placeholder initializer values never describe the library's storage. Writes in application code must satisfy the field contract. A shared reference field still cannot carry a refinement.
+
+## Library classpath
+
+The JDK is available automatically. For third-party libraries, pass their JARs or class directories. Multiple input paths are analyzed together, so specifications may live separately from the application:
+
+```sh
+java -jar latte/target/latte-cli.jar \
+    --classpath 'lib/library.jar:lib/dependency.jar' \
+    specs src/main/java
+```
+
+The classpath separator is platform-specific (`:` on Unix, `;` on Windows). `-cp` is an alias for `--classpath`.
+
+Embedding uses the same pipeline:
+
+```java
+var result = Verification.verify(
+    List.of("specs", "src/main/java"),
+    List.of("lib/library.jar", "lib/dependency.jar"));
+```
+
+`Verification.verify(Launcher)` also accepts a caller-configured Spoon launcher. Reading signatures does not initialize or execute library classes.
+
+The per-model registry is stored on the Spoon root package under `latte.analysis.external.v1`. Resolved executable references retain their external binding; `ExternalSpecifications.resolve(reference)` exposes the contract. Both passes use that lookup, while ordinary ownership, effects and transfer metadata remain on the same AST. Reanalysis rebuilds the registry; there is no process-global specification cache.
+
+## Validation and boundaries
+
+Unresolvable types, missing members, incompatible result or field types, misplaced annotations and duplicate specifications for the same target are errors. The verifier does not silently ignore an invalid contract. Keep one specification type per target and include its dependencies on the classpath.
+
+Expanded varargs calls currently require an explicit array argument when using an external contract. The verifier reports `UNSUPPORTED` for implicit packing rather than applying an array contract to individual elements. Varargs method references require a lambda that passes an explicit array. Ordinary reference-array ownership limitations still apply. Contract validation is not a replacement for Java compilation or a proof of the library implementation.
diff --git a/examples/refinements/ExternalLibraryContracts.java b/examples/refinements/ExternalLibraryContracts.java
new file mode 100644
index 0000000..8345a50
--- /dev/null
+++ b/examples/refinements/ExternalLibraryContracts.java
@@ -0,0 +1,59 @@
+import liquidjava.specification.*;
+import specification.*;
+
+@ExternalRefinementsFor("java.util.ArrayList")
+@RefinementPredicate("int size(ArrayList list)")
+interface ArrayListContracts<E> {
+  @StateRefinement(to = "size(this) == 0")
+  void ArrayList();
+
+  @StateRefinement(to = "size(this) == size(old(this)) + 1")
+  boolean add(E element);
+
+  @StateRefinement(from = "true")
+  @Refinement("_ == size(this)")
+  int size();
+
+  @StateRefinement(from = "size(this) > 0", to = "size(this) == size(old(this)) - 1")
+  E remove(@Refinement("_ >= 0 && _ < size(this)") int index);
+}
+
+@ExternalRefinementsFor("java.util.Arrays")
+interface ArrayContracts {
+  void fill(@Borrowed int[] values, int value);
+}
+
+@ExternalRefinementsFor("java.util.Objects")
+interface ObjectContracts {
+  @Free
+  @Refinement("_ != null")
+  Object requireNonNull(@Free Object value);
+}
+
+class ExternalLibraryContracts {
+  void aliasesShareLibraryState() {
+    java.util.ArrayList<Integer> list = new java.util.ArrayList<>();
+    java.util.ArrayList<Integer> alias = list;
+    alias.add(42);
+    @Refinement("_ == 1") int size = list.size();
+    list.remove(1); // Expect: REFINEMENT
+  }
+
+  void borrowedArrayRemainsLocal() {
+    int[] values = {0};
+    java.util.Arrays.fill(values, 3);
+    @Refinement("_ != null") int[] alias = values;
+    @Refinement("_ == 0") int stale = alias[0]; // Expect: REFINEMENT
+  }
+
+  void ownershipTransfer() {
+    Object value = new Object();
+    Object oldAlias = value;
+    @Refinement("_ != null") Object result = java.util.Objects.requireNonNull(value);
+    Object consumed = oldAlias; // Expect: PERMISSION
+  }
+
+  void sharedReceiver(java.util.ArrayList<Integer> list) {
+    list.size(); // Expect: SHARED_REFINEMENT
+  }
+}
diff --git a/latte/src/main/java/latte/analysis/ExternalSpecifications.java b/latte/src/main/java/latte/analysis/ExternalSpecifications.java
new file mode 100644
index 0000000..fedba32
--- /dev/null
+++ b/latte/src/main/java/latte/analysis/ExternalSpecifications.java
@@ -0,0 +1,352 @@
+package latte.analysis;
+
+import java.util.*;
+import java.util.stream.Collectors;
+import latte.api.Diagnostic;
+import spoon.reflect.CtModel;
+import spoon.reflect.code.*;
+import spoon.reflect.declaration.*;
+import spoon.reflect.reference.*;
+import spoon.reflect.visitor.filter.TypeFilter;
+
+/** Per-model library contracts, resolved against Java declarations before either analysis runs. */
+public record ExternalSpecifications(
+    Map<String, Specification> specifications, List<Diagnostic> diagnostics) {
+  public static final String KEY = "latte.analysis.external.v1";
+  private static final String BINDING = KEY + ".binding";
+  private static final String FIELD = KEY + ".field";
+
+  public record Binding(CtExecutable<?> actual, CtMethod<?> contract) {}
+
+  public record Specification(
+      CtType<?> target,
+      CtType<?> source,
+      Map<String, Binding> methods,
+      Map<String, CtField<?>> fields) {
+    public Specification {
+      methods = Map.copyOf(methods);
+      fields = Map.copyOf(fields);
+    }
+  }
+
+  public ExternalSpecifications {
+    specifications = Map.copyOf(specifications);
+    diagnostics = List.copyOf(diagnostics);
+  }
+
+  public static ExternalSpecifications collect(CtModel model) {
+    var specifications = new LinkedHashMap<String, Specification>();
+    var diagnostics = new ArrayList<Diagnostic>();
+    for (var element : model.getElements(new TypeFilter<>(CtElement.class))) {
+      element.putMetadata(BINDING, null);
+      element.putMetadata(FIELD, null);
+      if (Annotations.has(element, "ExternalRefinementsFor") && !(element instanceof CtType<?>))
+        error(diagnostics, "ExternalRefinementsFor belongs on a specification type", element);
+    }
+    for (CtType<?> source : model.getElements(new TypeFilter<>(CtType.class))) {
+      if (!Annotations.has(source, "ExternalRefinementsFor")) continue;
+      var names = Annotations.strings(source, "ExternalRefinementsFor", "value");
+      if (names.size() != 1 || names.get(0).isBlank()) {
+        error(diagnostics, "External refinements require one qualified target type", source);
+        continue;
+      }
+      String name = names.get(0);
+      CtType<?> target = source.getFactory().Type().createReference(name).getTypeDeclaration();
+      if (target == null) {
+        error(
+            diagnostics,
+            "Cannot resolve external type " + name + "; include its library on the classpath",
+            source);
+        continue;
+      }
+      if (specifications.containsKey(target.getQualifiedName())) {
+        error(diagnostics, "Duplicate external specification for " + name, source);
+        continue;
+      }
+      var methods = new LinkedHashMap<String, Binding>();
+      for (CtMethod<?> contract : source.getMethods()) {
+        boolean constructor = contract.getSimpleName().equals(target.getSimpleName());
+        var candidates = new ArrayList<CtExecutable<?>>();
+        if (constructor && target instanceof CtClass<?> clazz)
+          candidates.addAll(clazz.getConstructors());
+        else if (!constructor) candidates.addAll(target.getAllMethods());
+        String signature = signature(contract, constructor);
+        var matches =
+            candidates.stream()
+                .filter(actual -> inheritedMember(target, actual))
+                .filter(actual -> signature(actual, constructor).equals(signature))
+                .toList();
+        if (matches.isEmpty()) {
+          error(diagnostics, "No external member " + name + "#" + signature, contract);
+          continue;
+        }
+        var actual =
+            matches.stream()
+                .filter(member -> member.getParent(CtType.class) == target)
+                .findFirst()
+                .orElse(matches.get(0));
+        if (constructor && !contract.getType().getSimpleName().equals("void")
+            || !constructor
+                && actual instanceof CtMethod<?> method
+                && !erased(method.getType()).equals(erased(contract.getType()))) {
+          error(
+              diagnostics,
+              "External member has an incompatible result type: " + name + "#" + signature,
+              contract);
+          continue;
+        }
+        var binding = new Binding(actual, contract);
+        if (actual instanceof CtMethod<?> method
+            && method.isStatic()
+            && Annotations.has(contract, "StateRefinement")) {
+          error(
+              diagnostics,
+              "A static external method has no receiver state; use Refinement for its result",
+              contract);
+          continue;
+        }
+        methods.put(signature, binding);
+        contract.putMetadata(BINDING, binding);
+      }
+      var fields = new LinkedHashMap<String, CtField<?>>();
+      for (var contract : source.getFields()) {
+        var actual =
+            target.getAllFields().stream()
+                .filter(field -> field.getSimpleName().equals(contract.getSimpleName()))
+                .map(CtFieldReference::getFieldDeclaration)
+                .filter(Objects::nonNull)
+                .filter(field -> inheritedMember(target, field))
+                .findFirst()
+                .orElse(null);
+        if (actual == null || !erased(actual.getType()).equals(erased(contract.getType())))
+          error(
+              diagnostics,
+              "No compatible external field " + name + "#" + contract.getSimpleName(),
+              contract);
+        else {
+          fields.put(contract.getSimpleName(), contract);
+          contract.putMetadata(FIELD, actual);
+        }
+      }
+      specifications.put(
+          target.getQualifiedName(), new Specification(target, source, methods, fields));
+    }
+    var result = new ExternalSpecifications(specifications, diagnostics);
+    model.getRootPackage().putMetadata(KEY, result);
+    for (CtExecutableReference<?> reference :
+        model.getElements(new TypeFilter<>(CtExecutableReference.class))) {
+      result
+          .binding(reference)
+          .ifPresent(
+              binding -> {
+                reference.putMetadata(BINDING, binding);
+                if (reference.isParentInitialized()
+                    && reference.getParent() instanceof CtAbstractInvocation<?> call
+                    && expandedVarargs(binding.actual(), call.getArguments()))
+                  diagnostics.add(
+                      Diagnostic.at(
+                          Diagnostic.Kind.UNSUPPORTED,
+                          "External varargs contracts require an explicit array argument",
+                          reference.getParent()));
+                if (reference.isParentInitialized()
+                    && reference.getParent() instanceof CtExecutableReferenceExpression<?, ?>
+                    && binding.actual().getParameters().stream().anyMatch(CtParameter::isVarArgs))
+                  diagnostics.add(
+                      Diagnostic.at(
+                          Diagnostic.Kind.UNSUPPORTED,
+                          "External varargs method references require a lambda with an explicit array argument",
+                          reference.getParent()));
+              });
+    }
+    var collected = new ExternalSpecifications(specifications, diagnostics);
+    model.getRootPackage().putMetadata(KEY, collected);
+    return collected;
+  }
+
+  public static ExternalSpecifications on(CtElement element) {
+    var metadata = element.getFactory().getModel().getRootPackage().getMetadata(KEY);
+    return metadata instanceof ExternalSpecifications specifications
+        ? specifications
+        : new ExternalSpecifications(Map.of(), List.of());
+  }
+
+  public static boolean isSpecification(CtElement element) {
+    if (element == null) return false;
+    var type = element instanceof CtType<?> t ? t : element.getParent(CtType.class);
+    return type != null && Annotations.has(type, "ExternalRefinementsFor");
+  }
+
+  public static boolean isLibrary(CtElement element) {
+    var type = element instanceof CtType<?> t ? t : element.getParent(CtType.class);
+    return type != null && on(element).specifications().containsKey(type.getQualifiedName());
+  }
+
+  public static String owner(CtType<?> type) {
+    var names = Annotations.strings(type, "ExternalRefinementsFor", "value");
+    return names.size() == 1 ? names.get(0) : type.getQualifiedName();
+  }
+
+  public static CtExecutable<?> resolve(CtExecutableReference<?> reference) {
+    var binding = reference.getMetadata(BINDING);
+    if (binding instanceof Binding resolved) return resolved.contract();
+    return on(reference)
+        .binding(reference)
+        .map(Binding::contract)
+        .<CtExecutable<?>>map(contract -> contract)
+        .orElse(reference.getDeclaration());
+  }
+
+  public static CtField<?> resolve(CtFieldReference<?> reference) {
+    var registry = on(reference);
+    var actual = reference.getFieldDeclaration();
+    for (var type : lineage(reference.getDeclaringType())) {
+      var specification = registry.specifications().get(type.getQualifiedName());
+      if (specification != null && specification.fields().containsKey(reference.getSimpleName())) {
+        var contract = specification.fields().get(reference.getSimpleName());
+        if (actual != null
+            && contract.getMetadata(FIELD) instanceof CtField<?> specified
+            && specified
+                .getReference()
+                .getQualifiedName()
+                .equals(actual.getReference().getQualifiedName())) return contract;
+      }
+    }
+    return reference.getDeclaration();
+  }
+
+  public static Optional<Binding> binding(CtExecutable<?> contract) {
+    return contract != null && contract.getMetadata(BINDING) instanceof Binding binding
+        ? Optional.of(binding)
+        : Optional.empty();
+  }
+
+  public static boolean constructor(CtExecutable<?> contract) {
+    return contract instanceof CtConstructor<?>
+        || binding(contract)
+            .map(binding -> binding.actual() instanceof CtConstructor<?>)
+            .orElse(false);
+  }
+
+  public static boolean isStatic(CtField<?> field) {
+    return field.getMetadata(FIELD) instanceof CtField<?> actual
+        ? actual.isStatic()
+        : field.isStatic();
+  }
+
+  private Optional<Binding> binding(CtExecutableReference<?> reference) {
+    if (specifications.isEmpty()) return Optional.empty();
+    var actual = reference.getExecutableDeclaration();
+    String signature =
+        actual == null
+            ? (reference.isConstructor() ? "<init>" : reference.getSimpleName())
+                + "("
+                + reference.getParameters().stream()
+                    .map(ExternalSpecifications::erased)
+                    .collect(Collectors.joining(","))
+                + ")"
+            : signature(actual, reference.isConstructor());
+    var receiver = reference.getDeclaringType();
+    if (reference.isParentInitialized()
+        && reference.getParent() instanceof CtInvocation<?> call
+        && !reference.isStatic()
+        && !reference.isConstructor()
+        && call.getTarget() != null
+        && !(call.getTarget() instanceof CtTypeAccess<?>)
+        && call.getTarget().getType() != null) receiver = call.getTarget().getType();
+    for (var type : lineage(receiver)) {
+      var specification = specifications.get(type.getQualifiedName());
+      if (specification != null) {
+        var binding = specification.methods().get(signature);
+        if (binding != null
+            && (!reference.isStatic()
+                || actual == null
+                || binding
+                    .actual()
+                    .getParent(CtType.class)
+                    .getQualifiedName()
+                    .equals(actual.getParent(CtType.class).getQualifiedName())))
+          return Optional.of(binding);
+      }
+      if (reference.isConstructor()) break; // Constructors are never inherited.
+    }
+    return Optional.empty();
+  }
+
+  private static boolean expandedVarargs(
+      CtExecutable<?> executable, List<CtExpression<?>> arguments) {
+    var parameters = executable.getParameters();
+    if (parameters.isEmpty() || !parameters.get(parameters.size() - 1).isVarArgs()) return false;
+    if (parameters.size() != arguments.size()) return true;
+    var argument = arguments.get(arguments.size() - 1);
+    if (argument instanceof CtLiteral<?> literal && literal.getValue() == null) return false;
+    var type = argument.getType();
+    var expected =
+        argument
+            .getFactory()
+            .Type()
+            .createReference(erased(parameters.get(parameters.size() - 1).getType()));
+    return type == null || !type.isArray() || !type.isSubtypeOf(expected);
+  }
+
+  public static List<CtType<?>> lineage(CtTypeReference<?> reference) {
+    if (reference == null) return List.of();
+    var queue = new ArrayDeque<CtTypeReference<?>>();
+    queue.add(reference);
+    var visited = new HashSet<String>();
+    var result = new ArrayList<CtType<?>>();
+    while (!queue.isEmpty()) {
+      var next = queue.removeFirst();
+      if (!visited.add(next.getQualifiedName())) continue;
+      var type = next.getTypeDeclaration();
+      if (type == null) continue;
+      result.add(type);
+      if (type.getSuperclass() != null) queue.addLast(type.getSuperclass());
+      type.getSuperInterfaces().stream()
+          .sorted(Comparator.comparing(CtTypeReference::getQualifiedName))
+          .forEach(queue::addLast);
+    }
+    return List.copyOf(result);
+  }
+
+  /** Spoon includes members that are not inherited under Java's access and static rules. */
+  private static boolean inheritedMember(CtType<?> target, CtElement member) {
+    var owner = member.getParent(CtType.class);
+    if (owner == target) return true;
+    if (!(member instanceof CtModifiable modifiers) || modifiers.isPrivate()) return false;
+    if (member instanceof CtMethod<?> method && method.isStatic() && owner.isInterface())
+      return false;
+    if (modifiers.isPublic() || modifiers.isProtected()) return true;
+    return packagePath(target, owner, new HashSet<>());
+  }
+
+  private static boolean packagePath(CtType<?> type, CtType<?> owner, Set<String> visited) {
+    if (type == null || !visited.add(type.getQualifiedName())) return false;
+    if (type.getQualifiedName().equals(owner.getQualifiedName())) return true;
+    if (!type.getPackage().getQualifiedName().equals(owner.getPackage().getQualifiedName()))
+      return false;
+    return type.getSuperclass() != null
+        && packagePath(type.getSuperclass().getTypeDeclaration(), owner, visited);
+  }
+
+  private static String signature(CtExecutable<?> executable, boolean constructor) {
+    return (constructor ? "<init>" : executable.getSimpleName())
+        + "("
+        + executable.getParameters().stream()
+            .map(parameter -> erased(parameter.getType()))
+            .collect(Collectors.joining(","))
+        + ")";
+  }
+
+  private static String erased(CtTypeReference<?> type) {
+    if (type == null) return "java.lang.Object";
+    if (type instanceof CtTypeParameterReference parameter)
+      return erased(parameter.getBoundingType());
+    if (type instanceof CtArrayTypeReference<?> array)
+      return erased(array.getComponentType()) + "[]";
+    return type.getQualifiedName();
+  }
+
+  private static void error(List<Diagnostic> diagnostics, String message, CtElement site) {
+    diagnostics.add(Diagnostic.at(Diagnostic.Kind.SYNTAX, message, site));
+  }
+}
diff --git a/latte/src/main/java/latte/analysis/LatteAnalysis.java b/latte/src/main/java/latte/analysis/LatteAnalysis.java
index c289d37..b2e84fd 100644
--- a/latte/src/main/java/latte/analysis/LatteAnalysis.java
+++ b/latte/src/main/java/latte/analysis/LatteAnalysis.java
@@ -55,6 +55,8 @@ private record Flow(FlowState state, Exit exit) {}
 
   public List<Diagnostic> analyze(CtModel model) {
     diagnostics.clear();
+    var external = ExternalSpecifications.collect(model);
+    diagnostics.addAll(external.diagnostics());
     evaluations.clear();
     activeConstructors.clear();
     closures.clear();
@@ -81,8 +83,20 @@ public List<Diagnostic> analyze(CtModel model) {
                     f -> f.getReference().getQualifiedName(),
                     Annotations::permission,
                     (a, b) -> a));
+    var declaredFields = new HashMap<>(fieldPermissions);
+    external
+        .specifications()
+        .forEach(
+            (owner, specification) ->
+                specification
+                    .fields()
+                    .forEach(
+                        (name, field) ->
+                            declaredFields.put(owner + "#" + name, Annotations.permission(field))));
+    fieldPermissions = Map.copyOf(declaredFields);
     model.getElements(new TypeFilter<>(CtExecutable.class)).stream()
         .filter(e -> e instanceof CtMethod<?> || e instanceof CtConstructor<?>)
+        .filter(e -> !ExternalSpecifications.isLibrary(e))
         .forEach(this::executable);
     model
         .getElements(new TypeFilter<>(CtField.class))
@@ -120,10 +134,12 @@ private void executable(CtExecutable<?> executable) {
       initial = after;
     }
     var after =
-        executable instanceof CtConstructor<?> constructor
-            ? constructorBody(
-                constructor, defaults(constructor.getDeclaringType(), receiver, initial), scope)
-            : statement(executable.getBody(), initial, scope).state();
+        ExternalSpecifications.isSpecification(executable)
+            ? initial
+            : executable instanceof CtConstructor<?> constructor
+                ? constructorBody(
+                    constructor, defaults(constructor.getDeclaringType(), receiver, initial), scope)
+                : statement(executable.getBody(), initial, scope).state();
     new LatteFacts(initial, after, receiver).attach(executable);
   }
 
@@ -187,7 +203,7 @@ private FlowState constructorBody(CtConstructor<?> constructor, FlowState state,
       if (!statements.isEmpty()
           && statements.get(0) instanceof CtInvocation<?> invocation
           && invocation.getExecutable().isConstructor()) {
-        var target = invocation.getExecutable().getDeclaration();
+        var target = ExternalSpecifications.resolve(invocation.getExecutable());
         delegated =
             target instanceof CtConstructor<?> other
                 && other.getDeclaringType().equals(constructor.getDeclaringType());
@@ -210,14 +226,16 @@ private FlowState constructorBody(CtConstructor<?> constructor, FlowState state,
   }
 
   private Evaluation construct(
-      CtConstructor<?> declaration,
+      CtExecutable<?> declaration,
       Reference receiver,
       List<CtExpression<?>> nodes,
       List<Reference> values,
       FlowState before,
       CtElement call) {
     var state = arguments(nodes, values, declaration, before, call);
-    if (declaration == null || declaration.getBody() == null) {
+    if (!(declaration instanceof CtConstructor<?> constructor)
+        || declaration.getBody() == null
+        || ExternalSpecifications.isSpecification(declaration)) {
       var roots = values.stream().reduce(receiver, Reference::join);
       return new Evaluation(state.havocHeap(roots, Annotations.key(call)), receiver);
     }
@@ -247,7 +265,7 @@ private Evaluation construct(
       }
       state =
           constructorBody(
-              declaration, state, new Scope(declaration, receiver.objects().iterator().next()));
+              constructor, state, new Scope(declaration, receiver.objects().iterator().next()));
       var restored = new HashMap<>(bindings);
       var shadowed = new HashSet<String>();
       shadowed.add("this");
@@ -535,7 +553,7 @@ private Evaluation expression(CtExpression<?> expression, FlowState before, Scop
             facts(field.getTarget())
                 .map(LatteFacts::value)
                 .orElse(Reference.object(scope.receiver()));
-        var declaration = field.getVariable().getDeclaration();
+        var declaration = ExternalSpecifications.resolve(field.getVariable());
         var expected = Annotations.permission(declaration);
         if (!receiver.scalar() && after.permission(receiver) == Permission.SHARED)
           expected = Permission.SHARED;
@@ -568,7 +586,7 @@ private Evaluation expression(CtExpression<?> expression, FlowState before, Scop
         state = evaluated.state();
         arguments.add(evaluated.value());
       }
-      var declaration = call.getExecutable().getDeclaration();
+      var declaration = ExternalSpecifications.resolve(call.getExecutable());
       var value = Reference.object(allocation("new:", call));
       state = state.fresh(value, Permission.FREE);
       var allocatedType =
@@ -578,8 +596,8 @@ private Evaluation expression(CtExpression<?> expression, FlowState before, Scop
       if (mayFinalize(allocatedType, true)) finalizableObjects.addAll(value.objects());
       var constructor = declaration instanceof CtConstructor<?> c ? c : null;
       if (constructor != null) state = defaults(constructor.getDeclaringType(), value, state);
-      state = releaseArguments(arguments, value, constructor, state, call, scope);
-      result = construct(constructor, value, call.getArguments(), arguments, state, call);
+      state = releaseArguments(arguments, value, declaration, state, call, scope);
+      result = construct(declaration, value, call.getArguments(), arguments, state, call);
     } else if (expression instanceof CtInvocation<?> call) {
       var receiver =
           call.getExecutable().isConstructor()
@@ -592,7 +610,7 @@ private Evaluation expression(CtExpression<?> expression, FlowState before, Scop
         state = evaluated.state();
         arguments.add(evaluated.value());
       }
-      var declaration = call.getExecutable().getDeclaration();
+      var declaration = ExternalSpecifications.resolve(call.getExecutable());
       state = releaseArguments(arguments, receiver.value(), declaration, state, call, scope);
       var localClosure =
           call.getExecutable().isConstructor()
@@ -611,12 +629,7 @@ private Evaluation expression(CtExpression<?> expression, FlowState before, Scop
                         .equals("java.lang.Object")
                 ? new Evaluation(state, receiver.value())
                 : construct(
-                    declaration instanceof CtConstructor<?> c ? c : null,
-                    receiver.value(),
-                    call.getArguments(),
-                    arguments,
-                    state,
-                    call);
+                    declaration, receiver.value(), call.getArguments(), arguments, state, call);
         remember(expression, new LatteFacts(before, result.state(), result.value()));
         return result;
       } else if (declaration == null) {
@@ -809,7 +822,7 @@ private Evaluation field(CtFieldAccess<?> field, FlowState before, Scope scope)
       }
       var child = Reference.object(identity + "." + reference.getQualifiedName());
       if (mayFinalize(field.getType())) finalizableObjects.addAll(child.objects());
-      var permission = Annotations.permission(reference.getDeclaration());
+      var permission = Annotations.permission(ExternalSpecifications.resolve(reference));
       if (reference.isStatic() || state.permission(singleton) == Permission.SHARED)
         permission = Permission.SHARED;
       state =
@@ -886,7 +899,10 @@ private Evaluation returned(
       }
       value = value.join(current);
     }
-    if (paths.isEmpty() && (declaration == null || declaration.getBody() == null)) {
+    if (paths.isEmpty()
+        && (declaration == null
+            || declaration.getBody() == null
+            || ExternalSpecifications.isSpecification(declaration))) {
       value = fresh.join(receiver);
       for (var argument : arguments) value = value.join(argument);
       state = state.allocate(fresh, permission);
@@ -1204,7 +1220,7 @@ private Evaluation invokeClosure(
           }
         } else if (closure.expression()
             instanceof CtExecutableReferenceExpression<?, ?> reference) {
-          var declaration = reference.getExecutable().getDeclaration();
+          var declaration = ExternalSpecifications.resolve(reference.getExecutable());
           boolean unbound =
               reference.getTarget() instanceof CtTypeAccess<?>
                   && !reference.getExecutable().isStatic()
@@ -1227,7 +1243,7 @@ private Evaluation invokeClosure(
             var constructor = declaration instanceof CtConstructor<?> c ? c : null;
             if (constructor != null)
               state = defaults(constructor.getDeclaringType(), allocated, state);
-            var constructed = construct(constructor, allocated, nodes, values, state, call);
+            var constructed = construct(declaration, allocated, nodes, values, state, call);
             state =
                 Annotations.permission(functional) == Permission.FREE
                     ? constructed.state()
diff --git a/latte/src/main/java/latte/analysis/MutationEffects.java b/latte/src/main/java/latte/analysis/MutationEffects.java
index 8bac6f6..2d62695 100644
--- a/latte/src/main/java/latte/analysis/MutationEffects.java
+++ b/latte/src/main/java/latte/analysis/MutationEffects.java
@@ -49,6 +49,24 @@ private MutationEffects() {}
 
   public static Effect on(CtExecutable<?> method) {
     if (method != null && method.getMetadata(KEY) instanceof Effect effect) return effect;
+    var external = ExternalSpecifications.binding(method);
+    if (external.isPresent()) {
+      var roots = new HashMap<Integer, Set<String>>();
+      var actual = external.get().actual();
+      boolean receiver = !(actual instanceof CtMethod<?> m) || !m.isStatic();
+      var clauses = Annotations.named(method, "StateRefinement");
+      if (receiver
+          && (clauses.isEmpty()
+              || clauses.stream()
+                  .anyMatch(
+                      clause ->
+                          Annotations.strings(clause.getValues().get("to")).stream()
+                              .anyMatch(text -> !text.isBlank())))) roots.put(-1, Set.of("*"));
+      for (int i = 0; i < method.getParameters().size(); i++)
+        if (!method.getParameters().get(i).getType().isPrimitive()) roots.put(i, Set.of("*"));
+      // Ownership and receiver transitions do not promise purity of application global storage.
+      return new Effect(roots, true);
+    }
     var roots = new HashMap<Integer, Set<String>>();
     roots.put(-1, Set.of("*"));
     if (method != null)
@@ -61,10 +79,15 @@ static void collect(CtModel model, ReturnAliases aliases) {
     var methods =
         model.getElements(new TypeFilter<>(CtExecutable.class)).stream()
             .filter(e -> e instanceof CtMethod<?> || e instanceof CtConstructor<?>)
+            .filter(e -> !ExternalSpecifications.isLibrary(e))
             .toList();
+    methods.forEach(method -> method.putMetadata(KEY, null));
     Map<CtExecutable<?>, Effect> effects = new HashMap<>();
     for (CtExecutable<?> method : methods) {
-      var effect = method.getBody() == null ? on(method) : new Effect(Map.of(), false);
+      var effect =
+          method.getBody() == null || ExternalSpecifications.isSpecification(method)
+              ? on(method)
+              : new Effect(Map.of(), false);
       if (Annotations.named(method, "StateRefinement").stream()
           .anyMatch(
               a ->
@@ -75,7 +98,7 @@ static void collect(CtModel model, ReturnAliases aliases) {
     for (; ; ) {
       var next = new HashMap<>(effects);
       for (CtExecutable<?> method : methods) {
-        if (method.getBody() == null) continue;
+        if (method.getBody() == null || ExternalSpecifications.isSpecification(method)) continue;
         var effect = effects.get(method);
         if (method instanceof CtConstructor<?> constructor)
           for (var field : constructor.getDeclaringType().getFields())
@@ -93,7 +116,7 @@ static void collect(CtModel model, ReturnAliases aliases) {
         for (var write : elements(method, CtArrayWrite.class))
           effect = add(effect, aliases.origins(write.getTarget(), method), "[]");
         for (CtInvocation<?> call : elements(method, CtInvocation.class)) {
-          var declaration = call.getExecutable().getDeclaration();
+          var declaration = ExternalSpecifications.resolve(call.getExecutable());
           if (call.getExecutable().isConstructor()
               && call.getExecutable()
                   .getDeclaringType()
@@ -117,7 +140,7 @@ static void collect(CtModel model, ReturnAliases aliases) {
               effect = add(effect, aliases.origins(argument, method), "*");
         }
         for (CtConstructorCall<?> call : elements(method, CtConstructorCall.class)) {
-          var declaration = call.getExecutable().getDeclaration();
+          var declaration = ExternalSpecifications.resolve(call.getExecutable());
           if (call.getType() != null
               && call.getType().getQualifiedName().equals("java.lang.Object")) continue;
           var callee =
diff --git a/latte/src/main/java/latte/analysis/ReturnAliases.java b/latte/src/main/java/latte/analysis/ReturnAliases.java
index 14c83a7..2131162 100644
--- a/latte/src/main/java/latte/analysis/ReturnAliases.java
+++ b/latte/src/main/java/latte/analysis/ReturnAliases.java
@@ -35,12 +35,17 @@ static ReturnAliases collect(CtModel model) {
     var methods =
         model.getElements(new TypeFilter<>(CtExecutable.class)).stream()
             .filter(e -> e instanceof CtMethod<?> || e instanceof CtConstructor<?>)
+            .filter(e -> !ExternalSpecifications.isLibrary(e))
             .toList();
     Map<CtExecutable<?>, Set<Path>> summaries = Map.of();
     for (; ; ) {
       var next = new HashMap<>(summaries);
       for (CtExecutable<?> method : methods) {
         var paths = new HashSet<>(summaries.getOrDefault(method, Set.of()));
+        if (ExternalSpecifications.isSpecification(method)) {
+          next.put(method, Set.of());
+          continue;
+        }
         for (var returned : method.getElements(new TypeFilter<>(CtReturn.class)))
           if (returned.getParent(CtExecutable.class) == method)
             paths.addAll(
@@ -103,7 +108,7 @@ private static Set<Path> expression(
       return Set.copyOf(paths);
     }
     if (expression instanceof CtInvocation<?> call) {
-      var declaration = call.getExecutable().getDeclaration();
+      var declaration = ExternalSpecifications.resolve(call.getExecutable());
       if (declaration == null) return Set.of(new Path(EXTERNAL, List.of()));
       if (Annotations.permission(declaration) == Permission.FREE)
         return Set.of(new Path(FRESH, List.of()));
diff --git a/latte/src/main/java/latte/api/Main.java b/latte/src/main/java/latte/api/Main.java
index 56240cf..521dcb2 100644
--- a/latte/src/main/java/latte/api/Main.java
+++ b/latte/src/main/java/latte/api/Main.java
@@ -1,37 +1,53 @@
 package latte.api;
 
+import java.io.File;
+import java.util.*;
+import java.util.regex.Pattern;
+
 /** Minimal command-line entry point; nonzero exit status means verification did not succeed. */
 public final class Main {
   private Main() {}
 
   public static void main(String[] arguments) {
-    if (java.util.Arrays.stream(arguments).noneMatch(a -> !a.equals("--explain"))) {
-      System.err.println("Usage: latte [--explain] <Java file or source directory>...");
+    var paths = new ArrayList<String>();
+    var classpath = new ArrayList<String>();
+    boolean explain = false;
+    for (int i = 0; i < arguments.length; i++) {
+      if (arguments[i].equals("--explain")) explain = true;
+      else if ((arguments[i].equals("--classpath") || arguments[i].equals("-cp"))
+          && i + 1 < arguments.length)
+        classpath.addAll(Arrays.asList(arguments[++i].split(Pattern.quote(File.pathSeparator))));
+      else if (arguments[i].startsWith("-")) {
+        System.err.println("Unknown option or missing value: " + arguments[i]);
+        System.exit(2);
+        return;
+      } else paths.add(arguments[i]);
+    }
+    if (paths.isEmpty()) {
+      System.err.println(
+          "Usage: latte [--explain] [--classpath <JARs or directories>] <Java file or source directory>...");
       System.exit(2);
+      return;
     }
-    boolean explain = java.util.Arrays.asList(arguments).contains("--explain");
     boolean accepted = true;
-    for (String path : arguments) {
-      if (path.equals("--explain")) continue;
-      try {
-        var result = Verification.verify(path);
-        accepted &= result.accepted();
-        result
-            .diagnostics()
-            .forEach(
-                d ->
-                    System.err.printf(
-                        "%s:%d:%d: %s: %s%n",
-                        d.file(), d.line(), d.column(), d.kind(), d.message()));
-        if (explain)
-          result.diagnostics().stream()
-              .filter(d -> !d.detail().isEmpty())
-              .forEach(d -> System.err.println(d.detail()));
-        if (result.accepted()) System.out.println(path + ": verified");
-      } catch (RuntimeException failure) {
-        accepted = false;
-        System.err.println(path + ": could not analyze source: " + failure.getMessage());
-      }
+    try {
+      var result = Verification.verify(paths, classpath);
+      accepted = result.accepted();
+      result
+          .diagnostics()
+          .forEach(
+              d ->
+                  System.err.printf(
+                      "%s:%d:%d: %s: %s%n", d.file(), d.line(), d.column(), d.kind(), d.message()));
+      if (explain)
+        result.diagnostics().stream()
+            .filter(d -> !d.detail().isEmpty())
+            .forEach(d -> System.err.println(d.detail()));
+      if (result.accepted()) System.out.println(String.join(", ", paths) + ": verified");
+    } catch (RuntimeException failure) {
+      accepted = false;
+      System.err.println(
+          String.join(", ", paths) + ": could not analyze source: " + failure.getMessage());
     }
     if (!accepted) System.exit(1);
   }
diff --git a/latte/src/main/java/latte/api/Verification.java b/latte/src/main/java/latte/api/Verification.java
index b0e7c90..497054b 100644
--- a/latte/src/main/java/latte/api/Verification.java
+++ b/latte/src/main/java/latte/api/Verification.java
@@ -22,8 +22,17 @@ public boolean accepted() {
   }
 
   public static Result verify(String path) {
+    return verify(List.of(path), List.of());
+  }
+
+  /**
+   * Analyze application sources and external specifications together, with optional library JARs.
+   */
+  public static Result verify(List<String> paths, List<String> classpath) {
     var launcher = launcher();
-    launcher.addInputResource(path);
+    if (!classpath.isEmpty())
+      launcher.getEnvironment().setSourceClasspath(classpath.toArray(String[]::new));
+    paths.forEach(launcher::addInputResource);
     return verify(launcher);
   }
 
diff --git a/latte/src/main/java/latte/refinement/ConstantValues.java b/latte/src/main/java/latte/refinement/ConstantValues.java
index b30605f..ae73be8 100644
--- a/latte/src/main/java/latte/refinement/ConstantValues.java
+++ b/latte/src/main/java/latte/refinement/ConstantValues.java
@@ -17,6 +17,8 @@ static Optional<Term> resolve(String name, CtElement site) {
     if (!name.contains(".")) {
       CtType<?> owner = site instanceof CtType<?> type ? type : site.getParent(CtType.class);
       if (owner != null) {
+        if (latte.analysis.ExternalSpecifications.isSpecification(owner))
+          return resolve(latte.analysis.ExternalSpecifications.owner(owner) + "." + name, site);
         var field = owner.getField(name);
         if (field != null && field.isStatic() && field.isFinal())
           return expression(field.getDefaultExpression(), new HashSet<>());
diff --git a/latte/src/main/java/latte/refinement/Contracts.java b/latte/src/main/java/latte/refinement/Contracts.java
index b241f88..391b383 100644
--- a/latte/src/main/java/latte/refinement/Contracts.java
+++ b/latte/src/main/java/latte/refinement/Contracts.java
@@ -3,6 +3,7 @@
 import java.util.*;
 import java.util.regex.Pattern;
 import latte.analysis.Annotations;
+import latte.analysis.ExternalSpecifications;
 import latte.api.Diagnostic;
 import spoon.reflect.CtModel;
 import spoon.reflect.declaration.*;
@@ -44,10 +45,21 @@ public static Contracts collect(CtModel model) {
     var fields = new HashMap<String, CtField<?>>();
     var ancestors = new HashMap<String, List<String>>();
     var diagnostics = new ArrayList<Diagnostic>();
+    var external = ExternalSpecifications.on(model.getRootPackage());
+    external
+        .specifications()
+        .values()
+        .forEach(
+            specification ->
+                ancestors.put(
+                    specification.target().getQualifiedName(),
+                    hierarchy(specification.target(), new LinkedHashSet<>())));
     for (CtType<?> type : model.getElements(new TypeFilter<>(CtType.class))) {
-      ancestors.put(type.getQualifiedName(), hierarchy(type, new LinkedHashSet<>()));
+      String owner = ExternalSpecifications.owner(type);
+      if (!ExternalSpecifications.isSpecification(type))
+        ancestors.put(owner, hierarchy(type, new LinkedHashSet<>()));
       for (var field : type.getFields())
-        if (!field.isStatic()) {
+        if (!ExternalSpecifications.isStatic(field)) {
           String name = qualify(field, field.getSimpleName());
           fields.put(name, field);
           functions.put(
@@ -61,16 +73,16 @@ public static Contracts collect(CtModel model) {
         if (names.size() != new HashSet<>(names).size())
           diagnostics.add(Diagnostic.at(Diagnostic.Kind.SYNTAX, "Duplicate state name", type));
         states.put(
-            type.getQualifiedName(),
+            owner,
             Annotations.named(type, "StateSet").stream()
                 .map(
                     a ->
                         Annotations.strings(a.getValues().get("value")).stream()
-                            .map(n -> type.getQualifiedName() + "#" + n)
+                            .map(n -> owner + "#" + n)
                             .toList())
                 .toList());
         for (String name : names) {
-          String qualified = type.getQualifiedName() + "#" + name;
+          String qualified = owner + "#" + name;
           functions.put(qualified, new Prover.Function(List.of(Term.Sort.REF), Term.Sort.BOOL));
           ghosts.add(qualified);
         }
@@ -89,10 +101,6 @@ public static Contracts collect(CtModel model) {
             }
           }
       }
-      if (Annotations.has(element, "ExternalRefinementsFor"))
-        diagnostics.add(
-            Diagnostic.at(
-                Diagnostic.Kind.UNSUPPORTED, "External refinements are not implemented", element));
       for (String text : Annotations.strings(element, "RefinementAlias", "value")) {
         try {
           var match =
@@ -181,11 +189,16 @@ public String function(String type, String simple) {
 
   public static String qualify(CtElement element, String name) {
     var type = element instanceof CtType<?> t ? t : element.getParent(CtType.class);
-    return type == null ? name : type.getQualifiedName() + "#" + name;
+    return type == null ? name : ExternalSpecifications.owner(type) + "#" + name;
   }
 
   public static List<CtExecutable<?>> sources(CtExecutable<?> executable) {
     if (executable == null) return List.of();
+    if (!annotated(executable)) {
+      var external = ExternalSpecifications.resolve(executable.getReference());
+      if (external != executable && ExternalSpecifications.isSpecification(external))
+        return List.of(external);
+    }
     if (!(executable instanceof CtMethod<?> method) || annotated(method))
       return List.of(executable);
     var inherited = inherited(method);
@@ -214,6 +227,7 @@ private static void inherited(
                         && !candidate.isPrivate()
                         && candidate.getParameters().size() == method.getParameters().size())
             .filter(candidate -> method.isOverriding(candidate))
+            .map(candidate -> ExternalSpecifications.resolve(candidate.getReference()))
             .filter(Contracts::annotated)
             .toList();
     if (!matches.isEmpty()) {
@@ -231,9 +245,10 @@ public static CtExecutable<?> source(CtExecutable<?> executable) {
   }
 
   public static boolean annotated(CtExecutable<?> executable) {
-    return Annotations.has(executable, "Refinement")
-        || Annotations.has(executable, "StateRefinement")
-        || executable.getParameters().stream().anyMatch(p -> Annotations.has(p, "Refinement"));
+    return executable != null
+        && (Annotations.has(executable, "Refinement")
+            || Annotations.has(executable, "StateRefinement")
+            || executable.getParameters().stream().anyMatch(p -> Annotations.has(p, "Refinement")));
   }
 
   public static Term.Sort sort(String type) {
diff --git a/latte/src/main/java/latte/refinement/LiquidTypeChecking.java b/latte/src/main/java/latte/refinement/LiquidTypeChecking.java
index dcb2903..9e3a0fb 100644
--- a/latte/src/main/java/latte/refinement/LiquidTypeChecking.java
+++ b/latte/src/main/java/latte/refinement/LiquidTypeChecking.java
@@ -95,6 +95,7 @@ public List<Diagnostic> analyze(CtModel model) {
       }
       model.getElements(new TypeFilter<>(CtExecutable.class)).stream()
           .filter(e -> e instanceof CtMethod<?> || e instanceof CtConstructor<?>)
+          .filter(e -> !ExternalSpecifications.isLibrary(e))
           .forEach(
               e -> {
                 try {
@@ -104,7 +105,28 @@ public List<Diagnostic> analyze(CtModel model) {
                 }
               });
       for (var field : model.getElements(new TypeFilter<>(CtField.class)))
-        if (Annotations.has(field, "Refinement")) eligible(field, field);
+        if (Annotations.has(field, "Refinement")
+            && eligible(field, field)
+            && ExternalSpecifications.isSpecification(field)) {
+          var receiver = reference(field, "external-field:" + Annotations.key(field));
+          referenceTypes.put(receiver, ExternalSpecifications.owner(field.getDeclaringType()));
+          var state = TypingState.empty().bind("this", receiver);
+          var scope = new Scope(null, null, Map.of(), state);
+          var value = fresh("field", sort(field.getType()));
+          for (String text : Annotations.strings(field, "Refinement", "value"))
+            try {
+              prover.validate(
+                  predicate(
+                      text,
+                      Map.of("_", value, field.getSimpleName(), value),
+                      state,
+                      state,
+                      scope,
+                      field));
+            } catch (IllegalArgumentException | com.microsoft.z3.Z3Exception failure) {
+              report(Diagnostic.Kind.SYNTAX, failure.getMessage(), field);
+            }
+        }
     }
     return diagnostics.stream().distinct().toList();
   }
@@ -115,7 +137,7 @@ private void executable(CtExecutable<?> executable, CtExecutable<?> contract) {
     executable.getParameters().forEach(p -> declarations.put(p.getSimpleName(), p));
     CtType<?> type = executable.getParent(CtType.class);
     var fields =
-        type == null
+        type == null || ExternalSpecifications.isSpecification(executable)
             ? List.<CtField<?>>of()
             : executable instanceof CtConstructor<?> ? type.getFields() : visibleFields(type);
     fields.forEach(f -> declarations.put(f.getSimpleName(), f));
@@ -128,7 +150,7 @@ private void executable(CtExecutable<?> executable, CtExecutable<?> contract) {
     var scope = new Scope(executable, contract, Map.copyOf(declarations), null);
     var state = TypingState.empty();
     var receiver = reference(executable, "this:" + Annotations.key(executable));
-    if (type != null) referenceTypes.put(receiver, type.getQualifiedName());
+    if (type != null) referenceTypes.put(receiver, ExternalSpecifications.owner(type));
     state =
         state.bind("this", receiver).version(receiverName(receiver), fresh("state", Term.Sort.REF));
     state = state.assume(Term.binary("!=", receiver, Term.NULL));
@@ -226,6 +248,17 @@ && sort(method.getType()) == Term.Sort.REF
     }
     try {
       scope = new Scope(executable, contract, scope.declarations(), state);
+      if (ExternalSpecifications.isSpecification(executable)) {
+        var result =
+            ExternalSpecifications.constructor(executable)
+                ? receiver
+                : fresh("result", sort(((CtMethod<?>) executable).getType()));
+        for (String text : Annotations.strings(contract, "Refinement", "value"))
+          prover.validate(
+              predicate(
+                  text, Map.of("_", result, "return", result), state, state, scope, contract));
+        return;
+      }
       if (executable == contract && executable instanceof CtMethod<?> method)
         checkOverride(method, scope);
       var completion = statement(executable.getBody(), state, scope);
@@ -570,9 +603,10 @@ private TypingState loopEffects(CtLoop loop, TypingState state, Scope scope) {
           for (String identity : target.mutations()) modified.put(reference(call, identity), "*");
         continue;
       }
-      var declaration = call.getExecutable().getDeclaration();
+      var declaration = ExternalSpecifications.resolve(call.getExecutable());
       if (declaration == null) return havoc(state, scope);
       var effects = MutationEffects.on(declaration);
+      if (effects.globals()) return havoc(state, scope);
       String post =
           String.join(
               " ", Annotations.strings(Contracts.source(declaration), "StateRefinement", "to"));
@@ -588,6 +622,17 @@ private TypingState loopEffects(CtLoop loop, TypingState state, Scope scope) {
           modified.put(argument, "*");
         }
     }
+    for (CtConstructorCall<?> call : loop.getElements(new TypeFilter<>(CtConstructorCall.class))) {
+      if (call.getType().getQualifiedName().equals("java.lang.Object")) continue;
+      var effects = MutationEffects.on(ExternalSpecifications.resolve(call.getExecutable()));
+      if (effects.globals()) return havoc(state, scope);
+      for (int i = 0; i < call.getArguments().size(); i++)
+        if (effects.parameter(i)) {
+          var argument = loopReference(call.getArguments().get(i), state);
+          if (argument == null) return havoc(state, scope);
+          modified.put(argument, "*");
+        }
+    }
     for (CtFieldWrite<?> write : loop.getElements(new TypeFilter<>(CtFieldWrite.class))) {
       var receiver = loopReference(write.getTarget(), state);
       if (receiver != null && !write.getVariable().isStatic())
@@ -923,7 +968,7 @@ private Evaluation expressionValue(CtExpression<?> expression, TypingState befor
     if (expression instanceof CtThisAccess<?> || expression instanceof CtSuperAccess<?>)
       return new Evaluation(before, before.values().get("this"));
     if (expression instanceof CtFieldRead<?> field) {
-      var declaration = field.getVariable().getDeclaration();
+      var declaration = ExternalSpecifications.resolve(field.getVariable());
       if (field.getVariable().getSimpleName().equals("length")
           && field.getTarget() != null
           && field.getTarget().getType() != null
@@ -957,6 +1002,26 @@ else if (declaration != null)
         fieldValue = fieldValue(declaration, receiver.value(), receiver.state());
       if (fieldValue == null) fieldValue = fresh("field", sort(field.getType()));
       var after = receiver.state().assume(bounds(fieldValue, field.getType()));
+      if (ExternalSpecifications.isSpecification(declaration)
+          && Annotations.has(declaration, "Refinement")
+          && eligible(declaration, field)) {
+        for (String text : Annotations.strings(declaration, "Refinement", "value"))
+          after =
+              after.assume(
+                  predicate(
+                      text,
+                      Map.of(
+                          "_",
+                          fieldValue,
+                          declaration.getSimpleName(),
+                          fieldValue,
+                          "this",
+                          receiver.value()),
+                      after,
+                      after,
+                      scope,
+                      declaration));
+      }
       if (sort(field.getType()) == Term.Sort.REF) {
         var referenceValue = value(field, field.getType());
         after =
@@ -1393,7 +1458,8 @@ && sort(parameter.getType()) == Term.Sort.REF) {
                   : state.values().getOrDefault(ClosureFacts.RECEIVER, Term.NULL);
           var actual = unbound ? values.subList(1, values.size()) : values;
           var nodes = unbound ? arguments.subList(1, arguments.size()) : arguments;
-          var declaration = Contracts.source(reference.getExecutable().getDeclaration());
+          var declaration =
+              Contracts.source(ExternalSpecifications.resolve(reference.getExecutable()));
           if (reference.getExecutable().isConstructor()) {
             bound = result;
             state =
@@ -1452,7 +1518,7 @@ && sort(parameter.getType()) == Term.Sort.REF) {
 
   private void methodReference(
       CtExecutableReferenceExpression<?, ?> reference, TypingState captured, Scope scope) {
-    var target = reference.getExecutable().getDeclaration();
+    var target = ExternalSpecifications.resolve(reference.getExecutable());
     var type = reference.getType() == null ? null : reference.getType().getTypeDeclaration();
     if (target == null || type == null) return;
     var functional =
@@ -1590,7 +1656,10 @@ private TypingState arrayBounds(Term receiver, Term index, TypingState state, Ct
 
   private Location location(CtExpression<?> target, TypingState state, Scope scope) {
     if (target instanceof CtVariableAccess<?> variable) {
-      var declaration = variable.getVariable().getDeclaration();
+      var declaration =
+          target instanceof CtFieldAccess<?> field
+              ? ExternalSpecifications.resolve(field.getVariable())
+              : variable.getVariable().getDeclaration();
       String key =
           declaration == null
               ? variable.getVariable().getSimpleName()
@@ -1687,14 +1756,15 @@ private Evaluation call(
     if (local.isPresent() && !local.get().targets().isEmpty())
       return invokeClosure(
           local.get(), receiver.value(), argumentValues, arguments, call, state, scope);
-    var declaration = Contracts.source(reference.getDeclaration());
-    boolean constructor = call instanceof CtConstructorCall<?>;
+    var declaration = Contracts.source(ExternalSpecifications.resolve(reference));
+    boolean allocation = call instanceof CtConstructorCall<?>;
+    boolean constructor = reference.isConstructor();
     Term result =
-        constructor || sort(JavaTypes.result(call)) == Term.Sort.REF
+        allocation || sort(JavaTypes.result(call)) == Term.Sort.REF
             ? value(call, JavaTypes.result(call))
             : fresh("return", sort(JavaTypes.result(call)));
     state = state.assume(aliasMembership(result));
-    if (constructor) {
+    if (allocation) {
       receiver = new Evaluation(state, result);
       state = allocateObject(call, result, JavaTypes.result(call), state);
     }
@@ -1713,7 +1783,7 @@ private Evaluation call(
         possibleThrow(thrownType.getQualifiedName(), state, call);
       return new Evaluation(state.assume(bounds(result, JavaTypes.result(call))), result);
     }
-    var choices = Contracts.sources(reference.getDeclaration());
+    var choices = Contracts.sources(ExternalSpecifications.resolve(reference));
     if (choices.size() == 1) {
       var applied =
           applyContract(
@@ -1791,7 +1861,11 @@ private Evaluation applyContract(
       CtExpression<?> call,
       TypingState state,
       Scope scope) {
-    for (var thrownType : declaration.getThrownTypes())
+    for (var thrownType :
+        ExternalSpecifications.binding(declaration)
+            .map(ExternalSpecifications.Binding::actual)
+            .orElse(declaration)
+            .getThrownTypes())
       possibleThrow(thrownType.getQualifiedName(), havoc(state, scope), call);
     if (mayThrow(declaration))
       possibleThrow("java.lang.RuntimeException", havoc(state, scope), call);
@@ -1817,7 +1891,7 @@ private Evaluation applyContract(
       }
     }
     var clauses = Annotations.named(declaration, "StateRefinement");
-    if (constructor && clauses.isEmpty()) {
+    if (constructor && clauses.isEmpty() && !ExternalSpecifications.isSpecification(declaration)) {
       String type = referenceTypes.get(receiver.value());
       var states =
           contracts.states().getOrDefault(type, List.of()).stream()
@@ -1946,7 +2020,9 @@ private TypingState havocReachable(
     }
     // An unmodeled element set can include any previously read shared object.
     if (affected.keySet().stream().anyMatch(Reference::summarizesElements))
-      return havocObjects(state);
+      // The callee's receiver postcondition already describes its final state, even when
+      // an unknown argument element could alias it. Other potentially aliased objects lose facts.
+      return havocObjects(state).version(receiverName(receiver), versionOf(receiver, state));
     for (var effect : affected.entrySet()) {
       var object = reference(call, effect.getKey());
       if (object.equals(receiver) || !state.versions().containsKey(receiverName(object))) continue;
@@ -2150,7 +2226,8 @@ private String modifiedFields(CtExecutable<?> executable) {
   }
 
   private static boolean mayThrow(CtExecutable<?> executable) {
-    if (executable.getBody() == null) return true;
+    if (executable.getBody() == null || ExternalSpecifications.isSpecification(executable))
+      return true;
     return executable.getBody().getElements(new TypeFilter<>(CtElement.class)).stream()
         .anyMatch(
             e ->
diff --git a/latte/src/test/java/latte/refinement/ExternalClasspathTest.java b/latte/src/test/java/latte/refinement/ExternalClasspathTest.java
new file mode 100644
index 0000000..755924f
--- /dev/null
+++ b/latte/src/test/java/latte/refinement/ExternalClasspathTest.java
@@ -0,0 +1,81 @@
+package latte.refinement;
+
+import static org.junit.jupiter.api.Assertions.*;
+
+import java.nio.file.*;
+import java.util.*;
+import java.util.jar.*;
+import javax.tools.ToolProvider;
+import latte.api.Verification;
+import org.junit.jupiter.api.Test;
+import org.junit.jupiter.api.io.TempDir;
+
+class ExternalClasspathTest {
+  @TempDir Path directory;
+
+  @Test
+  void readsLibraryJarAndSeparateSpecificationsWithoutInitializingLibrary() throws Exception {
+    var source = directory.resolve("Counter.java");
+    Files.writeString(
+        source,
+        """
+        package library;
+        public class Counter {
+          static { if (true) throw new AssertionError("Library must not be initialized"); }
+          public static int increment(int number) { return number + 1; }
+        }
+        """);
+    var classes = Files.createDirectory(directory.resolve("classes"));
+    assertEquals(
+        0,
+        ToolProvider.getSystemJavaCompiler()
+            .run(null, null, null, "-d", classes.toString(), source.toString()));
+    var jar = directory.resolve("library.jar");
+    try (var output = new JarOutputStream(Files.newOutputStream(jar))) {
+      output.putNextEntry(new JarEntry("library/Counter.class"));
+      Files.copy(classes.resolve("library/Counter.class"), output);
+      output.closeEntry();
+    }
+    var specification = directory.resolve("Spec.java");
+    Files.writeString(
+        specification,
+        """
+        import liquidjava.specification.*;
+        @ExternalRefinementsFor("library.Counter") interface Spec {
+          @Refinement("_ == n + 1") int increment(@Refinement("_ < 2147483647") int n);
+        }
+        """);
+    var application = directory.resolve("Application.java");
+    Files.writeString(
+        application,
+        """
+        import liquidjava.specification.*;
+        class Application { void f() {
+          @Refinement("_ == 4") int result = library.Counter.increment(3);
+        }}
+        """);
+    var result =
+        Verification.verify(
+            List.of(specification.toString(), application.toString()), List.of(jar.toString()));
+    assertTrue(result.accepted(), result.diagnostics().toString());
+
+    var process =
+        new ProcessBuilder(
+                Path.of(System.getProperty("java.home"), "bin", "java").toString(),
+                "-cp",
+                System.getProperty("java.class.path"),
+                "latte.api.Main",
+                "--classpath",
+                jar.toString(),
+                specification.toString(),
+                application.toString())
+            .redirectErrorStream(true)
+            .start();
+    assertTrue(process.waitFor(30, java.util.concurrent.TimeUnit.SECONDS));
+    var output =
+        new String(
+            process.getInputStream().readAllBytes(), java.nio.charset.StandardCharsets.UTF_8);
+    assertEquals(0, process.exitValue(), output);
+    assertTrue(output.contains("verified"), output);
+  }
+}
diff --git a/latte/src/test/java/latte/refinement/ExternalSpecificationsTest.java b/latte/src/test/java/latte/refinement/ExternalSpecificationsTest.java
new file mode 100644
index 0000000..23eff76
--- /dev/null
+++ b/latte/src/test/java/latte/refinement/ExternalSpecificationsTest.java
@@ -0,0 +1,608 @@
+package latte.refinement;
+
+import static org.junit.jupiter.api.Assertions.*;
+
+import latte.api.*;
+import org.junit.jupiter.api.Test;
+import spoon.support.compiler.VirtualFile;
+
+class ExternalSpecificationsTest {
+  private Verification.Result check(String source) {
+    return Verification.verify(
+        new VirtualFile(
+            "import liquidjava.specification.*; import specification.*;\n" + source,
+            "Sample.java"));
+  }
+
+  private void accepts(String source) {
+    var result = check(source);
+    assertTrue(result.accepted(), result.diagnostics().toString());
+  }
+
+  private void rejects(String source, Diagnostic.Kind kind) {
+    var result = check(source);
+    assertTrue(
+        result.diagnostics().stream().anyMatch(d -> d.kind() == kind),
+        result.diagnostics().toString());
+  }
+
+  private static final String LIST =
+      """
+      @ExternalRefinementsFor("java.util.ArrayList")
+      @RefinementPredicate("int size(ArrayList list)")
+      interface ListSpec<E> {
+        @StateRefinement(to="size(this) == 0") void ArrayList();
+        @StateRefinement(to="size(this) == size(old(this)) + 1") boolean add(E value);
+        @StateRefinement(from="true") @Refinement("_ == size(this)") int size();
+        @StateRefinement(from="size(this) > 0", to="size(this) == size(old(this)) - 1")
+        E remove(@Refinement("_ >= 0 && _ < size(this)") int index);
+      }
+      """;
+
+  @Test
+  void libraryConstructorsAndTransitionsReachLocalAliases() {
+    accepts(
+        LIST
+            + """
+        class Sample { void f() {
+          java.util.ArrayList<Integer> list = new java.util.ArrayList<>();
+          java.util.ArrayList<Integer> alias = list;
+          alias.add(3);
+          @Refinement("_ == 1") int count = list.size();
+        }}
+        """);
+  }
+
+  @Test
+  void externalParameterRefinementsAreChecked() {
+    rejects(
+        LIST
+            + "class Sample { void f() { java.util.ArrayList<Integer> list = new java.util.ArrayList<>(); list.add(3); list.remove(1); }}",
+        Diagnostic.Kind.REFINEMENT);
+  }
+
+  @Test
+  void sharedLibraryReceiversStillRejectStateRefinements() {
+    rejects(
+        LIST + "class Sample { void f(java.util.ArrayList<Integer> list) { list.size(); }}",
+        Diagnostic.Kind.SHARED_REFINEMENT);
+  }
+
+  @Test
+  void resolvesStaticOverloadsByTheirJavaSignature() {
+    accepts(
+        """
+        @ExternalRefinementsFor("java.lang.Math") interface MathSpec {
+          @Refinement("_ == (left > right ? left : right)") int max(int left, int right);
+          @Refinement("_ == (a > b ? a : b)") long max(long a, long b);
+        }
+        class Sample { void f() {
+          @Refinement("_ == 7") int first = Math.max(3, 7);
+          @Refinement("_ == 5000000000") long second = Math.max(5000000000L, 7L);
+        }}
+        """);
+  }
+
+  @Test
+  void borrowedLibraryParametersDoNotEscapeButCanMutate() {
+    rejects(
+        """
+        @ExternalRefinementsFor("java.util.Arrays") interface ArraysSpec {
+          void fill(@Borrowed int[] values, int value);
+        }
+        class Sample { void f() {
+          int[] values = { 0 };
+          java.util.Arrays.fill(values, 3);
+          @Refinement("_ == 0") int stale = values[0];
+        }}
+        """,
+        Diagnostic.Kind.REFINEMENT);
+  }
+
+  @Test
+  void freeExternalParametersConsumeAllCallerAliases() {
+    rejects(
+        """
+        @ExternalRefinementsFor("java.util.Objects") interface ObjectsSpec {
+          @Free @Refinement("_ != null") Object requireNonNull(@Free Object object);
+        }
+        class Sample { void f() {
+          Object original = new Object(); Object alias = original;
+          @Refinement("_ != null") Object result = java.util.Objects.requireNonNull(original);
+          Object stale = alias;
+        }}
+        """,
+        Diagnostic.Kind.PERMISSION);
+  }
+
+  @Test
+  void externalConstructorParametersHaveOwnershipContracts() {
+    accepts(
+        """
+        @ExternalRefinementsFor("java.io.ByteArrayInputStream") interface InputSpec {
+          void ByteArrayInputStream(@Borrowed byte[] bytes);
+        }
+        class Sample { void f(@Borrowed byte[] bytes) {
+          new java.io.ByteArrayInputStream(bytes);
+        }}
+        """);
+  }
+
+  @Test
+  void rejectsMisspelledMemberSignatures() {
+    rejects(
+        "@ExternalRefinementsFor(\"java.util.ArrayList\") interface Spec { void ad(int n); }",
+        Diagnostic.Kind.SYNTAX);
+  }
+
+  @Test
+  void rejectsIncompatibleReturnTypes() {
+    rejects(
+        "@ExternalRefinementsFor(\"java.lang.Math\") interface Spec { int max(long a, long b); }",
+        Diagnostic.Kind.SYNTAX);
+  }
+
+  @Test
+  void rejectsDuplicateTargetSpecifications() {
+    rejects(
+        "@ExternalRefinementsFor(\"java.lang.Math\") interface One {} @ExternalRefinementsFor(\"java.lang.Math\") interface Two {}",
+        Diagnostic.Kind.SYNTAX);
+  }
+
+  @Test
+  void rejectsUnknownTargetWithoutCrashing() {
+    rejects(
+        "@ExternalRefinementsFor(\"missing.Library\") interface Spec {}", Diagnostic.Kind.SYNTAX);
+  }
+
+  @Test
+  void rejectsAnnotationOnAMethod() {
+    rejects(
+        "class Sample { @ExternalRefinementsFor(\"java.lang.Math\") void f() {} }",
+        Diagnostic.Kind.SYNTAX);
+  }
+
+  @Test
+  void externalBodiesAreOnlyPlaceholders() {
+    accepts(
+        """
+        @ExternalRefinementsFor("java.lang.Math") class Spec {
+          @Refinement("_ >= 0") public int abs(@Refinement("_ > -2147483648") int x) { return -1; }
+        }
+        class Sample { void f() { @Refinement("_ >= 0") int n = Math.abs(-3); }}
+        """);
+  }
+
+  @Test
+  void unspecifiedOverloadDoesNotUseAnotherOverloadsContract() {
+    rejects(
+        """
+        @ExternalRefinementsFor("java.lang.Math") interface Spec {
+          @Refinement("_ == 7") int max(int a, int b);
+        }
+        class Sample { void f() { @Refinement("_ == 7") long n = Math.max(3L, 7L); }}
+        """,
+        Diagnostic.Kind.REFINEMENT);
+  }
+
+  @Test
+  void inheritedInterfaceContractsApplyToConcreteReceivers() {
+    accepts(
+        """
+        @ExternalRefinementsFor("java.util.Collection") interface Spec<E> {
+          @StateRefinement(from="true") @Refinement("_ >= 0") int size();
+        }
+        class Sample { void f() {
+          java.util.ArrayList<String> list = new java.util.ArrayList<>();
+          @Refinement("_ >= 0") int n = list.size();
+        }}
+        """);
+  }
+
+  @Test
+  void borrowedReceiversRetainStateContracts() {
+    accepts(
+        LIST
+            + """
+        class Sample { void f(@Borrowed java.util.ArrayList<Integer> list) {
+          int before = list.size(); list.add(1);
+          @Refinement("_ == before + 1") int after = list.size();
+        }}
+        """);
+  }
+
+  @Test
+  void unlistedCallsInvalidateLibraryState() {
+    rejects(
+        LIST
+            + """
+        class Sample { void f() {
+          java.util.ArrayList<Integer> list = new java.util.ArrayList<>();
+          list.clear(); @Refinement("_ == 0") int n = list.size();
+        }}
+        """,
+        Diagnostic.Kind.REFINEMENT);
+  }
+
+  @Test
+  void constructorsNeverInheritTheirParentsExternalContract() {
+    rejects(
+        """
+        class Parent { Parent(int n) {} }
+        class Child extends Parent { Child(int n) { super(n); } }
+        @ExternalRefinementsFor("Parent") interface Spec {
+          @Refinement("false") void Parent(int n);
+        }
+        class Sample { void f() { Child c = new Child(1); @Refinement("false") int bad = 1; }}
+        """,
+        Diagnostic.Kind.REFINEMENT);
+  }
+
+  @Test
+  void constructorPreconditionsAreEnforced() {
+    rejects(
+        """
+        @ExternalRefinementsFor("java.util.ArrayList") interface Spec {
+          void ArrayList(@Refinement("_ >= 0") int capacity);
+        }
+        class Sample { void f() { new java.util.ArrayList<>(-1); }}
+        """,
+        Diagnostic.Kind.REFINEMENT);
+  }
+
+  @Test
+  void externalConstructorMutationInvalidatesLoopEntryFacts() {
+    rejects(
+        """
+        @ExternalRefinementsFor("java.io.ByteArrayInputStream") interface Spec {
+          void ByteArrayInputStream(@Borrowed byte[] bytes);
+        }
+        class Sample { void f(boolean again) {
+          byte[] bytes = {0};
+          while (again) {
+            @Refinement("_ == 0") byte value = bytes[0];
+            new java.io.ByteArrayInputStream(bytes);
+          }
+        }}
+        """,
+        Diagnostic.Kind.REFINEMENT);
+  }
+
+  @Test
+  void callbacksUseExternalMethodContracts() {
+    accepts(
+        """
+        @ExternalRefinementsFor("java.lang.Math") interface Spec {
+          @Refinement("_ == (x >= 0 ? x : (x == -2147483648 ? x : -x))") int abs(int x);
+        }
+        class Sample { void f() {
+          java.util.function.IntUnaryOperator absolute = Math::abs;
+          @Refinement("_ >= 0") int n = absolute.applyAsInt(-3);
+        }}
+        """);
+  }
+
+  @Test
+  void sharedExternalReturnsCannotCarryRefinements() {
+    rejects(
+        """
+        @ExternalRefinementsFor("java.util.Objects") interface Spec {
+          @Refinement("_ != null") Object requireNonNull(Object x);
+        }
+        """,
+        Diagnostic.Kind.SHARED_REFINEMENT);
+  }
+
+  @Test
+  void primitiveExternalFieldsCarryTheirDeclaredInvariant() {
+    accepts(
+        """
+        @ExternalRefinementsFor("java.awt.Point") interface Spec {
+          @Refinement("_ >= 0") int x = -999;
+        }
+        class Sample { void f() { java.awt.Point point = new java.awt.Point(1,2);
+          @Refinement("_ >= 0") int n = point.x;
+        }}
+        """);
+    rejects(
+        """
+        @ExternalRefinementsFor("java.awt.Point") interface Spec {
+          @Refinement("_ >= 0") int x = -999;
+        }
+        class Sample { void f() { java.awt.Point point = new java.awt.Point(1,2); point.x = -1; }}
+        """,
+        Diagnostic.Kind.REFINEMENT);
+  }
+
+  @Test
+  void staticFieldPlaceholdersAreNotRuntimeValues() {
+    rejects(
+        """
+        class Library { public static int count = 4; }
+        @ExternalRefinementsFor("Library") interface Spec {
+          @Refinement("_ >= 0") int count = -999;
+        }
+        class Sample { void f() { @Refinement("_ == -999") int n = Library.count; }}
+        """,
+        Diagnostic.Kind.REFINEMENT);
+    accepts(
+        """
+        class Library { public static int count = 4; }
+        @ExternalRefinementsFor("Library") interface Spec {
+          @Refinement("_ >= 0") int count = -999;
+        }
+        class Sample { void f() { @Refinement("_ >= 0") int n = Library.count; }}
+        """);
+  }
+
+  @Test
+  void rejectsInvalidExternalFieldTypes() {
+    rejects(
+        "@ExternalRefinementsFor(\"java.awt.Point\") interface Spec { long x = 0; }",
+        Diagnostic.Kind.SYNTAX);
+  }
+
+  @Test
+  void externalStateSetsUseLibraryTypeIdentity() {
+    accepts(
+        """
+        @ExternalRefinementsFor("java.io.ByteArrayInputStream") @StateSet({"open", "closed"})
+        interface Spec {
+          @StateRefinement(to="open(this)") void ByteArrayInputStream(byte[] bytes);
+          @StateRefinement(from="open(this)", to="closed(this)") void close();
+          @StateRefinement(from="closed(this)") @Refinement("_ >= 0") int available();
+        }
+        class Sample { void f() {
+          java.io.ByteArrayInputStream stream = new java.io.ByteArrayInputStream(new byte[0]);
+          stream.close(); @Refinement("_ >= 0") int n = stream.available();
+        }}
+        """);
+  }
+
+  @Test
+  void borrowedArgumentsRemainLocallyRefinable() {
+    accepts(
+        """
+        @ExternalRefinementsFor("java.util.Arrays") interface Spec {
+          void fill(@Borrowed int[] values, int value);
+        }
+        class Sample { void f() {
+          int[] values = { 0 }; java.util.Arrays.fill(values, 3);
+          @Refinement("_ != null") int[] alias = values;
+        }}
+        """);
+  }
+
+  @Test
+  void unspecifiedOwnershipEscapesArguments() {
+    rejects(
+        """
+        @ExternalRefinementsFor("java.util.Arrays") interface Spec {
+          void fill(int[] values, int value);
+        }
+        class Sample { void f() {
+          int[] values = { 0 }; java.util.Arrays.fill(values, 3);
+          @Refinement("_ != null") int[] alias = values;
+        }}
+        """,
+        Diagnostic.Kind.SHARED_REFINEMENT);
+  }
+
+  @Test
+  void freeResultsRemainRefinableAfterTransfer() {
+    accepts(
+        """
+        @ExternalRefinementsFor("java.util.Objects") interface Spec {
+          @Free @Refinement("_ != null") Object requireNonNull(@Free Object x);
+        }
+        class Sample { void f() {
+          Object x = new Object();
+          @Refinement("_ != null") Object result = java.util.Objects.requireNonNull(x);
+        }}
+        """);
+  }
+
+  @Test
+  void uniqueExternalArgumentsRejectBorrowedReferences() {
+    rejects(
+        """
+        @ExternalRefinementsFor("java.util.Arrays") interface Spec {
+          void fill(@Unique int[] values, int value);
+        }
+        class Sample { void f(@Borrowed int[] values) {
+          java.util.Arrays.fill(values, 3);
+        }}
+        """,
+        Diagnostic.Kind.PERMISSION);
+  }
+
+  @Test
+  void retainsBindingsAndOwnershipOnSpoonNodesAcrossReanalysis() {
+    var result =
+        check(
+            LIST
+                + """
+        class Sample { void f() {
+          java.util.ArrayList<Integer> list = new java.util.ArrayList<>(); list.add(1);
+        }}
+        """);
+    assertTrue(result.accepted(), result.diagnostics().toString());
+    var calls =
+        result
+            .model()
+            .getElements(
+                new spoon.reflect.visitor.filter.TypeFilter<>(
+                    spoon.reflect.code.CtInvocation.class));
+    var call =
+        calls.stream()
+            .filter(c -> c.getExecutable().getSimpleName().equals("add"))
+            .findFirst()
+            .orElseThrow();
+    var contract = latte.analysis.ExternalSpecifications.resolve(call.getExecutable());
+    assertEquals(
+        "ListSpec", contract.getParent(spoon.reflect.declaration.CtType.class).getSimpleName());
+    assertTrue(latte.analysis.LatteFacts.on(call.getTarget()).orElseThrow().refinable());
+    assertTrue(new latte.analysis.LatteAnalysis().analyze(result.model()).isEmpty());
+    assertTrue(new LiquidTypeChecking().analyze(result.model()).isEmpty());
+    rejects(
+        "class Sample { void f() { @Refinement(\"_ == 3\") int n = Math.max(2, 3); }}",
+        Diagnostic.Kind.REFINEMENT);
+  }
+
+  @Test
+  void varargsContractsRequireAnExplicitArray() {
+    String specification =
+        """
+        @ExternalRefinementsFor("java.lang.String") interface Spec {
+          String format(String format, @Borrowed Object... values);
+        }
+        """;
+    accepts(
+        specification
+            + """
+        class Sample { void f() { String.format("%s", new Object[]{new Object()}); }}
+        """);
+    rejects(
+        specification
+            + """
+        class Sample { void f() { String.format("%s", new Object()); }}
+        """,
+        Diagnostic.Kind.UNSUPPORTED);
+  }
+
+  @Test
+  void validatesUnusedExternalFieldPredicates() {
+    rejects(
+        """
+        @ExternalRefinementsFor("java.awt.Point") interface Spec {
+          @Refinement("_ >= missing") int x = 0;
+        }
+        """,
+        Diagnostic.Kind.SYNTAX);
+  }
+
+  @Test
+  void staticMethodsCannotDeclareReceiverState() {
+    rejects(
+        """
+        @ExternalRefinementsFor("java.lang.Math") interface Spec {
+          @StateRefinement(from="true") int abs(int value);
+        }
+        """,
+        Diagnostic.Kind.SYNTAX);
+  }
+
+  @Test
+  void hiddenFieldsDoNotInheritTheirParentsContract() {
+    rejects(
+        """
+        class Parent { int x; }
+        class Child extends Parent { int x; }
+        @ExternalRefinementsFor("Parent") interface Spec {
+          @Refinement("_ >= 0") int x = 0;
+        }
+        class Sample { void f(@Borrowed Child child) {
+          child.x = -1; @Refinement("_ >= 0") int bad = child.x;
+        }}
+        """,
+        Diagnostic.Kind.REFINEMENT);
+  }
+
+  @Test
+  void hiddenStaticMethodsDoNotInheritTheirParentsContract() {
+    rejects(
+        """
+        class Parent { static int value() { return 1; } }
+        class Child extends Parent { static int value() { return 2; } }
+        @ExternalRefinementsFor("Parent") interface Spec {
+          @Refinement("_ == 1") int value();
+        }
+        class Sample { void f() { @Refinement("_ == 1") int bad = Child.value(); }}
+        """,
+        Diagnostic.Kind.REFINEMENT);
+  }
+
+  @Test
+  void rejectsMembersThatJavaDoesNotInherit() {
+    var result =
+        Verification.verify(
+            "src/test/resources/liquidjava/testSuite/classes/inherited_external_visibility");
+    assertEquals(3, result.diagnostics().size(), result.diagnostics().toString());
+    assertTrue(result.diagnostics().stream().allMatch(d -> d.kind() == Diagnostic.Kind.SYNTAX));
+  }
+
+  @Test
+  void externalCallsDoNotImplyGlobalPurity() {
+    rejects(
+        """
+        class Library { static void invoke() { Sample.counter = 2; } }
+        @ExternalRefinementsFor("Library") interface Spec { void invoke(); }
+        class Sample { static int counter; void f() {
+          counter = 1; Library.invoke(); @Refinement("_ == 1") int stale = counter;
+        }}
+        """,
+        Diagnostic.Kind.REFINEMENT);
+  }
+
+  @Test
+  void externalReferenceFieldsUseOwnershipAndSharedPolicy() {
+    accepts(
+        """
+        class Library { Object value; }
+        @ExternalRefinementsFor("Library") interface Spec {
+          @Unique @Refinement("_ != null") Object value = null;
+        }
+        class Sample { void f(@Borrowed Library library) {
+          @Refinement("_ != null") Object value = library.value;
+        }}
+        """);
+    rejects(
+        """
+        class Library { Object value; }
+        @ExternalRefinementsFor("Library") interface Spec {
+          @Refinement("_ != null") Object value = null;
+        }
+        """,
+        Diagnostic.Kind.SHARED_REFINEMENT);
+  }
+
+  @Test
+  void placeholderBodiesDoNotSupplyReturnAliasFacts() {
+    var result =
+        check(
+            """
+        @ExternalRefinementsFor("java.util.Objects") class Spec {
+          @Borrowed @Refinement("_ != null") Object requireNonNull(@Borrowed Object x) { return null; }
+        }
+        class Sample { void f() {
+          Object original = new Object(); Object result = java.util.Objects.requireNonNull(original);
+        }}
+        """);
+    assertTrue(result.accepted(), result.diagnostics().toString());
+    var local =
+        result
+            .model()
+            .getElements(
+                new spoon.reflect.visitor.filter.TypeFilter<>(
+                    spoon.reflect.code.CtLocalVariable.class))
+            .stream()
+            .filter(v -> v.getSimpleName().equals("result"))
+            .findFirst()
+            .orElseThrow();
+    var facts = latte.analysis.LatteFacts.on(local).orElseThrow();
+    assertFalse(facts.value().objects().isEmpty());
+  }
+
+  @Test
+  void varargsMethodReferenceAdaptersAreRejectedExplicitly() {
+    rejects(
+        """
+        @ExternalRefinementsFor("java.lang.String") interface Spec {
+          String format(String format, Object... values);
+        }
+        interface Formatter { String apply(String pattern, Object value); }
+        class Sample { void f() { Formatter formatter = String::format; }}
+        """,
+        Diagnostic.Kind.UNSUPPORTED);
+  }
+}
diff --git a/latte/src/test/java/latte/refinement/VerificationTest.java b/latte/src/test/java/latte/refinement/VerificationTest.java
index 62ae911..b4a1497 100644
--- a/latte/src/test/java/latte/refinement/VerificationTest.java
+++ b/latte/src/test/java/latte/refinement/VerificationTest.java
@@ -128,10 +128,8 @@ void malformedPredicatesAreErrors() {
   }
 
   @Test
-  void externalRefinementsAreExplicitlyUnsupported() {
-    rejects(
-        "@ExternalRefinementsFor(\"java.util.List\") interface Sample {}",
-        Diagnostic.Kind.UNSUPPORTED);
+  void externalRefinementDeclarationsAreSupported() {
+    accepts("@ExternalRefinementsFor(\"java.util.List\") interface Sample {}");
   }
 
   @Test
diff --git a/latte/src/test/resources/liquidjava/supported-inputs.txt b/latte/src/test/resources/liquidjava/supported-inputs.txt
index 925e8f4..20ec420 100644
--- a/latte/src/test/resources/liquidjava/supported-inputs.txt
+++ b/latte/src/test/resources/liquidjava/supported-inputs.txt
@@ -148,6 +148,8 @@ ErrorUnresolvedUnaryOperator.java
 ErrorVarLocal.java
 ErrorVarargsCall.java
 ErrorYieldRefinedConstructor.java
+classes/alias_static_final_state_correct
+classes/arraylist_correct
 classes/boolean_ghost_correct
 classes/boolean_ghost_error
 classes/conflicting_state_names_correct
@@ -156,11 +158,24 @@ classes/downloader_refinement_error
 classes/downloader_state_refinement_error
 classes/email_correct
 classes/email_error
+classes/index_out_of_bounds_error
+classes/inherited_external_correct
+classes/inherited_external_error
+classes/inherited_source_correct
+classes/inherited_source_error
+classes/input_reader_error
 classes/iterator_error
+classes/method_overload_correct
+classes/method_overload_error
+classes/overload_constructors_correct
+classes/overload_constructors_error
 classes/refs_from_interface_error
 classes/refs_from_superclass_error
 classes/scoreboard_error
 classes/state_from_superclass_correct
 classes/state_refinement_no_to_typestate_correct
+classes/state_return_type_scope_correct
+classes/throwable_subclass_error
 classes/vending_machine_correct
 field_updates
+math/correctInvocation