Skip to content
@freespek

FreeSpek

FreeSpek

We are a loose collective of Formal Methods & Security Researchers in the blockchain space.

This org hosts current & past projects that we've worked on, including:

Solarkraft

Solarkraft is a tool for runtime monitoring of Soroban smart contracts. It tests whether a smart contract conforms to its specification during contract development, testing, and after contract deployment on the Stellar blockchain. The contract specification is written as an ensemble of TLA+ specifications, each capturing a property of the contract’s expected behavior. We use the Apalache model checker as a backend to verify the observed contract behavior.

learn more »

Exploring Automatic Model-Checking of the Ethereum specification

Together with Consensys R&D, this exploratory research project seeks to develop methods for automated verification of Ethereum Consensus Layer Specifications. Our goal is to improve the trust guarantees for these specifications by statically verifying protocol properties. We propose to establish translation rules from executable Python specifications to the TLA+ specification language, thus making the specifications amenable to model checking with Apalache.

learn more »

Pinned Loading

  1. solarkraft solarkraft Public

    Solarkraft: a runtime monitoring tool for Soroban, powered by TLA+ and Apalache

    TypeScript 12

Repositories

Showing 4 of 4 repositories
  • ssf-mc Public

    EF project Exploring Automatic Model-Checking of the Ethereum specification

    freespek/ssf-mc’s past year of commit activity
    TeX 4 Apache-2.0 0 2 1 Updated Nov 14, 2024
  • solarkraft Public

    Solarkraft: a runtime monitoring tool for Soroban, powered by TLA+ and Apalache

    freespek/solarkraft’s past year of commit activity
    TypeScript 12 Apache-2.0 0 17 1 Updated Oct 23, 2024
  • .github Public
    freespek/.github’s past year of commit activity
    0 0 0 0 Updated Jul 24, 2024
  • soroban-scripts Public

    Tiny scripts to simplify testing of / playing with Soroban smart contracts

    freespek/soroban-scripts’s past year of commit activity
    Shell 0 Apache-2.0 0 0 0 Updated Jun 6, 2024

People

This organization has no public members. You must be a member to see who’s a part of this organization.

Top languages

Loading…

Most used topics

Loading…