AI-driven formal modeling and verification for real-world systems.
We build tools that automatically synthesize and evaluate TLA+ specifications from source code, bridging the gap between system implementations and formal correctness.
| Project | Description |
|---|---|
| Specula | Framework for synthesizing high-quality TLA+ specifications from code · TLA+ CHALLENGE Winner · Page |
| SysMoBench | Benchmark for evaluating AI on formally modeling complex real-world systems · ICLR 2026 · Paper |
A feature complete and high performance multi-group Raft library in Go.
An enterprise-grade Java-based, Apache 2.0 licensed Ethereum client https://wiki.hyperledger.org/display/besu
A production-grade java implementation of RAFT consensus algorithm.
AI-driven formal modeling for real-world systems — synthesizing and benchmarking TLA+ specifications from source code.
An industrial-grade C++ implementation of RAFT consensus algorithm based on brpc, widely used inside Baidu to build highly-available distributed systems.
CometBFT: A distributed, Byzantine fault-tolerant, deterministic state machine replication engine. A fork and successor to Tendermint Core.
Loading…
Loading…
