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 20

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

    Benchmark for Verity-based smart contract verification research

    Lean 3

Repositories

Showing 10 of 131 repositories
  • morpho-midnight-verity Public
    lfglabs-dev/morpho-midnight-verity's past year of commit activity
    Lean 0 0 0 0 Updated Oct 5, 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 20 36 5 Updated Oct 5, 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 2 Updated Oct 4, 2026
  • rust-verification-benchmark-harbor Public

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

    lfglabs-dev/rust-verification-benchmark-harbor's past year of commit activity
    0 0 0 0 Updated Oct 1, 2026
  • 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 0 Updated Sep 22, 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 1 Updated Sep 15, 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,889 0 1 Updated Sep 15, 2026
  • lean-silicon Public

    A formally verified physical scalar coprocessor for leanVM-b.

    lfglabs-dev/lean-silicon's past year of commit activity
    Python 3 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
View all repositories