CreuSAT
supervisionary
Our great sponsors
| CreuSAT | supervisionary | |
|---|---|---|
| 8 | 1 | |
| 581 | 3 | |
| - | - | |
| 6.9 | 3.2 | |
| 9 days ago | almost 2 years ago | |
| Rust | Rust | |
| MIT License | MIT License |
Stars - the number of stars that a project has on GitHub. Growth - month over month growth in stars.
Activity is a relative number indicating how actively a project is being developed. Recent commits have higher weight than older ones.
For example, an activity of 9.0 indicates that a project is amongst the top 10% of the most actively developed projects that we are tracking.
CreuSAT
- CreuSAT - A formally verified SAT solver written in Rust and verified with Creusot
- CreuSAT。用Rust编写并通过Creusot验证的正式验证的SAT求解器 (CreuSAT: Formally verified SAT solver written in Rust and verified with Creusot)
- CreuSAT: Formally verified SAT solver written in Rust and verified with Creusot
- CreuSAT: A formally verified SAT solver written in Rust
supervisionary
-
What is a really cool thing you would want to write in Rust but don't have enough time, energy or bravery for?
Here's a proof-checker written in Rust for HOL, the same logic that Isabelle/HOL, HOL4, and HOL Light implements, up-to minor differences. However, the proof-checker has a very different design, compared to those systems, being written more like an operating system where proofs are constructed by issuing system calls (or, rather, calls into a Wasm host) and the kernel returning opaque handles to constructed objects to "user space".
What are some alternatives?
creusot - Creusot helps you prove your code is correct in an automated fashion. [Moved to: https://github.com/creusot-rs/creusot]
coq2rust - Coq to Rust program extraction. The whole tree is on the original Coq code base.
screwsat - A simple CDCL(Conflict-Driven-Clause-Learning) SAT solver in Rust.
coq-of-ocaml - Formal verification for OCaml
LucidMQ - Simple Ops Event Streaming. Alternative to Kafka and RabbitMQ
yew - Rust / Wasm framework for creating reliable and efficient web applications
wasmer - 🚀 The leading Wasm Runtime supporting WASIX, WASI and Emscripten
dioxus - Fullstack GUI library for web, desktop, mobile, and more.
xstate - Actor-based state management & orchestration for complex app logic.
Cycle.js - A functional and reactive JavaScript framework for predictable code
sycamore - A library for creating reactive web apps in Rust and WebAssembly
kani - Kani Rust Verifier