Lambda

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

How we engage
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. We've done this for over a decade. 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

  $1B in loans per year. Europe's largest revenue-based financing platform. We rebuilt and run the infrastructure.

• PropAMMs

  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

  Open-source validator sidecar we build and maintain. 40% of the Ethereum network runs our code. Grant-funded, no token.

• Ethrex

  A minimalist, zk-native Ethereum execution client we built from scratch in Rust.

• Lambdaworks

  Our cryptographic proof library, already running in production systems that move real money.

• Nous Research

  Working on 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

  18+ months building the Miden client. Execution and proving of transactions for the Miden network.

• Aligned

  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, and a wallet-as-a-service platform.

• Concrete

  Our programming language with Lean 4 integration. Verification is part of the language and the build.

• CommitLLM

  Prove a provider actually ran the model it claimed, without recomputing the inference.

30+ more open-source projects at 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 portfolio companies that are experts in theoretical cryptography and hacking: FuzzingLabs (security research and fuzzing) and 3MI Labs (theoretical cryptography).

Patronage

The tools and institutions we depend on need sustained investment, not just usage. We put money into the things we believe matter.

• 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. Most of our team graduated from UBA. We fund the next generation because public universities shouldn't have to beg for research money.

• Rust Foundation [$100k donation]

  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.

• Gleam Programming Language [Monthly donation]
• Roc Programming Language [Monthly donation]
• Argentine Astronomical Association [$10k/year]

  Annual donation covering Argentina's membership in the International Astronomical Union and sponsorship of the journal Astronomy & Astrophysics.

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.

From our blog

• Verified Code Optimization in Lean 4: Proven-Correct C Code with AMO-LEAN
• If It Compiles, It Is Correct: An Introduction to Lean 4 for Engineers
• How We Made an Ethereum Rust Execution Engine 20x Faster
• Building a Minimalist Post-Quantum Ethereum Client
• Responsible Disclosure of an Exploit in Succinct's SP1 zkVM
• The Future of ZK is in RISC-V zkVMs, but the Industry Must Be Careful

More at 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

Read more about our culture:
https://github.com/lambdaclass/lambdaclass_hacking_learning_path

Interested? Email hello@lambdaclass.com with "Joining Lambda" in the subject line.

We work in person. Proofs and protocol design happen at a whiteboard, and that doesn't work over video.

Get In Touch

If you have a problem where the software has to be right, not just "probably right," we should talk.

hello@lambdaclass.com