Skip to content
View joom's full-sized avatar

Highlights

  • Pro

Organizations

@bloomberg @CertiCoq

Block or report joom

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
Showing results

mirror of Fabrice Bellard's libbf tar releases, with fixes and CI

C 17 5 Updated Aug 19, 2025

Haskell package for construction and running of finite state transducers.

Haskell 7 1 Updated Apr 9, 2025

Verified extraction of neural network weights from Coq proofs to deployable formats

OCaml 3 Updated Feb 5, 2026

IsoCity: City building simulation game.

TypeScript 1,993 200 Updated Feb 9, 2026

An ascii (ratatui) physics based render engine for graphs (petgraph)

Rust 4 Updated Jan 28, 2026

Coi: A type-safe, component-based language for building high-performance web apps with WASM and fine-grained reactivity.

C++ 514 12 Updated Feb 12, 2026

Alternative interpretation of logical atomicity in Iris

Rocq Prover 6 Updated Nov 26, 2025

Semantic Search & Call Graphs for AI Agents (100% Local)

Go 1,214 97 Updated Feb 10, 2026

Formalizing the stable marriage problem and the Gale-Shapley algorithm in Lean

Lean 4 1 Updated Jan 13, 2026

Türkçe'ye daha yakın deneysel programlama dili / Experimental programming language closer to Turkish

Common Lisp 12 Updated Jun 14, 2024
C++ 4 Updated Dec 16, 2025

Formalization of the proofs in the POPL 2026 paper Typing Strictness

Rocq Prover 8 Updated Nov 14, 2025

LLM-powered typed-holes

Haskell 55 1 Updated May 2, 2025

The mechanized formalization of logical pinning, a lightweight borrowing model and proof discipline for precise reasoning about container-internal pointers.

Rocq Prover 7 Updated Jan 25, 2026

Verifying a Lazy Concurrent List-Based Set Algorithm in Iris

Coq 1 Updated Feb 5, 2025

Tampio: An object-oriented programming language made to resemble Finnish

Python 245 5 Updated May 7, 2019

Formalization of Vickrey-Clarke-Groves auction algorithm and mechanism (this repository is here for reference only; see mech.v for an up-to-date version)

Coq 4 Updated Mar 31, 2021

See README for more info

Haskell 2 Updated Jun 22, 2019

The STM API we know and love, but useable in more circumstances

Haskell 7 Updated Aug 11, 2023

Rocqet proof language

Rocq Prover 28 Updated Aug 11, 2025
OCaml 3 Updated Feb 12, 2026

Minimax verification

Dafny 2 Updated Jan 28, 2026

american fuzzy lop - a security-oriented fuzzer

C 4,059 667 Updated Jul 5, 2021

Safe interop between Rust and C++

Rust 6,656 396 Updated Feb 10, 2026

A bidirectional bindings generator for C++ and Rust.

Rust 974 60 Updated Feb 12, 2026

In collaboration with the Rust Foundation, Rust Project, and appropriate external stakeholders, make C++ and Rust interoperability easily accessible and approachable to the widest possible audience

69 2 Updated Nov 12, 2024

Structural search for Rust

Rust 14 1 Updated Nov 4, 2025

Specifications of the C++ standard library in BRiCk.

TeX 4 1 Updated Feb 11, 2026

Financial Contracts eDSL & Valuation in Haskell. Final year dissertation project for my bachalors degree at University of Nottigham.

Haskell 17 Updated Oct 4, 2025
Next