evm-dafny
quint
evm-dafny | quint | |
---|---|---|
1 | 6 | |
118 | 595 | |
4.2% | 1.8% | |
8.5 | 9.8 | |
16 days ago | 6 days ago | |
Dafny | TypeScript | |
Apache License 2.0 | Apache License 2.0 |
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.
evm-dafny
quint
-
Holiday protocols: secret Santa with Quint
Hi! I wrote a blogpost exploring a formal specification in Quint [1] for the secret santa game, and verifying some of its properties with Apalache [2].
Hope you enjoy it, and any feedback is welcome. Happy holidays!
[1]: https://github.com/informalsystems/quint
-
Quint: A specification language based on the temporal logic of actions (TLA)
I can sympathize! We are aiming to maintain most of the expressive power of TLA+ -- ideally everything you need for a concise, high-high level specification, that can be simulated and/or verified -- but with surface syntax that is more approachable coming from a programming background. If you're interested in seeing how it maps to TLA+, you can find much of that in this document: https://github.com/informalsystems/quint/blob/main/doc/lang....
We still have lots of ways to improve, and -- we think -- lots of opportunities to improve our interop and complementary qualities in relation to TLA+ and TLC. But we have found the tools in their current state useful enough to be worth sharing :)
- Quint – a new language based on TLA+ with modern syntax and developer tooling
-
Programming Languages Going Above and Beyond
It's still in pretty early development, but you may be interested in https://github.com/informalsystems/quint
> It combines the robust theoretical basis of the Temporal Logic of Actions (TLA) with state-of-the-art static analysis and development tooling.
And it is typed ;)
What are some alternatives?
dafny - Dafny is a verification-aware programming language
TypeScript - TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
prusti-dev - A static verifier for Rust, based on the Viper verification infrastructure.
tlaplus - TLC is a model checker for specifications written in TLA+. The TLA+Toolbox is an IDE for TLA+.
z3 - The Z3 Theorem Prover