[Dokmelody scratchpad notes]
[Main website]
tech/Formulog-code-analysis
Datalog + fixpoint semantic + SAT solver.
It performs static analysis of the code, with type check.