Skip to content

@SkyLabsAI SkyLabs AI

Change the repository type filter

All

    Repositories list

    23 repositories

    • auto-docs

      Public
      BlueRock Automation Docs
      cppformal-methodsformal-verification
      cppformal-methodsformal-verificationrocq-prover
      Rocq Prover
      •1•0•1•0•Updated Apr 24, 2026Apr 24, 2026

    • BRiCk

      Public
      Formalization of C++ for verification purposes.
      cpluspluscoqcoq-formalization
      cpluspluscoqcoq-formalizationcplusplus-14cplusplus-11coq-librarycplusplus-17cplusplus-20cplusplus-23
      Rocq Prover
      •
      Other
      •17•91•15•5•Updated Apr 24, 2026Apr 24, 2026

    • brick-libcpp

      Public
      Specifications of the C++ standard library in BRiCk.
      TeX
      •
      BSD 3-Clause "New" or "Revised" License
      •2•5•6•8•Updated Apr 24, 2026Apr 24, 2026

    • rocq-agent-toolkit

      Public
      Agent infrastructure for Rocq
      Python
      •0•9•36•13•Updated Apr 23, 2026Apr 23, 2026

    • rocq

      Public
      The Rocq Prover is an interactive theorem prover, or proof assistant. It provides a formal language to write mathematical definitions, executable algorithms and…
      OCaml
      •
      GNU Lesser General Public License v2.1
      •724•0•2•2•Updated Apr 23, 2026Apr 23, 2026

    • workspace

      Public
      Workspace in which all the SkyLabs AI tooling can be cloned.
      Shell
      •0•0•8•2•Updated Apr 21, 2026Apr 21, 2026

    • aac-tactics

      Public
      Coq plugin providing tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators [maintainer=@palmskog]
      OCaml
      •
      Other
      •25•0•0•1•Updated Apr 20, 2026Apr 20, 2026

    • flocq

      Public
      Rocq Prover
      •
      GNU Lesser General Public License v3.0
      •0•0•0•0•Updated Apr 13, 2026Apr 13, 2026

    • coqhammer

      Public
      CoqHammer: An Automated Reasoning Hammer Tool for Rocq - Proof Automation for Dependent Type Theory
      OCaml
      •
      Other
      •37•0•0•0•Updated Mar 27, 2026Mar 27, 2026

    • fm-ci

      Public
      Python
      •1•0•2•0•Updated Mar 9, 2026Mar 9, 2026

    • rocq-iris

      Public
      The Rocq development for Iris
      Rocq Prover
      •
      Other
      •0•1•0•0•Updated Mar 9, 2026Mar 9, 2026

    • rocq-stdlib

      Public
      Stdlib for the Rocq Prover
      Rocq Prover
      •
      GNU Lesser General Public License v2.1
      •32•0•0•0•Updated Mar 9, 2026Mar 9, 2026

    • rocq-stdpp

      Public
      An extended "Standard Library" for Rocq
      Rocq Prover
      •
      Other
      •0•1•0•0•Updated Mar 9, 2026Mar 9, 2026

    • rocq-ext-lib

      Public
      A library of Rocq definitions, theorems, and tactics
      Rocq Prover
      •
      BSD 2-Clause "Simplified" License
      •53•0•0•0•Updated Mar 9, 2026Mar 9, 2026

    • rocq-equations

      Public
      A function definition package for Rocq
      Rocq Prover
      •
      GNU Lesser General Public License v2.1
      •55•0•0•0•Updated Mar 9, 2026Mar 9, 2026

    • rocq-lsp

      Public
      Visual Studio Code Extension and Language Server Protocol for Rocq / Coq
      OCaml
      •
      GNU Lesser General Public License v2.1
      •53•0•0•0•Updated Mar 9, 2026Mar 9, 2026

    • vsrocq

      Public
      Visual Studio Code extension for Coq
      OCaml
      •
      MIT License
      •104•0•0•0•Updated Mar 9, 2026Mar 9, 2026

    • rocq-elpi

      Public
      Rocq plugin embedding elpi
      Rocq Prover
      •
      GNU Lesser General Public License v2.1
      •74•0•0•0•Updated Mar 9, 2026Mar 9, 2026

    • elpi

      Public
      Embeddable Lambda Prolog Interpreter
      Prolog
      •
      GNU Lesser General Public License v2.1
      •45•0•0•0•Updated Mar 9, 2026Mar 9, 2026

    • fm-workspace

      Public
      Shell
      •2•0•7•1•Updated Oct 29, 2025Oct 29, 2025

    • rocq-rfcs

      Public
      Coq Enhancement Proposals
      37•0•0•1•Updated Oct 20, 2025Oct 20, 2025

    • company-coq

      Public
      A Coq IDE build on top of Proof General's Coq mode
      Emacs Lisp
      •
      GNU General Public License v3.0
      •32•0•0•0•Updated Oct 20, 2025Oct 20, 2025

    • alectryon

      Public
      A collection of tools for writing technical documents that mix Coq code and prose.
      HTML
      •
      MIT License
      •42•0•0•0•Updated Oct 20, 2025Oct 20, 2025
    ProTip! When viewing an organization's repositories, you can use the props. filter to filter by custom property.