Summary: This is an impressive, just-finished master thesis by Sarek Høverstad Skotåm, who implemented a realistic yet formally verified SAT solver implemented in Rust, using Creusot, an experimental system to formally verify Rust programs, which is itself built on top of Why3.

CreuSAT implements a simple but modern CDCL solver, with many references to say CaDiCaL and Glucose; the authors have done an excellent job reading through the SAT literature and making wise choices. Implemented optimizations include watch literals (duh), but also some learned-clause simplification (simplification by unit clauses) and deletion, and restart.

Creusot (and Why3) are SMT-based program verifiers. As a user, you write the program and annotations around it (invariants, preconditions, etc.), the verifier translates those invariants / specifications to simple logic formulas optimized for SMT solvers. The programmer, hopefully, does not have to write proofs themselves (as opposed to tactics-based proof assistants). In practice the programmer does have to massage the code and the invariants quite a bit to make them easier / feasible to verify by automated solver, and there are more and more features to help for harder proofs (lemma functions, etc.). Still the expectation is that the amount of proof code written by user is relatively low, and hopefully the verification time is also relatively fast (… because there is less code, and solvers tend to explode instead of just taking longer when it doesn’t work). Correspondingly, CreuSAT is rather fast to check/verify.

Heh. I have the honor of being internal opponent during Sarek’s MSc defense later this month. I can pass on remarks or ask questions on anyone’s behalf if there’s interest.

That is awesome. Is Z3 formally verified? I believe it isn’t, right? If so, that’s definitely a value proposition over Z3. I’ve always wondered how much we can really trust Z3, which is becoming scary because of how ubiquitous it is.

Outstanding work!

A good place to read in more details is the master thesis manuscript (PDF).

Summary: This is an impressive, just-finished master thesis by Sarek Høverstad Skotåm, who implemented a realistic yet

formally verifiedSAT solver implemented in Rust, using Creusot, an experimental system to formally verify Rust programs, which is itself built on top of Why3.CreuSAT implements a simple but modern CDCL solver, with many references to say CaDiCaL and Glucose; the authors have done an excellent job reading through the SAT literature and making wise choices. Implemented optimizations include watch literals (duh), but also some learned-clause simplification (simplification by unit clauses) and deletion, and restart.

Creusot (and Why3) are SMT-based program verifiers. As a user, you write the program and annotations around it (invariants, preconditions, etc.), the verifier translates those invariants / specifications to simple logic formulas optimized for SMT solvers. The programmer, hopefully, does not have to write proofs themselves (as opposed to tactics-based proof assistants). In practice the programmer does have to massage the code and the invariants quite a bit to make them easier / feasible to verify by automated solver, and there are more and more features to help for harder proofs (lemma functions, etc.). Still the expectation is that the amount of proof code written by user is relatively low, and hopefully the verification time is also relatively fast (… because there is less code, and solvers tend to explode instead of just taking longer when it doesn’t work). Correspondingly, CreuSAT is rather fast to check/verify.

Heh. I have the honor of being internal opponent during Sarek’s MSc defense later this month. I can pass on remarks or ask questions on anyone’s behalf if there’s interest.

Sarek is also present on the HN thread (which might be a better fit for some types of questions): https://news.ycombinator.com/item?id=31780128

That is awesome. Is Z3 formally verified? I believe it isn’t, right? If so, that’s definitely a value proposition over Z3. I’ve always wondered how much we can

reallytrust Z3, which is becoming scary because of how ubiquitous it is.