I am running the Prusti Assistant extension in VS Code on Windows. My environment is properly configured with Java 11 (OpenJDK Temurin-11.0.31+11), and the Prusti server starts successfully.
However, when trying to verify a simple recursive data structure (a linked list using Box), the Viper server seems to crash, resulting in a 502 Bad Gateway error. Furthermore, the compiler attempts to write an ICE (Internal Compiler Error) log but fails on Windows with os error 123 (invalid filename/directory name syntax), likely because the generated timestamp string contains colons (:), which are forbidden in Windows file paths.
Minimal Reproducible Example:
pub struct List {
head: Link,
}
enum Link {
Empty,
More(Box<Node>),
}
struct Node {
elem: i32,
next: Link,
}
fn main() {
let test = Node {
elem: 17,
next: Link::Empty,
};
if test.elem > 23 {
panic!() // unreachable
}
}
Error logs:[2026-05-28T14:01:52Z INFO prusti_viper::verifier] Connecting to Prusti server at localhost:64939
thread 'rustc' panicked at prusti-viper\src\verifier.rs:265:21:
Verification request of program prusti_tutorial::main failed: reqwest::Error { kind: Status(502), url: Url { scheme: "http", cannot_be_a_base: false, username: "", password: None, host: Some(Domain("localhost")), port: Some(64939), path: "/bincode/verify/", query: None, fragment: None } }
stack backtrace:
note: Some details are omitted, run with `RUST_BACKTRACE=full` for a verbose backtrace.
error: the compiler unexpectedly panicked. this is a bug.
I am running the Prusti Assistant extension in VS Code on Windows. My environment is properly configured with Java 11 (
OpenJDK Temurin-11.0.31+11), and the Prusti server starts successfully.However, when trying to verify a simple recursive data structure (a linked list using
Box), the Viper server seems to crash, resulting in a502 Bad Gatewayerror. Furthermore, the compiler attempts to write an ICE (Internal Compiler Error) log but fails on Windows withos error 123(invalid filename/directory name syntax), likely because the generated timestamp string contains colons (:), which are forbidden in Windows file paths.Minimal Reproducible Example: