toy projects

Theorem Prover

• Designing a Theorem Prover, Lawrence C Paulson, slides
  • Implementation in OCaml, https://github.com/jubnzv/folderol

SMT

• SAT-MICRO: petit mais costaud! - Sylvain Conchon, Johannes Kanig, Stéphane Lescuyer, https://inria.hal.science/inria-00202831/document
  • Haskell version, https://hackage.haskell.org/package/sat-micro-hs
  • OCaml version, https://gist.github.com/Drup/4dc772ff82940608834fc65e3b80f583
• Semantics and applications to verification - Sylvain Conchon, Antoine Miné and Xavier Rival, https://www.di.ens.fr/~rival/semverif-2016/
  • toy-smt in OCaml, https://github.com/Ekdohibs/toy-smt
• A poor man’s MaxSMT, https://yurichev.com/blog/maxsmt/
• SMT Solvers: Theory and Implementation, https://leodemoura.github.io/files/oregon08.pdf
• Internals of SMT Solvers, https://leodemoura.github.io/files/SATSMT2013.pdf
• kissat is an SMT solver written by Armin Biere on a plain C. Simple enough for understanding.
• SATurne - is a simple, purely functional SAT solver written and verified in Coq. It's a tiny solver, absolutely not designed for performances nor scalability. It is, however, intended to be well-documented, easy to understand and extremely trustworthy.
• Modulus - building an SMT solver from the ground up.
• https://github.com/zutshi/ToySMT - is a small SMT solver made by Denis Yurichev. It supports only booleans and bitvecs. No integers, let alone reals and arrays and tuples and whatever.
• SATurne -a tiny verified SMT solver.

SAT

• A Very Small SAT Solver
• https://github.com/marijnheule/microsat
• lsat

Static Analyzer

• Semantics and application to program verification. The goal of the project is to implement a small static analyzer by abstract interpretation for a simple language. Slides, Project page
• UNO

Model Checker

• Build your own model checker in one month - Jin Song Dong, Jun Sun, https://ieeexplore.ieee.org/document/6606751
• X.21 Analysis Revisited: the Micro-Tracer, AT&T Bell Laboratories, Technical Memorandum 11271-8710230-12, October 23, 1987. (PDF). Source code - https://spinroot.com/gerard/micro.html

Fuzzing Engine

• Build simple fuzzer: part 1, part 2, part 3, part 4, part 5, part 6.
• Minimal symbolic model checker & fuzzer - https://github.com/xiw/mini-mc
• A very minimal implementation of the core idea of Hypothesis, https://github.com/DRMacIver/minithesis
• Writing the Fuzzer

Sanitizer

• KASAN-Baremetal, https://github.com/androidoffsec/baremetal_kasan/
• Mini-ASAN, https://github.com/andreafioraldi/asan-giovese
• MiniValgrind,
  • https://github.com/artemmukhin/MiniValgrind, MINIVALGRIND: ПРОСТОЙ ДЕТЕКТОР УТЕЧЕК ПАМЯТИ
  • https://github.com/rauhul/cs241/tree/94960ae9b15b8e4288dd893742384e9a8654ca08/mini_valgrind
  • http://ipo.spb.ru/journal/content/1905/MiniValgrind:%20%D0%BF%D1%80%D0%BE%D1%81%D1%82%D0%BE%D0%B9%20%D0%B4%D0%B5%D1%82%D0%B5%D0%BA%D1%82%D0%BE%D1%80%20%D1%83%D1%82%D0%B5%D1%87%D0%B5%D0%BA%20%D0%BF%D0%B0%D0%BC%D1%8F%D1%82%D0%B8.pdf