diff --git a/usvm-ts-calls/STARTUP_GRAPH_FREEZING.md b/usvm-ts-calls/STARTUP_GRAPH_FREEZING.md
new file mode 100644
index 0000000000..4337cd8dbe
--- /dev/null
+++ b/usvm-ts-calls/STARTUP_GRAPH_FREEZING.md
@@ -0,0 +1,76 @@
+# Freeze original class startup graphs
+
+`freeze-class-startup-inputs.py` consumes the unchanged selection ledger and original
+project acquisition receipts. It uses the existing `inspect-startup-closure` traversal,
+then writes a machine startup manifest with every original class, per-class graph
+receipts and shared thin source roots. It does not install dependencies or execute
+project code. Build the adapter before invoking the CLI.
+
+```sh
+python3 usvm-ts-calls/scripts/freeze-class-startup-inputs.py \
+  --ledger /absolute/path/selection-ledger.json \
+  --acquisition /absolute/path/manager-retry-attempt \
+  --acquisition /absolute/path/priority-attempt \
+  --acquisition /absolute/path/secondary-attempt \
+  --inspector /absolute/path/fast-check-adapter/dist/src/source-inspector-cli.js \
+  --frontend-typescript /absolute/path/pinned-frontend/node_modules/typescript \
+  --tool-revision EXACT_40_HEX_BUILD_REVISION \
+  --native-frontend-revision bundled:EXACT_FRONTEND_REVISION \
+  --output /absolute/path/new-startup-graph-attempt
+```
+
+Acquisition arguments are ordered preferences: the first successful frozen receipt
+wins; if none succeeded, the first failure remains explicit provenance. A failed
+whole devDependency installation does not automatically reject a class. Its graph
+can still qualify when every consumed runtime/config/lock input is proven by the
+exact original Git revision and all runtime edges are resolved or explicitly recorded
+as boundaries. Generated or installed inputs require their immutable acquisition
+snapshot. Changed inputs and unresolved static modules retain incomplete rows.
+
+Startup traversal follows actual TS/JS runtime code and literal CommonJS requests.
+JSON, native builtins and unresolved dynamic module requests remain explicit boundaries,
+including source offsets/expressions where the target cannot be statically resolved.
+The graph receipt never claims those boundaries have symbolic models or native replay
+support. Checked/native admission remains strict and separate. Initialization and
+binding limitations remain diagnostics rather than disappearing from the report.
+
+Original target/import bytes are copied verbatim. Physical installed runtime sources
+receive an explicit content-preserving `.usvm-installed` namespace mapping, while
+frontend roots contain only the acquired runtime source graph. Project copies are
+shared across classes; dependency snapshots are not copied wholesale. Each machine
+manifest row freezes its exact frontend config, selected source bytes and a graph
+receipt relative to the manifest root. Original installation receipts remain unchanged.
+
+The CLI reads the pinned frontend TypeScript option/lib inventory and compiler SHA.
+Startup-only compatibility projects unsupported type-check-only options and newer
+library declarations into that frontend environment. Original resolved options,
+each before/after boundary and unprojected unknown semantic options are retained.
+For example, `lib: ["es2024"]` can use the frontend's `esnext` declarations; this does
+not emulate ES2024 runtime operations. Unknown semantic/emission options are preserved
+for explicit frontend diagnostics. Checked and native replay configs are unchanged.
+
+Frontend compatibility also checks option names and enum values against that exact
+compiler's inventory. The receipt records `frontendCompilerProjection.status` and
+`unsupportedCompatibilityBoundaries` with typed
+`FRONTEND_COMPILER_OPTION_UNSUPPORTED` reasons. This is detection only: unsupported
+semantic/emission options and enum values remain unchanged. In particular, TypeScript
+5.4.5 cannot accept Utilityjs's `module: "node20"` or
+`rewriteRelativeImportExtensions`; `noEmit` does not prove those settings harmless.
+The former controls Node module/interoperability semantics, while the latter also
+affects semantic diagnostics and derived import-extension options. This change does
+not make `DisjointSet` start: it requires genuine frontend support for those options
+or a compatible compiler upgrade. An acquired graph can still have unsupported
+frontend compatibility, and `COMPATIBLE` is only an inventory check, not proof of
+successful IR generation or symbolic support.
+
+`acquisitionComplete` proves the frozen per-class graph, including explicit opaque
+boundaries. Genuine machine class entry, useful candidate values and class-only
+replay-checked coverage are later, distinct checks. Keep all original rows in those
+reports; do not select a new cohort from successful startups.
+
+Focused checks require a built adapter:
+
+```sh
+python3 -m unittest discover -s usvm-ts-calls/scripts \
+  -p test_freeze_class_startup_inputs.py -v
+```
diff --git a/usvm-ts-calls/STARTUP_RUNTIME_RESOLUTION.md b/usvm-ts-calls/STARTUP_RUNTIME_RESOLUTION.md
new file mode 100644
index 0000000000..660e46fc56
--- /dev/null
+++ b/usvm-ts-calls/STARTUP_RUNTIME_RESOLUTION.md
@@ -0,0 +1,29 @@
+# Resolve acquired startup runtime bytes
+
+`FrozenModuleResolver.resolveStartup(specifier, from, importKind)` is an additive
+acquisition API. The existing checked/native-replay `resolve` contract is unchanged.
+It selects actual in-root TypeScript or JavaScript runtime source, including installed
+packages, original generated JavaScript and package export patterns. Import and
+require conditions are selected separately; declaration entries never replace runtime.
+An explicit package export must exist exactly: missing `.js` exports are not guessed
+as `.ts` sources. Relative source imports retain the existing absent-JS/source-TS
+mapping, while present JavaScript always wins.
+
+The result is either a source edge or an explicit runtime boundary. Node builtins
+are recorded by name, containing source and import kind; JSON boundaries also verify
+JSON syntax and freeze the actual JSON bytes. Boundary acquisition does not implement
+JSON evaluation, native builtins or their symbolic models. Missing packages, unsupported
+formats, declaration-only entries, escaping paths and incompatible context-dependent
+aliases still fail explicitly.
+
+`freeze` adds `runtimeBoundaries` only when present, keeps consumed runtime/package/
+config/lock hashes, and enables JavaScript in the derived startup frontend configuration.
+The config is derived from explicit original compiler settings, rather than defaults
+computed by a newer TypeScript version. No imports or original source bytes are edited.
+
+Graph consumers must follow each source edge and retain every boundary diagnostic.
+Installed source paths are acquisition identities: they need a content-preserving,
+explicit original-to-materialized namespace mapping before frontend lowering, because
+physical `node_modules` paths have unstable frontend identities. Do not turn the full
+installation snapshot into frontend roots. A complete acquired graph is separate from
+engine support, successful class entry and replay-checked coverage.
diff --git a/usvm-ts-calls/scripts/freeze-class-startup-inputs.py b/usvm-ts-calls/scripts/freeze-class-startup-inputs.py
new file mode 100644
index 0000000000..4a658281ee
--- /dev/null
+++ b/usvm-ts-calls/scripts/freeze-class-startup-inputs.py
@@ -0,0 +1,274 @@
+#!/usr/bin/env python3
+"""Freeze startup graphs from acquired projects; never install or execute project code."""
+import argparse
+import concurrent.futures
+import hashlib
+import json
+from pathlib import Path
+import re
+import subprocess
+
+
+def digest(data):
+    return hashlib.sha256(data).hexdigest()
+
+
+def write_json(path, value):
+    path.parent.mkdir(parents=True, exist_ok=True)
+    path.write_text(json.dumps(value, indent=2, sort_keys=True) + '\n', encoding='utf-8')
+
+
+def safe_path(root, name):
+    relative = Path(name)
+    if relative.is_absolute() or '..' in relative.parts:
+        raise ValueError(f'Unsafe frozen input name: {name}')
+    file = root / relative
+    if not file.resolve().is_relative_to(root.resolve()):
+        raise ValueError(f'Frozen input escapes project: {name}')
+    return file
+
+
+def materialized_name(name):
+    parts = Path(name).parts
+    if 'node_modules' not in parts:
+        return name
+    first = parts.index('node_modules')
+    return Path(*parts[:first], '.usvm-installed', *['packages' if part == 'node_modules' else part
+                                                  for part in parts[first + 1:]]).as_posix()
+
+
+def frontend_environment(module):
+    script = ('const ts=require(process.argv[1]); const lib=ts.optionDeclarations.find(o=>o.name==="lib"); '
+              'process.stdout.write(JSON.stringify({version:ts.version,options:ts.optionDeclarations.map(o=>o.name),'
+              'libs:[...lib.element.type.keys()],enumOptions:Object.fromEntries('
+              'ts.optionDeclarations.filter(o=>o.type instanceof Map).map(o=>[o.name,[...o.type.keys()]]))}));')
+    value = json.loads(subprocess.check_output(['node', '-e', script, str(module)], text=True))
+    compiler = module / 'lib' / 'typescript.js' if module.is_dir() else module
+    value['compilerSha256'] = digest(compiler.read_bytes())
+    return value
+
+
+def project_frontend_options(original, environment):
+    projected = dict(original)
+    boundaries = []
+    supported = set(environment['options'])
+    type_only = {'noUncheckedSideEffectImports', 'strictBuiltinIteratorReturn', 'noCheck',
+                 'isolatedDeclarations', 'erasableSyntaxOnly', 'ignoreDeprecations'}
+    for name in sorted(type_only - supported):
+        if name in projected:
+            boundaries.append({'kind': 'type-check-option', 'option': name, 'original': projected.pop(name),
+                               'projected': None, 'reason': 'Unsupported frontend type-check-only option'})
+    libs = projected.get('lib')
+    if isinstance(libs, list):
+        available = {name.lower() for name in environment['libs']}
+        updated = list(dict.fromkeys(name if name.lower() in available else 'esnext' for name in libs))
+        if updated != libs:
+            if 'esnext' not in available:
+                raise ValueError('Frontend lacks the declared compatibility type library esnext')
+            boundaries.append({'kind': 'type-library-environment', 'option': 'lib', 'original': libs,
+                               'projected': updated, 'reason': 'Frontend declaration library; no runtime emulation claimed'})
+            projected['lib'] = updated
+    unsupported_options = sorted(set(projected) - supported)
+    unsupported = [{'reasonCode': 'FRONTEND_COMPILER_OPTION_UNSUPPORTED', 'kind': 'option-name',
+                    'option': name, 'original': projected[name], 'frontendVersion': environment['version']}
+                   for name in unsupported_options]
+    for name, values in environment.get('enumOptions', {}).items():
+        if name not in projected or name not in supported:
+            continue
+        value = projected[name]
+        supported_value = isinstance(value, str) and value.lower() in {item.lower() for item in values}
+        if not supported_value:
+            unsupported.append({'reasonCode': 'FRONTEND_COMPILER_OPTION_UNSUPPORTED', 'kind': 'option-value',
+                                'option': name, 'original': value, 'supportedValues': values,
+                                'frontendVersion': environment['version']})
+    return projected, {'environment': environment, 'boundaries': boundaries,
+                       'unprojectedUnsupportedOptions': unsupported_options,
+                       'unsupportedCompatibilityBoundaries': unsupported,
+                       'status': 'UNSUPPORTED' if unsupported else 'COMPATIBLE'}
+
+
+def inspect_case(case, receipt_path, inspector, output, timeout, environment=None, tool_proof=None):
+    installation = json.loads(receipt_path.read_bytes())
+    installed = installation.get('phase') == 'FROZEN' and installation.get('dependenciesInstalled') is True
+    root = Path(installation['sourceRoot'] if installed else installation['originalSourceRoot']).resolve()
+    revision = re.search(r'@([0-9a-f]{40}):', case['identity']).group(1)
+    class_id = re.sub(r'[^A-Za-z0-9_-]', '-', case['projectId'] + '-' + case['className']) + '-' + digest(case['identity'].encode())[:8]
+    source = safe_path(root, case['sourceFile'])
+    expected = subprocess.check_output(['git', '-C', str(root), 'show', f"{revision}:{case['sourceFile']}"])
+    graph = {'files': [case['sourceFile']]}
+    diagnostic = None
+    command = None
+    try:
+        if revision != installation['projectRevision'] or source.read_bytes() != expected:
+            raise ValueError('Original target revision or bytes changed')
+        command = ['node', str(inspector), 'inspect-startup-closure', str(root), str(source)]
+        result = subprocess.run(command, capture_output=True, text=True, timeout=timeout, check=True)
+        graph = json.loads(result.stdout)
+        diagnostic = graph.get('diagnostic')
+    except (ValueError, OSError, subprocess.SubprocessError) as error:
+        diagnostic = str(error)
+        if isinstance(error, subprocess.CalledProcessError) and error.stderr:
+            diagnostic += '\n' + error.stderr
+        graph['reasonCode'] = 'STARTUP_GRAPH_FAILED'
+    inputs = {case['sourceFile']: digest(expected)}
+    resolution = graph.get('resolution', {})
+    inputs.update(resolution.get('inputSha256', {}))
+    for name in graph['files']:
+        inputs.setdefault(name, digest(safe_path(root, name).read_bytes()))
+    if inputs[case['sourceFile']] != digest(expected):
+        diagnostic = 'Original target hash differs from graph input'
+        graph['reasonCode'] = 'ORIGINAL_SOURCE_CHANGED'
+    snapshot = installation.get('snapshot', {}).get('inputSha256', {})
+    frozen_match = installation.get('phase') == 'FROZEN' and all(snapshot.get(name) == value for name, value in inputs.items())
+    original_match = False
+    if not frozen_match:
+        original_match = True
+        for name, value in inputs.items():
+            try:
+                original = subprocess.check_output(['git', '-C', str(root), 'show', f'{revision}:{name}'], stderr=subprocess.DEVNULL)
+                if digest(original) != value:
+                    original_match = False
+            except subprocess.CalledProcessError:
+                original_match = False
+            if not original_match:
+                break
+    inputs_proven = frozen_match or original_match
+    current_match = all(digest(safe_path(root, name).read_bytes()) == value for name, value in inputs.items())
+    complete = inputs_proven and current_match and not graph.get('reasonCode')
+    compiler = json.loads(resolution.get('tsconfig', '{}')).get('compilerOptions', {})
+    original_compiler = dict(compiler)
+    projection = None
+    if environment is not None:
+        compiler, projection = project_frontend_options(compiler, environment)
+    frontend_files = [materialized_name(name) for name in graph['files']]
+    paths = compiler.get('paths', {})
+    compiler['paths'] = {name: [materialized_name(target) for target in targets] for name, targets in paths.items()}
+    compiler.update({'types': [], 'noEmit': True})
+    if not inputs_proven and diagnostic is None:
+        diagnostic = 'Graph input is not covered by an immutable installation snapshot or original revision bytes'
+    evidence = {'schemaVersion': 1, 'classId': class_id, 'identity': case['identity'], 'graph': graph,
+                'installationComplete': installed, 'inputProof': 'installation-snapshot' if frozen_match else 'original-revision' if original_match else 'incomplete', 'installationDiagnostic': installation.get('diagnostic'), 'graphCommand': command, 'acquisitionComplete': complete, 'diagnostic': diagnostic,
+                'originalCompilerOptions': original_compiler, 'frontendCompilerProjection': projection,
+                'originalInputSha256': inputs, 'sourceMappings': {name: materialized_name(name) for name in graph['files']},
+                'toolProof': tool_proof, 'installationReceipt': str(receipt_path), 'installationSha256': digest(receipt_path.read_bytes())}
+    write_json(output / 'graphs' / f'{class_id}.json', evidence)
+    return {'case': case, 'classId': class_id, 'revision': revision, 'root': root, 'inputs': inputs,
+            'installation': installation, 'receiptPath': receipt_path, 'complete': complete, 'evidence': evidence,
+            'originalClassBytes': expected,
+            'frontendConfig': json.dumps({'compilerOptions': compiler, 'files': sorted(frontend_files)})}
+
+
+def freeze_case(result, output):
+    case = result['case']
+    project_root = safe_path(output / 'sources', case['projectId'])
+    mappings = result['evidence']['sourceMappings']
+    copied = {}
+    for name, expected in result['inputs'].items():
+        materialized = mappings.get(name, name)
+        target = safe_path(project_root, materialized)
+        data = safe_path(result['root'], name).read_bytes()
+        if name == case['sourceFile']:
+            data = result['originalClassBytes']
+        actual = digest(data)
+        if actual != expected:
+            result['complete'] = False
+            result['evidence']['diagnostic'] = 'Original frozen input changed before materialization'
+        if target.exists() and target.read_bytes() != data:
+            raise ValueError(f'Conflicting shared materialized input: {materialized}')
+        target.parent.mkdir(parents=True, exist_ok=True)
+        target.write_bytes(data)
+        copied[materialized] = actual
+    receipt_name = f"receipts/{result['classId']}.json"
+    receipt = {'schemaVersion': 1, 'projectRevision': result['revision'], 'sourceRoot': str(project_root),
+               'classes': [{key: case[key] for key in ['identity', 'sourceFile', 'className']}],
+               'originalClassSha256': {case['sourceFile']: digest(result['originalClassBytes'])},
+               'snapshot': {'inputSha256': copied}, 'acquisitionComplete': result['complete'],
+               'phase': 'GRAPH_FROZEN' if result['complete'] else 'ACQUISITION_INCOMPLETE',
+               'originalAcquisitionReceipt': str(result['receiptPath']),
+               'originalAcquisitionSha256': digest(result['receiptPath'].read_bytes()),
+               'inputProof': result['evidence']['inputProof'], 'nodeVersion': result['installation'].get('nodeVersion'),
+               'packageManager': result['installation'].get('packageManager'),
+               'installationDiagnostic': result['installation'].get('diagnostic'),
+               'originalInputSha256': result['inputs'], 'sourceMappings': mappings,
+               'runtimeBoundaries': result['evidence']['graph'].get('resolution', {}).get('runtimeBoundaries', []),
+               'initializationIssues': result['evidence']['graph'].get('initializationIssues', []),
+               'diagnostic': result['evidence']['diagnostic'],
+               'originalCompilerOptions': result['evidence']['originalCompilerOptions'],
+               'frontendCompilerProjection': result['evidence']['frontendCompilerProjection'],
+               'toolProof': result['evidence']['toolProof'],
+               'scope': 'Acquired graph evidence; symbolic support and actual class startup remain separate'}
+    receipt_path = output / receipt_name
+    write_json(receipt_path, receipt)
+    write_json(output / 'graphs' / f"{result['classId']}.json", result['evidence'])
+    return {'classId': result['classId'], 'identity': case['identity'], 'projectRevision': result['revision'],
+            'sourceRoot': str(project_root), 'sourceFile': case['sourceFile'], 'className': case['className'],
+            'inputSha256': copied, 'frontendConfig': result['frontendConfig'], 'acquisitionReceipt': receipt_name,
+            'acquisitionSha256': digest(receipt_path.read_bytes()), 'acquisitionComplete': result['complete']}
+
+
+def main():
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument('--ledger', type=Path, required=True)
+    parser.add_argument('--acquisition', type=Path, action='append', required=True)
+    parser.add_argument('--inspector', type=Path, required=True)
+    parser.add_argument('--output', type=Path, required=True)
+    parser.add_argument('--frontend-typescript', type=Path, required=True)
+    parser.add_argument('--tool-revision', required=True)
+    parser.add_argument('--native-frontend-revision', required=True)
+    parser.add_argument('--jobs', type=int, default=3)
+    parser.add_argument('--graph-timeout-seconds', type=int, default=90)
+    parser.add_argument('--budget-millis', type=int, default=2000)
+    parser.add_argument('--solver-limit-millis', type=int, default=250)
+    parser.add_argument('--collected-states-limit', type=int, default=10)
+    parser.add_argument('--seed', type=int, default=17)
+    parser.add_argument('--profile', default='FROZEN_STOP')
+    args = parser.parse_args()
+    if args.jobs < 1 or args.graph_timeout_seconds < 1 or not re.fullmatch(r'[0-9a-f]{40}', args.tool_revision):
+        parser.error('Positive jobs/timeout and an exact tool revision are required')
+    ledger_bytes = args.ledger.read_bytes()
+    cases = json.loads(ledger_bytes)['decisions']
+    if len({case['identity'] for case in cases}) != len(cases):
+        parser.error('Original class identities must be unique')
+    output = args.output.resolve()
+    output.mkdir(parents=True, exist_ok=False)
+    receipts = {}
+    for case in cases:
+        candidates = [attempt.resolve() / case['projectId'] / 'acquisition.json' for attempt in args.acquisition]
+        available = [candidate for candidate in candidates if candidate.is_file()]
+        if not available:
+            parser.error(f"Missing acquisition receipt for original project {case['projectId']}")
+        receipts[case['projectId']] = next((candidate for candidate in available
+            if json.loads(candidate.read_bytes()).get('phase') == 'FROZEN'), available[0])
+    environment = frontend_environment(args.frontend_typescript.resolve())
+    write_json(output / 'frontend-environment.json', environment)
+    module_names = ['source-inspector-cli.js', 'local-source-closure.js', 'module-initialization.js',
+                    'frozen-module-resolution.js', 'startup-runtime-resolution.js']
+    tool_proof = {'sourcePipelineRevision': args.tool_revision, 'nativeFrontendRevision': args.native_frontend_revision,
+                  'nodeVersion': subprocess.check_output(['node', '--version'], text=True).strip(),
+                  'generatorSha256': digest(Path(__file__).read_bytes()),
+                  'inspectorInputSha256': {name: digest((args.inspector.parent / name).read_bytes()) for name in module_names},
+                  'inspectorTypeScript': frontend_environment(args.inspector.parent.parent.parent / 'node_modules' / 'typescript')}
+    write_json(output / 'tool-proof.json', tool_proof)
+    results = []
+    with concurrent.futures.ThreadPoolExecutor(max_workers=args.jobs) as pool:
+        futures = [pool.submit(inspect_case, case, receipts[case['projectId']], args.inspector.resolve(),
+                               output, args.graph_timeout_seconds, environment, tool_proof) for case in cases]
+        for future in concurrent.futures.as_completed(futures):
+            result = future.result()
+            results.append(result)
+            print(json.dumps({'classId': result['classId'], 'acquisitionComplete': result['complete'],
+                              'diagnostic': result['evidence']['diagnostic']}), flush=True)
+    rows = [freeze_case(result, output) for result in sorted(results, key=lambda item: item['case']['identity'])]
+    manifest = {'schemaVersion': 1, 'toolRevision': args.tool_revision,
+                'nativeFrontendRevision': args.native_frontend_revision, 'ledgerSha256': digest(ledger_bytes),
+                'expectedClassCount': len(cases), 'classes': rows, 'budgetMillis': args.budget_millis,
+                'solverLimitMillis': args.solver_limit_millis, 'collectedStatesLimit': args.collected_states_limit,
+                'seed': args.seed, 'profile': args.profile}
+    write_json(output / 'manifest.json', manifest)
+    print(json.dumps({'manifest': str(output / 'manifest.json'), 'classes': len(rows),
+                      'acquisitionComplete': sum(row['acquisitionComplete'] for row in rows)}), flush=True)
+    return 0
+
+
+if __name__ == '__main__':
+    raise SystemExit(main())
diff --git a/usvm-ts-calls/scripts/test_freeze_class_startup_inputs.py b/usvm-ts-calls/scripts/test_freeze_class_startup_inputs.py
new file mode 100644
index 0000000000..f8a94f65c8
--- /dev/null
+++ b/usvm-ts-calls/scripts/test_freeze_class_startup_inputs.py
@@ -0,0 +1,176 @@
+import importlib.util
+import json
+from pathlib import Path
+import subprocess
+import tempfile
+import unittest
+
+MODULE = Path(__file__).with_name('freeze-class-startup-inputs.py')
+SPEC = importlib.util.spec_from_file_location('startup_freeze', MODULE)
+freeze = importlib.util.module_from_spec(SPEC)
+SPEC.loader.exec_module(freeze)
+INSPECTOR = Path(__file__).parents[2] / 'usvm-ts-fast-check/fast-check-adapter/dist/src/source-inspector-cli.js'
+
+
+def original_project(directory):
+    root = directory / 'original'
+    files = {'Entry.ts': "import { value } from 'example'; export class Entry { read() { return value; } }",
+             'tsconfig.json': '{"compilerOptions":{"strict":true}}',
+             'package.json': '{"name":"fixture","version":"1.0.0"}',
+             'package-lock.json': '{"lockfileVersion":3}',
+             'node_modules/example/package.json': '{"name":"example","main":"./runtime.js","types":"./types.d.ts"}',
+             'node_modules/example/runtime.js': "const data = require('./data.json'); exports.value = data.answer;",
+             'node_modules/example/data.json': '{"answer":42}',
+             'node_modules/example/types.d.ts': 'export declare const value: 1;'}
+    for name, text in files.items():
+        file = root / name
+        file.parent.mkdir(parents=True, exist_ok=True)
+        file.write_text(text)
+    subprocess.run(['git', 'init', '--quiet', str(root)], check=True)
+    subprocess.run(['git', '-C', str(root), 'add', '--', 'Entry.ts', 'tsconfig.json', 'package.json', 'package-lock.json'], check=True)
+    subprocess.run(['git', '-C', str(root), '-c', 'user.name=Startup Test', '-c', 'user.email=test@example.invalid',
+                    '-c', 'core.hooksPath=/dev/null', '-c', 'commit.gpgsign=false', 'commit', '--quiet', '-m', 'Freeze fixture'], check=True)
+    revision = subprocess.check_output(['git', '-C', str(root), 'rev-parse', 'HEAD'], text=True).strip()
+    case = {'projectId': 'example--fixture', 'sourceFile': 'Entry.ts', 'className': 'Entry',
+            'identity': f'example--fixture@{revision}:Entry.ts#Entry'}
+    receipt = {'projectRevision': revision, 'sourceRoot': str(root), 'originalSourceRoot': str(root),
+               'phase': 'FROZEN', 'dependenciesInstalled': True, 'classes': [case],
+               'snapshot': {'inputSha256': {name: freeze.digest(text.encode()) for name, text in files.items()}}}
+    receipt_path = directory / 'acquisition.json'
+    freeze.write_json(receipt_path, receipt)
+    return root, case, receipt_path, files
+
+
+class StartupFreezeTest(unittest.TestCase):
+    def test_actual_graph_materialization_preserves_original_bytes_and_narrow_roots(self):
+        with tempfile.TemporaryDirectory(prefix='calls-startup-freeze-') as temporary:
+            directory = Path(temporary).resolve()
+            root, case, receipt, files = original_project(directory)
+            output = directory / 'output'
+
+            inspected = freeze.inspect_case(case, receipt, INSPECTOR, output, timeout=30)
+            row = freeze.freeze_case(inspected, output)
+            graph_receipt = json.loads((output / row['acquisitionReceipt']).read_bytes())
+            config = json.loads(row['frontendConfig'])
+
+            self.assertTrue(row['acquisitionComplete'])
+            self.assertEqual(files['Entry.ts'].encode(), (Path(row['sourceRoot']) / 'Entry.ts').read_bytes())
+            self.assertIn('.usvm-installed/example/runtime.js', config['files'])
+            self.assertTrue(all('node_modules' not in file for file in config['files']))
+            self.assertNotIn('.usvm-installed/example/types.d.ts', config['files'])
+            self.assertEqual('json', graph_receipt['runtimeBoundaries'][0]['kind'])
+            self.assertEqual(freeze.digest(receipt.read_bytes()), graph_receipt['originalAcquisitionSha256'])
+            self.assertNotIn('strictBuiltinIteratorReturn', config['compilerOptions'])
+            self.assertEqual(files['Entry.ts'], (root / 'Entry.ts').read_text())
+
+    def test_changed_runtime_bytes_cannot_upgrade_frozen_installation_to_complete_graph(self):
+        with tempfile.TemporaryDirectory(prefix='calls-startup-change-') as temporary:
+            directory = Path(temporary).resolve()
+            root, case, receipt, _ = original_project(directory)
+            (root / 'node_modules/example/runtime.js').write_text('exports.value = 99;')
+
+            inspected = freeze.inspect_case(case, receipt, INSPECTOR, directory / 'output', timeout=30)
+            row = freeze.freeze_case(inspected, directory / 'output')
+
+            self.assertFalse(row['acquisitionComplete'])
+            self.assertIn('not covered', inspected['evidence']['diagnostic'])
+
+    def test_irrelevant_failed_dev_dependency_install_does_not_veto_original_source_graph(self):
+        with tempfile.TemporaryDirectory(prefix='calls-startup-local-') as temporary:
+            directory = Path(temporary).resolve()
+            root, case, receipt_path, _ = original_project(directory)
+            (root / 'Entry.ts').write_text('export class Entry { read() { return 42; } }')
+            subprocess.run(['git', '-C', str(root), 'add', '--', 'Entry.ts'], check=True)
+            subprocess.run(['git', '-C', str(root), '-c', 'user.name=Startup Test', '-c', 'user.email=test@example.invalid',
+                            '-c', 'core.hooksPath=/dev/null', '-c', 'commit.gpgsign=false', 'commit', '--quiet', '-m', 'Use local graph'], check=True)
+            revision = subprocess.check_output(['git', '-C', str(root), 'rev-parse', 'HEAD'], text=True).strip()
+            case['identity'] = f'example--fixture@{revision}:Entry.ts#Entry'
+            receipt = json.loads(receipt_path.read_bytes())
+            receipt.update({'phase': 'FAILED', 'diagnostic': 'Unneeded devDependency quarantined', 'projectRevision': revision})
+            freeze.write_json(receipt_path, receipt)
+
+            inspected = freeze.inspect_case(case, receipt_path, INSPECTOR, directory / 'output', timeout=30)
+            row = freeze.freeze_case(inspected, directory / 'output')
+
+            self.assertTrue(row['acquisitionComplete'])
+            self.assertEqual('original-revision', inspected['evidence']['inputProof'])
+            self.assertEqual('Unneeded devDependency quarantined', inspected['evidence']['installationDiagnostic'])
+
+    def test_type_environment_projection_is_explicit_and_keeps_semantic_options(self):
+        original = {'strict': True, 'noUncheckedSideEffectImports': True, 'lib': ['es2024', 'dom'],
+                    'useDefineForClassFields': False, 'newSemanticOption': True}
+        environment = {'version': '5.4.5', 'options': ['strict', 'lib', 'useDefineForClassFields'],
+                       'libs': ['es2023', 'esnext', 'dom']}
+
+        projected, evidence = freeze.project_frontend_options(original, environment)
+
+        self.assertEqual(['esnext', 'dom'], projected['lib'])
+        self.assertNotIn('noUncheckedSideEffectImports', projected)
+        self.assertFalse(projected['useDefineForClassFields'])
+        self.assertTrue(projected['newSemanticOption'])
+        self.assertEqual(['newSemanticOption'], evidence['unprojectedUnsupportedOptions'])
+        self.assertEqual(2, len(evidence['boundaries']))
+        self.assertTrue(original['noUncheckedSideEffectImports'])
+        self.assertEqual(['es2024', 'dom'], original['lib'])
+
+    def test_frontend_reports_node20_and_rewrite_option_without_changing_them(self):
+        original = {'module': 'node20', 'moduleResolution': 'nodenext', 'noEmit': True,
+                    'rewriteRelativeImportExtensions': True}
+        environment = {'version': '5.4.5', 'options': ['module', 'moduleResolution', 'noEmit'], 'libs': [],
+                       'enumOptions': {'module': ['commonjs', 'node16', 'nodenext', 'preserve'],
+                                       'moduleResolution': ['node16', 'nodenext']}}
+
+        projected, evidence = freeze.project_frontend_options(original, environment)
+
+        self.assertEqual(original, projected)
+        self.assertEqual('UNSUPPORTED', evidence['status'])
+        unsupported = {item['option']: item for item in evidence['unsupportedCompatibilityBoundaries']}
+        self.assertEqual({'module', 'rewriteRelativeImportExtensions'}, set(unsupported))
+        self.assertEqual('option-value', unsupported['module']['kind'])
+        self.assertEqual('node20', unsupported['module']['original'])
+        self.assertEqual('option-name', unsupported['rewriteRelativeImportExtensions']['kind'])
+        self.assertTrue(unsupported['rewriteRelativeImportExtensions']['original'])
+        self.assertTrue(all(item['reasonCode'] == 'FRONTEND_COMPILER_OPTION_UNSUPPORTED'
+                            for item in unsupported.values()))
+
+    def test_frontend_accepts_supported_enum_values_case_insensitively(self):
+        original = {'module': 'ESNext', 'moduleResolution': 'NodeNext', 'noEmit': True}
+        environment = {'version': '5.4.5', 'options': ['module', 'moduleResolution', 'noEmit'], 'libs': [],
+                       'enumOptions': {'module': ['commonjs', 'esnext', 'nodenext'],
+                                       'moduleResolution': ['node16', 'nodenext']}}
+
+        projected, evidence = freeze.project_frontend_options(original, environment)
+
+        self.assertEqual(original, projected)
+        self.assertEqual('COMPATIBLE', evidence['status'])
+        self.assertEqual([], evidence['unsupportedCompatibilityBoundaries'])
+
+    def test_frontend_inventory_records_actual_compiler_enum_values(self):
+        compiler = INSPECTOR.parents[2] / 'node_modules' / 'typescript'
+
+        environment = freeze.frontend_environment(compiler)
+
+        self.assertIn('module', environment['options'])
+        self.assertIn('commonjs', environment['enumOptions']['module'])
+        self.assertIn('nodenext', environment['enumOptions']['moduleResolution'])
+        self.assertEqual(freeze.digest((compiler / 'lib' / 'typescript.js').read_bytes()),
+                         environment['compilerSha256'])
+
+    def test_failed_installation_remains_explicit_incomplete_row(self):
+        with tempfile.TemporaryDirectory(prefix='calls-startup-failure-') as temporary:
+            directory = Path(temporary).resolve()
+            _, case, receipt_path, _ = original_project(directory)
+            receipt = json.loads(receipt_path.read_bytes())
+            receipt.update({'phase': 'FAILED', 'diagnostic': 'Locked installation failed'})
+            freeze.write_json(receipt_path, receipt)
+
+            inspected = freeze.inspect_case(case, receipt_path, INSPECTOR, directory / 'output', timeout=30)
+            row = freeze.freeze_case(inspected, directory / 'output')
+
+            self.assertFalse(row['acquisitionComplete'])
+            self.assertEqual(case['identity'], row['identity'])
+            self.assertEqual('Locked installation failed', inspected['evidence']['installationDiagnostic'])
+
+
+if __name__ == '__main__':
+    unittest.main()
diff --git a/usvm-ts-fast-check/fast-check-adapter/src/frozen-module-resolution.ts b/usvm-ts-fast-check/fast-check-adapter/src/frozen-module-resolution.ts
index 7a5eabb782..c4bc6deefa 100644
--- a/usvm-ts-fast-check/fast-check-adapter/src/frozen-module-resolution.ts
+++ b/usvm-ts-fast-check/fast-check-adapter/src/frozen-module-resolution.ts
@@ -2,10 +2,12 @@ import { createHash } from 'node:crypto'
 import { existsSync, readFileSync, realpathSync, statSync } from 'node:fs'
 import path from 'node:path'
 import ts from 'typescript'
+import { resolveStartupRuntime, type RuntimeImportKind, type StartupRuntimeBoundary, type StartupRuntimeResolution } from './startup-runtime-resolution.js'
 
 export interface FrozenModuleResolution {
   inputSha256: Record<string, string>
   tsconfig: string
+  runtimeBoundaries?: StartupRuntimeBoundary[]
 }
 
 /** A bounded, offline runtime source resolver. Declaration files never stand in for executable code. */
@@ -16,13 +18,15 @@ export class FrozenModuleResolver {
   private readonly aliases = new Map<string, string>()
   private readonly edges = new Map<string, Map<string, string>>()
   private readonly configStack = new Set<string>()
+  private usedStartupResolution = false
+  private readonly startupBoundaries = new Map<string, StartupRuntimeBoundary>()
   private pathsDirectory: string | undefined
   private readonly resolutionHost: ts.ModuleResolutionHost
 
   constructor(private readonly root: string, entry: string) {
     const preparedConfig = path.join(root, '.usvm-frozen.tsconfig.json')
     const config = existsSync(preparedConfig) ? preparedConfig
-      : this.ancestors(path.dirname(entry)).map(directory => path.join(directory, 'tsconfig.json')).find(existsSync)
+      : this.ancestors(path.dirname(entry)).flatMap(directory => ['tsconfig.json', 'tsconfig.jsonc'].map(name => path.join(directory, name))).find(existsSync)
     this.rawOptions = config ? this.readConfig(config) : {
       target: 'ES2022', module: 'ESNext', moduleResolution: 'Node10', allowImportingTsExtensions: true,
     }
@@ -100,13 +104,45 @@ export class FrozenModuleResolver {
     return target
   }
 
+  resolveStartup(specifier: string, from: string, importKind: RuntimeImportKind = 'import'): StartupRuntimeResolution {
+    this.usedStartupResolution = true
+    const result = resolveStartupRuntime(this.root, this.options, specifier, from, importKind,
+      file => this.inputs.add(this.checkedPath(file)))
+    if (result.kind === 'boundary') {
+      this.startupBoundaries.set(`${from}\0${specifier}\0${importKind}`, result.boundary)
+      if (result.boundary.runtimeFile) this.recordMetadata(path.join(this.root, result.boundary.runtimeFile))
+      return result
+    }
+    const target = result.file
+    this.recordMetadata(target)
+    const bindings = this.edges.get(from) ?? new Map<string, string>()
+    bindings.set(specifier, target)
+    this.edges.set(from, bindings)
+    if (!specifier.startsWith('.')) {
+      const previous = this.aliases.get(specifier)
+      if (previous && previous !== target) throw new Error(`Context-dependent runtime alias is unsupported: ${specifier}`)
+      this.aliases.set(specifier, target)
+    }
+    return result
+  }
+
+  recordDynamicStartupBoundary(from: string, importKind: RuntimeImportKind, startOffset: number, expression: string): void {
+    const source = this.checkedPath(from)
+    this.usedStartupResolution = true
+    this.inputs.add(source)
+    this.startupBoundaries.set(`${source}\0dynamic\0${startOffset}`, {
+      sourceFile: path.relative(this.root, source).split(path.sep).join('/'),
+      specifier: '<unresolved dynamic target>', importKind, kind: 'dynamic-module', startOffset, expression,
+    })
+  }
+
   resolvedModule(specifier: string, from: string): ts.ResolvedModule | undefined {
     const target = this.edges.get(from)?.get(specifier)
     return target ? { resolvedFileName: target, isExternalLibraryImport: false } : undefined
   }
 
   freeze(files: string[]): FrozenModuleResolution | undefined {
-    if (this.inputs.size === 0 && this.aliases.size === 0) return undefined
+    if (this.inputs.size === 0 && this.aliases.size === 0 && this.startupBoundaries.size === 0) return undefined
     const allInputs = [...new Set([...this.inputs, ...files.map(file => path.join(this.root, file))])].sort()
     const inputSha256 = Object.fromEntries(allInputs.map(file => [
       path.relative(this.root, file).split(path.sep).join('/'),
@@ -114,11 +150,13 @@ export class FrozenModuleResolver {
     ]))
     const paths = Object.fromEntries([...this.aliases].sort(([a], [b]) => a.localeCompare(b)).map(([specifier, target]) =>
       [specifier, [path.relative(this.root, target).split(path.sep).join('/')]]))
-    const compilerOptions = { ...this.rawOptions, baseUrl: '.', paths,
+    const compilerOptions = { ...this.rawOptions, ...(this.usedStartupResolution ? { allowJs: true } : {}), baseUrl: '.', paths,
       types: [], noEmit: true, allowImportingTsExtensions: true }
     // This config deliberately roots only the inspected runtime closure; inherited include/exclude
     // cannot add unrelated project files to the coverage frontend.
-    return { inputSha256, tsconfig: JSON.stringify({ compilerOptions, files }, null, 2) + '\n' }
+    const resolution: FrozenModuleResolution = { inputSha256, tsconfig: JSON.stringify({ compilerOptions, files }, null, 2) + '\n' }
+    if (this.startupBoundaries.size > 0) resolution.runtimeBoundaries = [...this.startupBoundaries.values()]
+    return resolution
   }
 
   private resolvePackage(specifier: string, from: string): string | undefined {
diff --git a/usvm-ts-fast-check/fast-check-adapter/src/local-source-closure.ts b/usvm-ts-fast-check/fast-check-adapter/src/local-source-closure.ts
index 2aa6525024..84a5f1fd95 100644
--- a/usvm-ts-fast-check/fast-check-adapter/src/local-source-closure.ts
+++ b/usvm-ts-fast-check/fast-check-adapter/src/local-source-closure.ts
@@ -1,6 +1,7 @@
 import { readFileSync, realpathSync } from 'node:fs'
 import path from 'node:path'
 import ts from 'typescript'
+import { type RuntimeImportKind } from './startup-runtime-resolution.js'
 import { FrozenModuleResolver, type FrozenModuleResolution } from './frozen-module-resolution.js'
 import { unsupportedModuleInitialization } from './module-initialization.js'
 
@@ -39,9 +40,16 @@ function inspectSourceClosure(rootPath: string, entryPath: string, mode: 'checke
   const sources = new Map<string, ts.SourceFile>()
   const dependencies = new Map<string, string[]>()
 
-  const reject = (reasonCode: string, diagnostic: string): LocalSourceClosure => ({
-    files: [...files].sort(), reasonCode, diagnostic,
-  })
+  const reject = (reasonCode: string, diagnostic: string): LocalSourceClosure => {
+    const knownFiles = [...files].sort()
+    const result: LocalSourceClosure = { files: knownFiles, reasonCode, diagnostic }
+    if (mode === 'startup') {
+      const resolution = resolver.freeze(knownFiles)
+      if (resolution) result.resolution = resolution
+      result.initializationIssues = initializationIssues
+    }
+    return result
+  }
 
   while (pending.length > 0) {
     const file = pending.shift()!
@@ -58,7 +66,7 @@ function inspectSourceClosure(rootPath: string, entryPath: string, mode: 'checke
     const emittedModules = runtimeModuleSpecifiers(source, resolver.options)
     const edges: string[] = []
     dependencies.set(file, edges)
-    const imports: string[] = []
+    const imports: Array<{ specifier: string, importKind: RuntimeImportKind }> = []
     const ranges: Array<{ start: number, end: number }> = []
     runtimeImportRanges.set(file, ranges)
     for (const statement of source.statements) {
@@ -73,7 +81,7 @@ function inspectSourceClosure(rootPath: string, entryPath: string, mode: 'checke
         }
         if (!emittedModules.has(statement.moduleSpecifier.text)
           && importedBindingsUsedOnlyAsTypes(statement, source)) continue
-        imports.push(statement.moduleSpecifier.text)
+        imports.push({ specifier: statement.moduleSpecifier.text, importKind: 'import' })
         ranges.push({ start: statement.getStart(source), end: statement.end })
       } else if (ts.isExportDeclaration(statement)) {
         if (statement.isTypeOnly) continue
@@ -87,7 +95,7 @@ function inspectSourceClosure(rootPath: string, entryPath: string, mode: 'checke
           if (!ts.isStringLiteral(statement.moduleSpecifier)) {
             return reject('IMPORTED_CALLEES_UNSUPPORTED', `Nonliteral re-export in ${relative}`)
           }
-          imports.push(statement.moduleSpecifier.text)
+          imports.push({ specifier: statement.moduleSpecifier.text, importKind: 'import' })
         }
       } else if (ts.isImportEqualsDeclaration(statement)) {
         if (!statement.isTypeOnly) {
@@ -107,16 +115,35 @@ function inspectSourceClosure(rootPath: string, entryPath: string, mode: 'checke
 
     let dynamicImport = false
     const visit = (node: ts.Node): void => {
-      if (ts.isCallExpression(node) && (node.expression.kind === ts.SyntaxKind.ImportKeyword
-        || ts.isIdentifier(node.expression) && node.expression.text === 'require')) dynamicImport = true
+      if (ts.isCallExpression(node)) {
+        const requireCall = ts.isIdentifier(node.expression) && node.expression.text === 'require'
+        const literalRequire = requireCall && node.arguments.length === 1 && ts.isStringLiteral(node.arguments[0]!)
+        if (mode === 'startup' && literalRequire) {
+          imports.push({ specifier: (node.arguments[0] as ts.StringLiteral).text, importKind: 'require' })
+          ranges.push({ start: node.getStart(source), end: node.end })
+        } else if (node.expression.kind === ts.SyntaxKind.ImportKeyword || requireCall) {
+          if (mode === 'startup') {
+            const startOffset = node.getStart(source)
+            const importKind = requireCall ? 'require' : 'import'
+            resolver.recordDynamicStartupBoundary(file, importKind, startOffset, node.getText(source))
+            initializationIssues.push({ sourceFile: relative, startOffset,
+              diagnostic: `Unresolved dynamic runtime module boundary in ${relative} at offset ${startOffset}` })
+          } else dynamicImport = true
+        }
+      }
       ts.forEachChild(node, visit)
     }
     visit(source)
     if (dynamicImport) return reject('IMPORTED_CALLEES_UNSUPPORTED', `Dynamic import or require in ${relative}`)
 
-    for (const specifier of imports) {
+    for (const imported of imports) {
       try {
-        const target = resolver.resolve(specifier, file)
+        let target: string
+        if (mode === 'startup') {
+          const resolved = resolver.resolveStartup(imported.specifier, file, imported.importKind)
+          if (resolved.kind === 'boundary') continue
+          target = resolved.file
+        } else target = resolver.resolve(imported.specifier, file)
         pending.push(target)
         edges.push(target)
       } catch (error) {
@@ -132,7 +159,8 @@ function inspectSourceClosure(rootPath: string, entryPath: string, mode: 'checke
   // Ask TypeScript to validate the imported bindings as well as the files. Diagnostics
   // in unrelated function bodies do not determine closure admission.
   if (mode === 'startup' || files.size > 1 || [...runtimeImportRanges.values()].some(ranges => ranges.length > 0)) {
-    const options: ts.CompilerOptions = { ...resolver.options, noLib: true, noEmit: true, types: [] }
+    const options: ts.CompilerOptions = { ...resolver.options, ...(mode === 'startup' ? { allowJs: true } : {}),
+      noLib: true, noEmit: true, types: [] }
     const host = ts.createCompilerHost(options)
     const directories = new Set<string>()
     for (const file of sources.keys()) {
@@ -158,7 +186,15 @@ function inspectSourceClosure(rootPath: string, entryPath: string, mode: 'checke
       const closure = new Set(sources.values())
       const evaluationOrder = moduleEvaluationOrder(dependencies, entry)
       for (const source of closure) {
-        const unsupported = unsupportedModuleInitialization(source, checker, closure, evaluationOrder)
+        let unsupported: ts.Node | undefined
+        try {
+          unsupported = unsupportedModuleInitialization(source, checker, closure, evaluationOrder)
+        } catch (error) {
+          const diagnostic = `Initialization inspection failed in ${path.relative(root, source.fileName)}: ${String(error)}`
+          if (mode === 'checked') return reject('TOP_LEVEL_INITIALIZATION_UNSUPPORTED', diagnostic)
+          initializationIssues.push({ sourceFile: path.relative(root, source.fileName), startOffset: source.getStart(source), diagnostic })
+          continue
+        }
         if (unsupported !== undefined) {
           const sourceFile = path.relative(root, source.fileName)
           const startOffset = unsupported.getStart(source)
@@ -172,12 +208,21 @@ function inspectSourceClosure(rootPath: string, entryPath: string, mode: 'checke
     for (const [file, ranges] of runtimeImportRanges) {
       if (ranges.length === 0) continue
       const source = program.getSourceFile(file)!
-      const invalidImport = program.getSemanticDiagnostics(source).find(diagnostic =>
-        diagnostic.category === ts.DiagnosticCategory.Error && diagnostic.start !== undefined
-        && ranges.some(range => diagnostic.start! >= range.start && diagnostic.start! < range.end))
+      let invalidImport: ts.Diagnostic | undefined
+      try {
+        invalidImport = program.getSemanticDiagnostics(source).find(diagnostic =>
+          diagnostic.category === ts.DiagnosticCategory.Error && diagnostic.start !== undefined
+          && ranges.some(range => diagnostic.start! >= range.start && diagnostic.start! < range.end))
+      } catch (error) {
+        const diagnostic = `Binding inspection failed in ${path.relative(root, file)}: ${String(error)}`
+        if (mode === 'checked') return reject('IMPORTED_CALLEES_UNSUPPORTED', diagnostic)
+        initializationIssues.push({ sourceFile: path.relative(root, file), startOffset: source.getStart(source), diagnostic })
+        continue
+      }
       if (invalidImport) {
-        return reject('IMPORTED_CALLEES_UNSUPPORTED',
-          `${path.relative(root, file)}: ${ts.flattenDiagnosticMessageText(invalidImport.messageText, '\n')}`)
+        const diagnostic = `${path.relative(root, file)}: ${ts.flattenDiagnosticMessageText(invalidImport.messageText, '\n')}`
+        if (mode === 'checked') return reject('IMPORTED_CALLEES_UNSUPPORTED', diagnostic)
+        initializationIssues.push({ sourceFile: path.relative(root, file), startOffset: invalidImport.start!, diagnostic })
       }
     }
   }
@@ -193,7 +238,8 @@ function runtimeModuleSpecifiers(source: ts.SourceFile, options: ts.CompilerOpti
   const emitted = ts.transpileModule(source.text, {
     fileName: source.fileName,
     compilerOptions: { ...options, target: ts.ScriptTarget.ES2022, module: ts.ModuleKind.ESNext,
-      noEmit: false, emitDeclarationOnly: false, declaration: false },
+      noEmit: false, emitDeclarationOnly: false, declaration: false, declarationMap: false,
+      composite: false, incremental: false, isolatedDeclarations: false },
   }).outputText
   const javascript = ts.createSourceFile(`${source.fileName}.js`, emitted, ts.ScriptTarget.ES2022, true, ts.ScriptKind.JS)
   const specifiers = new Set<string>()
diff --git a/usvm-ts-fast-check/fast-check-adapter/src/startup-runtime-resolution.ts b/usvm-ts-fast-check/fast-check-adapter/src/startup-runtime-resolution.ts
new file mode 100644
index 0000000000..0a4350c5c2
--- /dev/null
+++ b/usvm-ts-fast-check/fast-check-adapter/src/startup-runtime-resolution.ts
@@ -0,0 +1,166 @@
+import { existsSync, readFileSync, realpathSync, statSync } from 'node:fs'
+import { isBuiltin } from 'node:module'
+import path from 'node:path'
+import ts from 'typescript'
+
+export type RuntimeImportKind = 'import' | 'require'
+export interface StartupRuntimeBoundary {
+  sourceFile: string
+  specifier: string
+  importKind: RuntimeImportKind
+  kind: 'node-builtin' | 'json' | 'dynamic-module'
+  startOffset?: number
+  expression?: string
+  runtimeFile?: string
+}
+export type StartupRuntimeResolution = { kind: 'source', file: string }
+  | { kind: 'boundary', boundary: StartupRuntimeBoundary }
+
+/** Actual acquired runtime bytes and explicit boundaries, without an engine-support claim. */
+export function resolveStartupRuntime(
+  root: string, options: ts.CompilerOptions, specifier: string, from: string,
+  importKind: RuntimeImportKind, recordInput: (file: string) => void,
+): StartupRuntimeResolution {
+  const relative = (file: string): string => path.relative(root, file).split(path.sep).join('/')
+  const inside = (file: string): boolean => {
+    const name = path.relative(root, path.resolve(file))
+    return name === '' || name !== '..' && !name.startsWith(`..${path.sep}`) && !path.isAbsolute(name)
+  }
+  const available = (file: string): boolean => inside(file) && existsSync(file) && inside(realpathSync(file))
+  const checked = (file: string): string => {
+    if (!available(file)) throw new Error(`Runtime module missing or outside frozen root: ${file}`)
+    return realpathSync(file)
+  }
+  const readPackage = (file: string): Record<string, unknown> => {
+    const canonical = checked(file)
+    recordInput(canonical)
+    return JSON.parse(readFileSync(canonical, 'utf8')) as Record<string, unknown>
+  }
+  const condition = (value: unknown): unknown => {
+    if (typeof value === 'string') return value
+    if (!value || typeof value !== 'object' || Array.isArray(value)) return undefined
+    for (const [name, entry] of Object.entries(value)) {
+      if (name !== importKind && name !== 'node' && name !== 'default') continue
+      const selected = condition(entry)
+      if (selected !== undefined) return selected
+    }
+    return undefined
+  }
+  const selectSubpath = (value: unknown, key: string): unknown => {
+    if (!value || typeof value !== 'object' || Array.isArray(value)) return key === '.' ? value : undefined
+    const entries = value as Record<string, unknown>
+    if (!Object.keys(entries).some(name => name.startsWith('.'))) return key === '.' ? value : undefined
+    if (Object.hasOwn(entries, key)) return entries[key]
+    const patterns = Object.keys(entries).filter(name => name.includes('*')).sort((a, b) =>
+      b.indexOf('*') - a.indexOf('*') || b.length - a.length)
+    for (const pattern of patterns) {
+      const [before, after] = pattern.split('*')
+      if (pattern.split('*').length !== 2 || !key.startsWith(before!) || !key.endsWith(after!)) continue
+      const wildcard = key.slice(before!.length, key.length - after!.length)
+      const replace = (entry: unknown): unknown => typeof entry === 'string' ? entry.replaceAll('*', wildcard)
+        : entry && typeof entry === 'object' && !Array.isArray(entry)
+          ? Object.fromEntries(Object.entries(entry).map(([name, nested]) => [name, replace(nested)])) : entry
+      return replace(entries[pattern])
+    }
+    return undefined
+  }
+  const resolveFile = (candidate: string, seen = new Set<string>()): string | undefined => {
+    if (!inside(candidate) || seen.has(candidate)) return undefined
+    seen.add(candidate)
+    if (available(candidate) && statSync(candidate).isFile()) return checked(candidate)
+    const suffix = path.extname(candidate)
+    const sourceFallback = suffix === '.js' ? candidate.slice(0, -3) + '.ts'
+      : suffix === '.mjs' ? candidate.slice(0, -4) + '.mts'
+        : suffix === '.cjs' ? candidate.slice(0, -4) + '.cts' : undefined
+    if (sourceFallback && available(sourceFallback)) return checked(sourceFallback)
+    if (!['.ts', '.tsx', '.mts', '.cts', '.js', '.jsx', '.mjs', '.cjs'].includes(suffix)) {
+      const candidates = ['.ts', '.tsx', '.mts', '.cts', '.js', '.jsx', '.mjs', '.cjs']
+        .map(extension => candidate + extension).filter(available)
+      const installedRuntime = path.relative(root, candidate).split(path.sep).includes('node_modules')
+      const javascript = candidates.find(file => /\.[cm]?js$/.test(file))
+      if (installedRuntime && javascript) return checked(javascript)
+      if (candidates.length > 1) throw new Error(`Ambiguous extensionless runtime module: ${candidate}`)
+      if (candidates.length === 1) return checked(candidates[0]!)
+    }
+    if (available(candidate) && statSync(candidate).isDirectory()) {
+      const metadata = path.join(candidate, 'package.json')
+      if (available(metadata)) {
+        const pkg = readPackage(metadata)
+        if (typeof pkg.main === 'string') {
+          const target = resolveFile(path.resolve(candidate, pkg.main), seen)
+          if (target) return target
+        }
+      }
+      return resolveFile(path.join(candidate, 'index'), seen)
+    }
+    return undefined
+  }
+
+  from = checked(from)
+  if (isBuiltin(specifier)) {
+    return { kind: 'boundary', boundary: { sourceFile: relative(from), specifier, importKind, kind: 'node-builtin' } }
+  }
+
+  let target: string | undefined
+  if (specifier.startsWith('.')) {
+    target = resolveFile(path.resolve(path.dirname(from), specifier))
+  } else {
+    // Config aliases take precedence. Package metadata must choose runtime rather than declaration files.
+    const host: ts.ModuleResolutionHost = {
+      getCurrentDirectory: () => root,
+      fileExists: file => path.basename(file) !== 'package.json' && !/\.d\.[cm]?ts$/.test(file)
+        && available(file) && statSync(file).isFile(),
+      readFile: () => undefined,
+      directoryExists: file => available(file) && statSync(file).isDirectory(),
+      realpath: checked,
+    }
+    const alias = ts.resolveModuleName(specifier, from, { ...options, allowJs: true }, host).resolvedModule
+    if (alias && !alias.isExternalLibraryImport) target = alias.resolvedFileName
+    if (!target) {
+      const parts = specifier.split('/')
+      const packageName = specifier.startsWith('@') ? parts.slice(0, 2).join('/') : parts[0]!
+      const subpath = parts.slice(packageName.startsWith('@') ? 2 : 1).join('/')
+      let directory = path.dirname(from)
+      while (inside(directory) && !target) {
+        const own = path.join(directory, 'package.json')
+        const installed = path.join(directory, 'node_modules', packageName, 'package.json')
+        for (const metadata of [own, installed]) {
+          if (!available(metadata)) continue
+          const pkg = readPackage(metadata)
+          if (metadata === own && pkg.name !== packageName) continue
+          const packageRoot = path.dirname(checked(metadata))
+          const exported = pkg.exports === undefined ? undefined
+            : condition(selectSubpath(pkg.exports, subpath ? `./${subpath}` : '.'))
+          if (pkg.exports !== undefined && (typeof exported !== 'string' || !exported.startsWith('./'))) {
+            throw new Error(`No ${importKind} runtime package export for ${specifier}`)
+          }
+          const entry = exported ?? (subpath || pkg.main || 'index')
+          if (typeof entry !== 'string') throw new Error(`Invalid runtime package entry for ${specifier}`)
+          const candidate = path.resolve(packageRoot, entry)
+          const packageRelative = path.relative(packageRoot, candidate)
+          if (packageRelative === '..' || packageRelative.startsWith(`..${path.sep}`) || path.isAbsolute(packageRelative)) {
+            throw new Error(`Runtime package entry escapes its package: ${specifier}`)
+          }
+          const exactExportExists = available(candidate) && statSync(candidate).isFile()
+          target = exported !== undefined ? exactExportExists ? checked(candidate) : undefined : resolveFile(candidate)
+          if (!target) throw new Error(`Missing acquired ${importKind} runtime entry for ${specifier}`)
+          break
+        }
+        if (directory === root) break
+        directory = path.dirname(directory)
+      }
+    }
+  }
+  if (!target) throw new Error(`Unresolved acquired runtime module ${specifier} in ${relative(from)}`)
+  target = checked(target)
+  recordInput(target)
+  if (target.endsWith('.json')) {
+    JSON.parse(readFileSync(target, 'utf8'))
+    return { kind: 'boundary', boundary: { sourceFile: relative(from), specifier, importKind,
+      kind: 'json', runtimeFile: relative(target) } }
+  }
+  if (/\.d\.[cm]?ts$/.test(target) || !/\.[cm]?[jt]sx?$/.test(target)) {
+    throw new Error(`Acquired runtime module is declaration-only or unsupported: ${specifier} -> ${target}`)
+  }
+  return { kind: 'source', file: target }
+}
diff --git a/usvm-ts-fast-check/fast-check-adapter/test/startup-runtime-resolution.test.ts b/usvm-ts-fast-check/fast-check-adapter/test/startup-runtime-resolution.test.ts
new file mode 100644
index 0000000000..081fa7f01e
--- /dev/null
+++ b/usvm-ts-fast-check/fast-check-adapter/test/startup-runtime-resolution.test.ts
@@ -0,0 +1,177 @@
+import assert from 'node:assert/strict'
+import { createHash } from 'node:crypto'
+import { mkdirSync, mkdtempSync, realpathSync, rmSync, symlinkSync, writeFileSync } from 'node:fs'
+import { tmpdir } from 'node:os'
+import path from 'node:path'
+import test from 'node:test'
+import { inspectLocalSourceClosure, inspectStartupSourceClosure } from '../src/local-source-closure.js'
+import { FrozenModuleResolver } from '../src/frozen-module-resolution.js'
+
+function workspace(files: Record<string, string>, action: (root: string, entry: string) => void): void {
+  const root = realpathSync(mkdtempSync(path.join(tmpdir(), 'usvm-runtime-')))
+  try {
+    for (const [name, text] of Object.entries({ 'entry.ts': 'export class Entry {}', ...files })) {
+      const file = path.join(root, name)
+      mkdirSync(path.dirname(file), { recursive: true })
+      writeFileSync(file, text)
+    }
+    action(root, path.join(root, 'entry.ts'))
+  } finally {
+    rmSync(root, { recursive: true, force: true })
+  }
+}
+
+test('startup chooses actual package runtime rather than its declaration and checked mode still rejects it', () => {
+  workspace({
+    'node_modules/example/package.json': JSON.stringify({ name: 'example', types: './types.d.ts',
+      exports: { types: './types.d.ts', import: './runtime.mjs', require: './runtime.cjs' } }),
+    'node_modules/example/types.d.ts': 'export declare const value: 1;',
+    'node_modules/example/runtime.mjs': 'export const value = 2;',
+    'node_modules/example/runtime.cjs': 'exports.value = 3;',
+  }, (root, entry) => {
+    const imported = new FrozenModuleResolver(root, entry)
+    const required = new FrozenModuleResolver(root, entry)
+
+    assert.deepEqual(imported.resolveStartup('example', entry),
+      { kind: 'source', file: path.join(root, 'node_modules/example/runtime.mjs') })
+    assert.deepEqual(required.resolveStartup('example', entry, 'require'),
+      { kind: 'source', file: path.join(root, 'node_modules/example/runtime.cjs') })
+    assert.throws(() => imported.resolve('example', entry), /Split import\/require/)
+    const frozen = imported.freeze(['entry.ts', 'node_modules/example/runtime.mjs'])!
+    assert.ok(frozen.inputSha256['node_modules/example/package.json'])
+    assert.equal(frozen.inputSha256['node_modules/example/runtime.mjs'],
+      createHash('sha256').update('export const value = 2;').digest('hex'))
+    assert.equal(frozen.inputSha256['node_modules/example/types.d.ts'], undefined)
+    assert.equal(JSON.parse(frozen.tsconfig).compilerOptions.allowJs, true)
+  })
+})
+
+test('startup freezes JSON bytes and explicitly records native builtins without pretending they are source', () => {
+  workspace({ 'data.json': '{"answer":42}' }, (root, entry) => {
+    const resolver = new FrozenModuleResolver(root, entry)
+
+    assert.equal(resolver.resolveStartup('./data.json', entry, 'require').kind, 'boundary')
+    assert.equal(resolver.resolveStartup('node:fs', entry).kind, 'boundary')
+    const frozen = resolver.freeze(['entry.ts'])!
+
+    assert.equal(frozen.inputSha256['data.json'], createHash('sha256').update('{"answer":42}').digest('hex'))
+    assert.deepEqual(frozen.runtimeBoundaries, [
+      { sourceFile: 'entry.ts', specifier: './data.json', importKind: 'require', kind: 'json', runtimeFile: 'data.json' },
+      { sourceFile: 'entry.ts', specifier: 'node:fs', importKind: 'import', kind: 'node-builtin' },
+    ])
+    assert.throws(() => resolver.resolveStartup('node:missing_builtin', entry), /Unresolved/)
+  })
+})
+
+test('startup follows package export patterns and preserves exact exported runtime paths', () => {
+  workspace({
+    'node_modules/example/package.json': JSON.stringify({ name: 'example', exports: { './*': './lib/*.js' } }),
+    'node_modules/example/lib/helper.js': 'export const value = 2;',
+    'node_modules/example/lib/missing.ts': 'export const value = 3;',
+  }, (root, entry) => {
+    const resolver = new FrozenModuleResolver(root, entry)
+
+    assert.deepEqual(resolver.resolveStartup('example/helper', entry),
+      { kind: 'source', file: path.join(root, 'node_modules/example/lib/helper.js') })
+    assert.throws(() => resolver.resolveStartup('example/missing', entry), /Missing acquired/)
+  })
+})
+
+test('startup retains alias precedence and actual generated JavaScript bytes', () => {
+  workspace({
+    'tsconfig.json': JSON.stringify({ compilerOptions: { baseUrl: '.', paths: { example: ['./generated.js'] } } }),
+    'generated.js': 'export const value = 5;',
+    'rt.wat.js': 'export const value = 7;',
+    'generated.ts': 'export const value = 6;',
+  }, (root, entry) => {
+    const resolver = new FrozenModuleResolver(root, entry)
+
+    assert.deepEqual(resolver.resolveStartup('example', entry), { kind: 'source', file: path.join(root, 'generated.js') })
+    assert.deepEqual(resolver.resolveStartup('./generated.js', entry), { kind: 'source', file: path.join(root, 'generated.js') })
+    assert.deepEqual(resolver.resolveStartup('./rt.wat', entry, 'require'), { kind: 'source', file: path.join(root, 'rt.wat.js') })
+    assert.throws(() => resolver.resolve('./generated.js', entry), /JavaScript runtime source is unsupported/)
+  })
+})
+
+test('startup rejects declaration-only entries and dependencies escaping the acquired root', () => {
+  workspace({
+    'node_modules/example/package.json': '{"name":"example","main":"./types.d.ts"}',
+    'node_modules/example/types.d.ts': 'export declare const value: 1;',
+  }, (root, entry) => {
+    const resolver = new FrozenModuleResolver(root, entry)
+    symlinkSync(path.join(root, '..'), path.join(root, 'escape'))
+
+    assert.throws(() => resolver.resolveStartup('example', entry), /declaration-only/)
+    assert.throws(() => resolver.resolveStartup('../outside', entry), /Unresolved/)
+    assert.throws(() => resolver.resolveStartup('./escape/anything.ts', entry), /Unresolved/)
+  })
+})
+
+
+test('shared startup traversal follows generated JavaScript require and records JSON/native boundaries', () => {
+  workspace({
+    'entry.ts': "import { value } from './generated.js'; export class Entry { read() { return value; } }",
+    'generated.js': "const data = require('./data.json'); const fs = require('node:fs'); exports.value = data.answer;",
+    'data.json': '{"answer":42}',
+    'tsconfig.jsonc': '{"compilerOptions":{"strict":true}}',
+  }, (root, entry) => {
+    const graph = inspectStartupSourceClosure(root, entry)
+
+    assert.equal(graph.reasonCode, undefined)
+    assert.deepEqual(graph.files, ['entry.ts', 'generated.js'])
+    assert.ok(graph.resolution!.inputSha256['data.json'])
+    assert.ok(graph.resolution!.inputSha256['tsconfig.jsonc'])
+    assert.equal(graph.resolution!.runtimeBoundaries!.length, 2)
+    assert.ok(graph.initializationIssues!.length > 0)
+    assert.equal(JSON.parse(graph.resolution!.tsconfig).compilerOptions.strictBuiltinIteratorReturn, undefined)
+    assert.equal(inspectLocalSourceClosure(root, entry).reasonCode, 'IMPORTED_CALLEES_UNSUPPORTED')
+  })
+})
+
+test('startup records an unresolved dynamic boundary and checked mode still rejects it', () => {
+  workspace({ 'entry.ts': 'export class Entry { load(name: string) { return require(name); } }' }, (root, entry) => {
+    const graph = inspectStartupSourceClosure(root, entry)
+
+    assert.equal(graph.reasonCode, undefined)
+    assert.deepEqual(graph.files, ['entry.ts'])
+    assert.equal(graph.resolution!.runtimeBoundaries![0]!.kind, 'dynamic-module')
+    assert.equal(graph.resolution!.runtimeBoundaries![0]!.expression, 'require(name)')
+    assert.match(graph.initializationIssues![0]!.diagnostic, /Unresolved dynamic/)
+    assert.equal(inspectLocalSourceClosure(root, entry).reasonCode, 'IMPORTED_CALLEES_UNSUPPORTED')
+  })
+})
+
+
+test('paths-only startup aliases have an explicit bounded current directory', () => {
+  workspace({
+    'tsconfig.json': '{"compilerOptions":{"paths":{"alias":["./helper.ts"]}}}',
+    'helper.ts': 'export const value = 1;',
+  }, (root, entry) => {
+    const resolver = new FrozenModuleResolver(root, entry)
+
+    assert.deepEqual(resolver.resolveStartup('alias', entry), { kind: 'source', file: path.join(root, 'helper.ts') })
+  })
+})
+
+test('absent JSON-looking relative source paths retain real TS source rather than a fabricated JSON asset', () => {
+  workspace({ 'resource.json.ts': 'export default { answer: 42 };' }, (root, entry) => {
+    const resolver = new FrozenModuleResolver(root, entry)
+
+    assert.deepEqual(resolver.resolveStartup('./resource.json', entry),
+      { kind: 'source', file: path.join(root, 'resource.json.ts') })
+    assert.equal(resolver.resolve('./resource.json', entry), path.join(root, 'resource.json.ts'))
+  })
+})
+
+test('installed extensionless runtime entries use actual JavaScript ahead of adjacent TypeScript source', () => {
+  workspace({
+    'node_modules/example/package.json': '{"name":"example","main":"./v10"}',
+    'node_modules/example/v10.js': 'exports.value = 1;',
+    'node_modules/example/v10.ts': 'export const value = 2;',
+  }, (root, entry) => {
+    const resolver = new FrozenModuleResolver(root, entry)
+
+    assert.deepEqual(resolver.resolveStartup('example', entry),
+      { kind: 'source', file: path.join(root, 'node_modules/example/v10.js') })
+  })
+})