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.
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.
- 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
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
AI
- 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
- 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
- Universidad de Buenos Aires: $1M donation for scholarships
- Rust Foundation: $100K donation
- Gleam Programming Language: monthly donations
- Roc Programming Language: monthly donations
- Argentine Astronomical Association: $10K/year