inline-imports.py github.com

Creates stand-alone source files from developments by inlining the loading of all dependencies.

find-bug.py github.com

Automatically minimizes source files producing an error, creating small test cases for Coq bugs.

absolutize-imports.py github.com

Processes source files to make loading of dependencies robust against shadowing of file names.

Official Coq wiki github.com

VsCoq Legacy github.com

Backwards-compatible extension for the Visual Studio Code and VSCodium editors using Coq's legacy XML protocol.

Dune dune.build

Composable and opinionated build system for OCaml and Coq (former jbuilder).

Coq tag on Theoretical Computer Science Stack Exchange cstheory.stackexchange.com

Program Logics for Certified Compilers cs.princeton.edu

Book that explains how to construct program logics using separation logic, accompanied by a formal model in Coq which is applied to the Clight programming language and other examples.

Official Coq Zulip chat coq.zulipchat.com

Planet Coq link aggregator coq.pl-a.net

Official Coq standard library coq.inria.fr

coqdoc coq.inria.fr

Standard documentation tool that generates LaTeX or HTML files from Coq code.

Ltac2 coq.inria.fr

Experimental typed tactic language similar to Coq's classic Ltac language.

coq_makefile coq.inria.fr

Build tool distributed with Coq and based on generating a makefile.

CoqIDE coq.inria.fr

Standalone graphical tool for interacting with Coq.

Official Coq manual coq.inria.fr

Coq Package Index coq.inria.fr

Collection of Coq packages based on opam.

Coq Zulip chat archive coq.gitlab.io

Official Coq Discourse forum coq.discourse.group

Tactician coq-tactician.github.io

Interactive tool which learns from previously written tactic scripts across all the installed Coq packages and suggests the next tactic to be executed or tries to automate proof synthesis fully.

Coq Tactics in Plain English charlesaverill.github.io

Guide to Coq tactics with explanations and examples.

Foundations of Separation Logic chargueraud.org

Introduction to using separation logic to reason about sequential imperative programs in Coq.

Coq in a Hurry cel.archives-ouvertes.fr

Introduction to how Coq can be used to define logical concepts and functions and reason about them.

Lysxia's blog blog.poisson.chat

Certified Programming with Dependent Types adam.chlipala.net

Textbook about practical engineering with Coq which teaches advanced practical tricks and a very specific style of proof.

Move and Sui with Sam Blackshear from Mysten Labs zeroknowledge.fm

Move AMA covering Move origin story twitter.com

Comparing Diem-style Move and Sui Move sui.io

Move and SmartContract Development starcoinorg.github.io

Maintained by the Starcoin team.

The Move Prover research.facebook.com

Exact and Linear-Time Gas-Cost Analysis research.facebook.com

Move IntelliJ plugin plugins.jetbrains.com

Maintained by the Pontem team (source code).

Move Playground playground.pontem.network

Like Remix for Move. Alpha version of a Web IDE. See instructions. Maintained by the Pontem team.

Movey movey.net

A crates.io-style repository of Move packages.

Move Patterns move-patterns.com

A book on Move software design patterns maintained by @villesundell.

Move Book move-language.github.io

Move book maintained by the Move core team (中文).

MoveChina move-china.com

The largest Chinese community for the Move programming language.

Move Book move-book.com

Move book maintained by @damirka (中文).

Aptos-movevm Denial of Service Vulnerability medium.com

Comparing Move and Rust smart contract development medium.com

Starcoin IDE marketplace.visualstudio.com

Maintained by the Starcoin team (source code).

Move VS Code plugin marketplace.visualstudio.com

Maintained by the Move core team (source code).

Move Language imcoding.online

Interactive Move language course, free for everyone, maintained by imcoding.online (中文).

Token github.com

Another ERC20-like Token. Deployed on Starcoin.

STC github.com

A token that instantiates the Starcoin standard above. Deployed on Starcoin.

NFT github.com

An ERC721-like token. Deployed on Starcoin.

Merkle Airdrop github.com

Utility for airdropping a large number of NFTs. Deployed on Starcoin.

Math github.com

Math utility functions. From Starcoin.

DAO github.com

For on-chain proposals and voting. Deployed on Starcoin.

Account github.com

Fork of the above. From Starcoin.