The OpenSourceVerif organization brings together cutting-edge research and development in formal verification, with a focus on two core areas:

• The TRust2 project, which is dedicated to building formally verified toolchains for the Rust programming language across multiple theorem provers, including Rocq, Isabelle/HOL, and Lean4.

• eBPF-related formal verification, covering both the Linux eBPF and Solana eBPF virtual machines. Our work spans eBPF ISA semantics, verifier safety, and the correctness of Just-In-Time (JIT) compilers.

🌈 True to our name, all projects developed under this organization are open-source and released under the MIT license.

👋 We warmly welcome you to join us—whether by contributing to the repositories you are interested in, or by using our tools and sharing your valuable feedback.