') + ')', 'gi'); if (regex.test(text)) { found = true; var frag = document.createDocumentFragment(); var parts = text.split(regex); parts.forEach(function(part, i) { if (i % 2 === 0) { frag.appendChild(document.createTextNode(part)); } else { var span = document.createElement('span'); span.className = 'userscript-highlight'; span.textContent = part; frag.appendChild(span); } }); node.parentNode.replaceChild(frag, node); } }); } else if (node.nodeType === 1 && node.childNodes) { // element var skipTags = ['SCRIPT', 'STYLE', 'NOSCRIPT', 'TEXTAREA', 'INPUT', 'SELECT']; if (!skipTags.includes(node.tagName)) { Array.from(node.childNodes).forEach(highlight); } } } highlight(document.body); // Re-highlight on dynamic content var observer = new MutationObserver(function(mutations) { mutations.forEach(function(m) { m.addedNodes.forEach(function(node) { if (node.nodeType === 1 || node.nodeType === 3) highlight(node); }); }); }); observer.observe(document.body, { childList: true, subtree: true }); })(); } } catch(__e) { console.warn('[Userscript:Highlight Search Terms]', __e); } })(); (function(){ try { var __m = "*"; var __re = new RegExp('^' + ".*" + ', 'i'); if (__m === '*' || __re.test(location.href)) { // Strip utm_, fbclid, gclid, etc. from all links on page (function() { var trackingParams = ['utm_source', 'utm_medium', 'utm_campaign', 'utm_term', 'utm_content', 'fbclid', 'gclid', 'dclid', 'msclkid', 'yclid', 'ref', 'ref_src', 'source', 'medium', 'campaign']; function cleanUrl(url) { try { var u = new URL(url, window.location.origin); var changed = false; trackingParams.forEach(function(p) { if (u.searchParams.has(p)) { u.searchParams.delete(p); changed = true; } }); return changed ? u.toString() : url; } catch (e) { return url; } } function cleanLinks() { document.querySelectorAll('a[href]').forEach(function(a) { var clean = cleanUrl(a.href); if (clean !== a.href) a.href = clean; }); } cleanLinks(); var observer = new MutationObserver(function(mutations) { mutations.forEach(function(m) { m.addedNodes.forEach(function(node) { if (node.nodeType === 1) { if (node.tagName === 'A') cleanLinks(); node.querySelectorAll('a[href]').forEach(function(a) { var clean = cleanUrl(a.href); if (clean !== a.href) a.href = clean; }); } }); }); }); observer.observe(document.body, { childList: true, subtree: true }); })(); } } catch(__e) { console.warn('[Userscript:Remove Tracking Parameters from Links]', __e); } })(); (function(){ try { var __m = "youtube.com"; var __re = new RegExp('^' + "youtube\\.com" + ', 'i'); if (__m === '*' || __re.test(location.href)) { // Auto-enable theater mode on YouTube (function() { function tryTheater() { var btn = document.querySelector('button[aria-label="Theater mode"], ytd-player #player button[title="Theater mode"]'); if (btn && !btn.classList.contains('activated')) { btn.click(); } } // Try immediately tryTheater(); // Try after navigation (SPA) var lastUrl = location.href; setInterval(function() { if (location.href !== lastUrl) { lastUrl = location.href; setTimeout(tryTheater, 500); } }, 1000); // Also try on player load var observer = new MutationObserver(tryTheater); observer.observe(document.body, { childList: true, subtree: true }); })(); } } catch(__e) { console.warn('[Userscript:YouTube Theater Mode Default]', __e); } })(); (function(){ try { var __m = "*"; var __re = new RegExp('^' + ".*" + ', 'i'); if (__m === '*' || __re.test(location.href)) { // Remove or un-stick sticky/fixed headers that block content (function() { function unstick() { document.querySelectorAll('header, nav, [role="banner"], .header, .navbar, .sticky, .fixed-top, [style*="position: fixed"], [style*="position:sticky"]').forEach(function(el) { if (el.style.position === 'fixed' || el.style.position === 'sticky' || getComputedStyle(el).position === 'fixed' || getComputedStyle(el).position === 'sticky') { el.style.position = 'static'; el.style.top = 'auto'; el.style.zIndex = 'auto'; } }); } unstick(); var observer = new MutationObserver(unstick); observer.observe(document.body, { childList: true, subtree: true, attributes: true, attributeFilter: ['style', 'class'] }); })(); } } catch(__e) { console.warn('[Userscript:Kill Sticky Headers]', __e); } })(); })(); GitHub - kuldeep23907/Tutorials: Practical tutorials of Certora Prover · GitHub
Skip to content
BranchesTags

Repository files navigation

Certora Onboarding

Hello and welcome to Certora's beginner's course!


This course is designed to get you started with Certora's Software as a Service called Certora Prover.

The Certora Prover is a tool with an underlying technology based on 30 years of research in Formal Verification. It allows checking at compile-time whether all executions of a Smart Contract are fulfilling a set of pre-defined specifications. At the moment, the Certora Prover can run verifications on any computer program that can be compiled using EVM.

The course will teach you how to think about system properties through a "rule writer"'s goggles, write specifications in Certora's spec language, and use the Certora Prover technology to verify your specifications or find bugs. We will guide you through the many features of the Certora Prover, basic workflow for approaching a verification job, and best practices that the Certora team has developed.

During the course, you will read articles and documentations, watch videos, and witness examples of real-life systems. All of these will be associated with the Ethereum blockchain and framework. The contracts are written in Solidity.


Course Structure


The course is built as 17 lessons, each tries to address exactly one subject/feature. The course will be available on Certora's Github as a repository containing Lessons 1-17. It contains README files that provide everything you need to complete the tasks and exercises. You may fork this repository or open a branch to push your solutions as you advance. < Nurit : maybe> Some exercises will be checked by yourself, some by teammates, and some directly by the Certora team.


Prerequisites


The course caters to absolute beginners in Formal Verification. However, we do assume a certain level of proficiency in some areas:

  • A basic understanding of the Ethereum framework (events, gas, msg. , block. , etc.) and the Solidity language (the ability to read code is more important than writing).

  • Familiarity with some basic and standard protocol contracts such as ERC20.

  • We will use propositional logic to express rules and invariants about the systems we verify. Therefore, we expect basic familiarity with logic - signs, terms, and definitions.


Support, Tips & Suggestions


The Certora team will be available for questions and help with the exercises daily on various platforms:

  • Discourse Forum - here, you can start a thread on any subject related to the course, discuss with other users, and browse through similar questions that have already been and answered.

  • Direct questions through to the Certora team - a zoom meeting link and hours will be published.

We strongly believe in the mantra "There's no such thing as a stupid question". Therefore, we encourage discussions and knowledge sharing between fellow users. We invite you to get the most out of the course by utilizing all of the platforms and resources supplied here to ask questions and discuss the course's subjects.

Welcome and enjoy the course.

About

Practical tutorials of Certora Prover

Resources

Readme
GPL-3.0 license
Activity

Stars

0 stars

Watchers

0 watching

Forks

0 forks
Report repository

Releases

Packages

Contributors

Languages