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. Blockchain infrastructure, verified compilers, proof systems, safety-critical software. Billions of dollars flow through code we've written.
100+ engineers. Founded in 2014. Part of Ergodic Group. Teams in Buenos Aires, Montevideo, and Barcelona.
Links:
More at blog.lambdaclass.com
Most software is fragile. We ship code that controls financial systems, vehicles, aircraft, and critical infrastructure, yet we still rely on testing to catch bugs. Testing is better than nothing, but it only checks the cases you think of.
Meanwhile, AI is generating more code than ever. That's great for speed, but it makes the correctness problem worse. More code, written faster, with less human review. The need for mathematical guarantees about software behavior is growing, not shrinking.
Rust already proved that 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.
That's why Lambda exists. We've been building this kind of software since 2014. The world needs software you can prove works. We know how to build it.
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 & Verifiable AI
AI systems where you need to know the output is correct, not just
plausible. Verified inference pipelines and provable guarantees on
model behavior.
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.
ZK proof systems, execution clients, verifiable computation. We've been building this infrastructure since 2018.
AI that you can actually trust. Verified inference, provable guarantees on model outputs. Not just "seems to work."
Control systems and flight software that has to work. Formal proofs, not just test suites.
Trading systems, settlement logic, smart contracts. Bugs here cost real money. We prove they don't exist.
Embedded software for vehicles. When the code controls brakes and steering, you want mathematical proof it's correct.
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.
We believe in transparency: both our selection process and the foundational year are demanding. They're designed to challenge you and help you grow.
60% of applicants do not complete the selection process. 50% of those who join do not continue after the first year due to cultural, technical, or methodological differences. 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.
Note: For the type of work we do, we think remote work is not particularly effective.
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.
Blockchain Infrastructure
Ethereum execution client in Rust. L1 and L2 support. We made it 20x faster through profiling-driven optimization. 800+ GitHub stars.
Lean Ethereum consensus client written in Rust.
Cryptographic proof library used in production. SNARKs, STARKs, and composable components for building custom proof systems. 700+ GitHub stars.
Rust implementation of the Cairo VM for provable programs. 570+ GitHub stars.
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. 310+ GitHub stars.
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.
Most systems languages make you choose between speed and safety. Rust doesn't. Its ownership model catches memory bugs, data races, and use-after-free errors at compile time. No garbage collector, no runtime overhead.
For the kind of software we build (execution clients, proof systems, VMs), Rust gives us C-level performance with guarantees that C can't provide. It's not perfect, but it's the best tool that exists right now for writing fast software that doesn't crash.
Some systems need to stay up no matter what. Telecom switches, messaging backends, financial systems that can't go down for maintenance. Erlang was built for this. It's been doing it since the 80s.
The BEAM VM gives you lightweight processes, fault isolation, and hot code upgrades. If one process crashes, the rest keep running. Elixir brings modern syntax and tooling to the same runtime.
When we need high-throughput backends that handle millions of concurrent connections with low latency and near-zero downtime, Erlang/Elixir is what we reach for.
We support projects we believe in through sponsorships, donations, and collaboration.
If you have a problem where the software has to be right, not just "probably right," we should talk.
