Skip to content
View hengxin's full-sized avatar
🎯
Focusing
🎯
Focusing

Block or report hengxin

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 supported. This note will be visible to only you.
Report abuse

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

Report abuse

Starred repositories

13 stars written in Rocq Prover
Clear filter

The CompCert formally-verified C compiler

Rocq Prover 2,063 240 Updated Oct 20, 2025

Formal Reasoning About Programs

Rocq Prover 711 94 Updated Nov 3, 2025

A framework for formally verifying distributed systems implementations in Coq

Rocq Prover 609 56 Updated Jun 27, 2025

Verified Software Toolchain

Rocq Prover 475 96 Updated Nov 10, 2025

A Learning Environment for Theorem Proving with the Coq proof assistant

Coq 415 53 Updated Jun 30, 2023

A formalization of geometry in Coq based on Tarski's axiom system

Coq 200 27 Updated May 8, 2025

An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework

Coq 191 19 Updated Dec 8, 2023

A framework for smart contract verification in Coq

Rocq Prover 124 22 Updated Oct 27, 2025

Modeling and Proving in Computational Type Theory

Rocq Prover 117 13 Updated Aug 6, 2025

A mechanisation of Wasm in Coq(Rocq)

Rocq Prover 110 13 Updated Aug 20, 2025

Coq Lecture Notes (WIP)

Coq 56 11 Updated Oct 17, 2020

A framework for verification of causal consistency for distributed key-value stores and their clients in Coq [maintainer=@palmskog]

Coq 32 7 Updated Dec 30, 2023
Coq 29 1 Updated Mar 4, 2024