romac

The Rust compiler (rustc) is written in Rust, but there can always be bugs in the compiler, regardless of whether it's written in a memory-safe language or not.

FTL v0.1.0 was just released, adding async Rust support (multi-thread Tokio runtime) and lots of missing pieces in the Linux compatibility layer.

(not my project)

Yes there are many such crates, which can indeed kinda fill the gap. One of the more recent one is https://docs.rs/bon

There is a single-page version of the book that you can save as a PDF: https://betrusted.io/xous-book/print.html

You can also go the other way around and generate traces [1] from the TLA+ or Quint [2] specs using the Apalache model checker [3], map each action in the trace to an action on your system under test, and check that the abstract and concrete states match at each step.

[1] https://apalache-mc.org/docs/adr/015adr-trace.html

[2] https://quint-lang.org

[3] https://apalache-mc.org

If you are interested in TLA+, you might want to check out Quint (https://quint-lang.org), a modern take on a specification language which shares the same underlying temporal logic of actions, but with a syntax more familiar to programmers.

And they are pushing in that direction: https://machinelearning.apple.com/research/homomorphic-encry...

If you haven't seen those already, you might also want to check out:

  - Apalache: a symbolic model checker for TLA+ backed by Z3 (https://apalache-mc.org)
  - Quint: a modern and executable specification language with TLA+-like semantics, that integrates with Apalache (https://quint-lang.org)

I wonder if this could be made to work in the browser using CheerpJ?

https://cheerpj.com