dafny

LLM verified with Monte Carlo Tree Search

formalization of the Dependent Object Types (DOT) calculus

verification toolchain for TypeScript (Tech Preview)

An auto-active verifier embedded into Lean

DafnyBench: A Benchmark for Formal Software Verification

Make agents prove that their code is correct.

Aver is a programming language for auditable AI-written code

vRAG: Verified Code Synthesis with Retrieval-Augmented Generation [FSE-2024]

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

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).

Verified kernels, written in Dafny and compiled to JavaScript, for correct-by-construction state in interactive web applications

A tool for deductive verification of Python programs based on Dafny

Dafny verifies proofs; claimcheck confirms intent.

Dafny for Metatheory of Programming Languages

Exercises and exam solutions for programming in C and Dafny (1st-year CS course)

Dafny 2 for Visual Studio Code (Legacy)

AI-assisted verification of Dafny Programs

A Formal Method playground for limboole, Z3, nuXmv, Alloy, Spectra, Dafny, and more...

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