Heimdall automates translation of eBPF C programs to Rust with formal equivalence proofs for 94.1% of 102 tested programs using LLMs, static analysis, and Z3-based checking.
Navas, Noam Rinetzky, Leonid Ryzhyk, and Mooly Sagiv
4 Pith papers cite this work, alongside 87 external citations. Polarity classification is still indexing.
4
Pith papers citing it
87
external citations · external index
citation-role summary
background 1
citation-polarity summary
years
2026 4verdicts
UNVERDICTED 4roles
background 1polarities
background 1representative citing papers
Kops enables extension of the eBPF JIT with native operations using proof sequences checked by the existing verifier and native emits, validated by Lean 4 proofs, delivering up to 24% microbenchmark and 12% application speedups.
HELIX is an end-to-end verified code generator from mathematical formulations of cyber-physical systems to LLVM IR, using Coq, algebraic transformations, term rewriting, and sparse vector abstractions.
Defines formal semantics for C with OpenMP directives extending CompCert, with a guarantee that successful executions are race-free.
citing papers explorer
-
Heimdall: Formally Verified Automated Migration of Legacy eBPF Programs to Rust
Heimdall automates translation of eBPF C programs to Rust with formal equivalence proofs for 94.1% of 102 tested programs using LLMs, static analysis, and Z3-based checking.
-
Kops: Safely Extending the eBPF Compilation Pipeline with Native Operations
Kops enables extension of the eBPF JIT with native operations using proof sequences checked by the existing verifier and native emits, validated by Lean 4 proofs, delivering up to 24% microbenchmark and 12% application speedups.
-
HELIX: Verified compilation of cyber-physical control systems to LLVM IR
HELIX is an end-to-end verified code generator from mathematical formulations of cyber-physical systems to LLVM IR, using Coq, algebraic transformations, term rewriting, and sparse vector abstractions.
-
A Formal Semantics of C with OpenMP Parallelism (Extended Version)
Defines formal semantics for C with OpenMP directives extending CompCert, with a guarantee that successful executions are race-free.