DeterV: Verifying Deterministic Parallel Execution
DeterV is a deterministic parallel runtime which uses Verus to verify its correctness and equivalence to serial execution in the input order and attains a 3:1 proof-to-code ratio and incurs only trivial runtime overhead compared to an unverified baseline.