formal

package
v1.0.0 Latest Latest
Warning

This package is not in the latest version of its module.

 Go to latest Published: Mar 25, 2026 License: GPL-3.0 Imports: 4 Imported by: 0

Documentation

Overview

Package formal provides formal verification support: TLA+ generation, invariants, model checking.

Index

Constants

This section is empty.

Variables

This section is empty.

Functions

func GenerateCoqSkeleton 

func GenerateCoqSkeleton(lib *protocol.Library, name string) (string, error)

GenerateCoqSkeleton generates a Coq proof skeleton for encode/decode correctness.

func GenerateTLAPlus 

func GenerateTLAPlus(lib *protocol.Library, name string) (string, error)

GenerateTLAPlus converts a PSL protocol to TLA+ specification.

Types

type Invariant 

type Invariant struct {
	Name        string `json:"name"`
	Expression  string `json:"expression"`
	Description string `json:"description"`
}

Invariant represents a protocol invariant.

type VerificationResult 

type VerificationResult struct {
	Invariant      Invariant `json:"invariant"`
	Satisfied      bool      `json:"satisfied"`
	CounterExample string    `json:"counter_example,omitempty"`
}

VerificationResult holds the result of a verification check.

func CheckInvariants 

func CheckInvariants(lib *protocol.Library, name string, samples [][]byte) ([]VerificationResult, error)

CheckInvariants checks basic invariants against sample data.

Source Files

View all Source files

Jump to

Keyboard shortcuts

? : This menu
/ : Search site
f or F : Jump to
y or Y : Canonical URL
go.dev uses cookies from Google to deliver and enhance the quality of its services and to analyze traffic. Learn more.