Skip to content
View liyishuai's full-sized avatar
🐔
I program with Coq !
🐔
I program with Coq !
256 followers · 164 following

Sponsors

@sparanoid

Achievements

Achievement: StarstruckAchievement: YOLOAchievement: Pair Extraordinairex2Achievement: Galaxy BrainAchievement: QuickdrawAchievement: Arctic Code Vault ContributorAchievement: Pull Sharkx3

Achievements

Achievement: StarstruckAchievement: YOLOAchievement: Pair Extraordinairex2Achievement: Galaxy BrainAchievement: QuickdrawAchievement: Arctic Code Vault ContributorAchievement: Pull Sharkx3

Organizations

@rocq-prover @plclub @rocq-community @ocaml-community

Block or report liyishuai

Block user

Prevent this user from interacting with your repositories and sending you notifications. Learn more about blocking users.

You must be logged in to block users.

Maximum 250 characters. Please don’t include any personal information such as legal names or email addresses. Markdown is supported. This note will only be visible to you.
Report abuse

Contact GitHub support about this user’s behavior. Learn more about reporting abuse.

Report abuse

  • coq Public

    Forked from rocq-prover/rocq

    Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive develo…

    OCaml 1 GNU Lesser General Public License v2.1 Updated May 1, 2026

  • opam Public

    Forked from rocq-prover/opam

    Archive for all Coq related OPAM packages organized in various repositories

    OCaml 1 GNU Lesser General Public License v2.1 Updated May 1, 2026

  • gswap Public

    交易所

    HTML GNU Affero General Public License v3.0 Updated May 1, 2026

  • unison Public

    Forked from bcpierce00/unison

    Unison file synchronizer

    OCaml GNU General Public License v3.0 Updated May 1, 2026

  • Shadowrocket Public

    Forked from LOWERTOP/Shadowrocket

    Shadowrocket 使用手册补完计划

    Updated May 1, 2026

  • certicoq Public

    Forked from CertiRocq/certirocq

    A Verified Compiler for Gallina, Written in Gallina

    Rocq Prover 1 MIT License Updated Apr 29, 2026

  • rust-rocksdb Public

    Forked from tikv/rust-rocksdb

    rust wrapper for rocksdb

    Rust Apache License 2.0 Updated Apr 29, 2026

  • ci Public

    Forked from PingCAP-QE/ci

    PingCAP's CI configurations and scripts.

    Groovy Apache License 2.0 Updated Apr 29, 2026

  • titan Public

    Forked from tikv/titan

    A RocksDB plugin for key-value separation, inspired by WiscKey.

    C++ Apache License 2.0 Updated Apr 28, 2026

  • rocksdb Public

    Forked from tikv/rocksdb

    A library that provides an embeddable, persistent key-value store for fast storage.

    C++ GNU General Public License v2.0 Updated Apr 28, 2026

  • tikv Public

    Forked from tikv/tikv

    Distributed transactional key-value database, originally created to complement TiDB

    Rust Apache License 2.0 Updated Apr 27, 2026

  • ublock-static-filters Public

    Gist -> GitHub mirror for auto sync

    Updated Apr 27, 2026

  • SubConv Public

    Forked from SubConv/SubConv

    Yet Another Subscription Converter for Clash

    Python Mozilla Public License 2.0 Updated Apr 26, 2026

  • pd Public

    Forked from tikv/pd

    Placement driver for TiKV

    Go Apache License 2.0 Updated Apr 24, 2026

  • hibikilogy.github.io Public

    Forked from hibikilogy/hibikilogy.github.io

    《京吹学报》

    HTML Updated Apr 17, 2026

  • base Public

    Forked from janestreet/base

    Standard library for OCaml

    OCaml MIT License Updated Apr 16, 2026

  • openclaw Public

    Forked from openclaw/openclaw

    Your own personal AI assistant. Any OS. Any Platform. The lobster way. 🦞

    TypeScript MIT License Updated Apr 10, 2026

  • tidb Public

    Forked from pingcap/tidb

    TiDB - the open-source, cloud-native, distributed SQL database designed for modern applications.

    Go Apache License 2.0 Updated Mar 26, 2026

  • singa Public

    Forked from apache/singa

    a distributed deep learning platform

    C++ Apache License 2.0 Updated Mar 23, 2026

  • HTML5_Genetic_Cars Public

    Forked from red42/HTML5_Genetic_Cars

    A genetic algorithm car evolver in HTML5 canvas.

    JavaScript zlib License Updated Mar 13, 2026

  • evolver Public

    Forked from EvoMap/evolver

    The GEP-Powered Self-Evolution Engine for AI Agents. Genome Evolution Protocol. | evomap.ai

    JavaScript MIT License Updated Mar 11, 2026

  • shanten-number Public

    Forked from tomohxx/shanten-number

    A tool for calculating the shanten number in Japanese mahjong.

    C++ GNU Lesser General Public License v3.0 Updated Mar 6, 2026

  • QuickChick Public

    Forked from QuickChick/QuickChick

    Randomized Property-Based Testing Plugin for Coq

    Rocq Prover Other Updated Mar 4, 2026

  • etcd Public

    Forked from etcd-io/etcd

    Distributed reliable key-value store for the most critical data of a distributed system

    Go Apache License 2.0 Updated Feb 27, 2026

  • openclaw-plugin-research Public

    OpenClaw plugin for maintaining a centralized project-generic research database.

    TypeScript Mozilla Public License 2.0 Updated Feb 26, 2026

  • openclaw-13623 Public

    MIT License Updated Feb 24, 2026

  • coq-http Public

    HTTP specification in Coq, testable and verifiable

    Rocq Prover 18 2 Mozilla Public License 2.0 Updated Feb 22, 2026

  • file-sync Public

    File synchroniser specification in Coq

    Rocq Prover 3 Mozilla Public License 2.0 Updated Feb 22, 2026

  • coq-json Public

    JSON in Coq

    Rocq Prover 4 4 BSD 3-Clause "New" or "Revised" License Updated Feb 22, 2026

  • coq-async-test Public

    Testing asynchronous system

    Rocq Prover 2 1 Mozilla Public License 2.0 Updated Feb 22, 2026