Stars
Claude skills for Lean 4 theorem proving
A Lean tactic for Canonical, a search procedure for terms in dependent type theory.
Verification infrastructure for the Isabelle/HOL interactive proof assistant
Verina (Verifiable Code Generation Arena) is a high-quality benchmark enabling a comprehensive and modular evaluation of code, specification, and proof generation as well as their compositions.
Verification tool for distributed protocols based on inductive proof decomposition.
Quickly rewrite git repository history (filter-branch replacement)
FANDANGO is a language-based fuzzer that leverages formal input specifications (grammars) combined with constraints to generate diverse sets of valid inputs for programs under test.
Asterinas is a secure, fast, and general-purpose OS kernel, written in Rust and providing Linux-compatible ABI.
Loom is a framework for automated generation of foundational multi-modal verifiers. This repository is a mirror with stable snapshots. Submit issues and PRs here.
A list of known attacks against Bitcoin / crypto asset owning entities that occurred in meatspace.
Formal proof with the Coq theorem prover of the equivalence of three semantics for a language describing the behavior of distributed systems.
Interactive playground for exploring and sharing TLA+ specifications in the browser.
Tool qualification tests and reports for the TLA+ model checker
Formal Verification tool for Move on Sui
GitHub Action which automatically updates Lean projects
Tool for automatically inferring inductive invariants of distributed protocols.
[FSE-2024] Towards AI-Assisted Synthesis of Verified Dafny Methods
An analysis tool for Python that blurs the line between testing and type systems.
solver for the reachability modulo theories problem
Helper toolkit for creating your own Lean 4 UserWidgets
A generic C++ API for SMT solving. It provides abstract classes which can be implemented by different SMT solvers.
Pono: A flexible and extensible SMT-based model checker
ngernest / chamelean
Forked from thanhnguyen-aws/plausibleProperty-based testing for Lean via metaprogramming