Lambdaclass

Lambda

We are a deep tech engineering firm founded in 2014. We build software that is fast and provably correct using Lean 4, Rust, and Erlang/Elixir. With 100+ engineers specializing in formal verification, cryptography, distributed systems, and high-performance software, we operate teams in Buenos Aires, Montevideo, and Barcelona as part of Ergodic Group.

Philosophy

Most software relies on faith rather than proof. We advocate for mathematical guarantees about software behavior. Formal verification is an evolution beyond memory safety: the machine checks the reasoning, the code is public by default, and correctness is a property of the system, not a hope.

Areas of Work

Verified Optimization
Verifiable Computation (zero-knowledge proofs, verifiable execution)
High-Performance Systems
Distributed Systems (consensus, P2P networking, fault-tolerant architectures)
Safety-Critical Software (aerospace, automotive, finance)
Artificial Intelligence
Engineering Software
Post-Quantum Cryptography

Selected Projects

Blockchain Infrastructure

Ethrex — Ethereum execution client in Rust (20x performance optimization)
Ethlambda — Lean Ethereum consensus client, post-quantum ready
Lambda Ethereum Consensus — Elixir-based consensus client
Lambdaworks — Cryptographic proof library (SNARKs, STARKs)
Cairo VM — Rust Cairo VM implementation powering Starknet's sequencer (30K–220K Cairo steps/sec)
Cairo Native — Sierra IR to MLIR compiler

Verification & Compilers

AMO-Lean — Verified optimizations in Lean 4
Lambda Compiler Kit — Formally verified compiler toolkit
Concrete — Programming language with Lean 4 integration

Tekton — Self-hosted AI coding agent platform

Engineering

Dedaliano — Browser-based structural analysis tool

Systems & Infrastructure

Spawned — Erlang-style actor model for Rust
eth-agent — Ethereum interactions for AI agents

Selected Clients

Levenue — Rebuilt and operates infrastructure for Europe's largest revenue-based financing platform ($1B in loans annually)
Commit-Boost — Open-source validator sidecar securing 40% of Ethereum validators
Nous Research — Building Psyche, a decentralized AI training network in Rust
Miden — 18+ months developing the Miden client for transaction execution and proving
Aligned — ZK security research, SP1 exploit discovery, Ethrex integration, and LambdaVM development
Starknet — Built the Rust Cairo VM powering the sequencer

Patronage