# Dafny Quote OK Image Format

https://profs.info.uaic.ro/stefan.ciobaca/dafny-qoi-ifm2024.pdf
https://qoiformat.org/qoi-specification.pdf
https://github.com/ciobaca/qoi-dafny

## Improve performance for encoding and decoding

## Add separate support for RGB inputs



# OpenPGP Key Server

Implement, specify, and verify in Dafny a PGP key server (a HAGRID
clone) in Dafny. This project was a 2020 VerifyThis Long Term
Challenge.

Resources: [challenge website](https://verifythis.github.io/01hagrid/)



# Verified memcached clone

Implement, specify, and verify in Dafny a memcached clone, described
below. This project is the current VerifyThis Long Term Challenge.

Resources: [challenge website](https://verifythis.github.io/03memcached/)



# A library for Dynamic Programming in Dafny

https://github.com/Haidau-Alina-Adriana/Licenta/blob/main/Documentatie/Licenta.pdf
https://github.com/roxana413/Licenta-Dafny/blob/main/Documentation/Lucrare_de_licenta.pdf

Implement, specify, and verify a Dafny module for dynamic programming.



# A library for Backtracking in Dafny

https://github.com/radup99/Sudoku-Dafny/blob/master/final.dfy



# A library for greedy algorithms in Dafny

https://github.com/cristirusu-99/ASP-Greedy-Dafny
https://github.com/ElisaChicos/Licenta/blob/main/Documentatie/main.pdf
https://github.com/alexxandra21/Licenta2023/blob/main/Documentatie/main.pdf
https://docta.ucm.es/rest/api/core/bitstreams/6e267d5e-d292-4f02-b8c1-9c7f85ff6eed/content


# Implement, specify, and verify the Fourier-Motzkin algorithm

https://www.cs.utexas.edu/~isil/cs389L/lecture-omega-6up.pdf



# Implement, specify, and verify a library for mini-max in Dafny

E.g. for games like connect4, tic-tac-toe, chess



# Prove in Dafny the soundness and completeness of natural deduction
  for Propositional Logic

https://cs.uwaterloo.ca/~cbruni/CS245Resources/lectures/2018_Spring/09_Propositional_Logic_Natural_Deduction_Soundness_and_Completeness_post.pdf