Formal verification for control logic

Prove your design is right, before it runs.

Write the requirements, draw the circuit that implements them, simulate it, prove its properties or get the steps that break them, and generate the MC/DC tests that show each condition counts. A model checker works underneath, out of sight.

Try it online Follow the tutorial

Nothing to install to try it. Free for noncommercial use.

A door controller drawn as a circuit: two assertions proved, one failing with its counterexample in the scope

From a requirement to its proof and its tests

One project, a vehicle's door alarm, taken through every step: the documentation's tutorial does exactly this.

Requirements, each with its logic

Keep the requirements in a table: an identifier, the text a reviewer reads, and a formula for its logic, such as door_open and speed > 5. Each requirement's circuit is built from its formula, and its MC/DC coverage is shown beside it.

A requirements table: four requirements, their formulas, and their MC/DC coverage, all complete

Circuits you draw, and simulate

Inputs, gates, comparisons, arithmetic, delays, timers and counters, wired pin to pin on a canvas in the style of Simulink, grouped into subsystems, checked as you draw. Give the inputs their values step by step, and read the signals in the scope.

A circuit simulated for ten steps: the values on its wires, and its signals in the scope

Proofs, or the steps that break them

An assertion is proved to hold at every step, for every input; or it fails, with the trace that breaks it, played on the canvas. A target is reached, or proved unreachable. No test bench to write: the model checker considers every input.

Verification: both assertions fail, each with its counterexample, and the target is reached

Proof certificates anyone can check

A property proved can come with its proof: an SMT-LIB 2 script that any SMT solver checks, independently of Intrepid. Three questions, each of which must answer unsat. You do not have to trust the tool.

; A proof certificate from intrepid:
; no target of the circuit is reachable.
; Engine: br. Kind: inductive invariant.
; Each check-sat must answer unsat.

$ z3 ack_silences.smt2
unsat
unsat
unsat

MC/DC tests, and a report to print

Mark a decision, and get the tests that show each of its conditions alone decides the outcome, as the standards for safety critical software ask. Export them for the test bench, and print the report: a page per requirement, with its text, its circuit and its tests.

The MC/DC tests of the alarm: four conditions covered by six tests

Use it where you work

The same editors in three places, and the library underneath for those who write programs. A project made in one opens in the others.

Intrepid Studio

The editors in your browser, served from your own machine on a folder of yours. Nothing leaves the machine.

pip install intrepid-studio
intrepid-studio ./my-project

On PyPI

The VS Code extension

The Intrepid Circuit Editor, in Visual Studio Code: your circuits and requirements are files of your workspace.

How to install it

The demo

The editors on a website: nothing to install. Your project stays in your browser until you download it.

Try it online

intrepyd, for Python

The simulator and the model checkers as a Python library. It reads Lustre, IEC 61131-3 Structured Text and Simulink models.

pip install intrepyd

Its documentation

Underneath

Engines in parallel

Bounded model checking with k-induction, backward reachability and IC3/PDR, on the Z3 SMT solver, run as a portfolio: the first useful answer wins.

Measured against Kind2

On the 848 Lustre benchmarks of Kind2, with a 30 second timeout, intrepyd solves 823 and Kind2 798, with the same verdict on every one both solve. The comparison

Your models, as they are

A Lustre model opens as a circuit, its properties as assertions; a circuit exports to a Python program. Simulink and Stateflow models are next in the editors.

Learn it

The editors' tutorial

Intrepid Studio and the VS Code extension: a door alarm, from its requirements to its report, through every feature.

Start the tutorial

intrepyd's tutorial

The Python library: from a first netlist to the model checkers, the test generation and the translation of models.

Start the tutorial

License

Free for noncommercial use: personal projects, teaching, research, and noncommercial organizations, under the PolyForm Noncommercial License 1.0.0. intrepyd comes with a noncommercial license for its engines.

Companies need a commercial license. Ask for one at license@intrepid-studio.eu: the editors write that email for you, with what is needed to issue it.

Ask for a license