Skip to main content

SemantifyrSemantifyrSemantifyr

Semantic library-driven formal verification of engineering models.

Try it live Learn the language

Try it online

In-browser editor

A lightweight editor for quick experimentation. Supports syntax highlighting, diagnostics, content assist, and an integrated verification panel. No installation or account required.

Open the live editor

JupyterHub environment

A full-fledged VS Code environment with the Semantifyr extension, multi-file project support, and integration with SysML v2 and the Theta model checker backend.

Access requires a user account. Contact the maintainers if you don't have one yet.

Launch JupyterHub

Get started

Tutorials

Build a traffic light model from scratch, discover and fix a safety bug, then refactor it into a reusable library.

Start the tutorials

Language Reference

Quick-lookup reference for every Semantifyr construct: classes, features, transitions, properties, expressions, and more.

Browse the reference

Contribute

Semantifyr is open source. Fork the repository, build from source, and start contributing to the compiler, frontends, or tooling.

Developer guide