Anton Setzer

Safety-critical railway systems such as Railway interlockings and the European Rail Traffic Management System (ERTMS) require strong, independently checkable guarantees of correctness. This requirement is reinforced by the new standard governing the use of software in the railway domain, EN50716 [18], which firmly promotes formal verification as part of an end-to-end assurance process. Many modern railway verification workflows rely on SMT solvers, such as Z3, to discharge safety properties expressed in propositional logic or its suitable extensions. In this paper, we show how a Z3-based verification toolchain can be extended with proof checking via independent validation of the solver’s output, thereby increasing trust in the overall verification process. To this end, we present a bespoke proof-checking framework for railway verification, capable of handling propositional logic, as well as inequality reasoning based on the Farkas lemma. The latter plays a major role in ERTMS logic, where positioning constraints are often expressed as linear inequalities. We demonstrate the application of the Farkas lemma through a small case study, showcasing the effectiveness of the tool. The methodology developed for handling Farkas certificates can serve as a foundation for incorporating additional SMT reasoning rules. The proof-checking framework has been formally specified in Rocq, with the checker extracted from the formalisation. This approach has been developed together with our industrial partner. It is concise, tailored to their framework, and independent from other larger proof checking mechanisms.

This paper extends the previous paper [6] by implementing two blockchain simulators of Solidity-style smart contracts – a simple and a complex one, using the interactive theorem prover Agda. In the previous article [6], we built a simple and complex abstract model of Solidity-style smart contracts in Agda. These models had many features, such as calling different smart contracts, supporting the ability to call different smart contracts, and providing simple and complex instructions. Because of the use of coalgebras for representing smart contracts they supported loops and conditionals, using the support of those features for coalgebraic programs in Agda. The complex model supported gas costs and pure functions, similar to the Solidity language. In this paper, we implement and design interfaces which allow to interactively interact with users in the simple and complex models. This makes use of the fact that Agda is as well a dependently typed programming language. Therefore we can write interactive programs which are running in the same language in which we will in a future next step verify smart contracts, avoiding the translation of programs which could be a source of errors. The simple blockchain simulator we have created can call other contracts, transfer funds to specific contracts, and update contracts. The complex blockchain simulator has in addition features that can deal with more complex blockchain instructions, support gas costs, and evaluate and update pure functions.

Manuscripts should be submitted using EditFlow at https://ef.msp.org/submit/asl_jsl, where instructions directed specifi cally at using the system can also be found. Authors should keep a complete copy of their submission and all electronic fi les from which it was created. They should also consult the more general guidelines for the submission of manuscripts at https://aslonline.org/journals/the-journal-of-symbolic-logic/submission-guidelines/. These instructions include the Association's standards about previous publication and plagiarism as well as information about copyrights and electronic copies of published papers. No print off prints will be supplied but authors will receive a link to a freely accessible electronic pdf of their published article. Print off prints may be purchased if required.

Manuscripts should be submitted using EditFlow at https://ef.msp.org/submit/asl_jsl, where instructions directed specifi cally at using the system can also be found. Authors should keep a complete copy of their submission and all electronic fi les from which it was created. They should also consult the more general guidelines for the submission of manuscripts at https://aslonline.org/journals/the-journal-of-symbolic-logic/submission-guidelines/. These instructions include the Association's standards about previous publication and plagiarism as well as information about copyrights and electronic copies of published papers. No print offprints will be supplied but authors will receive a link to a freely accessible electronic pdf of their published article. Print offprints may be purchased if required.

We present two models of the block chain of Bitcoin in the interactive theorem prover Agda. The first one is based on a simple model of bank accounts, while having transactions with multiple inputs and outputs. The second model models transactions, which refer directly to unspent transaction outputs, rather than user accounts. The resulting blockchain gives rise to a transaction tree. That model is formalised using an extended form of induction-recursion, one of the unique features of Agda. The set of transaction trees and transactions is defined inductively, while simultaneously recursively defining the list of unspent transaction outputs. Both structures model standard transactions, coinbase transactions, transaction fees, the exact message to be signed by those spending money in a transaction, block rewards, blocks, and the blockchain, and the second structure models as well maturation time for coinbase transactions and Merkle trees. Hashing and cryptographic operations and their correctness are dealt with abstractly by postulating corresponding operations. An indication is given how the correctness of this model could be specified and proven in Agda.