From proofs to practice

Research projects

I participate in the TRust² project, working on formal verification of Rust. Our Solana verification work is part of TRust², with the Solana eBPF virtual machine serving as a real-world Rust case study.

End-to-end formal verification of the Solana eBPF JIT compiler

January 2025 – December 2025

Connecting the Rust JIT implementation with formal models of eBPF and x86-64 to study end-to-end compiler correctness.

View project

Porting an eBPF JIT compiler to RISC-V for Solana

2025–2026

An open source project for Solana, developing a RISC-V backend for its eBPF JIT compiler.

View project Source code

Linux patches

• bpf: Reject negative offsets for ALU ops

  Related vulnerability record: CVE-2025-40169.

• bpf: Add range tracking for BPF_DIV and BPF_MOD

  Range tracking for division and modulo operations, with related selftests.

• bpf: Add bitwise tracking for BPF_END

  Related selftests. This change introduced another issue, which has since been fixed; see the follow-up discussion.

• bpf: Fix out-of-bounds read in bpf_patch_call_args()

  A fix for an out-of-bounds read in BPF call argument patching.

• Simplify min()/max(), contains() and normalize() cnum implementation

  Simplification of the cnum implementation.

Solana issues & pull requests

• Assembler: register inconsistency

  Issue #562 in solana-labs/rbpf.

• Interpreter LD_DW_IMM: add !sbpf_version.disable_lddw() checking

  Issue #563 in solana-labs/rbpf.

• Cleanup: unused JIT-generated instruction

  Pull request #78 in anza-xyz/sbpf.

• Feature: expand X86Instruction::opcode to optimize multiplications

  Pull request #68 in anza-xyz/sbpf.

• Cleanup: remove unreachable None branch in emit_profile_instruction_count

  Pull request #131 in anza-xyz/sbpf.