awakesecurity/spectacle

Embedded specification language & model checker in Haskell

Haskell

182

57 commits

updated May 7, 2026

README

spectacle

Language.Spectacle defines an embedded language for writing formal specifications of software in the temporal logic of actions. Specifications written in spectacle can be model-checked and shown to either be correct with respect to temporal properties or refuted by a counterexample. Examples of specifications written in spectacle are provided under test/integration.

Contributors

52 commits

2 commits

1 commits

1 commits

Similar repos

HigherOrderCO/Kind

A modern proof language

3,762

ziglang/zig-spec

225

codedownio/sandwich

Yet another test framework for Haskell.

73

awesomo4000/awesome-provable

A curated set of links to formal methods involving provable code.

225

argotorg/act

Smart contract specification language

279

dafny-lang/dafny

Dafny is a verification-aware programming language

3,549

RyanGlScott/ghc-software-foundations

The Software Foundations book, in GHC

83

brandonfromph/mirr-project

MIRR is a hardware rule language for safety-critical systems. You describe conditions and reactions…

1

Languages

Haskell

98.7%

Nix

1.1%

awakesecurity/spectacle

Embedded specification language & model checker in Haskell

Haskell

182

57 commits

updated May 7, 2026

README

spectacle

Language.Spectacle defines an embedded language for writing formal specifications of software in the temporal logic of actions. Specifications written in spectacle can be model-checked and shown to either be correct with respect to temporal properties or refuted by a counterexample. Examples of specifications written in spectacle are provided under test/integration.

Similar repos

HigherOrderCO/Kind

A modern proof language

3,762

ziglang/zig-spec

225

codedownio/sandwich

Yet another test framework for Haskell.

73

awesomo4000/awesome-provable

A curated set of links to formal methods involving provable code.

225

argotorg/act

Smart contract specification language

279

dafny-lang/dafny

Dafny is a verification-aware programming language

3,549

RyanGlScott/ghc-software-foundations

The Software Foundations book, in GHC

83

brandonfromph/mirr-project

MIRR is a hardware rule language for safety-critical systems. You describe conditions and reactions…

1

Contributors

52 commits

2 commits

1 commits

1 commits

Languages

Haskell

98.7%

Nix

1.1%