We build software that is fast and provably correct.
We use Lean 4, Rust, and Erlang/Elixir to build systems where bugs are not acceptable. We work across blockchain infrastructure, AI, finance, aerospace, and automotive. We build verified compilers, proof systems, distributed systems, and safety-critical software. Billions of dollars flow through code we've written.
Founded by Federico Carrone. 100+ engineers specializing in formal verification, cryptography, distributed systems, and high-performance software. Part of Ergodic Group. Teams in Buenos Aires, Montevideo, and Barcelona. Since 2014.
Blog / X / GitHub / YouTube / LinkedIn
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 in Succinct's SP1 zkVM and published our findings.
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.
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, and the
high-performance backends that support them. We build
infrastructure that lets AI training scale beyond centralized clusters.
Post-Quantum Cryptography
Quantum computers will break current cryptographic schemes. We're
already building post-quantum clients and signature systems. When
the transition happens, our software will be ready.
Our Engagement Model
We don't work hourly. We don't do staff augmentation.
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've done this multiple times over the last decade. If correctness is a nice-to-have rather than a requirement, we're not the right partner.
Some of the clients we work with and can share. Many we can't.
Europe's largest revenue-based financing platform. We helped lower infrastructure costs on a system that processes around $1B in loans per year.
Ethereum validator sidecar now running on close to 40% of the network. Open source, grant-funded, no token.
Building Psyche, a Rust-based decentralized AI training network that lets anyone contribute compute to model training over standard broadband.
18+ months building the Miden client. Execution and proving of transactions for the Miden network.
Partnership on 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.
We built the Rust Cairo VM that powers Starknet, taking sequencer throughput from 30K to 220K Cairo steps per second.
We work closely with other Ergodic portfolio companies that are experts in theoretical cryptography and hacking: FuzzingLabs (security research and fuzzing) and 3MI Labs (theoretical cryptography).
The tools and institutions we depend on need sustained investment, not just usage. We put money into the things we believe matter.
Scholarships for thesis students in Computer Science, Mathematics, and Data Sciences at the Faculties of Engineering and Exact Sciences. Most of our team graduated from UBA. We fund the next generation because public universities shouldn't have to beg for research money.
Rust is the backbone of most of what we build. We donated $100k to the Rust Foundation because the language's long-term health is inseparable from ours. Read more.
Annual donation covering Argentina's membership in the International Astronomical Union and sponsorship of the journal Astronomy & Astrophysics.
If you have a problem where the software has to be right, not just "probably right," we should talk.
More at blog.lambdaclass.com
We're looking for people who work on formal verification, compilers, systems programming, cryptography, and AI. If you care about getting things right, actually right, not just passing tests, talk to us.
60% of applicants do not complete the selection process. 50% of those who join do not continue after the first year. We're selecting for people who can navigate ambiguity, exercise judgment on hard problems, and thrive in an environment where the answer isn't always clear.
Current openings:
Read more about our culture:
https://github.com/lambdaclass/lambdaclass_hacking_learning_path
Interested? hello@lambdaclass.com.
For the type of work we do, remote work is not effective.
Testing tells you "I tried 10,000 inputs and it didn't break." Formal verification tells you "it can't break. Here's the proof."
Tests cover cases you think of. Proofs cover all of them. That's the difference between hoping your software works and knowing it does.
We use Lean 4 for this. A proof assistant that doubles as a programming language. The proofs are readable by humans and checkable by machines.
C-level performance with compile-time guarantees against memory bugs, data races, and use-after-free errors. No garbage collector. For execution clients, proof systems, and VMs, it's the best tool available.
When the system has to stay up. The BEAM VM gives us lightweight processes, fault isolation, and hot code upgrades. Millions of concurrent connections, low latency, near-zero downtime.
Blockchain Infrastructure
Ethereum execution client in Rust. L1 and L2 support. We made it 20x faster through profiling-driven optimization.
Lean Ethereum consensus client written in Rust.
Cryptographic proof library used in production. SNARKs, STARKs, and composable components for building custom proof systems.
Rust implementation of the Cairo VM for provable programs.
Verification
Verified mathematical optimizations in Lean 4. Proofs that compiler transformations preserve semantics, with code generation for production use.
Formally verified data structures and algorithms in Lean 4, with extracted high-performance implementations.
Verifiable computation infrastructure targeting RISC-V. Prove that arbitrary programs executed correctly without re-running them.
Formally verified toolkit for building compilers. Verified passes and transformations in Lean 4.
Compilers & Languages
Compiler from Cairo's Sierra IR to MLIR. Native execution for provable programs.
Programming language with Lean 4 integration for scalable, formally verifiable systems.
