Introdution

• open-source C++ informal semantic verification framework
• an alternative to formal verification without formal-math syntax

Documentation

• Overview & comparison
• other documentation (manuals, tutorial) is stored in Naive3.binaries archive

Download (see Releases)

• Naive3.binaries - all binaries (except clang) with documentation
• Naive3.clang - clang with 4 new attributes, clang-format with contract support
• Naive3.libraries - verified core libraries

Source code (see Releases)

• Naive3.sources - source-code for all binaries (except LLVM)

Examples

Canonical example

fn open(file& a)
  read(a, closed)
  write(a, any & opened)
  -> void;

Marketing example

fn xml::reader::move_to_attributes()
   read(node_m, enum(node_kind::start_tag_name, node_kind::start_tag_attrs))
   write(this, any)
   write(node_m, node_kind::start_tag_attrs)
   -> void;

Screenshots

Status

• not recommened for any use except initial experiments
• experimental and subject to change without warning.
• distributed with bugs and with no warranty.
• dependencies (windows SDK, LLVM) have known bugs, which may crash the applications or execute arbitrary code.
• used for verification of ~300KLOC (from core libraries to the framework itself).

Features

• complete verification, including generic code and termination
• almost full core language support, incl. aliasing (there is no borrowing), partially-valid state (dangling pointers) etc.
• cross-platform build without any scripts
• verified program can be compiled by any C++compiler (with suported modules)

License

• fixed to Boost or equivalent.