# Lambda (LambdaClass)

> We build software that is fast and provably correct. 100+ engineers specializing in formal verification, cryptography, distributed systems, and high-performance software. Founded by Federico Carrone. Part of Ergodic Group. Teams in Buenos Aires, Montevideo, and Barcelona. Since 2014.

## Canonical URLs

- Homepage: https://lambdaclass.com/
- Sitemap: https://lambdaclass.com/sitemap.xml
- Full profile: https://lambdaclass.com/llms-full.txt

We use Lean 4, Rust, and Erlang/Elixir to build systems where bugs are expensive: zero-knowledge proof systems and Ethereum infrastructure, formally verified compilers and code, and high-performance distributed systems. Our software runs on 40% of Ethereum validators and secures and moves billions in value in production.

## What we believe

Tests miss cases. Reviews miss assumptions. Production finds the rest. And now AI writes more of the code, with fewer people reading it, so the case for actually proving software behaves is stronger than ever. For the systems we work on, test coverage is not the same as a checked proof.

Rust made software safer without giving up performance: it handles memory safety. Formal verification handles the next part, the program logic. We use Lean 4 to prove a program does what it should, and the compiler checks the proof. That wasn't practical five years ago; it is now. We found and [responsibly disclosed a critical exploit](https://blog.lambdaclass.com/responsible-disclosure-of-an-exploit-in-succincts-sp1-zkvm-found-in-partnership-with-3mi-labs-and-aligned-which-arises-from-the-interaction-of-two-distinct-security-vulnerabilities/) in Succinct's SP1 zkVM, and we hold our own code to the same bar.

## What we do

- **Verifiable computation & blockchain infrastructure**: Zero-knowledge proof systems, execution and consensus clients, custom VMs. The work is verifiable end to end: you can check that a computation ran correctly without running it again yourself.
- **Formal verification**: We prove programs correct in Lean 4, then generate the production code from those proofs. We do this for work in aerospace, automotive, and finance, where a bug costs lives or millions.
- **High-performance & distributed systems**: Rust, RISC-V, GPU-optimized code, and Erlang/Elixir for systems with strict latency and uptime requirements. We build infrastructure that coordinates across thousands of nodes and keeps running when individual components fail, from Ethereum clients to decentralized AI training networks. Our consensus client, Ethlambda, is built to be post-quantum ready.

## Engagement model

We take ownership of hard technical systems and stay responsible for them. We come in, fix the problems, rebuild the team if it needs rebuilding, and stick around as long-term partners, often as the entire tech team. The companies we work with can't ship software that's wrong: regulated industries, financial infrastructure, systems where failure is measured in dollars or lives. If you just need extra developers, we're not the right fit.

## What we've built

Things we've built, for clients and in the open. Some clients we can name; many we can't.

- [Levenue](https://www.levenue.com/): $1B in loans per year. Europe's largest revenue-based financing platform. We rebuilt and run the infrastructure.
- [PropAMMs](https://pamm.wtf/): Onchain market making we built with Titan Builder. About $10M in daily volume after two weeks, at prices 1.5 bps tighter than Binance and 8 bps tighter than Uniswap on ETH.
- [Commit-Boost](https://www.commit-boost.org/): Open-source validator sidecar we build and maintain. 40% of the Ethereum network runs our code. Grant-funded, no token.
- [Ethrex](https://github.com/lambdaclass/ethrex): A minimalist, zk-native Ethereum execution client we built from scratch in Rust.
- [Lambdaworks](https://github.com/lambdaclass/lambdaworks): Our cryptographic proof library, already running in production systems that move real money.
- [Nous Research](https://nousresearch.com/): Working on [Hermes Agent](https://github.com/nousresearch/hermes-agent), Nous's open-source personal AI agent with persistent memory that creates and improves its own skills from experience. We also build Psyche, a Rust-based decentralized AI training network that lets anyone contribute compute to model training over standard broadband.
- [Miden](https://polygon.technology/polygon-miden): 18+ months building the Miden client. Execution and proving of transactions for the Miden network.
- [Aligned](https://alignedlayer.com/): ZK security research, including the SP1 exploit discovery, and Ethrex integration for Aligned's rollup infrastructure. We're also building [LambdaVM](https://github.com/yetanotherco/lambda_vm), a RISC-V zkVM designed to power Ethereum, and a wallet-as-a-service platform.
- [Concrete](https://github.com/lambdaclass/concrete): Our programming language with Lean 4 integration. Verification is part of the language and the build.
- [CommitLLM](https://commitllm.com): Prove a provider actually ran the model it claimed, without recomputing the inference.

30+ more open-source projects at [github.com/lambdaclass](https://github.com/lambdaclass), including Ethlambda, Lambda Ethereum Consensus, CairoVM, Cairo Native, AMO-Lean, Lambda Compiler Kit, Spawned, Dedaliano, eth-agent, and Tekton.

We work closely with other [Ergodic](https://ergodicgroup.com/) portfolio companies that are experts in theoretical cryptography and hacking: FuzzingLabs (security research and fuzzing) and 3MI Labs (theoretical cryptography).

## Our Stack

Lean 4 for formal verification: machine-checked proofs that software does what it's supposed to do. Not testing. Proving. Rust for performance-critical systems: C-level speed with compile-time guarantees against memory bugs and data races. Erlang/Elixir for systems that have to stay up: fault isolation, hot code upgrades, millions of concurrent connections.

## Patronage

- Universidad de Buenos Aires [$1M donation]: Scholarships for thesis students in Computer Science, Mathematics, and Data Sciences at the Faculties of Engineering and Exact Sciences.
- [Rust Foundation](https://www.rust-lang.org/) [$100k donation]: Rust is the backbone of most of what we build. [Read more](https://rustfoundation.org/media/lambdaclass-donates-100k-to-the-rust-foundation/).
- [Gleam Programming Language](https://gleam.run/) [Monthly donation]
- [Roc Programming Language](https://www.roc-lang.org/) [Monthly donation]
- Argentine Astronomical Association [$10k/year]: Annual donation covering Argentina's membership in the International Astronomical Union.

## Blog

- [Verified Code Optimization in Lean 4: Proven-Correct C Code with AMO-LEAN](https://blog.lambdaclass.com/amo-lean-towards-formally-verified-optimization-via-equality-saturation-in-lean-4/)
- [If It Compiles, It Is Correct: An Introduction to Lean 4 for Engineers](https://blog.lambdaclass.com/if-it-compiles-it-is-correct-almost-an-introduction-to-lean-4-for-zk-systems-and-engineering-2/)
- [How We Made an Ethereum Rust Execution Engine 20x Faster](https://blog.lambdaclass.com/engineering-ethereums-speed-how-we-made-ethrex-20x-faster/)
- [Building a Minimalist Post-Quantum Ethereum Client](https://blog.lambdaclass.com/building-a-minimalist-post-quantum-ethereum-client-ethlambdas-architecture/)
- [Responsible Disclosure of an Exploit in Succinct's SP1 zkVM](https://blog.lambdaclass.com/responsible-disclosure-of-an-exploit-in-succincts-sp1-zkvm-found-in-partnership-with-3mi-labs-and-aligned-which-arises-from-the-interaction-of-two-distinct-security-vulnerabilities/)
- [The Future of ZK is in RISC-V zkVMs, but the Industry Must Be Careful](https://blog.lambdaclass.com/the-future-of-zk-is-in-risc-v-zkvms-but-the-industry-must-be-careful-how-succincts-sp1s-departure-from-standards-causes-bugs/)
- More at [blog.lambdaclass.com](https://blog.lambdaclass.com/)

## Work with us

We're looking for people who work on formal verification, compilers, systems programming, cryptography, and AI. If that's the kind of work you want to do, talk to us. Current openings: Lean 4 proof engineers, Rust systems engineers, Business development, RISC-V engineers. We work in person. Proofs and protocol design happen at a whiteboard, and that doesn't work over video.

To apply, email hello@lambdaclass.com with "Joining Lambda" in the subject line. Culture: [https://github.com/lambdaclass/lambdaclass_hacking_learning_path](https://github.com/lambdaclass/lambdaclass_hacking_learning_path)

## Links

- [GitHub](https://github.com/lambdaclass/)
- [X](https://x.com/class_lambda)
- [YouTube](https://www.youtube.com/@lambdaclass/)
- [LinkedIn](https://www.linkedin.com/company/lambdaclass/)
- [Founder](https://federicocarrone.com/)

## Contact

- Email: hello@lambdaclass.com