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.

[FSE-2024] Towards AI-Assisted Synthesis of Verified Dafny Methods

DafnyBench: A Benchmark for Formal Software Verification

DaisyNFS is an NFS server verified using Dafny and Perennial.

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

Dafny for Metatheory of Programming Languages

A tool for deductive verification of Python programs based on Dafny

Dafny 2 for Visual Studio Code (Legacy)

Exercises and exam solutions for programming in C and Daphny

Exercises for the Dafny Tutorial

AI-assisted verification of Dafny Programs

piggy-backing on the Dafny language implementation to explore interactive semi-automated verified program synthesis, combining LLMs and symbolic reasoning

Short introduction to Dafny

Examples of formal verifications written in Dafny.

Library of formally verified abstract data types in Dafny.

Yul semantics and verification in Dafny

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.