Archive
Archive
2024â
- January 4, 2024 - đĻ Translating Rust match patterns to Coq with coq-of-rust
- January 18, 2024 - đĻ Upgrade the Rust version of coq-of-rust
- February 2, 2024 - đĻ The importance of formal verification
- February 14, 2024 - 𧎠Experiment on translation from Haskell to Coq
- February 22, 2024 - đĻĢ Translating Go to Coq, part 1
- February 29, 2024 - đĻ Improvements in the Rust translation to Coq, part 1
- March 8, 2024 - đĻ Improvements in the Rust translation to Coq, part 2
- March 22, 2024 - đĻ Improvements in the Rust translation to Coq, part 3
- April 3, 2024 - đĻ Monadic notation for the Rust translation
- April 26, 2024 - đĻ Translation of the Rust's core and alloc crates
- May 10, 2024 - đ Translation of Python code to Coq
- May 14, 2024 - đ Simulation of Python code in Coq
- May 22, 2024 - đ Simulation of Python code from traces in Coq
- June 5, 2024 - đĻ Software correctness from first principles
- June 28, 2024 - đĒ Coq of Solidity â part 1
- August 7, 2024 - đĒ Coq of Solidity â part 2
- August 12, 2024 - đĒ Coq of Solidity â part 3
- August 13, 2024 - đĒ Coq of Solidity â part 4
- August 19, 2024 - đĻ Formal verification of the type checker of Sui â part 1
- October 13, 2024 - đ˛ What we do at Formal Land
- October 14, 2024 - đĻ Formal verification of the type checker of Sui â part 2
- October 15, 2024 - đĻ Formal verification of the type checker of Sui â part 3
- October 16, 2024 - đĒ Enhancements to coq-of-solidity â 1
- October 21, 2024 - â Verification of the Smoo.th library â 1
- October 22, 2024 - đ˛ What we bring you
- October 28, 2024 - â Verification of the Smoo.th library â 2
- November 1, 2024 - âŧī¸ A formal verification tool for Noir â 1
- November 14, 2024 - đĻ Example of verification for the Move's checker of Sui
- November 15, 2024 - âŧī¸ A formal verification tool for Noir â 2
- December 20, 2024 - đĻ How does formal verification of smart contracts work?
- December 20, 2024 - đģ Translation of Circom to Coq
- December 26, 2024 - đĻ Mutually recursive functions with notation
2023â
- January 24, 2023 - đĻ Our current formal verification efforts
- April 26, 2023 - đĻ Representation of Rust methods in Coq
- May 28, 2023 - đĻ Monad for side effects in Rust
- August 25, 2023 - đĻ Trait representation in Coq
- November 8, 2023 - đĻ Optimizing Rust translation to Coq with THIR and bundled traits
- November 26, 2023 - đĻ Translation of function bodies from Rust to Coq
- December 13, 2023 - đĻ Verifying an ERC-20 smart contract in Rust