This repo is the marketing website for LFG Labs (lfglabs.dev), built with Next.js.
LFG Labs sells formal proving-as-a-service for DeFi smart contracts. We take Solidity contracts, write machine-checkable specs in Lean 4, and produce mathematical proofs that the implementation matches the spec across all inputs — not just test cases. This is not an audit; it's a mathematical guarantee.
Verity is our Ethereum Foundation-funded Lean 4 framework bridging Solidity and formal mathematics. It compiles to EVM bytecode via Yul. Stats: 431 theorems, 0 unproven steps, 1 axiom (keccak256), 403 Foundry tests, 11 contracts. Verity is to LFG Labs what Next.js is to Vercel — the open-source lead magnet; LFG Labs is the managed service layer.
DeFi protocols with non-trivial on-chain logic: lending/money markets, stablecoins, DEXs/AMMs, bridges, derivatives/perpetuals, yield optimizers, onchain credit/RWAs, L2/protocol infra. Buyer is always deeply technical (CTO, co-founder, head of engineering, chief scientist). Disqualified: CEXs, gaming/NFT without DeFi, non-EVM chains, dead protocols.
- vs Manual audits (Trail of Bits, Zellic, OpenZeppelin, etc.): Audits are human opinions frozen in time — they miss unknown unknowns and become stale the moment code changes. Formal proofs give stronger guarantees (all inputs, not sampled ones) and let teams iterate post-verification without restarting from scratch.
- vs Certora: Certora does bounded model checking (no violation found up to depth N). Verity produces full mathematical proofs (no violation exists, period). Complementary, not substitutes.
"Verity Research Ask" — co-authoring an EF research paper on formal verification of Solidity. Protocols participate as case studies (free verification, credited in paper). Foot-in-the-door for proving-as-a-service relationships.