LFG Labs

RFVB v1.0 (2026-10-02): 100 Lean 4 proof tasks over mechanically extracted Rust code, specified by the crates' own property-based tests

RSGB v1.0: 100 Lean 4 + Z3 SMT formal specification generation tasks over mechanically extracted Rust code

Can frontier models spot a backdoor hidden in a pull request? 13 synthetic backdoored PRs, harness and results.

Benchmark for Verity-based smart contract verification research

Formally verified smart contracts gives mathematical certainty across all inputs and execution paths. We bet that agents will make full formal verification practical.

RFVB v1.0: 100 Lean 4 proof tasks over mechanically extracted Rust code, specified by the crates' own property-based tests

Rust Verification Benchmark v1.0: 100 Harbor environments for formal proofs over real Rust code

Private Lido SRv3 formal methods final report package

Lean evidence for three EIP-8282 builder deposit/exit predeploy guarantees (abstract model CHECKED; Verity OPEN)