Deductive Verification as an Alternative to "Push-Button" Technologies

Apr 5, 2024

#programverification

Continuing the series of articles on development driven by deductive verification, here we propose a comparison of this methodology with the most closely related techniques that have already secured their place in practical software engineering. By formalizing the description of procedures for both — searching for confirmation of a program’s compliance with specifications, and verifying already found solutions, we will try to convince the reader that manually implementing the first procedure while automating the second can become a quite practical compromise, offering several advantages over fully automatic methods.

Read: https://www.inferara.com/papers/deductive-verification-as-alternative-to-push-button-technologies/

We have just begun posting a series of introductory blog posts about TLA+ and the first one is ready to go. So if you haven't tried TLA+ before but heard about it — it is a good entry point.

#tlaplus
#modelchecking

https://www.inferara.com/blog/do-not-die-hard-with-tla-plus-1/

Mathematics and Computation
"A Theory Revolutionizing Technology and Science"
Avi Wigderson

Avi Wigderson is the recipient of the 2023 ACM A.M. Turing Award.

Commit to marriage with TLA+ pt.2

To demonstrate the practical feasibility of the formalism proposed to the public in a series of papers we published, we are currently working on a Coq model for the simplest and most well-documented among the low-level computing platforms common in the industry – WASM.

Using this example, we plan to show how the concept of congruent templates applies to the modularization of the formal specification and the code it covers while remaining within the purely mathematical formalism of the control flow graph.

Meanwhile, here is the second part of a series of introductory blog posts about TLA+.

https://www.inferara.com/blog/commit-to-marriage-with-tla-plus-2/

Coq -> NixOS, installation

There are two main methods to set up a Coq proof assistant on NixOS that supports interactive proof mode in VSCode or VSCodium. Let's dive into them.

The first option is to use the official Nix environment packages: coq and coqPackages.coq-lsp. This method is somewhat simpler, but there are a couple of drawbacks. The installation can be slightly outdated, and for VSCode, it is required to use the Coq LSP extension.

Our experience and usage scenarios make us conclude that, this extension is a bit less convenient compared to VsCoq.

The second method is to utilize the OCaml opam repository, using the coq and vscoq-language-server packages.

This approach involves dealing with a common NixOS issue, but it has the advantage of providing the latest versions of the prover and libraries, along with a more comfortable interactive environment in the editor.

For this method, you'll need to plug the following Nix packages:

- gcc and gnumake for building your project and some packages in opam;
- ocaml and opam as the main repository for the Coq environment;
- vscode, vscodium, or another compatible editor to serve as your IDE.

You can find detailed instructions for installing Coq from opam on the Coq website, which also explains how to build a project from _CoqProject using coq_makefile.

During the compilation of some packages from opam, you might encounter a typical NixOS problem: the unavailability of standard paths for C headers, such as gmp.h.

The simplest solution is to create a shell.nix file with the following content:

with import <nixpkgs> {};
mkShell {
  nativeBuildInputs = [
    ocaml
    opam
    pkg-config
    gcc
    bintools-unwrapped
    gmp
  ];
}

Run the command nix-shell in the directory containing this file. This will place you in an environment where you can compile #include <gmp.h> without any issues. If any opam install ... command results in a dependency handling error, restarting it inside such a nix-shell should complete successfully.

By following these steps, you can ensure you have a modern, efficient setup for your Coq projects in VSCode or VSCodium.

🚀 INFERARA Q2 2024 Progress! 🚀

We've had an exciting second quarter at Inferara! Here’s what we’ve been up to:

- Published new blogs to share knowledge in formal methods, particularly in model checking with TLA+.
- Proudly announce that our Inference grammar parser is ready and being actively tested internally.
- Published a Rust crate with the grammar parser (will be publicly announced soon).
- Welcome thousands of visitors to our site, and welcome our new followers.

Stay connected for more innovative updates and join us on our journey to protect the future of blockchain! ⭐️

Visit us at http://www.inferara.com and follow us on X https://x.com/Inferara_kk

Specifying Algorithms Using Non-Deterministic Computations

Jul 4, 2024

#inference

In this article, we will discuss the use of the formalism of non-deterministic computations as a language for specifying algorithms. Through presented examples, we will show how extending Rust with just a few constructs with non-deterministic semantics allows us to formulate algorithm specifications, describing their behavior with the same rigor and completeness as predicate logic statements.

Read: https://www.inferara.com/papers/specifying-algorithms-using-non-deterministic-computations/

Hi everyone! Long time no posting here. But now we have a cool news.

We are happy to announce that Inferara has achieved official organizational status in Japan.
Our headquarters is officially registered in Fukuoka City.

https://www.inferara.com/en/contact/

Additionally, we have been using for some time Discord for a more casual chatting and conversations not limited to the professional domain. So if you want to discuss news from the formal methods/blockchain world, please join us.

https://discord.gg/NgWfmnmS5C

Here we will continue posting our work updates.

Introduction to Logic in Computer Science

Our latest blog post offers a concise overview of these topics based on Michael Huth and Mark Ryan's renowned book, Logic in Computer Science.

In this post, we cover:

- The importance of formal methods in program verification
- How to use propositional logic for precise specifications
- Syntax and semantics of logical expressions
- Techniques for constructing logical proofs
- Understanding standard forms like CNF and DNF

https://inferara.com/en/blog/introduction-into-logic-in-computer-science/

Blogged

https://www.inferara.com/en/blog/c-runtime/

Blogged

https://www.inferara.com/en/blog/arena-based-allocation-in-compilers/

We have updated our site. The main page now is way more informative.

https://www.inferara.com/en/

mut for struct can be convenient but error prone, what is your opinion?

https://x.com/Inferara_kk/status/1899272540142633391

New Approach to Formal Verification Methods for Combating Vulnerabilities in Smart Contracts

https://www.inferara.com/en/blog/new-approach-to-formal-verification-smart-contracts/

Blogged

https://www.inferara.com/en/blog/simplifying-continuation-passing-style-in-rust/

#rust

Blogged

https://www.inferara.com/en/blog/embedded-c-libraries/

We just published a Rust crate that provides an effective solution for formatting WebAssembly Text (WAT) code.

This crate is designed to tokenize, parse, and pretty print WAT code, thereby improving both readability and consistency.

It supports no_std environments, so it can be built for WASM.

https://github.com/Inferara/inf-wasm-tools/tree/main/wat-fmt

Blogged

https://www.inferara.com/en/blog/abstract-methods-with-auto-inferred-arguments/

Exploring how game-theoretical modeling can be applied to decentralized exchange (DEX) protocols to identify design weaknesses and strategic attack vectors.

https://www.inferara.com/en/blog/game-theoretical-assessment-dex-protocols/