diff --git a/quint/package.json b/quint/package.json
index 2bedfad9b..4936e6528 100644
--- a/quint/package.json
+++ b/quint/package.json
@@ -55,7 +55,6 @@
     "@types/line-column": "^1.0.0",
     "@types/seedrandom": "^3.0.4",
     "antlr4ts": "^0.5.0-alpha.4",
-    "axios": "1.4.0",
     "chalk": "^4.1.2",
     "eol": "^0.9.1",
     "immutable": "^4.3.0",
@@ -68,7 +67,7 @@
     "yargs": "^17.2.1"
   },
   "scripts": {
-    "compile": "genversion -e src/version.ts && tsc && copyfiles -u 1 ./src/builtin.qnt ./dist/src/",
+    "compile": "genversion -e src/version.ts && tsc && copyfiles -u 1 ./src/reflection.proto ./src/builtin.qnt ./dist/src/",
     "prepare": "rm -rf ./dist && npm run compile && chmod +x ./dist/src/cli.js",
     "test": "mocha --reporter-option maxDiffSize=0 -r ts-node/register test/*.test.ts test/**/*.test.ts",
     "coverage": "nyc npm run test",
diff --git a/quint/src/quintVerifier.ts b/quint/src/quintVerifier.ts
index cd5141faa..6fe22c079 100644
--- a/quint/src/quintVerifier.ts
+++ b/quint/src/quintVerifier.ts
@@ -27,7 +27,6 @@ import * as protoDescriptor from 'protobufjs/ext/descriptor'
 import { setTimeout } from 'timers/promises'
 import { promisify } from 'util'
 import { ItfTrace } from './itf'
-import axios from 'axios'
 import { Buffer } from 'buffer'
 
 import type { PackageDefinition as ProtoPackageDefinition } from '@grpc/proto-loader'
@@ -187,11 +186,6 @@ const grpcStubOptions = {
 }
 
 async function loadProtoDefViaReflection(): Promise<VerifyResult<ProtoPackageDefinition>> {
-  // const packageDefinition = proto.loadSync(
-  //   reflectionProtoFile,
-  //   grpcStubOptions
-  // );
-
   type ServerReflectionResponseSuccess = {
     file_descriptor_response: {
       file_descriptor_proto: Buffer[]
@@ -213,12 +207,11 @@ async function loadProtoDefViaReflection(): Promise<VerifyResult<ProtoPackageDef
   }
 
   // Obtain a reflection service client
-  const response = await axios.get(
-    'https://github.com/grpc/grpc/raw/master/src/proto/grpc/reflection/v1alpha/reflection.proto',
-    { responseType: 'text' }
-  )
-  const protoJson = protobuf.parse(response.data, grpcStubOptions).root.toJSON()
-  const packageDefinition = proto.fromJSON(protoJson, grpcStubOptions)
+  // To load from HTTP:
+  // const protoJson = protobuf.parse(response.data, grpcStubOptions).root.toJSON()
+  // const packageDefinition = proto.fromJSON(protoJson, grpcStubOptions)
+  const protoPath = require.resolve('./reflection.proto');
+  const packageDefinition = proto.loadSync(protoPath, grpcStubOptions);
   const reflectionProtoDescriptor = grpc.loadPackageDefinition(packageDefinition) as unknown as ServerReflectionPkg
   const serverReflectionService = reflectionProtoDescriptor.grpc.reflection.v1alpha.ServerReflection
   const reflectionClient = new serverReflectionService(APALACHE_SERVER_URI, grpc.credentials.createInsecure())
diff --git a/quint/src/reflection.proto b/quint/src/reflection.proto
new file mode 100644
index 000000000..816852f82
--- /dev/null
+++ b/quint/src/reflection.proto
@@ -0,0 +1,136 @@
+// Copyright 2016 gRPC authors.
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//     http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+
+// Service exported by server reflection
+
+syntax = "proto3";
+
+package grpc.reflection.v1alpha;
+
+service ServerReflection {
+  // The reflection service is structured as a bidirectional stream, ensuring
+  // all related requests go to a single server.
+  rpc ServerReflectionInfo(stream ServerReflectionRequest)
+      returns (stream ServerReflectionResponse);
+}
+
+// The message sent by the client when calling ServerReflectionInfo method.
+message ServerReflectionRequest {
+  string host = 1;
+  // To use reflection service, the client should set one of the following
+  // fields in message_request. The server distinguishes requests by their
+  // defined field and then handles them using corresponding methods.
+  oneof message_request {
+    // Find a proto file by the file name.
+    string file_by_filename = 3;
+
+    // Find the proto file that declares the given fully-qualified symbol name.
+    // This field should be a fully-qualified symbol name
+    // (e.g. <package>.<service>[.<method>] or <package>.<type>).
+    string file_containing_symbol = 4;
+
+    // Find the proto file which defines an extension extending the given
+    // message type with the given field number.
+    ExtensionRequest file_containing_extension = 5;
+
+    // Finds the tag numbers used by all known extensions of the given message
+    // type, and appends them to ExtensionNumberResponse in an undefined order.
+    // Its corresponding method is best-effort: it's not guaranteed that the
+    // reflection service will implement this method, and it's not guaranteed
+    // that this method will provide all extensions. Returns
+    // StatusCode::UNIMPLEMENTED if it's not implemented.
+    // This field should be a fully-qualified type name. The format is
+    // <package>.<type>
+    string all_extension_numbers_of_type = 6;
+
+    // List the full names of registered services. The content will not be
+    // checked.
+    string list_services = 7;
+  }
+}
+
+// The type name and extension number sent by the client when requesting
+// file_containing_extension.
+message ExtensionRequest {
+  // Fully-qualified type name. The format should be <package>.<type>
+  string containing_type = 1;
+  int32 extension_number = 2;
+}
+
+// The message sent by the server to answer ServerReflectionInfo method.
+message ServerReflectionResponse {
+  string valid_host = 1;
+  ServerReflectionRequest original_request = 2;
+  // The server set one of the following fields accroding to the message_request
+  // in the request.
+  oneof message_response {
+    // This message is used to answer file_by_filename, file_containing_symbol,
+    // file_containing_extension requests with transitive dependencies. As
+    // the repeated label is not allowed in oneof fields, we use a
+    // FileDescriptorResponse message to encapsulate the repeated fields.
+    // The reflection service is allowed to avoid sending FileDescriptorProtos
+    // that were previously sent in response to earlier requests in the stream.
+    FileDescriptorResponse file_descriptor_response = 4;
+
+    // This message is used to answer all_extension_numbers_of_type requst.
+    ExtensionNumberResponse all_extension_numbers_response = 5;
+
+    // This message is used to answer list_services request.
+    ListServiceResponse list_services_response = 6;
+
+    // This message is used when an error occurs.
+    ErrorResponse error_response = 7;
+  }
+}
+
+// Serialized FileDescriptorProto messages sent by the server answering
+// a file_by_filename, file_containing_symbol, or file_containing_extension
+// request.
+message FileDescriptorResponse {
+  // Serialized FileDescriptorProto messages. We avoid taking a dependency on
+  // descriptor.proto, which uses proto2 only features, by making them opaque
+  // bytes instead.
+  repeated bytes file_descriptor_proto = 1;
+}
+
+// A list of extension numbers sent by the server answering
+// all_extension_numbers_of_type request.
+message ExtensionNumberResponse {
+  // Full name of the base type, including the package name. The format
+  // is <package>.<type>
+  string base_type_name = 1;
+  repeated int32 extension_number = 2;
+}
+
+// A list of ServiceResponse sent by the server answering list_services request.
+message ListServiceResponse {
+  // The information of each service may be expanded in the future, so we use
+  // ServiceResponse message to encapsulate it.
+  repeated ServiceResponse service = 1;
+}
+
+// The information of a single service used by ListServiceResponse to answer
+// list_services request.
+message ServiceResponse {
+  // Full name of a registered service, including its package name. The format
+  // is <package>.<service>
+  string name = 1;
+}
+
+// The error code and error message sent by the server when an error occurs.
+message ErrorResponse {
+  // This field uses the error codes defined in grpc::StatusCode.
+  int32 error_code = 1;
+  string error_message = 2;
+}