# 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 not acceptable. We work across blockchain infrastructure, AI, finance, aerospace, automotive, and engineering. We build verified compilers, proof systems, distributed systems, and safety-critical software. Our code secures and moves billions in value across production systems.

## What we believe

Most software is built on faith. Faith that tests covered the right cases, that the reviewer caught the edge case, that the system behaves correctly under conditions nobody anticipated. We don't think that's good enough for infrastructure that people depend on.

AI is generating more code than ever, with less human review. The need for mathematical guarantees about software behavior is growing, not shrinking.

Rust proved you can make software safer without sacrificing performance. Formal verification is the next step: not just memory safety, but proving your logic is right. Tools like Lean 4 make this practical today in ways it wasn't five years ago. Mathematical proof is not perfectionism. It's the only honest answer to the question: does this work?

We write software where the machine checks the reasoning, the code is public by default, and correctness is a property of the system, not a hope. We discovered 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 published our findings.

## What we do

- **Verified Optimization**: We prove optimizations correct in Lean 4, then generate production code from those proofs. The math says it's right, and the machine checks the math.
- **Verifiable Computation**: Zero-knowledge proof systems and verifiable execution environments. You can verify a computation happened correctly without re-running it.
- **High-Performance Systems**: Rust, RISC-V, GPU-optimized code, Erlang/Elixir for high-throughput backends with strict latency requirements. Execution clients, proof infrastructure, custom VMs.
- **Distributed Systems**: Consensus protocols, peer-to-peer networking, fault-tolerant architectures. From Ethereum execution and consensus clients to decentralized training networks and actor-based concurrency in Rust. We build systems that coordinate across thousands of nodes and keep running when individual components fail.
- **Safety-Critical Software**: Aerospace, automotive, finance. Industries where a bug can kill people or lose millions. We write software with machine-checked proofs that it does what it's supposed to.
- **AI**: Decentralized training networks, inference systems, autonomous coding agents, and the high-performance backends that support them. We build infrastructure that lets AI training scale beyond centralized clusters and agents that ship code without human intervention.
- **Engineering Software**: Structural analysis, simulation, and scientific computing tools. Browser-based applications that bring professional-grade engineering to anyone with a web browser.
- **Post-Quantum Cryptography**: Quantum computers will break current cryptographic schemes. We're already building post-quantum clients and signature systems.

## Engagement model

We become the engineering core. We come in, fix the technical problems, rebuild the team if needed, and stay as long-term partners. In many cases we become the entire tech team. We work with companies where software correctness is a hard requirement: regulated industries, financial infrastructure, systems where failure is measured in dollars or lives. If you need extra developers, we're not the right fit.

## Selected work

- [Levenue](https://www.levenue.com/): $1B in loans per year. Europe's largest revenue-based financing platform. We rebuilt and run the infrastructure.
- [Commit-Boost](https://www.commit-boost.org/): 40% of Ethereum validators. Open-source validator sidecar, grant-funded, no token.
- [Nous Research](https://nousresearch.com/): Building 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, a RISC-V zkVM designed to power Ethereum.
- [Starknet](https://www.starknet.io/): 30K to 220K Cairo steps per second. We built the Rust Cairo VM that powers Starknet's sequencer.

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).

## Technology

### Blockchain Infrastructure

- [Ethrex](https://github.com/lambdaclass/ethrex): Ethereum execution client in Rust. L1 and L2 support. We made it 20x faster through profiling-driven optimization.
- [Ethlambda](https://github.com/lambdaclass/ethlambda): Lean Ethereum consensus client in Rust. Post-quantum ready.
- [Lambdaworks](https://github.com/lambdaclass/lambdaworks): Cryptographic proof library used in production. SNARKs, STARKs, and composable components for building custom proof systems.
- [CairoVM](https://github.com/lambdaclass/cairo-vm): Rust implementation of the Cairo VM for provable programs.

### Verification & Compilers

- [AMO-Lean](https://github.com/lambdaclass/amo-lean): Verified mathematical optimizations in Lean 4. Proofs that compiler transformations preserve semantics, with code generation for production use.
- Verified Libraries: Formally verified data structures and algorithms in Lean 4, with extracted high-performance implementations.
- RISC-V Verifiable Computation: Verifiable computation infrastructure targeting RISC-V. Prove that arbitrary programs executed correctly without re-running them.
- [Lambda Compiler Kit](https://github.com/lambdaclass/lambda_compiler_kit): Formally verified toolkit for building compilers. Verified passes and transformations in Lean 4.
- [Cairo Native](https://github.com/lambdaclass/cairo_native): Compiler from Cairo's Sierra IR to MLIR. Native execution for provable programs.
- [Concrete](https://github.com/lambdaclass/concrete): Programming language with Lean 4 integration for scalable, formally verifiable systems.

### AI

- [Tekton](https://github.com/lambdaclass/tekton): Self-hosted AI coding agent platform. Submit tasks, get pull requests. Runs on NixOS with isolated containers on bare metal.

### Engineering

- [Dedaliano](https://github.com/lambdaclass/dedaliano): Browser-based structural analysis. Model, calculate, and visualize 2D/3D bar structures using the Direct Stiffness Method.

### Systems & Infrastructure

- [Spawned](https://github.com/lambdaclass/spawned): Erlang-style actor model for Rust. Write sequential code, get concurrency for free.
- [eth-agent](https://github.com/lambdaclass/eth-agent): One-liner Ethereum interactions for AI agents. Stablecoin transfers, token swaps, cross-chain bridging with built-in spending limits.

## 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. Current openings: Lean 4 proof engineers, Rust systems engineers, Business development, RISC-V engineers. For the type of work we do, remote work is not effective.

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