Stars
A graduate course on formalized mathematics at the Faculty of Mathematics and Physics, University of Ljubljana, Fall semester 2024/25
Examples and exercises from the book Program Proofs translated to Gobra
Repository for the VMI Summer Retreat Workshop on Hacking AI Agents
Research prototype tool for modular formal verification of C and Java programs
A LaTeX class for books, reports or theses based on https://github.com/kenohori/thesis and https://github.com/Tufte-LaTeX/tufte-latex.
Compositional Verification of Composite Byzantine Protocols
Material for the class on verification of distributed and asynchronous systems, developed by Jon Howell and Manos Kapritsos
Anvil is an experimental framework to build practical, formally verified, cluster management controllers.
Manage your dotfiles across multiple diverse machines, securely.
My tutorial on disclosing data for double blind peer review and make it archived open data upon acceptance.
A memory allocator verified with Verus
The axiom profiler for exploring and visualizing SMT solver quantifier instantiations (made via E-matching).
Standard library for the Gobra verifier for Go. Contains definitions and lemmas useful for verifying large projects.
Capability-based verifier for safe Rust clients of interior mutability
I speak only of myself since I do not wish to convince, I have no right to drag others into my river, I oblige no one to follow me and everybody practices his art in his own way.
egg is a flexible, high-performance e-graph library
Inspect a command's effects before modifying your live system