Skip to content
@specula-org

specula-org

Specula-org

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.

Core Projects

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

Pinned Loading

  1. Specula Specula Public

    Specula: A framework for finding deep bugs in system code using TLA+

    Python 97 15

  2. SysMoBench SysMoBench Public

    SysMoBench: Evaluating AI on Formally Modeling Complex Real-World Systems

    TLA 11 1

  3. specula-case-studies specula-case-studies Public

    specula-case-studies

    TLA 3

Repositories

Showing 10 of 14 repositories
  • specula-case-studies Public

    specula-case-studies

    specula-org/specula-case-studies’s past year of commit activity
    TLA 3 0 0 0 Updated Mar 13, 2026
  • sofa-jraft Public Forked from sofastack/sofa-jraft

    A production-grade java implementation of RAFT consensus algorithm.

    specula-org/sofa-jraft’s past year of commit activity
    Java 0 Apache-2.0 1,249 0 0 Updated Mar 11, 2026
  • Specula Public

    Specula: A framework for finding deep bugs in system code using TLA+

    specula-org/Specula’s past year of commit activity
    Python 97 Apache-2.0 15 0 0 Updated Mar 10, 2026
  • specula-org/autobahn-artifact’s past year of commit activity
    Python 0 Apache-2.0 11 0 0 Updated Mar 9, 2026
  • substrate Public Forked from paritytech/substrate

    Substrate: The platform for blockchain innovators

    specula-org/substrate’s past year of commit activity
    Rust 0 Apache-2.0 2,821 0 0 Updated Mar 9, 2026
  • dragonboat Public Forked from lni/dragonboat

    A feature complete and high performance multi-group Raft library in Go.

    specula-org/dragonboat’s past year of commit activity
    Go 0 Apache-2.0 574 0 0 Updated Mar 9, 2026
  • besu Public Forked from besu-eth/besu

    An enterprise-grade Java-based, Apache 2.0 licensed Ethereum client https://wiki.hyperledger.org/display/besu

    specula-org/besu’s past year of commit activity
    Java 0 Apache-2.0 1,079 0 0 Updated Mar 9, 2026
  • .github Public

    AI-driven formal modeling for real-world systems — synthesizing and benchmarking TLA+ specifications from source code.

    specula-org/.github’s past year of commit activity
    0 0 0 0 Updated Mar 8, 2026
  • braft Public Forked from baidu/braft

    An industrial-grade C++ implementation of RAFT consensus algorithm based on brpc, widely used inside Baidu to build highly-available distributed systems.

    specula-org/braft’s past year of commit activity
    C++ 0 Apache-2.0 920 0 0 Updated Mar 2, 2026
  • cometbft Public Forked from cometbft/cometbft

    CometBFT: A distributed, Byzantine fault-tolerant, deterministic state machine replication engine. A fork and successor to Tendermint Core.

    specula-org/cometbft’s past year of commit activity
    Go 0 Apache-2.0 808 0 0 Updated Mar 2, 2026

Most used topics

Loading…