Search results

Informally prove correctness property of the chain sync mini-protocol with fixed chain

type: enhancement

Status: Open.

#99 In input-output-hk/ouroboros-high-assurance;

· javierdiaz72 opened on Jan 16, 2024

Formally specify correctness property of the chain sync mini-protocol with fixed chain

type: enhancement

Status: Open.

#97 In input-output-hk/ouroboros-high-assurance;

· javierdiaz72 opened on Jan 12, 2024

· 

Delivery of the verification of the chain synchronization protocol

Specify the multicast semantics of mini-protocol programs

type: enhancement

Status: Open.

#96 In input-output-hk/ouroboros-high-assurance;

· jeltsch opened on Dec 10, 2023

· 

Delivery of the mini-protocol framework

Specify the broadcast semantics of mini-protocol programs

type: enhancement

Status: Open.

#95 In input-output-hk/ouroboros-high-assurance;

· jeltsch opened on Dec 9, 2023

· 

Delivery of the mini-protocol framework

Modularize the chain synchronization client program

type: enhancement

Status: Open.

#72 In input-output-hk/ouroboros-high-assurance;

· javierdiaz72 opened on Sep 11, 2023

· 

Delivery of the specification of the chain synchronization protocol

Address feedback from Praos specification walkthrough

type: enhancement

Status: Open.

#64 In input-output-hk/ouroboros-high-assurance;

· javierdiaz72 opened on Sep 1, 2023

· 

Delivery of the Ouroboros Praos specification

Enforce the ability to send and receive “done” messages

type: improvement

Status: Open.

#59 In input-output-hk/ouroboros-high-assurance;

· jeltsch opened on Aug 9, 2023

· 

Delivery of the mini-protocol framework

Introduce proper citations

type: improvement

Status: Open.

#56 In input-output-hk/ouroboros-high-assurance;

· jeltsch opened on Aug 7, 2023

· 

Delivery of the mini-protocol framework

Use the fixed AFP version of <code>Finite_Map_Extras</code>

type: improvement

Status: Open.

#47 In input-output-hk/ouroboros-high-assurance;

· javierdiaz72 opened on Jun 30, 2023

· 

Delivery of the Ouroboros Praos specification

Integrate the BFT specification

type: enhancement

Status: Open.

#35 In input-output-hk/ouroboros-high-assurance;

· jeltsch opened on Apr 18, 2023

· 

Delivery of the Ouroboros BFT specification

Integrate the chain selection density equivalence code

type: enhancement

Status: Open.

#34 In input-output-hk/ouroboros-high-assurance;

· jeltsch opened on Apr 18, 2023

· 

Delivery of the Ouroboros Genesis specification

Integrate the chain selection property code

type: enhancement

Status: Open.

#33 In input-output-hk/ouroboros-high-assurance;

· jeltsch opened on Apr 18, 2023

· 

Delivery of the verification of one-by-one chain selection