Skip to content
View pabloski80's full-sized avatar
16 followers · 367 following

Achievements

Achievement: Quickdraw

Achievements

Achievement: Quickdraw

Block or report pabloski80

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

Lists (16)

Sort Name ascending (A-Z)
Sort by
Name ascending (A-Z) Name descending (Z-A) Newest Oldest Last updated

Starred repositories

7 stars written in Rocq Prover
Clear filter

AbsInt / CompCert

The CompCert formally-verified C compiler

Rocq Prover 2,061 241 Updated Oct 20, 2025

mit-plv / fiat-crypto

Cryptographic Primitive Code Generation by Fiat

Rocq Prover 779 157 Updated Nov 3, 2025

mit-plv / bedrock2

A work-in-progress language and compiler for verified low-level programming

Rocq Prover 318 51 Updated Oct 29, 2025

mit-plv / fiat

Mostly Automated Synthesis of Correct-by-Construction Programs

Rocq Prover 154 35 Updated Sep 28, 2025

ymherklotz / vericert

A formally verified high-level synthesis tool based on CompCert and written in Coq.

Rocq Prover 94 5 Updated Sep 5, 2025

mit-plv / bedrock

Coq library for verified low-level programming

Coq 60 6 Updated Jun 15, 2017

plum-umd / checkedc

Contributions to Microsoft's Checked C project developed by PLUMmers

Coq 11 8 Updated Dec 1, 2023

Starred topics