A collection of Dafny proofs: verified solutions to LeetCode problems plus a small reusable library of lemmas and data-structure helpers.
leetcode/— 29 LeetCode problems with verified specs (sqrt, two-sum, max subarray, k-th factor, invert/symmetric binary tree, range update, merge sorted array, merge k sorted lists, best-time-to-buy-and-sell-stock, LRU cache, basic calculator III, burst balloons, trapping rain water (1-D exact volume; 2-D exact volume via the escape-level fixpoint), median of two sorted arrays (partition-search value correctness, no verified cost model), critical connections (bridges proven to be exactly the edges whose removal disconnects their endpoints, plus Tarjan's low[v] > disc[u] criterion proven equivalent on a DFS tree, plus a verified DFS that constructs such a tree -- no cross edges and all), etc.).lib/Seq.dfy,SeqMethods.dfy,List.dfy,MinMax.dfy,Pow.dfy— sequence and arithmetic utilities.seq/—Count,Digits,Fold,Map,Palindrome,Subseq,Undup.math/—Abs,DivMod,EvenOdd,Factors,Gcd.adt/—BinaryTree,BST,Graph(topological sort via Kahn's BFS),PriorityQueue(min leftist heap).
- Root-level
.dfyfiles — small standalone experiments (vector class, set abstractions, bounded-choice permutation/selection methods; no probabilistic uniformity specs).
- Dafny 4.11.0 (bundles Z3 4.12.1 / 4.14.1).
- Download the official release zip from
the Dafny releases page
— installing via
dotnet tool install Dafnydoes not ship a Z3 binary, so verification will fail.
Single file:
dafny verify lib/Seq.dfyEverything (skipping any [wip]-prefixed files, in parallel):
find . -name '*.dfy' | awk '!/\[wip\]/' \
| xargs -I{} -P 8 -n 1 timeout 120 dafny verify {}.github/workflows/ci.yaml checks every .dfy file across six matrix slices
(one per directory) with Dafny 4.11.0 and --verification-time-limit 30.
Files containing {:test} run through dafny test; the rest run through
dafny verify. [wip]-prefixed files are skipped.
See LICENSE.