Z3-solver is a popular backend for specifying properties about programs. Dafny, Viper, Boogie are all systems built on top of it. The issue is that much real w

Z3-solver is a popular backend for specifying properties about programs. Dafny, Viper, Boogie are all systems built on top of it. The issue is that much real world software is not written in these languages (or Haskell) Typescript and python are a lot more interesting. https://adsharma.github.io/pysmt/ https://adsharma.github.io/pysmt/ The proposal is to have a programming language and a specification language both with a pythonic syntax living in one file. Coupled with a transpiler, it could make a capable system vs the C++/TLA+ based alternative.