LLM verified with Monte Carlo Tree Search

formalization of the Dependent Object Types (DOT) calculus

A compiler for automatically re-targeting sequential Java code to Apache Spark.

Program Analysis, Software Verification & Testing. Python3, CAS, Dafny, Z3, CVC4, UCLID, ZChaff, NuSMV, AFL, Scala, CBMC & LLVM Framework (CO).

DaisyNFS is an NFS server verified using Dafny and Perennial.

Dafny for Metatheory of Programming Languages

Towards AI-Assisted Synthesis of Verified Dafny Methods

Dafny 2 for Visual Studio Code (Legacy)

A tool for deductive verification of Python programs based on Dafny

Programming fundamentals

Exercises for the Dafny Tutorial

Dafny Interactive Verification Environment (DIVE)

A repository that describes my explorations on formal verification using Dafny, techniques from programming language theory such as CYK parsing, Earley parsing, type-theoretic things like lambda calculus etc.

Short introduction to Dafny

Examples of formal verifications written in Dafny.

Abstract Proven Symbolic Execution Engine

Library of formally verified abstract data types in Dafny.

🧠️🖥️2️⃣️0️⃣️0️⃣️1️⃣️💾️📜️ The sourceCode:Dafny category for AI2001, containing Dafny programming language datasets

some formal verification exercises using dafny.

Dafny