diff --git a/Cargo.lock b/Cargo.lock
index 4c82ed411b2..a625edefcd5 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -1858,9 +1858,9 @@ dependencies = [
 
 [[package]]
 name = "once_cell"
-version = "1.17.0"
+version = "1.17.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "6f61fba1741ea2b3d6a1e3178721804bb716a68a6aeba1149b5d52e3d464ea66"
+checksum = "b7e5500299e16ebb147ae15a00a942af264cf3688f47923b8fc2cd5858f23ad3"
 
 [[package]]
 name = "openssl"
@@ -2165,6 +2165,7 @@ dependencies = [
  "lazy_static",
  "log",
  "num_cpus",
+ "once_cell",
  "prusti-common",
  "prusti-utils",
  "reqwest",
@@ -2239,6 +2240,7 @@ dependencies = [
  "lazy_static",
  "log",
  "num-traits",
+ "once_cell",
  "prusti-common",
  "prusti-interface",
  "prusti-rustc-interface",
diff --git a/prusti-server/Cargo.toml b/prusti-server/Cargo.toml
index 9b1351a58d9..a98017d3db3 100644
--- a/prusti-server/Cargo.toml
+++ b/prusti-server/Cargo.toml
@@ -31,6 +31,7 @@ reqwest = { version = "0.11", default-features = false, features = ["json", "rus
 warp = "0.3"
 tokio = "1.20"
 rustc-hash = "1.1.0"
+once_cell = "1.17.1"
 
 [dev-dependencies]
 lazy_static = "1.4.0"
diff --git a/prusti-server/src/backend.rs b/prusti-server/src/backend.rs
new file mode 100644
index 00000000000..5a36ad6c399
--- /dev/null
+++ b/prusti-server/src/backend.rs
@@ -0,0 +1,41 @@
+use crate::dump_viper_program;
+use prusti_common::{
+    config,
+    vir::{LoweringContext, ToViper},
+    Stopwatch,
+};
+use viper::{VerificationContext, VerificationResult};
+
+pub enum Backend<'a> {
+    Viper(viper::Verifier<'a>, &'a VerificationContext<'a>),
+}
+
+impl<'a> Backend<'a> {
+    pub fn verify(&mut self, program: &prusti_common::vir::program::Program) -> VerificationResult {
+        match self {
+            Backend::Viper(viper, context) => {
+                let mut stopwatch =
+                    Stopwatch::start("prusti-server backend", "construction of JVM objects");
+
+                let ast_utils = context.new_ast_utils();
+
+                ast_utils.with_local_frame(16, || {
+                    let ast_factory = context.new_ast_factory();
+                    let viper_program = program.to_viper(LoweringContext::default(), &ast_factory);
+
+                    if config::dump_viper_program() {
+                        stopwatch.start_next("dumping viper program");
+                        dump_viper_program(
+                            &ast_utils,
+                            viper_program,
+                            &program.get_name_with_check_mode(),
+                        );
+                    }
+
+                    stopwatch.start_next("viper verification");
+                    viper.verify(viper_program)
+                })
+            }
+        }
+    }
+}
diff --git a/prusti-server/src/lib.rs b/prusti-server/src/lib.rs
index dcc06e31660..64b7b670ffd 100644
--- a/prusti-server/src/lib.rs
+++ b/prusti-server/src/lib.rs
@@ -10,7 +10,9 @@ mod client;
 mod process_verification;
 mod server;
 mod verification_request;
+mod backend;
 
+pub use backend::*;
 pub use client::*;
 pub use process_verification::*;
 pub use server::*;
diff --git a/prusti-server/src/process_verification.rs b/prusti-server/src/process_verification.rs
index bc227525505..32c9b0b9179 100644
--- a/prusti-server/src/process_verification.rs
+++ b/prusti-server/src/process_verification.rs
@@ -4,8 +4,9 @@
 // License, v. 2.0. If a copy of the MPL was not distributed with this
 // file, You can obtain one at http://mozilla.org/MPL/2.0/.
 
-use crate::{VerificationRequest, ViperBackendConfig};
+use crate::{Backend, VerificationRequest, ViperBackendConfig};
 use log::info;
+use once_cell::sync::Lazy;
 use prusti_common::{
     config,
     report::log::{report, to_legal_file_name},
@@ -18,7 +19,7 @@ use viper::{
 };
 
 pub fn process_verification_request<'v, 't: 'v>(
-    verification_context: &'v VerificationContext<'t>,
+    verification_context: &'v Lazy<VerificationContext<'t>, impl Fn() -> VerificationContext<'t>>,
     mut request: VerificationRequest,
     cache: impl Cache,
 ) -> viper::VerificationResult {
@@ -97,35 +98,43 @@ pub fn process_verification_request<'v, 't: 'v>(
         }
     };
 
-    ast_utils.with_local_frame(16, || {
-        let viper_program = build_or_dump_viper_program();
-        let program_name = request.program.get_name();
-
-        // Create a new verifier each time.
-        // Workaround for https://github.com/viperproject/prusti-dev/issues/744
-        let mut stopwatch = Stopwatch::start("prusti-server", "verifier startup");
-        let mut verifier =
-            new_viper_verifier(program_name, verification_context, request.backend_config);
+    let mut stopwatch = Stopwatch::start("prusti-server", "verifier startup");
+
+    // Create a new verifier each time.
+    // Workaround for https://github.com/viperproject/prusti-dev/issues/744
+    let mut backend = match request.backend_config.backend {
+        VerificationBackend::Carbon | VerificationBackend::Silicon => Backend::Viper(
+            new_viper_verifier(
+                request.program.get_name(),
+                verification_context,
+                request.backend_config,
+            ),
+            verification_context,
+        ),
+    };
 
-        stopwatch.start_next("verification");
-        let mut result = verifier.verify(viper_program);
+    stopwatch.start_next("backend verification");
+    let mut result = backend.verify(&request.program);
 
-        // Don't cache Java exceptions, which might be due to misconfigured paths.
-        if config::enable_cache() && !matches!(result, VerificationResult::JavaException(_)) {
-            info!(
-                "Storing new cached result {:?} for program {}",
-                &result,
-                request.program.get_name()
-            );
-            cache.insert(hash, result.clone());
-        }
+    // Don't cache Java exceptions, which might be due to misconfigured paths.
+    if config::enable_cache() && !matches!(result, VerificationResult::JavaException(_)) {
+        info!(
+            "Storing new cached result {:?} for program {}",
+            &result,
+            request.program.get_name()
+        );
+        cache.insert(hash, result.clone());
+    }
 
-        normalization_info.denormalize_result(&mut result);
-        result
-    })
+    normalization_info.denormalize_result(&mut result);
+    result
 }
 
-fn dump_viper_program(ast_utils: &viper::AstUtils, program: viper::Program, program_name: &str) {
+pub fn dump_viper_program(
+    ast_utils: &viper::AstUtils,
+    program: viper::Program,
+    program_name: &str,
+) {
     let namespace = "viper_program";
     let filename = format!("{program_name}.vpr");
     info!("Dumping Viper program to '{}/{}'", namespace, filename);
diff --git a/prusti-server/src/server.rs b/prusti-server/src/server.rs
index 2492feb484c..1d13a9a01c3 100644
--- a/prusti-server/src/server.rs
+++ b/prusti-server/src/server.rs
@@ -6,6 +6,7 @@
 
 use crate::{process_verification_request, VerificationRequest};
 use log::info;
+use once_cell::sync::Lazy;
 use prusti_common::{config, Stopwatch};
 use std::{
     net::{Ipv4Addr, SocketAddr},
@@ -46,18 +47,18 @@ where
     F: FnOnce(SocketAddr),
 {
     let stopwatch = Stopwatch::start("prusti-server", "JVM startup");
-    let viper = Arc::new(Viper::new_with_args(
-        &config::viper_home(),
-        config::extra_jvm_args(),
-    ));
+    let viper = Arc::new(Lazy::new(|| {
+        Viper::new_with_args(&config::viper_home(), config::extra_jvm_args())
+    }));
+
     stopwatch.finish();
 
     let cache_data = PersistentCache::load_cache(config::cache_path());
     let cache = Arc::new(Mutex::new(cache_data));
-    let build_verification_request_handler = |viper_arc: Arc<Viper>, cache| {
+    let build_verification_request_handler = |viper_arc: Arc<Lazy<Viper, _>>, cache| {
         move |request: VerificationRequest| {
             let stopwatch = Stopwatch::start("prusti-server", "attach thread to JVM");
-            let viper_thread = viper_arc.attach_current_thread();
+            let viper_thread = Lazy::new(|| viper_arc.attach_current_thread());
             stopwatch.finish();
             process_verification_request(&viper_thread, request, &cache)
         }
diff --git a/prusti-viper/Cargo.toml b/prusti-viper/Cargo.toml
index d35bca947a3..d21e4c5d9ab 100644
--- a/prusti-viper/Cargo.toml
+++ b/prusti-viper/Cargo.toml
@@ -26,6 +26,7 @@ backtrace = "0.3"
 rustc-hash = "1.1.0"
 derive_more = "0.99.16"
 itertools = "0.10.3"
+once_cell = "1.17.1"
 
 [dev-dependencies]
 lazy_static = "1.4"
diff --git a/prusti-viper/src/verifier.rs b/prusti-viper/src/verifier.rs
index 73b5f371d62..be34575f012 100644
--- a/prusti-viper/src/verifier.rs
+++ b/prusti-viper/src/verifier.rs
@@ -4,24 +4,31 @@
 // License, v. 2.0. If a copy of the MPL was not distributed with this
 // file, You can obtain one at http://mozilla.org/MPL/2.0/.
 
-use prusti_common::vir::{optimizations::optimize_program};
+use crate::encoder::{
+    counterexamples::{counterexample_translation, counterexample_translation_refactored},
+    Encoder,
+};
+use ::log::{debug, error, info};
+use once_cell::sync::Lazy;
 use prusti_common::{
-    config, report::log, Stopwatch, vir::program::Program,
+    config,
+    report::log,
+    vir::{optimizations::optimize_program, program::Program},
+    Stopwatch,
+};
+use prusti_interface::{
+    data::{VerificationResult, VerificationTask},
+    environment::Environment,
+    specs::typed,
+    PrustiError,
 };
-use vir_crate::common::check_mode::CheckMode;
-use crate::encoder::Encoder;
-use crate::encoder::counterexamples::counterexample_translation;
-use crate::encoder::counterexamples::counterexample_translation_refactored;
-use prusti_interface::data::VerificationResult;
-use prusti_interface::data::VerificationTask;
-use prusti_interface::environment::Environment;
-use prusti_interface::PrustiError;
-use viper::{self, PersistentCache, Viper};
-use prusti_interface::specs::typed;
-use ::log::{info, debug, error};
-use prusti_server::{VerificationRequest, PrustiClient, process_verification_request, spawn_server_thread, ViperBackendConfig};
 use prusti_rustc_interface::span::DUMMY_SP;
-use prusti_server::tokio::runtime::Builder;
+use prusti_server::{
+    process_verification_request, spawn_server_thread, tokio::runtime::Builder, PrustiClient,
+    VerificationRequest, ViperBackendConfig,
+};
+use viper::{self, PersistentCache, Viper};
+use vir_crate::common::check_mode::CheckMode;
 
 /// A verifier is an object for verifying a single crate, potentially
 /// many times.
@@ -34,10 +41,7 @@ where
 }
 
 impl<'v, 'tcx> Verifier<'v, 'tcx> {
-    pub fn new(
-        env: &'v Environment<'tcx>,
-        def_spec: typed::DefSpecificationMap,
-    ) -> Self {
+    pub fn new(env: &'v Environment<'tcx>, def_spec: typed::DefSpecificationMap) -> Self {
         Verifier {
             env,
             encoder: Encoder::new(env, def_spec),
@@ -81,13 +85,15 @@ impl<'v, 'tcx> Verifier<'v, 'tcx> {
         let mut programs: Vec<Program> = if config::simplify_encoding() {
             stopwatch.start_next("optimizing Viper program");
             let source_file_name = self.encoder.env().name.source_file_name();
-            polymorphic_programs.into_iter().map(
-                |program| Program::Legacy(optimize_program(program, &source_file_name).into())
-            ).collect()
+            polymorphic_programs
+                .into_iter()
+                .map(|program| Program::Legacy(optimize_program(program, &source_file_name).into()))
+                .collect()
         } else {
-            polymorphic_programs.into_iter().map(
-                |program| Program::Legacy(program.into())
-            ).collect()
+            polymorphic_programs
+                .into_iter()
+                .map(|program| Program::Legacy(program.into()))
+                .collect()
         };
         programs.extend(self.encoder.get_core_proof_programs());
 
@@ -96,9 +102,9 @@ impl<'v, 'tcx> Verifier<'v, 'tcx> {
         stopwatch.finish();
 
         // Group verification results
-        let mut verification_errors : Vec<_> = vec![];
-        let mut consistency_errors : Vec<_> = vec![];
-        let mut java_exceptions : Vec<_> = vec![];
+        let mut verification_errors: Vec<_> = vec![];
+        let mut consistency_errors: Vec<_> = vec![];
+        let mut java_exceptions: Vec<_> = vec![];
         for (method_name, result) in verification_results.into_iter() {
             match result {
                 viper::VerificationResult::Success => {}
@@ -124,16 +130,17 @@ impl<'v, 'tcx> Verifier<'v, 'tcx> {
 
         for (method, error) in consistency_errors.into_iter() {
             PrustiError::internal(
-                format!("consistency error in {method}: {error}"), DUMMY_SP.into()
-            ).emit(&self.env.diagnostic);
+                format!("consistency error in {method}: {error}"),
+                DUMMY_SP.into(),
+            )
+            .emit(&self.env.diagnostic);
             result = VerificationResult::Failure;
         }
 
         for (method, exception) in java_exceptions.into_iter() {
             error!("Java exception: {}", exception.get_stack_trace());
-            PrustiError::internal(
-                format!("in {method}: {exception}"), DUMMY_SP.into()
-            ).emit(&self.env.diagnostic);
+            PrustiError::internal(format!("in {method}: {exception}"), DUMMY_SP.into())
+                .emit(&self.env.diagnostic);
             result = VerificationResult::Failure;
         }
 
@@ -145,15 +152,16 @@ impl<'v, 'tcx> Verifier<'v, 'tcx> {
 
             // annotate with counterexample, if requested
             if config::counterexample() {
-                if config::unsafe_core_proof(){
+                if config::unsafe_core_proof() {
                     if let Some(silicon_counterexample) = &verification_error.counterexample {
                         if let Some(def_id) = error_manager.get_def_id(&verification_error) {
-                            let counterexample = counterexample_translation_refactored::backtranslate(
-                                &self.encoder,
-                                error_manager.position_manager(),
-                                def_id,
-                                silicon_counterexample,
-                            );
+                            let counterexample =
+                                counterexample_translation_refactored::backtranslate(
+                                    &self.encoder,
+                                    error_manager.position_manager(),
+                                    def_id,
+                                    silicon_counterexample,
+                                );
                             prusti_error = counterexample.annotate_error(prusti_error);
                         } else {
                             prusti_error = prusti_error.add_note(
@@ -207,9 +215,10 @@ impl<'v, 'tcx> Verifier<'v, 'tcx> {
 
 /// Verify a list of programs.
 /// Returns a list of (program_name, verification_result) tuples.
-fn verify_programs(env: &Environment, programs: Vec<Program>)
-    -> Vec<(String, viper::VerificationResult)>
-{
+fn verify_programs(
+    env: &Environment,
+    programs: Vec<Program>,
+) -> Vec<(String, viper::VerificationResult)> {
     let source_path = env.name.source_path();
     let rust_program_name = source_path
         .file_name()
@@ -226,7 +235,9 @@ fn verify_programs(env: &Environment, programs: Vec<Program>)
             config::verify_specifications_backend()
         } else {
             config::viper_backend()
-        }.parse().unwrap();
+        }
+        .parse()
+        .unwrap();
         let request = VerificationRequest {
             program,
             backend_config: ViperBackendConfig::new(backend),
@@ -241,9 +252,7 @@ fn verify_programs(env: &Environment, programs: Vec<Program>)
         };
         info!("Connecting to Prusti server at {}", server_address);
         let client = PrustiClient::new(&server_address).unwrap_or_else(|error| {
-            panic!(
-                "Could not parse server address ({server_address}) due to {error:?}"
-            )
+            panic!("Could not parse server address ({server_address}) due to {error:?}")
         });
         // Here we construct a Tokio runtime to block until completion of the futures returned by
         // `client.verify`. However, to report verification errors as early as possible,
@@ -253,25 +262,28 @@ fn verify_programs(env: &Environment, programs: Vec<Program>)
             .enable_all()
             .build()
             .expect("failed to construct Tokio runtime");
-        verification_requests.map(|(program_name, request)| {
-            let remote_result = runtime.block_on(client.verify(request));
-            let result = remote_result.unwrap_or_else(|error| {
-                panic!(
-                    "Verification request of program {program_name} failed: {error:?}"
-                )
-            });
-            (program_name, result)
-        }).collect()
+        verification_requests
+            .map(|(program_name, request)| {
+                let remote_result = runtime.block_on(client.verify(request));
+                let result = remote_result.unwrap_or_else(|error| {
+                    panic!("Verification request of program {program_name} failed: {error:?}")
+                });
+                (program_name, result)
+            })
+            .collect()
     } else {
         let mut stopwatch = Stopwatch::start("prusti-viper", "JVM startup");
-        let viper = Viper::new_with_args(&config::viper_home(), config::extra_jvm_args());
         stopwatch.start_next("attach current thread to the JVM");
-        let viper_thread = viper.attach_current_thread();
+        let viper =
+            Lazy::new(|| Viper::new_with_args(&config::viper_home(), config::extra_jvm_args()));
+        let viper_thread = Lazy::new(|| viper.attach_current_thread());
         stopwatch.finish();
         let mut cache = PersistentCache::load_cache(config::cache_path());
-        verification_requests.map(|(program_name, request)| {
-            let result = process_verification_request(&viper_thread, request, &mut cache);
-            (program_name, result)
-        }).collect()
+        verification_requests
+            .map(|(program_name, request)| {
+                let result = process_verification_request(&viper_thread, request, &mut cache);
+                (program_name, result)
+            })
+            .collect()
     }
 }