Top 4 Scala Verification Projects
-
-
chiseltest
The batteries-included testing and formal verification library for Chisel-based RTL designs.
-
InfluxDB
Power Real-Time Data Analytics at Scale. Get real-time insights from all types of time series data with InfluxDB. Ingest, query, and analyze billions of data points in real-time with unbounded cardinality.
-
-
gobra
Gobra is an automated, modular verifier for Go programs, based on the Viper verification infrastructure.
TLA+ has also had an SMT-based backend, Apalache [1], for a few years now. In general, you encode your system model (which would be the Rust functions for Verus, the TLA model for Apalache) and your desired properties into an SMT formula, and you let the solver have a go at it. The deal is that the SMT language is quite expressive, which makes such encodings... not easy, but not impossible. And after you're done with it, you can leverage all the existing solvers that people have built.
While there is a series of "standard" techniques for encoding particular program languages features into SMT (e.g., handling higher-order functions, which SMT solves don't handle natively), the details of how you encode the model/properties are extremely specific to each formalism, and you need to be very careful to ensure that the encoding is sound. You'd need to go and read the relevant papers to see how this is done.
[1]: https://apalache.informal.systems
Scala Verification related posts
Index
What are some of the best open-source Verification projects in Scala? This list will help you:
| Project | Stars | |
|---|---|---|
| 1 | apalache | 414 |
| 2 | chiseltest | 207 |
| 3 | chiselverify | 134 |
| 4 | gobra | 97 |
Sponsored