Suggestions and Feedback on IronSpec Framework, and Introduction to FSVT

[Mulatijiang]

Dear Authors of the IronSpec Framework,

Greetings!
I am Murat, an undergraduate student from Beijing Jiaotong University. I have recently been studying and reproducing your IronSpec framework, and I have greatly benefited from your work. I sincerely appreciate your efforts in open-sourcing such an excellent project, which provides valuable learning resources for researchers in the field.

After carefully reading and experimenting with the framework, I noticed a few minor issues that might affect reproducibility or clarity for new users. Based on this experience, I have also developed my own formal specification verification tool built on top of IronSpec. I hope the following suggestions and feedback can be of help:

---

1. Suggestions for Improving the IronSpec Framework

1.1 README File Improvements

• Spelling Errors
  • Line 154: Arguemnts → Arguments (in the parameter description section).
  • Line 19: Script path ./setup/configureIronspec.sh → ./setup/configureIronSpec.sh (ensure consistent casing).
• Confusing Script Naming

# Two different commands are mentioned:
./setup/cloudlabConfigureIronSpec.sh  # for cloud environments, not typically used locally
./setup/configureIronSpec.sh          # for default setup

I suggest clearly distinguishing the intended use cases for each script or unifying their naming conventions (e.g., using configureIronSpec.sh as the main entry point).

• Command Format and Comment Clarifications

  • ASC Module Confusion:
    In the Automatic Sanity Checking (ASC) section, there is still reference to “mutation testing.” I recommend updating the title and description for clarity:
    "The general command to run automatic sanity checking (ASC) follows this form:"

  • Broken URL Rendering:
    One of the reference links is broken due to a line break. Suggested fix:

["Deductive verification of smart contracts with dafny"](https://arxiv.org/abs/2208.02920)

1.2 Script File Optimization

• runASCExpriments.sh (AWS Module)

  • Irrelevant Comments:
    The comment # clone eth2.0 repo... does not reflect the actual logic related to AWS. Consider removing or updating it to match the module's functionality.

  • Submodule Update Issue:
    Users may encounter errors due to outdated submodules. I suggest adding the following command after cloning the project to ensure consistency:

git submodule update --init --recursive --force

1.3 Output Result and Code Fixes

• finalresult Module

  • Missing Table Number:
    Output files start with table2, skipping table1. Please consider adding table1 or adjusting the numbering logic.

  • Incorrect Command Argument:
    In the result-aggregation command:

# The second instance of "Encrypt" should be "Decrypt"
echo "|   AWS ESDK     |   Decrypt    |  $(grep "FLAG" ...decrypt... |" >> $outputfile

---

FSVT Tool and Gratitude

Inspired by IronSpec, I have developed a tool called FSVT (Formal Specification Verification Tool), which enhances and builds upon your framework. FSVT has completed its core functionality and has been successfully applied to the same benchmark projects used in IronSpec.

If you're interested, I would be delighted to share more about FSVT or discuss potential integration ideas. It would be a great honor if my tool could contribute to your research in any way. I would also deeply appreciate any guidance or suggestions for future improvements.

Thank you once again for your outstanding contribution to the open-source community. I look forward to your response and wish you continued success in your research!

Best regards,
Murat
Beijing Jiaotong University