Mike Dodds

lean-aristotle-mcp. Python

jstar-old. jStar is a verification tool based on separation logic.

starling-tool. An automatic verifier for concurrent algorithms.

denyguarantee-v3. Lean

acl2-mcp. Python

acl2-swf-experiments. Common Lisp

lean-c-semantics. Lean

stellite-tool. A tool for verifying C/C++ program transformations. Based on Alloy.

claudes-cycles-lean. Lean

adler-proofs. Adler-32 verified twice: a comparative formal-verification case study using Lean+Aeneas and Verus, with both proofs sorry-free and verifying the same byte-at-a-time spec.

ACL2Lean. ACL2-to-Lean4 bridge with parser, evaluator, translator, and proving tactics

aeneas-vcvio-demos. End-to-end demos: real Rust → Aeneas → Lean → VCVio game-based cryptographic security proofs (no sorry; make verify gates the axioms)