Skip to content
@lfglabs-dev

LFG Labs

We are formally verifying critical software

Pinned Loading

  1. verity verity Public

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

    Lean 148 19

  2. ethereum-verification-benchmark ethereum-verification-benchmark Public

    Benchmark for Verity-based smart contract verification research

    Lean 3

Repositories

Showing 10 of 129 repositories
  • lido-srv3-proof-closure Public

    Private Lido SRv3 formal methods final report package

    lfglabs-dev/lido-srv3-proof-closure's past year of commit activity
    Lean 0 0 0 8 Updated Sep 12, 2026
  • eip-8282-proof-closure Public

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

    lfglabs-dev/eip-8282-proof-closure's past year of commit activity
    Lean 0 MIT 0 0 0 Updated Sep 12, 2026
  • verity Public

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

    lfglabs-dev/verity's past year of commit activity
    Lean 148 MIT 19 23 2 Updated Sep 11, 2026
  • ethereum-verification-benchmark Public

    Benchmark for Verity-based smart contract verification research

    lfglabs-dev/ethereum-verification-benchmark's past year of commit activity
    Lean 3 0 2 1 Updated Sep 11, 2026
  • lean-silicon Public

    A formally verified physical scalar coprocessor for leanVM-b.

    lfglabs-dev/lean-silicon's past year of commit activity
    Python 2 Apache-2.0 0 0 3 Updated Sep 8, 2026
  • EVMYulLean Public Forked from NethermindEth/EVMYulLean

    Executable formal model of the EVM and Yul in Lean 4.

    lfglabs-dev/EVMYulLean's past year of commit activity
    Lean 0 Apache-2.0 23 0 2 Updated Aug 30, 2026
  • eip-8282-proof-flow-map Public

    Source-grounded EIP-8282 architecture and Lean 4 proof-flow planning map

    lfglabs-dev/eip-8282-proof-flow-map's past year of commit activity
    HTML 1 0 0 1 Updated Aug 20, 2026
  • EIPs Public Forked from ethereum/EIPs

    The Ethereum Improvement Proposal repository

    lfglabs-dev/EIPs's past year of commit activity
    Python 0 CC0-1.0 6,867 0 1 Updated Aug 17, 2026
  • evmbench Public Forked from paradigmxyz/evmbench

    A benchmark and harness for finding and exploiting smart contract bugs

    lfglabs-dev/evmbench's past year of commit activity
    Python 0 Apache-2.0 77 0 0 Updated Aug 10, 2026
  • frontier-evals Public

    LFG Labs mirror of OpenAI frontier-evals for EVMBench data

    lfglabs-dev/frontier-evals's past year of commit activity
    Python 0 MIT 0 0 0 Updated Aug 7, 2026
View all repositories