LFG Labs AG · Verity Labs
Find the attack. Check the proof.
LFG Labs AG is the company behind Verity Labs, our formal-verification and audits service brand, and Verity, our open-source verification framework. We help protocol teams examine smart-contract security properties, find failures and verify remediation.
Security leadership
Thomas Marchand leads security delivery and the Verity framework. He is the security lead for LFG Labs AG and the contact for assessment scope and technical findings. Benjamin Flores leads client coordination and research scoping. Our two-person team combines security research, verification engineering and client delivery.
Contact thomas@lfglabs.dev for security matters or ben@lfglabs.dev to discuss an engagement.
Authorized adversarial testing
For teams seeking adversarial testing, we scope assessments around explicit permission and concrete security properties. The agreed work can include attack-path analysis, invariant-breaking transaction sequences, fuzzing and property testing, and reproducible proof-of-concept exploit validation in isolated local forks or test environments.
Before testing a client target, the engagement must identify the authorizing owner, exact contracts and versions, permitted techniques, test environment, time window and stop conditions. Public source code is evidence for research; it is not permission to attack a deployed protocol.
From a finding to a verifiable result
- Agree the boundary. Specify assets, attacker capabilities, trust assumptions and the properties to assess.
- Challenge the property. Reproduce candidate failures against the agreed code in a controlled environment. Record the initial state and transaction sequence.
- Validate and remediate. Explain exploitability within the tested assumptions, review fixes and rerun the reproduction.
- Check the proof. Where included in scope, use Lean to establish the specified property across the modeled execution paths. State the model boundary and remaining assumptions.
Inspectable security work
These examples document our verification and security engineering. They do not imply authorization to offensively test the organizations or their live systems.
- Ethereum EIP-8282: machine-checked properties for builder deposit and exit contracts.
- Lido staking infrastructure: scoped verification of ETH allocation and accounting.
- SafeLens: offline multisig transaction verification, built for the Ethereum Foundation.
- Ethereum verification benchmark: evaluating AI-assisted proof development against smart-contract properties.
- Verity source code: the open-source Lean framework supported by Ethereum Foundation funding.
AI-assisted security research
Our intended use of AI for adversarial testing is to generate candidate attacks, validate vulnerabilities and compare findings with machine-checked specifications. Offensive execution must stay within owned or explicitly authorized targets and isolated test environments. A generated exploit or passing test is not a proof of general correctness.
Read our testing boundaries and vulnerability reporting guidance.