katamaran-project/katamaran

Katamaran is a semi-automated separation logic verifier for the Sail specification language. It works on an embedded version of Sail called μSail and verifies separation logic-based contracts of functions by generating (succinct) first-order verification conditions.

GitHub repository with 20 stars and 4 forks.

Language: Rocq Prover

Topics: instruction-set-architecture, separation-logic, symbolic-execution, verification

Open provider repository

Latest metric snapshot

2026-06-05: 20 stars and 4 forks.

Trending in Rocq Prover

  1. 1. SkyLabsAI/BRiCk

    Formalization of C++ for verification purposes.

    GitHub repository with 92 stars and 16 forks.

    Trending score: 0.05; stars gained: +0; forks gained: +0.

    Language: Rocq Prover

    Topics: coq, coq-formalization, coq-library, cplusplus, cplusplus-11, cplusplus-14

  2. 2. uds-psl/MPCTT

    Modeling and Proving in Computational Type Theory

    GitHub repository with 123 stars and 13 forks.

    Trending score: 0.05; stars gained: +0; forks gained: +0.

    Language: Rocq Prover

  3. 3. takanuva/tarski-rocq

    Shrinking induction-recursion... sometimes you just wanna be small!

    GitHub repository with 10 stars and 0 forks.

    Trending score: 0.00; stars gained: +0; forks gained: +0.

    Language: Rocq Prover