• About TC
  • Affiliate Disclaimer
  • Privacy Policy
  • TOS
  • Contact
Tuesday, August 26, 2025
Techcratic
No Result
View All Result
  • AI
    Artificial Intelligence

    7 Python Built-ins That Seem Like a Joke (Until You Use Them)

    Artificial Intelligence

    Learn Python (+ AI) and Become a Certified Data Analyst for FREE This Week

    Artificial Intelligence

    From JSON to Dashboard: Visualizing DuckDB Queries in Streamlit with Plotly

    Artificial Intelligence

    The “Super Weight:” How Even a Single Parameter can Determine a Large Language Model’s…

    Artificial Intelligence

    10 Python One-Liners to Optimize Your Machine Learning Pipelines

    Artificial Intelligence

    Streamline employee training with an intelligent chatbot powered by Amazon Q Business

    Artificial Intelligence

    Writing Your First GPU Kernel in Python with Numba and CUDA

    Artificial Intelligence

    Build a scalable containerized web application on AWS using the MERN stack with Amazon Q…

    Artificial Intelligence

    Introducing Amazon Bedrock AgentCore Identity: Securing agentic AI at scale

  • Apple
    macOS Tahoe will add three new apps to your Mac, here’s what’s coming

    macOS Tahoe adds three new apps to your Mac, here’s what’s coming

    Seven products Apple will discontinue following iPhone 17 event

    Seven products Apple will discontinue following iPhone 17 event

    How to watch iPhone 17 event Awe Dropping live

    How to watch iPhone 17 event Awe Dropping live

    How to watch Apple’s iPhone 17 event live on September 9

    How to watch Apple’s iPhone 17 event live on September 9

    Apple’s September iPhone event: Date, time, and what will Apple launch

    Apple’s September iPhone event: Date, time, and what will Apple launch

    iPad Pro, M4 iMac, iPhone 15 Pro Max, MacBook Air, more 9to5Mac

    iPad Pro, M4 iMac, iPhone 15 Pro Max, MacBook Air, more 9to5Mac

    Apple researchers taught an LLM to predict tokens up to 5x faster

    Apple still debating Mistral and Perplexity M&A amid looming Google Search shakeup

    Microphone, volume control for iPhone

    Microphone, volume control for iPhone

    The iPhone 17 Pro might finally get a feature rumored since the iPhone 12

    The iPhone 17 Pro might finally get a feature rumored since the iPhone 12

  • ComputerWorld
    Dropbox to offer its genAI service Dash for download

    Dropbox to offer its genAI service Dash for download

    Intel warns US govt equity stake could disrupt its global business and strategic deals

    Intel warns US govt equity stake could disrupt its global business and strategic deals

    US threat of sanctions on EU officials over tech law raises risks for enterprises

    US threat of sanctions on EU officials over tech law raises risks for enterprises

    As US takes 10% stake in Intel, new questions arise for enterprise buyers

    As US takes 10% stake in Intel, new questions arise for enterprise buyers

    AI bigwigs bow to US gov’t demands on pricing, but could see long-term benefits

    AI bigwigs bow to US gov’t demands on pricing, but could see long-term benefits

    Why IT leaders think generative AI will create jobs

    Why IT leaders think generative AI will create jobs

    Developers who don’t document code? Blame the bosses

    Developers who don’t document code? Blame the bosses

    Rise of AI crawlers and bots causing web traffic havoc

    Rise of AI crawlers and bots causing web traffic havoc

    Adobe Acrobat Studio brings genAI power to PDFs

    Adobe Acrobat Studio brings genAI power to PDFs

  • Gaming
    Starship Troopers Extermination: Last Man Standing

    Starship Troopers Extermination: Last Man Standing

    I don’t need 64 GB of RAM but I am tempted when prices are as low as they are right now for genuinely speedy sticks

    Is Steam down again? Yep, and it does this every Tuesday

    As Dusk Falls Pt.2: WHO THE F IS BRUCE?!

    As Dusk Falls Pt.2: WHO THE F IS BRUCE?!

    DIABLO 4 SEASON 1 REVIEW

    DIABLO 4 SEASON 1 REVIEW

    REDRAGON S101 GAMING KEYBOARD

    CRKD’s Vortex is a twist on a Peak Design backpack, but for gaming

    Sonic Frontiers Final Review: The Supercut

    Sonic Frontiers Final Review: The Supercut

    Gears of War: Reloaded PC performance: The updated graphics are easy work for any desktop GPU from the past six years but they’re still enough to give handhelds grief

    Gears of War: Reloaded PC performance: The updated graphics are easy work for any desktop GPU from the past six years but they’re still enough to give handhelds grief

    Gotham Knights Running on SteamOS! Steam Deck Handheld Gameplay

    Gotham Knights Running on SteamOS! Steam Deck Handheld Gameplay

    Linus Torvalds has apparently met Bill Gates for the first time in person and before you ask, no he didn’t clock him in the face

    It’s downright nuts how good this fan remake of Fallout 1 in Doom looks, and I’m begging Bethesda to take note

  • Retro Rewind
    Retro Rewind: Game Players Issue 80 Magazine January 1996

    Retro Rewind: Game Players Issue 80 Magazine January 1996

    Retro Rewind: Video Game Trader Winter 2014

    Retro Rewind: Video Game Trader Winter 2014

    Retro Rewind: Electronic Games April 1995

    Retro Rewind: Electronic Games April 1995

    Retro Rewind: Electronic Gaming Monthly Magazine Number 55 February 1994

    Retro Rewind: Electronic Gaming Monthly Magazine Number 57 April 1994

    Retro Rewind: Blast from the Past – 35 Iconic Commercials of 1988!

    Retro Rewind: Blast from the Past – 35 Iconic Commercials of 1988!

    Retro Rewind: PC World Magazine August 1998

    Retro Rewind: PC World Magazine August 1998

    Retro Rewind: Computer Shopper Magazine September 1997

    Retro Rewind: Computer Shopper Magazine September 1997

    Retro Rewind: PC Magazine December 2015

    Retro Rewind: PC Magazine December 2015

    Retro Rewind: EDGE Magazine RETRO #1: The Guide to Classic Videogame Playing and Collecting

    Retro Rewind: EDGE Magazine RETRO #1: The Guide to Classic Videogame Playing and Collecting

  • Tech Art
    HOW I RENDER in IBISPAINT | My MOST UPDATED RENDERING TUTORIAL

    HOW I RENDER in IBISPAINT | My MOST UPDATED RENDERING TUTORIAL

    Don’t make these shading mistakes

    Don’t make these shading mistakes

    AR Car Showroom App Review – Augmented Reality Vehicle Showcase

    AR Car Showroom App Review – Augmented Reality Vehicle Showcase

    Infinite design tutorial (vector art) step by step | ultimate focus tamil

    Infinite design tutorial (vector art) step by step | ultimate focus tamil

    (877) Awesome Peach and Gold Spray Paint Mixed Media Pour

    (877) Awesome Peach and Gold Spray Paint Mixed Media Pour

    Kirito's Elucidator (Sword Art Online) – MAN AT ARMS

    Kirito's Elucidator (Sword Art Online) – MAN AT ARMS

    Using Colored Pencil with Art Markers | Mixed Media Tips

    Using Colored Pencil with Art Markers | Mixed Media Tips

    The Black Feminist Subconscious of Ufuoma Essi’s Films

    The Black Feminist Subconscious of Ufuoma Essi’s Films

    AK Interactive 3rd Gen | Black Primer | Try out

    AK Interactive 3rd Gen | Black Primer | Try out

  • Tech Deals
    DUMOS L Shaped Desk Computer Gaming Corner Table 50 Inch Home Office Writing Student…

    DUMOS L Shaped Desk Computer Gaming Corner Table 50 Inch Home Office Writing Student…

    Mini PC, with 12th Gen Intel Twin Lake N150 (Up to 3.4Ghz), 16GB DDR4 RAM 512GB SSD…

    Mini PC, with 12th Gen Intel Twin Lake N150 (Up to 3.4Ghz), 16GB DDR4 RAM 512GB SSD…

    Western Digital WD Red 10TB NAS Internal Hard Drive, 5400 RPM Class, 256 MB Cache, 3.5”…

    Western Digital WD Red 10TB NAS Internal Hard Drive, 5400 RPM Class, 256 MB Cache, 3.5”…

    Vantec USB 3.1 Type C 4-Port Bus-Powered Travel Hub Components Other UGT-MH410U3-C

    Vantec USB 3.1 Type C 4-Port Bus-Powered Travel Hub Components Other UGT-MH410U3-C

    Toshiba Canvio Advance 1TB Portable External Hard Drive USB 3.0, Black – HDTCA10XK3AA

    Toshiba Canvio Advance 1TB Portable External Hard Drive USB 3.0, Black – HDTCA10XK3AA

    TCL 98-Inch Class QM8K Series QD-Mini LED 4K UHD Google Smart TV Next Generation…

    TCL 98-Inch Class QM8K Series QD-Mini LED 4K UHD Google Smart TV Next Generation…

    TCL 75-Inch Class QM7K Series QD-Mini LED 4K UHD Google Smart TV Best Premium Mini-LED…

    TCL 75-Inch Class QM7K Series QD-Mini LED 4K UHD Google Smart TV Best Premium Mini-LED…

    TCL 65-Inch Class QM6K Series QD-Mini LED 4K UHD Google Smart TV Best Value Mini-LED TV…

    TCL 65-Inch Class QM6K Series QD-Mini LED 4K UHD Google Smart TV Best Value Mini-LED TV…

    TEAMGROUP QX 2TB 3D NAND QLC 2.5 Inch SATA III Internal Solid State Drive SSD R/W Speed…

    TEAMGROUP QX 2TB 3D NAND QLC 2.5 Inch SATA III Internal Solid State Drive SSD R/W Speed…

  • Techs Got To Eat
    Spicy Chickpea Shakshuka Mug: 5-Minute Vegetarian Fuel

    Spicy Chickpea Shakshuka Mug: 5-Minute Vegetarian Fuel

    Bacon & Spinach Mug Quiche: 3-Minute Gourmet Breakfast

    Bacon & Spinach Mug Quiche: 3-Minute Gourmet Breakfast

    Cheesy Broccoli Rice Mug: 5-Minute Super Comfort Food

    Cheesy Broccoli Rice Mug: 5-Minute Super Comfort Food

    Top 10 Vegetarian Recipes for 2025: Easy and Nutritious Meals for Busy People

    Top 10 Vegetarian Recipes for 2025: Easy and Nutritious Meals for Busy People

    Bacon Mug Lasagna: 5-Minute Microwave Meat Lover’s Dream

    Bacon Mug Lasagna: 5-Minute Microwave Meat Lover’s Dream

    Bacon Fried Rice Mug: 5-Minute Microwave Meal

    Bacon Fried Rice Mug: 5-Minute Microwave Meal

    Bacon & Cheddar Mug Biscuit: 2-Minute Savory Comfort

    Bacon & Cheddar Mug Biscuit: 2-Minute Savory Comfort

    Loaded Bacon Cheesy Potato Mug: 5-Minute Comfort Food

    Loaded Bacon Cheesy Potato Mug: 5-Minute Comfort Food

    Peanut Butter Banana Mug Muffin: 5-Minute Protein Snack

    Peanut Butter Banana Mug Muffin: 5-Minute Protein Snack

  • Tesla
    BestEvMod Center Console Armrest Pad Cover Compatible with Tesla Cybertruck 2024 2025…

    BestEvMod Center Console Armrest Pad Cover Compatible with Tesla Cybertruck 2024 2025…

    Carwiner Center Console Cover for Tesla Model 3 Model Y, PU Leather Armrest Box Cushion…

    Carwiner Center Console Cover for Tesla Model 3 Model Y, PU Leather Armrest Box Cushion…

    Tesla announces Cybertruck expansion into South Korea

    Tesla announces Cybertruck expansion into South Korea

    Metra – Speaker Plate – Fits Select BMW, Porsche, Range Rover, Tesla (82-8601)

    Metra – Speaker Plate – Fits Select BMW, Porsche, Range Rover, Tesla (82-8601)

    DREIEYECAM Dash cam for Tesla Model S AP1 Full HD 1080P WiFi G-Sensor WDR is Auto Video…

    DREIEYECAM Dash cam for Tesla Model S AP1 Full HD 1080P WiFi G-Sensor WDR is Auto Video…

    Center Console Organizer Tray for Tesla Model Y 2024-2020(Not Fit 2024 2025Model Y…

    Center Console Organizer Tray for Tesla Model Y 2024-2020(Not Fit 2024 2025Model Y…

    Wuyaoyao Car Interior LED Lights, 4 in 1 Car Ambient Lighting Kit, Automotive Neon Light…

    Wuyaoyao Car Interior LED Lights, 4 in 1 Car Ambient Lighting Kit, Automotive Neon Light…

    Seat Adjustment Button Black Trims For Tesla Model 3/Y 2021 2022 2023 Front Passenger…

    Seat Adjustment Button Black Trims For Tesla Model 3/Y 2021 2022 2023 Front Passenger…

    Car Windshield Cleaning Tool, Microfiber Auto Window Cleaner with 4 Cloth Pads & Long…

    Car Windshield Cleaning Tool, Microfiber Auto Window Cleaner with 4 Cloth Pads & Long…

  • UFO
    Under Armour Men’s Freedom Banner Short Sleeve T Shirt

    Under Armour Men’s Freedom Banner Short Sleeve T Shirt

    #most #famous #encounters of #3types with #extraterrestrial in #history P.1.3 –

    #most #famous #encounters of #3types with #extraterrestrial in #history P.1.3 –

    ANCIENT ALIEN IMAGES FOUND | The Proof Is Out There | #Shorts

    ANCIENT ALIEN IMAGES FOUND | The Proof Is Out There | #Shorts

    Funny Hawaiian Shirts for Men Palm Beach Shirts Tropical Vacation Shirts O3

    Funny Hawaiian Shirts for Men Palm Beach Shirts Tropical Vacation Shirts O3

    #love #truth

    #love #truth

    M18 Brushless Motor Drone with 4K Camera Mini RC Quadcopter for Adults Dual Cameras Optical Flow Positioning

    M18 Brushless Motor Drone with 4K Camera Mini RC Quadcopter for Adults Dual Cameras Optical Flow Positioning

    Desert Landscape Pictures Ufo Canvas Wall Art Desert Cactus Painting Alien Ufo Desert Poster Vintage Ufo Wall Art Trippy Spaceship Canvas Picture Vintage Desert Artwork for Wall 16x24inch No Frame

    Desert Landscape Pictures Ufo Canvas Wall Art Desert Cactus Painting Alien Ufo Desert Poster Vintage Ufo Wall Art Trippy Spaceship Canvas Picture Vintage Desert Artwork for Wall 16x24inch No Frame

    Calvine “UFO” Investigation Update

    Calvine “UFO” Investigation Update

    Sailwind Men’s Henley Shirts Long Sleeve Button T-Shirt Casual Stylish Cotton Pullover Shirt with Pocket

    Sailwind Men’s Henley Shirts Long Sleeve Button T-Shirt Casual Stylish Cotton Pullover Shirt with Pocket

  • AI
    Artificial Intelligence

    7 Python Built-ins That Seem Like a Joke (Until You Use Them)

    Artificial Intelligence

    Learn Python (+ AI) and Become a Certified Data Analyst for FREE This Week

    Artificial Intelligence

    From JSON to Dashboard: Visualizing DuckDB Queries in Streamlit with Plotly

    Artificial Intelligence

    The “Super Weight:” How Even a Single Parameter can Determine a Large Language Model’s…

    Artificial Intelligence

    10 Python One-Liners to Optimize Your Machine Learning Pipelines

    Artificial Intelligence

    Streamline employee training with an intelligent chatbot powered by Amazon Q Business

    Artificial Intelligence

    Writing Your First GPU Kernel in Python with Numba and CUDA

    Artificial Intelligence

    Build a scalable containerized web application on AWS using the MERN stack with Amazon Q…

    Artificial Intelligence

    Introducing Amazon Bedrock AgentCore Identity: Securing agentic AI at scale

  • Apple
    macOS Tahoe will add three new apps to your Mac, here’s what’s coming

    macOS Tahoe adds three new apps to your Mac, here’s what’s coming

    Seven products Apple will discontinue following iPhone 17 event

    Seven products Apple will discontinue following iPhone 17 event

    How to watch iPhone 17 event Awe Dropping live

    How to watch iPhone 17 event Awe Dropping live

    How to watch Apple’s iPhone 17 event live on September 9

    How to watch Apple’s iPhone 17 event live on September 9

    Apple’s September iPhone event: Date, time, and what will Apple launch

    Apple’s September iPhone event: Date, time, and what will Apple launch

    iPad Pro, M4 iMac, iPhone 15 Pro Max, MacBook Air, more 9to5Mac

    iPad Pro, M4 iMac, iPhone 15 Pro Max, MacBook Air, more 9to5Mac

    Apple researchers taught an LLM to predict tokens up to 5x faster

    Apple still debating Mistral and Perplexity M&A amid looming Google Search shakeup

    Microphone, volume control for iPhone

    Microphone, volume control for iPhone

    The iPhone 17 Pro might finally get a feature rumored since the iPhone 12

    The iPhone 17 Pro might finally get a feature rumored since the iPhone 12

  • ComputerWorld
    Dropbox to offer its genAI service Dash for download

    Dropbox to offer its genAI service Dash for download

    Intel warns US govt equity stake could disrupt its global business and strategic deals

    Intel warns US govt equity stake could disrupt its global business and strategic deals

    US threat of sanctions on EU officials over tech law raises risks for enterprises

    US threat of sanctions on EU officials over tech law raises risks for enterprises

    As US takes 10% stake in Intel, new questions arise for enterprise buyers

    As US takes 10% stake in Intel, new questions arise for enterprise buyers

    AI bigwigs bow to US gov’t demands on pricing, but could see long-term benefits

    AI bigwigs bow to US gov’t demands on pricing, but could see long-term benefits

    Why IT leaders think generative AI will create jobs

    Why IT leaders think generative AI will create jobs

    Developers who don’t document code? Blame the bosses

    Developers who don’t document code? Blame the bosses

    Rise of AI crawlers and bots causing web traffic havoc

    Rise of AI crawlers and bots causing web traffic havoc

    Adobe Acrobat Studio brings genAI power to PDFs

    Adobe Acrobat Studio brings genAI power to PDFs

  • Gaming
    Starship Troopers Extermination: Last Man Standing

    Starship Troopers Extermination: Last Man Standing

    I don’t need 64 GB of RAM but I am tempted when prices are as low as they are right now for genuinely speedy sticks

    Is Steam down again? Yep, and it does this every Tuesday

    As Dusk Falls Pt.2: WHO THE F IS BRUCE?!

    As Dusk Falls Pt.2: WHO THE F IS BRUCE?!

    DIABLO 4 SEASON 1 REVIEW

    DIABLO 4 SEASON 1 REVIEW

    REDRAGON S101 GAMING KEYBOARD

    CRKD’s Vortex is a twist on a Peak Design backpack, but for gaming

    Sonic Frontiers Final Review: The Supercut

    Sonic Frontiers Final Review: The Supercut

    Gears of War: Reloaded PC performance: The updated graphics are easy work for any desktop GPU from the past six years but they’re still enough to give handhelds grief

    Gears of War: Reloaded PC performance: The updated graphics are easy work for any desktop GPU from the past six years but they’re still enough to give handhelds grief

    Gotham Knights Running on SteamOS! Steam Deck Handheld Gameplay

    Gotham Knights Running on SteamOS! Steam Deck Handheld Gameplay

    Linus Torvalds has apparently met Bill Gates for the first time in person and before you ask, no he didn’t clock him in the face

    It’s downright nuts how good this fan remake of Fallout 1 in Doom looks, and I’m begging Bethesda to take note

  • Retro Rewind
    Retro Rewind: Game Players Issue 80 Magazine January 1996

    Retro Rewind: Game Players Issue 80 Magazine January 1996

    Retro Rewind: Video Game Trader Winter 2014

    Retro Rewind: Video Game Trader Winter 2014

    Retro Rewind: Electronic Games April 1995

    Retro Rewind: Electronic Games April 1995

    Retro Rewind: Electronic Gaming Monthly Magazine Number 55 February 1994

    Retro Rewind: Electronic Gaming Monthly Magazine Number 57 April 1994

    Retro Rewind: Blast from the Past – 35 Iconic Commercials of 1988!

    Retro Rewind: Blast from the Past – 35 Iconic Commercials of 1988!

    Retro Rewind: PC World Magazine August 1998

    Retro Rewind: PC World Magazine August 1998

    Retro Rewind: Computer Shopper Magazine September 1997

    Retro Rewind: Computer Shopper Magazine September 1997

    Retro Rewind: PC Magazine December 2015

    Retro Rewind: PC Magazine December 2015

    Retro Rewind: EDGE Magazine RETRO #1: The Guide to Classic Videogame Playing and Collecting

    Retro Rewind: EDGE Magazine RETRO #1: The Guide to Classic Videogame Playing and Collecting

  • Tech Art
    HOW I RENDER in IBISPAINT | My MOST UPDATED RENDERING TUTORIAL

    HOW I RENDER in IBISPAINT | My MOST UPDATED RENDERING TUTORIAL

    Don’t make these shading mistakes

    Don’t make these shading mistakes

    AR Car Showroom App Review – Augmented Reality Vehicle Showcase

    AR Car Showroom App Review – Augmented Reality Vehicle Showcase

    Infinite design tutorial (vector art) step by step | ultimate focus tamil

    Infinite design tutorial (vector art) step by step | ultimate focus tamil

    (877) Awesome Peach and Gold Spray Paint Mixed Media Pour

    (877) Awesome Peach and Gold Spray Paint Mixed Media Pour

    Kirito's Elucidator (Sword Art Online) – MAN AT ARMS

    Kirito's Elucidator (Sword Art Online) – MAN AT ARMS

    Using Colored Pencil with Art Markers | Mixed Media Tips

    Using Colored Pencil with Art Markers | Mixed Media Tips

    The Black Feminist Subconscious of Ufuoma Essi’s Films

    The Black Feminist Subconscious of Ufuoma Essi’s Films

    AK Interactive 3rd Gen | Black Primer | Try out

    AK Interactive 3rd Gen | Black Primer | Try out

  • Tech Deals
    DUMOS L Shaped Desk Computer Gaming Corner Table 50 Inch Home Office Writing Student…

    DUMOS L Shaped Desk Computer Gaming Corner Table 50 Inch Home Office Writing Student…

    Mini PC, with 12th Gen Intel Twin Lake N150 (Up to 3.4Ghz), 16GB DDR4 RAM 512GB SSD…

    Mini PC, with 12th Gen Intel Twin Lake N150 (Up to 3.4Ghz), 16GB DDR4 RAM 512GB SSD…

    Western Digital WD Red 10TB NAS Internal Hard Drive, 5400 RPM Class, 256 MB Cache, 3.5”…

    Western Digital WD Red 10TB NAS Internal Hard Drive, 5400 RPM Class, 256 MB Cache, 3.5”…

    Vantec USB 3.1 Type C 4-Port Bus-Powered Travel Hub Components Other UGT-MH410U3-C

    Vantec USB 3.1 Type C 4-Port Bus-Powered Travel Hub Components Other UGT-MH410U3-C

    Toshiba Canvio Advance 1TB Portable External Hard Drive USB 3.0, Black – HDTCA10XK3AA

    Toshiba Canvio Advance 1TB Portable External Hard Drive USB 3.0, Black – HDTCA10XK3AA

    TCL 98-Inch Class QM8K Series QD-Mini LED 4K UHD Google Smart TV Next Generation…

    TCL 98-Inch Class QM8K Series QD-Mini LED 4K UHD Google Smart TV Next Generation…

    TCL 75-Inch Class QM7K Series QD-Mini LED 4K UHD Google Smart TV Best Premium Mini-LED…

    TCL 75-Inch Class QM7K Series QD-Mini LED 4K UHD Google Smart TV Best Premium Mini-LED…

    TCL 65-Inch Class QM6K Series QD-Mini LED 4K UHD Google Smart TV Best Value Mini-LED TV…

    TCL 65-Inch Class QM6K Series QD-Mini LED 4K UHD Google Smart TV Best Value Mini-LED TV…

    TEAMGROUP QX 2TB 3D NAND QLC 2.5 Inch SATA III Internal Solid State Drive SSD R/W Speed…

    TEAMGROUP QX 2TB 3D NAND QLC 2.5 Inch SATA III Internal Solid State Drive SSD R/W Speed…

  • Techs Got To Eat
    Spicy Chickpea Shakshuka Mug: 5-Minute Vegetarian Fuel

    Spicy Chickpea Shakshuka Mug: 5-Minute Vegetarian Fuel

    Bacon & Spinach Mug Quiche: 3-Minute Gourmet Breakfast

    Bacon & Spinach Mug Quiche: 3-Minute Gourmet Breakfast

    Cheesy Broccoli Rice Mug: 5-Minute Super Comfort Food

    Cheesy Broccoli Rice Mug: 5-Minute Super Comfort Food

    Top 10 Vegetarian Recipes for 2025: Easy and Nutritious Meals for Busy People

    Top 10 Vegetarian Recipes for 2025: Easy and Nutritious Meals for Busy People

    Bacon Mug Lasagna: 5-Minute Microwave Meat Lover’s Dream

    Bacon Mug Lasagna: 5-Minute Microwave Meat Lover’s Dream

    Bacon Fried Rice Mug: 5-Minute Microwave Meal

    Bacon Fried Rice Mug: 5-Minute Microwave Meal

    Bacon & Cheddar Mug Biscuit: 2-Minute Savory Comfort

    Bacon & Cheddar Mug Biscuit: 2-Minute Savory Comfort

    Loaded Bacon Cheesy Potato Mug: 5-Minute Comfort Food

    Loaded Bacon Cheesy Potato Mug: 5-Minute Comfort Food

    Peanut Butter Banana Mug Muffin: 5-Minute Protein Snack

    Peanut Butter Banana Mug Muffin: 5-Minute Protein Snack

  • Tesla
    BestEvMod Center Console Armrest Pad Cover Compatible with Tesla Cybertruck 2024 2025…

    BestEvMod Center Console Armrest Pad Cover Compatible with Tesla Cybertruck 2024 2025…

    Carwiner Center Console Cover for Tesla Model 3 Model Y, PU Leather Armrest Box Cushion…

    Carwiner Center Console Cover for Tesla Model 3 Model Y, PU Leather Armrest Box Cushion…

    Tesla announces Cybertruck expansion into South Korea

    Tesla announces Cybertruck expansion into South Korea

    Metra – Speaker Plate – Fits Select BMW, Porsche, Range Rover, Tesla (82-8601)

    Metra – Speaker Plate – Fits Select BMW, Porsche, Range Rover, Tesla (82-8601)

    DREIEYECAM Dash cam for Tesla Model S AP1 Full HD 1080P WiFi G-Sensor WDR is Auto Video…

    DREIEYECAM Dash cam for Tesla Model S AP1 Full HD 1080P WiFi G-Sensor WDR is Auto Video…

    Center Console Organizer Tray for Tesla Model Y 2024-2020(Not Fit 2024 2025Model Y…

    Center Console Organizer Tray for Tesla Model Y 2024-2020(Not Fit 2024 2025Model Y…

    Wuyaoyao Car Interior LED Lights, 4 in 1 Car Ambient Lighting Kit, Automotive Neon Light…

    Wuyaoyao Car Interior LED Lights, 4 in 1 Car Ambient Lighting Kit, Automotive Neon Light…

    Seat Adjustment Button Black Trims For Tesla Model 3/Y 2021 2022 2023 Front Passenger…

    Seat Adjustment Button Black Trims For Tesla Model 3/Y 2021 2022 2023 Front Passenger…

    Car Windshield Cleaning Tool, Microfiber Auto Window Cleaner with 4 Cloth Pads & Long…

    Car Windshield Cleaning Tool, Microfiber Auto Window Cleaner with 4 Cloth Pads & Long…

  • UFO
    Under Armour Men’s Freedom Banner Short Sleeve T Shirt

    Under Armour Men’s Freedom Banner Short Sleeve T Shirt

    #most #famous #encounters of #3types with #extraterrestrial in #history P.1.3 –

    #most #famous #encounters of #3types with #extraterrestrial in #history P.1.3 –

    ANCIENT ALIEN IMAGES FOUND | The Proof Is Out There | #Shorts

    ANCIENT ALIEN IMAGES FOUND | The Proof Is Out There | #Shorts

    Funny Hawaiian Shirts for Men Palm Beach Shirts Tropical Vacation Shirts O3

    Funny Hawaiian Shirts for Men Palm Beach Shirts Tropical Vacation Shirts O3

    #love #truth

    #love #truth

    M18 Brushless Motor Drone with 4K Camera Mini RC Quadcopter for Adults Dual Cameras Optical Flow Positioning

    M18 Brushless Motor Drone with 4K Camera Mini RC Quadcopter for Adults Dual Cameras Optical Flow Positioning

    Desert Landscape Pictures Ufo Canvas Wall Art Desert Cactus Painting Alien Ufo Desert Poster Vintage Ufo Wall Art Trippy Spaceship Canvas Picture Vintage Desert Artwork for Wall 16x24inch No Frame

    Desert Landscape Pictures Ufo Canvas Wall Art Desert Cactus Painting Alien Ufo Desert Poster Vintage Ufo Wall Art Trippy Spaceship Canvas Picture Vintage Desert Artwork for Wall 16x24inch No Frame

    Calvine “UFO” Investigation Update

    Calvine “UFO” Investigation Update

    Sailwind Men’s Henley Shirts Long Sleeve Button T-Shirt Casual Stylish Cotton Pullover Shirt with Pocket

    Sailwind Men’s Henley Shirts Long Sleeve Button T-Shirt Casual Stylish Cotton Pullover Shirt with Pocket

No Result
View All Result
Techcratic
No Result
View All Result
Home Hacker News

Introducing clean, a formal verification DSL for zk circuits in Lean4

Hacker News by Hacker News
March 27, 2025
in Hacker News
Reading Time: 19 mins read
126
A A
0

2025-03-27 14:33:00
blog.zksecurity.xyz

We are really excited to share our initial steps towards building clean, an embedded DSL and formal verification framework for ZK circuits in Lean4.
As we recently shared, Zero Knowledge circuits are full of bugs, but fortunately, techniques like formal verification can provide a huge confidence boost in the correctness of ZK circuits.
Clean enables us to define circuits in Lean4, specify their desired properties, and – most importantly – formally prove them!
This work is part of the zkEVM Formal Verification Project which aims to provide infrastructure and tooling to enable formal verification for zkEVMs.
Read about clean below, or watch our presentation on it in the zkEVM project updates call.

Objectives

Our objective is to build an embedded DSL for writing zk circuits in Lean4, that allows us to reason about them in a formal way.
We believe that co-locating circuit definitions with their desired specification and correctness proof will allow us to create a robust library of reusable formally verified circuit gadgets.

We currently target AIR arithmetization, and we assume to have a table lookup primitive available by the underlying proof system.

How to formally verify ZK circuits

In order to reason formally about ZK circuits, we first need to define a formal model. This involves the following steps:

  1. Defining what primitives our circuit language supports, i.e., which are the operations that we can use to define circuits.
  2. Defining the semantics of such primitives.
  3. Defining what are the properties we are interested to formally prove for a given circuit.

Our language allows us to specify a circuit, which is composed of two main objects.

  • A collection of variables, and
  • constraints and lookup relations over those variables.
    The goal of a zero-knowledge proof system is exactly to convince a verifier that the prover knows a witness (i.e., an assignment of the variables) that satisfies the constraints and lookups of a given circuit.

At a fundamental level, for a given circuit we are interested in how the satisfaction of the constraints and the witness are related.
In other words: if a witness satisfies the constraints, what property can we infer about it?

Let’s make a concrete example.
Consider a circuit defined over one variable x and that is composed of only one contraint:

This is a very common gadget that ensures that x is a boolean value, i.e., it is either 0 or 1.
The specification of this ciruit can be expressed as:

Albeit being a very simple example, it shows the basic idea: we are interested in formally proving that if an assignment to the variables satisfies the constraints, then the specification holds as well.
We are also interested in the other direction: if an honest prover holds a witness that satisfies the specification, then there exists an assignment of the variables that satisfies the constraints.
Take the following alternative implementation of a boolean check

This new constraint is sound, because the only valid assignment that satifies it is x = 0, which is a boolean value.
However, it is not complete, as an honest prover that holds a valid boolean x = 1 cannot provide a witness that satisfies the constraint.

More formally, the two properties we want to prove are:

  • Soundness: if the prover can exhibit any witness that satisfies the constraints and lookup relations defined by the circuit, then some specification property holds over that witness. Proving this property ensures that the circuit is not underconstrained.
  • Completeness: for every possible input, an honest prover can always exhibit a witness that satisfies the constraints and lookup relations defined by the circuit. Proving this property ensures that the circuit is not overconstrained.

DSL design

In our DSL, we support four basic operations for defining circuits.

inductive Operation (F : Type) [Field F] where
  | witness : (m: ℕ) -> (compute : Environment F -> Vector F m) -> Operation F
  | assert : Expression F -> Operation F
  | lookup : Lookup F -> Operation F
  | subcircuit : {n : ℕ} -> SubCircuit F n -> Operation F

Indeed, we can:

  • Witness: introduce m new variables in the circuit, and add them to the witness.
    This operation accepts also a compute function, which represents the witness generation function, in the honest prover case.
  • Assert: add a new constraint to the circuit.
  • Lookup: add a new lookup relation to the circuit. A lookup defines which variables are being looked up and in which other table.
  • Subcircuit: add a new subcircuit to the circuit.
    The subcircuit is instantiated in the current environment, and the internal variables of the subcircuit are added to the witness.
    This is the main way to gain composability of gadgets.

To enhance usability, we provide a way to define a circuit using a monadic interface, with a lot of convenience functions.
This interface allows us to define the circuits using very natural syntax constructs.

Design of the composable verification framework

The main building block of our framework is the FormalCircuit structure.

structure FormalCircuit (F: Type) (β α: TypeMap)
  [Field F] [ProvableType α] [ProvableType β]
where
  main: Var β F -> Circuit F (Var α F)
  assumptions: β F -> Prop
  spec: β F -> α F -> Prop

  soundness:
    ∀ offset : ℕ, ∀ env,
    -- for all inputs that satisfy the assumptions
    ∀ b_var : Var β F, ∀ b : β F, eval env b_var = b ->
    assumptions b ->
    -- if the constraints hold
    constraints_hold.soundness env (circuit.main b_var |>.operations offset) ->
    -- the spec holds on the input and output
    let a := eval env (circuit.output b_var offset)
    spec b a
  
  completeness:
    -- for all environments which _use the default witness generators for local variables_
    ∀ offset : ℕ, ∀ env, ∀ b_var : Var β F,
    env.uses_local_witnesses (circuit.main b_var |>.operations offset) ->
    -- for all inputs that satisfy the assumptions
    ∀ b : β F, eval env b_var = b ->
    assumptions b ->
    -- the constraints hold
    constraints_hold.completeness env (circuit.main b_var |>.operations offset)

This structure tightly packages in a dependent-type way, the following objects:

  • β and α are respectively the input and output “shapes”, essentially they define a structured collection of elements.
  • main: the circuit definition itself.
  • assumptions: the assumptions that the circuit makes on the inputs. All properties are proved assuming that the input variables satisfy these assumptions.
  • spec: the specification property of the circuit.
  • soundness: proof for soundness of the circuit.
  • completeness: proof for completeness of the circuit.

A FormalCircuit encapsulates a formally proved, reusable gadget: when instantiating a FormalCircuit as a subcircuit, we are able to reuse the soundness and completeness proofs of the subcircuit to prove the soundness and completeness properties of the whole circuit.
This is accomplished by automatically replacing the constraints of a subcircuit with its (formally verified) spec.
In this way we can formally verify even large circuits by applying a divide-et-impera approach: we start by defining and proving correctness of low-level reusable gadgets, and then combine them to build more and more complex circuits.

A concrete example: 8-bit addition

Let’s walk through one of the simple gadgets we have implemented and verified: addition on 8-bit numbers.
This is a gadget that takes as input two bytes and an input carry, and returns the sum of the two bytes modulo 256, and the output carry.
First, we need to define the input and output shapes.

structure Inputs (F : Type) where
  x: F
  y: F
  carry_in: F

structure Outputs (F : Type) where
  z: F
  carry_out: F

Now, we define the assumptions the circuit makes on the input values, and the specification that the circuit should satisfy.

def assumptions (input : Inputs (F p)) :=
  let { x, y, carry_in } := input
  x.val  256 ∧ y.val  256 ∧ (carry_in = 0 ∨ carry_in = 1)

def spec (input : Inputs (F p)) (out : Outputs (F p)) :=
  let { x, y, carry_in } := input
  out.z.val = (x.val + y.val + carry_in.val) % 256 ∧
  out.carry_out.val = (x.val + y.val + carry_in.val) / 256

The main circuit is defined as follows.

def add8_full_carry (input : Var Inputs (F p)) :
    Circuit (F p) (Var Outputs (F p)) := do
  let { x, y, carry_in } := input

  -- witness the result
  let z  witness (fun eval => mod_256 (eval (x + y + carry_in)))

  -- do a lookup over the byte table for z
  lookup (ByteLookup z)

  -- witness the output carry
  let carry_out  witness (fun eval => floordiv (eval (x + y + carry_in)) 256)
  
  -- ensures that the output carry is boolean
  -- by instantiating the Boolean.circuit as a subcircuit
  assertion Boolean.circuit carry_out

  -- main 8-bit addition constraint
  assert_zero (x + y + carry_in - z - carry_out * (const 256))

  return { z, carry_out }

Finally, we define the FormalCircuit structure, which packages all those definitions, together with the soundness and completeness proofs

def circuit : FormalCircuit (F p) Inputs Outputs where
  main := add8_full_carry
  assumptions := assumptions
  spec := spec
  soundness := by
    ...
  completeness := by
    ...

Notice that this definition is generic over the field prime p, however we require an additional assumption on the prime, namely $p > 512$, otherwise the circuit is not sound!

variable {p : ℕ} [Fact p.Prime]
variable [p_large_enough: Fact (p > 512)]

Verifying concrete AIR tables

The FormalCircuit abstraction provides a modular definition of verified circuits, and it is mostly arithmetization-agnostic.
However, we want to target AIR as a concrete arithmetization, as it is a very popular choice in the zkVM design space.
AIR circuits are defined over traces: constraints are specificed together with an application domain, which represent which rows they should be applied to.
In principle, one could choose an arbitrary domain, however, in practice we choose domains that have a succinct representation in terms of vanishing polynomial.

Here are some examples of domains that have succinct representations and are used in practice.

  • The constraint is applied to one specific row of the trace. This is often referred to as a boundary constraint.
  • The constraint is applied to all rows of the trace. This is often referred to as a recurring constraint. One feature is that constraints applied to every row can access neighbouring rows: for example they could access the next row or the previous row.
  • The constraint is applied to all rows, except a chosen small set of rows. For example, it could be applied to every row except the last one, or except the first one.
  • The constraint is applied to every $n$ rows of the trace.

As a concrete example, let’s say that we want to give constraint over a trace for computing correctly the Fibonacci sequence, which is defined as follows.
$$
\begin{cases}
F_0 = 0 \\
F_1 = 1 \\
F_n = F_{n-2} + F_{n-1}
\end{cases}
$$

We can implement it with a trace composed of two columns: $x$ and $y$.
The invariant we want to prove is: on the $i$-th row, $x_i$ sould contain $F_i$ and $y_i$ should contain $F_{i+1}$.
We can achieve this behaviour by imposing the following contraints.

  • We impose a boundary constraint on the first row: $x_0 = 0$ and $y_0 = 1$.
  • Additionally, we impose two recurring constraints, implementing the recursive relation: for every $i$ – except the last one –, $y_{i+1} = x_i + y_i$, and $x_{i+1} = y_i$.
    This set of constraints is depicted in the following figure.


Fibonacci trace

It is straight-forward to see that if a trace satisfies those constraints, then in the $i$-th row we will find the $i$-th Fibonacci number in the first column.

Notice that this set of constraints can be thought also as defining a correct sequence of states, one for each row:

  • the boundary constraint is ensuring that the initial state is valid, while
  • the recurring constraint is ensuring that the state transition function is executed correctly.

In our framework, we support AIR constraints by:

  • Defining an inductive trace data structure, which we model as a sequence of rows.
  • Modeling what it means to apply a contraint to a trace using a particular domain: this in practice is done by providing an assignment from abstract variables to concrete trace cells and then applying the original constraint semantics.

You can check out the soundness proof for the Fibonacci table using 8-bit addition here, which satisfies the following, slightly more complicated, specification:
$$
\text{For every row } i, \quad x_i = (F_i \mod 256)
$$

Upcoming work

The framework is still in early stages fo development, but it is already showing promising results.
Some planned next steps are:

  • Continue adding low-level gadgets so that we have a rich library of basic reusable circuits.
  • Defining common hash function circuits and proving their correctness.
  • Build a formally verified minimal VM for a subset of RISC-V.

The whole project is open source and available on GitHub, make sure to check it out!

Source Link


Keep your files stored safely and securely with the SanDisk 2TB Extreme Portable SSD. With over 69,505 ratings and an impressive 4.6 out of 5 stars, this product has been purchased over 8K+ times in the past month. At only $129.99, this Amazon’s Choice product is a must-have for secure file storage.

Help keep private content private with the included password protection featuring 256-bit AES hardware encryption. Order now for just $129.99 on Amazon!


Unlock unlimited streaming with a free Amazon Prime trial!
Sign up today!

Help Power Techcratic’s Future – Scan To Support

If Techcratic’s content and insights have helped you, consider giving back by supporting the platform with crypto. Every contribution makes a difference, whether it’s for high-quality content, server maintenance, or future updates. Techcratic is constantly evolving, and your support helps drive that progress.

As a solo operator who wears all the hats, creating content, managing the tech, and running the site, your support allows me to stay focused on delivering valuable resources. Your support keeps everything running smoothly and enables me to continue creating the content you love. I’m deeply grateful for your support, it truly means the world to me! Thank you!

BITCOIN

Bitcoin Logo

Bitcoin QR Code

bc1qlszw7elx2qahjwvaryh0tkgg8y68enw30gpvge

Scan the QR code with your crypto wallet app

DOGECOIN

Dogecoin Logo

Dogecoin QR Code

D64GwvvYQxFXYyan3oQCrmWfidf6T3JpBA

Scan the QR code with your crypto wallet app

ETHEREUM

Ethereum Logo

Ethereum QR Code

0xe9BC980DF3d985730dA827996B43E4A62CCBAA7a

Scan the QR code with your crypto wallet app

Please read the Privacy and Security Disclaimer on how Techcratic handles your support.

Disclaimer: As an Amazon Associate, Techcratic may earn from qualifying purchases.

Tags: Hacker News
Share162Share28ShareShare4ShareTweet101
Hacker News

Hacker News

Stay updated with Hacker News, where technology meets entrepreneurial spirit. Get the latest on tech trends, startup news, and discussions from the tech community. Read the latest updates here at Techcratic.

Related Posts

bkdevs/async-server: It’s like Claude Code + Linear + GitHub PR
Hacker News

bkdevs/async-server: It’s like Claude Code + Linear + GitHub PR

August 26, 2025
1.3k
IBM and AMD Join Forces to Build the Future of Computing
Hacker News

IBM and AMD Join Forces to Build the Future of Computing

August 26, 2025
1.3k
We regret but have to temporary suspend the shipments to USA
Hacker News

We regret but have to temporary suspend the shipments to USA

August 26, 2025
1.3k
China’s Share in Global Display Capacity to Reach 75% in 2028
Hacker News

China’s Share in Global Display Capacity to Reach 75% in 2028

August 26, 2025
1.3k
pandax381/xv6-riscv-net: Xv6 for RISC-V with Networking
Hacker News

pandax381/xv6-riscv-net: Xv6 for RISC-V with Networking

August 26, 2025
1.3k
Omarchy is out
Hacker News

Omarchy is out

August 25, 2025
1.3k
IBM’s Power11 Processor Architecture at Hot Chips 2025
Hacker News

IBM’s Power11 Processor Architecture at Hot Chips 2025

August 25, 2025
1.3k
GitHub – ENDESGA/PEP: Prediction-Encoded Pixels
Hacker News

GitHub – ENDESGA/PEP: Prediction-Encoded Pixels

August 25, 2025
1.3k
Load More
Next Post
Smartphone

Samsung's sixth One UI 7 beta for the Galaxy S24 rolls out as launch nears

Your Tech Resources

  • 30 Second Tech ™
  • AI
  • App Zone ™
  • Apple
  • Ars Technica
  • CNET
  • ComputerWorld
  • Crypto News
  • Cybersecurity
  • Endgadget
  • ExtremeTech
  • Forbes
  • Fossbytes
  • Gaming
  • GeekWire
  • Gizmodo
  • Google News
  • Hacker News
  • Harvard Tech
  • I Like Cats ™
  • I Like Dogs ™
  • LifeHacker
  • MacRumors
  • Macworld
  • Mashable
  • Microsoft
  • MIT Tech
  • PC World
  • Photofocus
  • Physics
  • Random Tech
  • Retro Rewind ™
  • Robot Report
  • SiliconANGLE
  • SlashGear
  • Smartphone
  • StackSocial
  • Tech Art
  • Tech Careers
  • Tech Deals
  • Techcratic ™
  • TechCrunch
  • Techdirt
  • TechRepublic
  • Techs Got To Eat ™
  • TechSpot
  • Tesla
  • The Verge
  • TNW
  • Trusted Reviews
  • UFO
  • VentureBeat
  • Visual Capitalist
  • Wired
  • ZDNet

Tech News

  • 30 Second Tech ™
  • AI
  • Apple Insider
  • Ars Technica
  • CNET
  • ComputerWorld
  • Crypto News
  • Cybersecurity
  • Endgadget
  • ExtremeTech
  • Fossbytes
  • Gaming
  • GeekWire
  • Gizmodo

Tech News

  • Harvard Tech
  • MacRumors
  • Macworld
  • Mashable
  • Microsoft
  • MIT Tech
  • Physics
  • PC World
  • Random Tech
  • Retro Rewind ™
  • SiliconANGLE
  • SlashGear
  • Smartphone
  • StackSocial
  • Tech Careers

Tech News​

  • Tech Art
  • TechCrunch
  • Techdirt
  • TechRepublic
  • Techs Got To Eat ™
  • TechSpot
  • Tesla
  • The Verge
  • TNW
  • Trusted Reviews
  • UFO
  • VentureBeat
  • Visual Capitalist
  • Wired
  • ZDNet

Site Links

  • About Techcratic
  • Affiliate Disclaimer
  • Affiliate Link Policy
  • Contact Techcratic
  • Dealors Discount Store
  • Privacy and Security Disclaimer
  • Privacy Policy
  • RSS Feed
  • Site Map
  • Support Techcratic
  • Techcratic
  • Tech Deals
  • TOS
  • 𝕏
Click For A Secret Deal

BestEvMod Center Console Armrest Pad Cover Compatible with Tesla Cybertruck 2024 2025…

Stock exchanges representatives warn against turning financial assets into cryptocurrencies

macOS Tahoe adds three new apps to your Mac, here’s what’s coming

Global Exchanges Urge Crackdown on Tokenized Stocks Over Investor Risk

Starship Troopers Extermination: Last Man Standing

bkdevs/async-server: It’s like Claude Code + Linear + GitHub PR

Techcratic – Your All In One Tech Hub
© 2020 – 2025
All Rights Reserved
∞

No Result
View All Result
  • 30 Second Tech ™
  • AI
  • App Zone ™
  • Apple
  • Ars Technica
  • CNET
  • Crypto News
  • Cybersecurity
  • Endgadget
  • Gaming
  • I Like Cats ™
  • I Like Dogs ™
  • MacRumors
  • Macworld
  • Tech Deals
  • Techcratic ™
  • Techs Got To Eat ™
  • Tesla
  • UFO
  • Wired