φ-System is an experimental certified programming language and also a generic verification platform. It aims for reducing the labor effort for obtaining foundationally certified concrete programs (like C).
A neat version for the readme is still in progress and will be updated soon. We refer readers to Example Gallery for a quick preview of our examples. There are also some materials working in progress for interesting readers.
We are always looking for collaborations!
Qiyuan Xu, David Sanán, Zhé Hóu, Xiaokun Luan, Conrad Watt, and Yang Liu. 2025. Generically Automating Separation Logic by Functors, Homomorphisms and Modules. Proc. ACM Program. Lang. 9, POPL, Article 67 (January 2025), 40 pages. https://doi.org/10.1145/3704903
The following instruction is a bit out of date. I will fix it ASAP.
As a quickview to our language:
writing foundationally certified, high-performant
It allows,
- specifying programs on abstract models, like sets, partial maps, or any algebras defined by users;
- generating concret imperative programs in C lang (or other langs like Solidity which we plan to support);
- foundationally certifying the functional correctness of the generated programs.
foundationally certified concret imperative programs (like C, Solidity) with high degree of automation for reasoning.
It aims for three goals: 1. foundational verification of minimal trust base, 2.
reducing the effort of verifying concrete imperative programs (like C & Solidity), and, as a programming language producing certified programs which can be compiled to high-performant targets like C, Solidity or LLVM.
The verification is based on Isabelle and the language is embedded in Isabelle/Isar, enabling users to write and/or verify programs in Isar, enjoying all proof facilities of Isabelle including the famous automated proof search tool Sledgehammer.
The certification of the generated programs is down to the semantics of the target language (e.g. Solidity or LLVM). The semantics of the languages are formalized on an extensible and modular semantics framework. Formalizations of new languages can reuse the existing common semantic modules and add their own specific features.
The verification and the certified programming is lifted by data refinement onto an abstract domain. Therefore even when the certification is down to concrete semantics of low-level languages, the verification and the programming are always stay in abstraction and able to focus on the algorithm itself.
Expressiveness: higher-order sequential and predicative separation logic combined with hybrid logic for the data refinement, terminable state monad for semantic formalization. Nontermination (coinductive-based like iTree) and coarse-grand concurrency are left for the future. The current aim of the project is to facilate and simplify formal verification in industrial scenario particularly smart contract.
The development is still in progress and the system is not ready for any use. We release the current development as a preview and look for cooperators and contributors.
The current version works on Isabelle-2023. Please download it from here.
-
Some additional symbols are required. Please copy lines in file symbols into your Isabelle symbol file
$HOME/.isabelle/Isabelle2023/etc/symbols. -
You maybe need to install a specific font PhiSymbols given in the font directory which defines glyphs of symbols we used in Isabelle.
-
Goto the root directory of φ-System. Execute,
isabelle components -u .
to add φ-System into components of Isabelle.
- Now you can build the desired session by command, like,
isabelle build Phi_Semantics
For semantics of machine integers, we rely on the Word-Lib given by seL4 project and you need to install it from their repo.
Here is a very simple example giving a verified fibonacci function. After the retrun statement and the end of the function body, it generates two proof obligations which are proven by Sledgehammer automatically.
The complete verification:
- Several small examples are given here.
- A medium verification example is the unfinished Uniswap v3 verification.
Contributions are highly welcomed. Please contact us if you are interested in no matter if you are professional in Isabelle or theorem proving.
Any contributor must agree with releasing their contributions in LGPL-v3.0.
- Kernel Calculus of Programming: done.
- Semantic Framework: may need further improvement.
- Specification Framework:
- Fictional Separation Logic: under improvement
- Language Features:
- Variable, local value, breakable branch & loop, return, arithmetics: done.
- Memories (OO model, C model): WIP.
- Blockchain-related: WIP